Янус (обратимый во времени язык программирования вычислений)

Янус

Парадигма	императивный ( процессуальный ), обратимый
Разработано	Кристофер Лутц, Ховард Дерби, Тецуо Ёкояма и Роберт Глюк
Впервые появился	1982, 2007
Веб-сайт	тэцуо .jp / ссылка /янус .html
Основные реализации
Детская площадка Януса

Janus — обратимый во времени язык программирования, написанный в Калифорнийском технологическом институте в 1982 году. Операционная семантика языка была формально определена вместе с программным инвертором и обратимым самоинтерпретатором в 2007 году Тецуо Ёкоямой и Робертом Глюком. Инвертор и интерпретатор Janus бесплатно предоставляются исследовательской группой TOPPS в DIKU . Еще один интерпретатор Janus был реализован на Прологе в 2009 году. В исследовательской группе RC3 разработан оптимизирующий компилятор. Ниже кратко изложены формулировки, представленные в документе 2007 года.

Janus — это структурированный императивный язык программирования, который работает с глобальным хранилищем без выделения кучи и не поддерживает динамические структуры данных. Будучи обратимым языком программирования, Янус выполняет детерминированные вычисления как в прямом, так и в обратном направлении. Расширение Janus включает параметры процедур и объявления локальных переменных (локально-делокальные). Кроме того, другие варианты Janus поддерживают динамические структуры данных, такие как списки.

Синтаксис

Мы указываем синтаксис Януса, используя форму Бэкуса-Наура .

Программа Janus представляет собой последовательность одного или нескольких объявлений переменных, за которыми следует последовательность одного или нескольких объявлений процедур:

<program> ::= <v-decl> <v-decls> <p-decl> <p-decls>
<v-decls> ::= <v-decl> <v-decls> | ""
<p-decls> ::= <p-decl> <p-decls> | ""

Обратите внимание: Янус, как указано в статье 2007 года, допускает ноль или более переменных, но программа, которая запускается с пустой памятью, создает пустую память. Программа, которая ничего не делает, тривиально обратима и на практике неинтересна.

Объявление переменной определяет либо переменную, либо одномерный массив:

<v-decl> ::= <v> | <v> "[" <c> "]"

Обратите внимание: объявления переменных не несут никакой информации о типе. Это связано с тем, что все значения (и все константы) в Janus являются неотрицательными 32-битными целыми числами, поэтому все значения находятся в диапазоне от 0 до 2. ³² − 1 = 4294967295. Однако обратите внимание, что интерпретатор Janus, размещенный на TOPPS, использует обычные 32-битные целые числа с дополнением до двух , поэтому все значения находятся между -2 ³¹ = -2147483648 и 2 ³¹ − 1 = 2147483647. Все переменные инициализируются значением 0.

Теоретических ограничений на размеры массивов нет, но указанный интерпретатор требует размер не менее 1.

Объявление процедуры состоит из ключевого слова procedure, за которым следует уникальный идентификатор процедуры и оператор:

<p-decl> ::= "procedure" <id> <s>

Точкой входа в программу Janus является процедура с именем main. Если такой процедуры не существует, точкой входа является последняя процедура в тексте программы.

Оператор — это присваивание, замена, if-then-else, цикл, вызов процедуры, отмена вызова процедуры, пропуск или последовательность операторов:

<s> := <x> <mod-op> "=" <e> | <x> "[" <e> "]" <mod-op> "=" <e>
     | <x> "<=>" <x>
     | "if" <e> "then" <s> "else" <s> "fi" <e>
     | "from" <e> "do" <s> "loop" <s> "until" <e>
     | "call" <id> | "uncall" <id>
     | "skip"
     | <s> <s>

Чтобы присваивания были обратимыми, требуется, чтобы переменная в левой части не появлялась в выражениях по обе стороны от присваивания. (Обратите внимание, что присвоение ячеек массива имеет выражения с обеих сторон присваивания.)

Обмен( <x> "<=>" <x>) тривиально обратимо.

