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

Янус это обратимый во времени язык программирования, написанный на Калтех в 1982 г.^[1] В операционная семантика языка были официально указаны вместе с программный инвертор и обратимый переводчик-самоучитель, в 2007 году Тэцуо Ёкояма и Роберт Глюк.^[2] Инвертор и интерпретатор Janus предоставляются бесплатно Исследовательская группа TOPPS в ДИКУ.^[3] Другой интерпретатор Януса был реализован в Пролог в 2009.^[4] Ниже резюмируется язык, представленный в документе 2007 года.

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

Синтаксис

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

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

<программа> ::= <v-decl> <v-decls> <p-decl> <p-decls><v-decls> ::= <v-decl> <v-decls> | ""<p-decls> ::= <p-decl> <p-decls> | ""

Обратите внимание, Янус, как указано в документе 2007 года,^[2] допускает ноль или более переменных, но программа, которая начинается с пустого хранилища, создает пустое хранилище. Программа, которая ничего не делает, тривиально обратима и не интересна на практике.

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

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

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

Теоретических ограничений на размеры массивов нет, но для указанного интерпретатора требуется размер не менее 1.^[3]

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

<p-decl> ::= "процедура" <я бы> <s>

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

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

<s> := <Икс> <мод-опера> "=" <е> | <Икс> "[" <е> "]" <мод-опера> "=" <е>     | <Икс> "<=>" <Икс>     | "если" <е> "тогда" <s> "еще" <s> "фи" <е>     | "из" <е> "делать" <s> "петля" <s> "до того как" <е>     | "вызов" <я бы> | "отозвать" <я бы>     | «пропустить» | <s> <s>

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

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

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

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

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

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

<е> ::= <c> | <Икс> | <Икс> "[" <е> "]" | <е> <бен-опера> <е>

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

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

<бен-опера> ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="

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

<мод-опера> ::= "+" | "-" | "^"

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

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

Пример

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

процедура fib from i = n do x1 + = x2 x1 <=> x2 i - = 1 до i = 2

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

Предполагая следующую прелюдию к процедуре, мы получаем 4-е число Фибоначчи в x2:

i n x1 x2 процедура main n + = 4 i + = n x1 + = 1 x2 + = 1 call fib

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

Обратное выдумать является:

процедура fib from i = 2 do i + = 1 x1 <=> x2 x1 - = x2 цикл до i = n

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

Рекомендации