Janus (lenguaje de programación de computación reversible en el tiempo)

Janus es un lenguaje de programación reversible en el tiempo escrito en Caltech en 1982. ^{[ 1 ]} La semántica operacional del lenguaje fue especificada formalmente, junto con un inversor de programa y un auto-intérprete invertible , en 2007 por Tetsuo Yokoyama y Robert Glück. ^{[ 2 ] [ 3 ]} Un inversor e intérprete de Janus está disponible gratuitamente por el grupo de investigación TOPPS en DIKU . ^{[ 4 ]} Otro intérprete de Janus fue implementado en Prolog en 2009. ^{[ 5 ]} Se ha desarrollado un compilador optimizador en el grupo de investigación RC3. ^{[ 6 ] [ 7 ]} A continuación se resume el lenguaje presentado en el artículo de 2007. ^{[ 2 ]}

Janus es un lenguaje de programación imperativo estructurado que opera en un almacén global sin asignación de memoria dinámica y no admite estructuras de datos dinámicas. Como lenguaje de programación reversible, Janus realiza cálculos deterministas en ambas direcciones, hacia adelante y hacia atrás. Una extensión de Janus incluye parámetros de procedimiento y declaraciones de variables locales (local-delocal). ^{[ 3 ]} Además, otras variantes de Janus admiten estructuras de datos dinámicas, como listas. ^{[ 8 ] [ 9 ]}

Especificamos la sintaxis de Janus utilizando la forma Backus-Naur .

Un programa Janus es una secuencia de una o más declaraciones de variables, seguida de una secuencia de una o más declaraciones de procedimientos:

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

Cabe señalar que Janus, tal como se especifica en el artículo de 2007, ^{[ 2 ]} permite cero o más variables, pero un programa que comienza con un almacén vacío, produce un almacén vacío. Un programa que no hace nada es trivialmente invertible y no resulta interesante en la práctica.

Una declaración de variable define una variable o una matriz unidimensional:

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

Tenga en cuenta que las declaraciones de variables no contienen información de tipo. Esto se debe a que todos los valores (y todas las constantes) en Janus son enteros no negativos de 32 bits, por lo que todos los valores están entre 0 y 2³² ⁻ 1 = 4294967295. Sin embargo, tenga en cuenta que el intérprete de Janus alojado en TOPPS utiliza enteros de 32 bits en complemento a dos , por lo que todos los valores allí están entre −2³¹ ⁼ −2147483648 y ^2³¹ − 1 = 2147483647. Todas las variables se inicializan con el valor 0.

No existen límites teóricos para los tamaños de los arreglos, pero dicho intérprete exige un tamaño de al menos 1. ^{[ 4 ]}

Una declaración de procedimiento consta de la palabra clave procedure, seguida de un identificador de procedimiento único y una instrucción:

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

El punto de entrada de un programa Janus es un procedimiento llamado main. Si no existe dicho procedimiento, el último procedimiento del texto del programa es el punto de entrada.

Una instrucción es una asignación, un intercambio, una instrucción if-then-else, un bucle, una llamada a procedimiento, una cancelación de llamada a procedimiento, un salto o una secuencia de instrucciones:

< 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 > | "omitir" | < s > < s >

Para que las asignaciones sean reversibles, se requiere que la variable del lado izquierdo no aparezca en las expresiones de ninguno de los lados de la asignación. (Nota: la asignación de celdas de matriz tiene una expresión en ambos lados de la asignación).

Un intercambio ( <x> "<=>" <x>) es trivialmente reversible.

Para que las condicionales sean reversibles, proporcionamos tanto una prueba (el ` <e>after` "if") como una aserción (el ` <e>after` "fi"). La semántica establece que la prueba debe cumplirse antes de la ejecución de la rama `then`, y la aserción después . Por el contrario, la prueba no debe cumplirse antes de la ejecución de la rama `else`, y la aserción no debe cumplirse después. En el programa invertido, la aserción se convierte en la prueba, y la prueba en la aserción. (Dado que todos los valores en Janus son enteros, se emplea la semántica habitual de C, donde 0 indica falso).

Para que los bucles sean reversibles, proporcionamos una aserción (el ` <e>after` "from") y una prueba (el ` <e>after` "until"). La semántica establece que la aserción debe cumplirse solo al entrar en el bucle, y la prueba solo al salir de él. En el programa invertido, la aserción se convierte en la prueba, y la prueba en la aserción. Un ` <e>after` adicional "loop"permite realizar trabajo después de que la prueba se evalúe como falsa. Este trabajo debe asegurar que la aserción sea falsa posteriormente.

Una llamada a procedimiento ejecuta las instrucciones de un procedimiento en sentido directo. Una llamada a procedimiento deshabilitada ejecuta las instrucciones de un procedimiento en sentido inverso. Los procedimientos no tienen parámetros, por lo que el paso de variables se realiza mediante efectos secundarios en el almacenamiento global.

Una expresión es una constante ( entero ), una variable, una variable indexada o la aplicación de una operación binaria :

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

Las constantes en Janus (y el intérprete de Janus alojado por TOPPS ) ya se han comentado anteriormente.

Un operador binario es uno de los siguientes, con una semántica similar a la de sus contrapartes en C:

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

Los operadores de modificación son un subconjunto de los operadores binarios tales que para todo v,${\displaystyle \lambda v'.\oplus \left(v',v\right)}$es una función biyectiva y, por lo tanto, invertible, donde${\displaystyle \oplus }$es un operador de modificación:

< operación mod > ::= "+" | "-" | "^" 

Las funciones inversas son "-", "+", y "^", respectivamente.

La restricción de que la variable asignada no aparezca en una expresión a ninguno de los lados de la asignación nos permite demostrar que el sistema de inferencia de Janus es determinista hacia adelante y hacia atrás.

El lenguaje Janus fue concebido inicialmente en Caltech en 1982. Trabajos posteriores formalizaron la semántica del lenguaje en forma de semántica natural y semántica denotacional . ^{[ 10 ]} La semántica de los lenguajes de programación puramente reversibles también puede tratarse de forma reversible en el nivel meta.

Escribimos un procedimiento de Janus fibpara encontrar el n -ésimo número de Fibonacci , para n>2, i=n, ​​x1=1 y x2=1:

procedimiento fib de i = n hacer x1 += x2 x1 <=> x2 i -= 1 hasta que i = 2 

Al finalizar, x1es el ( n -1)-ésimo número de Fibonacci y x2es el n- ^ésimo número de Fibonacci. i es una variable iteradora que va de n a 2. Como i se decrementa en cada iteración, la suposición ( i = n) solo es verdadera antes de la primera iteración. La prueba es ( i = 2) solo es verdadera después de la última iteración del bucle (suponiendo n > 2).

Suponiendo el siguiente preludio al procedimiento, terminamos con el cuarto número de Fibonacci en x2:

en x1 x2 procedimiento principal n += 4 i += n x1 += 1 x2 += 1 llamar mentira 

Tenga en cuenta que nuestra función principal tendría que hacer un poco más de trabajo si quisiéramos que manejara n≤2, especialmente enteros negativos.

Lo inverso de fibes:

procedimiento fib desde i = 2 hacer i += 1 x1 <=> x2 x1 -= x2 bucle hasta que i = n 

Como puede observarse, los programas Janus pueden transformarse mediante inversión local, donde se intercambian la condición del bucle y la aserción, se invierte el orden de las instrucciones y, a su vez, se invierte cada instrucción dentro del bucle. El programa inverso puede utilizarse para hallar n cuando x1 es el (n-1) ^{-ésimo número} de Fibonacci y x2 es el n ^-ésimo número de Fibonacci.