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 Janus está disponible gratuitamente por el grupo de investigación TOPPS en DIKU . [4] Otro intérprete Janus fue implementado en Prolog en 2009. [5] Un compilador optimizador ha sido desarrollado 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 y no admite estructuras de datos dinámicas. Como lenguaje de programación reversible, Janus realiza cálculos deterministas tanto en dirección hacia delante como 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 > | ""Tenga en cuenta que Janus, 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 es 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 números enteros de 32 bits no negativos, por lo que todos los valores están entre 0 y 2 32 − 1 = 4294967295. Sin embargo, tenga en cuenta que el intérprete de Janus alojado por TOPPS utiliza números enteros de 32 bits en complemento a dos regulares , por lo que todos los valores están entre −2 31 = −2147483648 y 2 31 − 1 = 2147483647. Todas las variables se inicializan con el valor 0.
No existen límites teóricos para los tamaños de las matrices, 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 declaración:
< p-decl > ::= "procedimiento" < id > < s >El punto de entrada de un programa Janus es un procedimiento denominado main. Si no existe dicho procedimiento, el último procedimiento del texto del programa es el punto de entrada.
Una declaración es una asignación, un intercambio, un if-then-else, un bucle, una llamada a un procedimiento, una anulación de una llamada a un procedimiento, un salto o una secuencia de declaraciones:
< s > := < x > < mod-op > "=" < e > | < x > "[" < e > "]" < mod-op > "=" < e > | < x > " < = > " < x > | "si" < e > "entonces" < s > "sino" < s > "fi" < e > | "desde" < e > "hacer" < s > "bucle" < s > "hasta" < e > | "llamar" < id > | "cancelar llamada" < id > | "saltar" | < s > < s >Para que las asignaciones sean reversibles, se exige que la variable del lado izquierdo no aparezca en las expresiones de ninguno de los lados de la asignación. (Tenga en cuenta que 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 los condicionales sean reversibles, proporcionamos tanto una prueba (el <e>after "if") como una aserción (el <e>after "fi"). La semántica es que la prueba debe cumplirse antes de la ejecución de la rama then, y la aserción debe cumplirse después de ella. 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 de ella. En el programa invertido, la aserción se convierte en la prueba, y la prueba se convierte en la aserción. (Dado que todos los valores en Janus son números enteros, se emplea la semántica habitual de C que indica que 0 indica falso).
Para que los bucles sean reversibles, proporcionamos de manera similar una aserción (el <e>after "from") y una prueba (el <e>after "until"). La semántica es que la aserción debe cumplirse solo al ingresar al bucle, y la prueba debe cumplirse solo al salir del bucle. En el programa invertido, la aserción se convierte en la prueba, y la prueba se convierte en la aserción. Un <e>after adicional "loop"permite realizar un trabajo después de que la prueba se evalúe como falsa. El trabajo debe garantizar que la aserción sea falsa posteriormente.
Una llamada a un procedimiento ejecuta las instrucciones de un procedimiento en dirección hacia adelante. Una anulación de llamada a un procedimiento ejecuta las instrucciones de un procedimiento en dirección hacia atrás. Los procedimientos no tienen parámetros, por lo que todo el paso de variables se realiza mediante efectos secundarios en el almacén global.
Una expresión es una constante (entero), una variable, una variable indexada o una 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 analizado anteriormente.
Un operador binario es uno de los siguientes, con una semántica similar a sus contrapartes de C:
< bin-op > ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | " < =" | " > ="Los operadores de modificación son un subconjunto de los operadores binarios tales que para todo v, es una función biyectiva y, por lo tanto, invertible, donde es un operador de modificación:
< operación mod > ::= "+" | "-" | "^"Las funciones inversas son "-", "+", y "^", respectivamente.
La restricción de que la variable asignada no aparece en una expresión en 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 yo -= 1 hasta i = 2
Al finalizar, x1es el ( n −1)-ésimo número de Fibonacci y x2es el n º 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 que n > 2).
Suponiendo el siguiente preludio al procedimiento, terminamos con el cuarto número de Fibonacci en x2:
en x1 x2procedimiento principal n += 4 yo += n x1 += 1 x2 += 1 Llamar mentira
Tenga en cuenta que nuestro principal tendría que hacer un poco más de trabajo si tuviéramos que manejar n≤2, especialmente números enteros negativos.
La inversa de fibes:
procedimiento fib desde i = 2 hacer yo += 1 x1 <=> x2 x1 -= x2 bucle hasta que i = n
Como puede ver, los programas Janus se pueden transformar mediante inversión local, donde se intercambian la prueba y la afirmación del bucle, se invierte el orden de las declaraciones y cada declaración del bucle se invierte a su vez. El programa inverso se puede utilizar para encontrar n cuando x1 es el (n-1) ésimo y x2 es el n ésimo número de Fibonacci.