We specify the syntax of Janus using Backus–Naur form. A Janus program is a sequence of one or more variable declarations, followed by a sequence of one or more procedure declarations: ::= ::= | "" ::= | ""
Note, Janus as specified in the 2007 paper, allows zero or more variables, but a program that starts with an empty store, produces an empty store. A program that does nothing is trivially invertible, and not interesting in practice. A variable declaration defines either a variable or a one-dimensional array: ::= | ""
Note, variable declarations carry no type information. This is because all values in Janus are non-negative 32-bit integers, so all values are between 0 and 232 − 1 = 4294967295. Note however, that the Janus interpreter hosted by TOPPS uses regular two's complement 32-bit integers, so all values there are between −231 = −2147483648 and 231 − 1 = 2147483647. All variables are initialized to the value 0. There are no theoretical bounds to the sizes of arrays, but the said interpreter demands a size of at least 1. A procedure declaration consists of the keyword procedure, followed by a unique procedure identifier and a statement: ::= "procedure"
The entry point of a Janus program is a procedure named main. If no such procedure exists, the last procedure in the program text is the entry point. A statement is either an assignment, a swap, an if-then-else, a loop, a procedure call, a procedure uncall, a skip, or a sequence of statements: := "=" | "" "=" | "<=>" | "if" "then" "else" "fi" | "from" "do" "loop" "until" | "call" | "uncall" | "skip" |
For assignments to be reversible, it is demanded that the variable on the left-hand side does not appear in the expressions on either side of the assignment. A swap is trivially reversible. For conditionals to be reversible, we provide both a test and an assertion. The semantics is that the test must hold before the execution of the then-branch, and the assertion must hold after it. Conversely, the test must not hold before the execution of the else-branch, and the assertion must not hold after it. In the inverted program, the assertion becomes the test, and the test becomes the assertion. For loops to be reversible, we similarly provide an assertion and a test. The semantics is that the assertion must hold only on entry to the loop, and the test must hold only on exit from the loop. In the inverted program, the assertion becomes the test, and the test becomes the assertion. An additional after "loop" allows to perform work after the test is evaluated to false. The work should ensure that the assertion is false subsequently. A procedure call executes the statements of a procedure in a forward direction. A procedure uncall executes the statements of a procedure in the backward direction. There are no parameters to procedures, so all variable passing is done by side-effects on the global store. An expression is a constant, a variable, an indexed variable, or an application of a binary operation: ::= | | "" |
The constants in Janus have already been discussed above. A binary operator is one of the following, having semantics similar to their C counterparts: ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="
The modification operators are a subset of the binary operators such that for all v, is a bijective function, and hence invertible, where is a modification operator: ::= "+" | "-" | "^"
The inverse functions are "-", "+", and "^", respectively. The restriction that the variable assigned to does not appear in an expression on either side of the assignment allows us to prove that the inference system of Janus is forward and backward deterministic.
Example
We write a Janus procedure fib to find the n-th Fibonacci number, for n>2, i=n, x1=1, and x2=1:
procedure fib from i = n do x1 += x2 x1 <=> x2 i -= 1 until i = 2
Upon termination, x1 is the -th Fibonacci number and x2 is the nth Fibonacci number. i is an iterator variable that goes from n to 2. As i is decremented in every iteration, the assumption is only true prior to the first iteration. The test is is only true after the last iteration of the loop. Assuming the following prelude to the procedure, we end up with the 4th Fibonacci number in x2:
i n x1 x2 procedure main n += 4 i += n x1 += 1 x2 += 1 call fib
Note, our main would have to do a bit more work if we were to make it handle n≤2, especially negative integers. The inverse of fib is:
procedure fib from i = 2 do i += 1 x1 <=> x2 x1 -= x2 loop until i = n
As you can see, Janus performs local inversion, where the loop test and assertion are swapped, the order of statements is reversed, and every statement in the loop is itself reversed. The reverse program can be used to find n when x1 is the th and x2 is the nth Fibonacci number.