Чтобы условные выражения были обратимыми, мы предоставляем как тест ( <e> после "if") и утверждение ( <e> после "fi"). Семантика заключается в том, что тест должен выполняться до выполнения перехода then, а утверждение должно выполняться после него. И наоборот, тест не должен выполняться до выполнения ветки else, а утверждение не должно выполняться после нее. В перевернутой программе утверждение становится проверкой, а проверка — утверждением. (Поскольку все значения в Janus являются целыми числами, используется обычная C-семантика, согласно которой 0 указывает на ложь.)

Чтобы циклы были обратимыми, мы аналогичным образом обеспечиваем утверждение ( <e> после "from") и тест ( <e> после "until"). Семантика заключается в том, что утверждение должно выполняться только при входе в цикл, а тест должен выполняться только при выходе из цикла. В перевернутой программе утверждение становится проверкой, а проверка — утверждением. Дополнительный <e> после "loop" позволяет выполнять работу после того, как тест оценен как ложный. Работа должна гарантировать, что утверждение впоследствии окажется ложным.

процедуры Вызов выполняет инструкции процедуры в прямом направлении. процедуры Отмена вызова выполняет операторы процедуры в обратном направлении. В процедурах нет параметров, поэтому вся передача переменных осуществляется с помощью побочных эффектов в глобальном хранилище.

Выражение — это константа (целое число), переменная, индексированная переменная или применение бинарной операции:

<e> ::= <c> | <x> | <x> "[" <e> "]" | <e> <bin-op> <e>

Константы в Janus (и интерпретаторе Janus, размещенном на TOPPS ) уже обсуждались выше.

Бинарный оператор — это один из следующих операторов, имеющий семантику, аналогичную его аналогам в C:

<bin-op> ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="

Операторы модификации представляют собой подмножество бинарных операторов, таких что для всех v $\lambda v'.\oplus \left(v',v\right)$ является биективной функцией и, следовательно, обратимой, где $\oplus$ является оператором модификации:

<mod-op> ::= "+" | "-" | "^"

Обратные функции: "-", "+", и "^", соответственно.

Ограничение на то, что присвоенная переменная не появляется в выражении по обе стороны от присваивания, позволяет нам доказать, что система вывода Януса является прямой и обратной детерминированностью.

Семантика

Язык Янус был первоначально задуман в Калифорнийском технологическом институте в 1982 году. Последующие работы формализовали семантику языка в форме естественной семантики и денотационной семантики. Семантику чисто обратимых языков программирования также можно обратимо рассматривать на метауровне.

Пример

Пишем процедуру Януса fib чтобы найти n -е число Фибоначчи для n>2, i=n, ​​x1=1 и x2=1:

procedure fib
    from i = n
    do
        x1 += x2
        x1 <=> x2
        i -= 1
    until i = 2

По окончании, x1 — ( n −1)-е число Фибоначчи и x2 это н ^й Число Фибоначчи. i — переменная-итератор, изменяющаяся от n до 2. Поскольку i уменьшается на каждой итерации, предположение ( i = n) верно только до первой итерации. Тест такой( i = 2) истинно только после последней итерации цикла (при условии, что n > 2).

Если принять следующую прелюдию к процедуре, мы получим четвертое число Фибоначчи в x2:

i n x1 x2
procedure main
    n += 4
    i += n
    x1 += 1
    x2 += 1
    call fib

Обратите внимание: нашему main пришлось бы проделать немного больше работы, если бы мы хотели, чтобы он обрабатывал n≤2, особенно отрицательные целые числа.

Обратная сторона fib является:

procedure fib
    from  i = 2
    do
        i += 1
        x1 <=> x2
        x1 -= x2
    loop
    until i = n

Как видите, программы Януса можно преобразовать с помощью локальной инверсии, при которой проверка цикла и утверждение меняются местами, порядок операторов меняется на обратный, и каждый оператор в цикле сам по себе инвертируется. Обратная программа может использоваться для нахождения n , когда x1 равно (n-1) ^й и x2 - это n ^й Число Фибоначчи.