Janus (time-reversible computing programming language)

<h2 id="syntax">Syntax</h2>
We specify the syntax of Janus using <a href="/facts/Backus%25E2%2580%2593Naur_form/xbMXDntc">Backus–Naur form</a>.
A Janus program is a sequence of one or more variable declarations, followed by a sequence of one or more procedure declarations:

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

Note, Janus as specified in the 2007 paper,<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a> 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:

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

Note, variable declarations carry no type information. This is because all values (and all constants) 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 <a href="/facts/TOPPS_(research_group)/njRzX8QS">TOPPS</a> uses regular <a href="/facts/Two%2527s_complement/xhjYpnsc">two's complement</a> 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 class="footnote-ref" id="fnref:13" href="#fn:13">13</a>
A procedure declaration consists of the keyword procedure, followed by a unique procedure identifier and a statement:

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

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:

<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>

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. (Note, array cell assignment has an expression on both sides of the assignment.)
A swap (<x> "<=>" <x>) is trivially reversible.
For conditionals to be reversible, we provide both a test (the <e> after "if") and an assertion (the <e> after "fi"). 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. (Since all values in Janus are integers, the usual C-semantics that 0 indicates false are employed.)
For loops to be reversible, we similarly provide an assertion (the <e> after "from") and a test (the <e> after "until"). 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 <e> 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 (integer), a variable, an indexed variable, or an application of a binary operation:

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

The constants in Janus (and the Janus interpreter hosted by <a href="/facts/TOPPS_(research_group)/njRzX8QS">TOPPS</a>) have already been discussed above.
A binary operator is one of the following, having semantics similar to their C counterparts:

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

The modification operators are a subset of the binary operators such that for all v, 
 
 
 
 λ
 
 v
 ′
 
 .
 ⊕
 
 (
 
 
 v
 ′
 
 ,
 v
 
 )
 
 
 
 {\displaystyle \lambda v'.\oplus \left(v',v\right)}
 
 is a bijective function, and hence invertible, where 
 
 
 
 ⊕
 
 
 {\displaystyle \oplus }
 
 is a modification operator:

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

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.

<h2 id="semantics">Semantics</h2>
The language Janus was initially conceived at Caltech in 1982. Subsequent work formalized the language semantics in the form of natural semantics and the denotational semantics.<a class="footnote-ref" id="fnref:14" href="#fn:14">14</a> The semantics of purely reversible programming languages can also be treated reversibly at the meta level.

<h2 id="example">Example</h2>
We write a Janus procedure fib to find the n-th <a href="/facts/Fibonacci_sequence/mqxpAUQD">Fibonacci number</a>, 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 (n−1)-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 (i = n) is only true prior to the first iteration. The test is (i = 2) is only true after the last iteration of the loop (assuming n > 2).
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 programs can be transformed by 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 inverse program can be used to find n when x1 is the (n-1)th and x2 is the nth Fibonacci number.

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Christopher Lutz (1986). "Janus: a time-reversible language". <a href="http://tetsuo.jp/ref/janus.html" target="_blank">http://tetsuo.jp/ref/janus.html</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Tetsuo Yokoyama; Robert Glück (2007). "A reversible programming language and its invertible self-interpreter". Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. New York, NY, USA: ACM. pp. 144–153. doi:10.1145/1244381.1244404. ISBN 978-1-59593-620-2. <a href="978-1-59593-620-2" target="_blank">978-1-59593-620-2</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Yokoyama, Tetsuo; Axelsen, Holger Bock; Glück, Robert (5 May 2008). "Principles of a reversible programming language". Proceedings of the 5th conference on Computing frontiers. pp. 43–54. doi:10.1145/1366230.1366239. ISBN 978-1-60558-077-7. S2CID 14228334. <a href="978-1-60558-077-7" target="_blank">978-1-60558-077-7</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">"Janus Playground". <a href="http://topps.diku.dk/pirc/janus-playground/" target="_blank">http://topps.diku.dk/pirc/janus-playground/</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">"A reversible interpreter". <a href="http://www.complang.tuwien.ac.at/adrian/revcomp" target="_blank">http://www.complang.tuwien.ac.at/adrian/revcomp</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">"RC3: Reversible Computing Compiler Collection". <a href="https://git.thm.de/thm-rc3/release" target="_blank">https://git.thm.de/thm-rc3/release</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Deworetzki, Niklas; Kutrib, Martin; Meyer, Uwe; Ritzke, Pia-Doreen (2022). "Optimizing Reversible Programs". Reversible Computation. Lecture Notes in Computer Science. Vol. 13354. pp. 224–238. doi:10.1007/978-3-031-09005-9_16. ISBN 978-3-031-09004-2. <a href="978-3-031-09004-2" target="_blank">978-3-031-09004-2</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Tetsuo Yokoyama; Robert Glück (2007). "A reversible programming language and its invertible self-interpreter". Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. New York, NY, USA: ACM. pp. 144–153. doi:10.1145/1244381.1244404. ISBN 978-1-59593-620-2. <a href="978-1-59593-620-2" target="_blank">978-1-59593-620-2</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Yokoyama, Tetsuo; Axelsen, Holger Bock; Glück, Robert (5 May 2008). "Principles of a reversible programming language". Proceedings of the 5th conference on Computing frontiers. pp. 43–54. doi:10.1145/1366230.1366239. ISBN 978-1-60558-077-7. S2CID 14228334. <a href="978-1-60558-077-7" target="_blank">978-1-60558-077-7</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Glück, Robert; Yokoyama, Tetsuo (2016). "A Linear-Time Self-Interpreter of a Reversible Imperative Language". Computer Software. 33 (3): 3_108–3_128. doi:10.11309/jssst.33.3_108. <a href="https://doi.org/10.11309/jssst.33.3_108" target="_blank">https://doi.org/10.11309/jssst.33.3_108</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Glück, Robert; Yokoyama, Tetsuo (2023). "Reversible computing from a programming language perspective". Theoretical Computer Science. 953: 113429. doi:10.1016/j.tcs.2022.06.010. <a href="https://doi.org/10.1016%2Fj.tcs.2022.06.010" target="_blank">https://doi.org/10.1016%2Fj.tcs.2022.06.010</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">Tetsuo Yokoyama; Robert Glück (2007). "A reversible programming language and its invertible self-interpreter". Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. New York, NY, USA: ACM. pp. 144–153. doi:10.1145/1244381.1244404. ISBN 978-1-59593-620-2. <a href="978-1-59593-620-2" target="_blank">978-1-59593-620-2</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
<li id="fn:13">"Janus Playground". <a href="http://topps.diku.dk/pirc/janus-playground/" target="_blank">http://topps.diku.dk/pirc/janus-playground/</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></li>
<li id="fn:14">Paolini, Luca; Piccolo, Mauro; Roversi, Luca (2018). "A Certified Study of a Reversible Programming Language". Proc. 21st International Conference on Types for Proofs and Programs (TYPES 2015).: 7:1–7:21. doi:10.4230/LIPIcs.TYPES.2015.7. <a href="https://doi.org/10.4230%2FLIPIcs.TYPES.2015.7" target="_blank">https://doi.org/10.4230%2FLIPIcs.TYPES.2015.7</a> <a href="#fnref:14" class="footnote-back-ref">↩</a></li>
</ol>

Janus (time-reversible computing programming language) open-in-new

Janus (time-reversible computing programming language)