Content deleted Content added
merged duplicate references |
merged duplicate references |
||
Line 3:
== Core concepts and design principles ==
The fundamental goal of a reversible programming language is to support computation that is deterministic in both the forward and backward directions.
| last1 = Glück
| first1 = Robert
Line 19:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> This is typically achieved by ensuring that every primitive operation and composite statement within the language is locally invertible.
Key in the design of many reversible languages is cleanliness or garbage-free computation.<ref>{{cite arXiv
Line 75 ⟶ 59:
To achieve local invertibility and cleanliness, reversible languages typically incorporate several features:
* '''Reversible Updates:''' Standard assignment statements (<code>x = expression</code>) are inherently irreversible because they overwrite and erase the previous value of x. Reversible languages replace these with reversible updates, often denoted using operators like <code>+=</code>, <code>-=</code>, <code>^=</code> (bitwise XOR).<ref name="Yokoyama-
| last1 = Yokoyama
| first1 = Tetsuo
Line 94 ⟶ 78:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> An important restriction is that the variable being updated (e.g., x in <code>x += e</code>) must not appear in the expression on the right-hand side (e) to ensure the operation is bijective.<ref name="Yokoyama-
| last1 = Choudhury
| first1 = Vikraman
Line 103 ⟶ 87:
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* '''Reversible Control Flow:''' Conventional control flow structures like [[If-then-else]] and [[While loop]]s merge computational paths, making them irreversible. Reversible languages introduce specialized constructs. Conditionals often require both a test condition (evaluated on entry) and an assertion (a predicate that must hold true on exit from one branch and false on exit from the other).<ref name="Palazzo-2501.05259">{{cite arXiv
| last1 = Palazzo
| first1 = Matteo
Line 115 ⟶ 99:
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref name="Yokoyama-
* '''Procedure Calls:''' Languages need mechanisms to invoke procedures both forwards and backwards. This is often achieved through paired commands like <code>call</code> (forward execution) and <code>uncall</code> or <code>rcall</code> (backward execution).<ref name="Choudhury"/>
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref name="Yokoyama-
| last1 = Haulund
| first1 = Tue
Line 158 ⟶ 130:
== Janus Language ==
[[Janus (time-reversible computing programming language)|Janus]] is widely recognized as the first structured, imperative programming language designed explicitly for reversible computation.<ref name="Yokoyama-
===Design philosophy===
Line 165 ⟶ 137:
===Syntax and semantics===
* ''Program Structure:'' A Janus program consists of global variable declarations followed by procedure declarations. The execution starts at a procedure named <code>main</code>, or the last procedure defined if <code>main</code> is absent.
* ''Data Types:'' Janus primarily uses 32-bit integers (interpreters may differ on signed vs. unsigned) and one-dimensional integer arrays of fixed size.<ref name="Yokoyama-
* ''Statements:''
** '''Assignment:''' Reversible updates <code>x op= e</code> or <code>x[e] op= e</code>, where <code>op</code> is <code>+</code>, <code>-</code>, or <code>^</code> (bitwise XOR). The variable <code>x</code> must not appear in the expression <code>e</code>.<ref name="Yokoyama-
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.
** '''Conditional:''' <code>if e1 then s1 else s2 fi e2</code>. The expression <code>e1</code> is the test evaluated upon forward entry. The expression <code>e2</code> is an assertion evaluated upon forward exit; it must be true if <code>s1</code> was executed and false if <code>s2</code> was executed. For backward execution (e.g., via <code>uncall</code>), <code>e2</code> acts as the test to determine which inverse branch (s1<sup>−1</sup> or s2<sup>−1</sup>) to take, and <code>e1</code> becomes the assertion checked upon exiting backward.<ref
** '''Loop:''' <code>from e1 do s1 loop s2 until e2</code>. Upon forward entry, assertion <code>e1</code> must be true. <code>s1</code> is executed. Then, test <code>e2</code> is evaluated. If true, the loop terminates. If false, <code>s2</code> is executed, after which assertion <code>e1</code> must now be false for the loop to continue back to <code>s1</code>. In reverse, <code>e2</code> is the entry assertion, s2<sup>−1</sup> is executed, <code>e1</code> is the test (loop continues if false, terminates if true), and s1<sup>−1</sup> is executed if the loop continues.<ref name="Yokoyama-
** '''Stack Operations:''' <code>push(x, stack)</code> and <code>pop(x, stack)</code>. Reversibility often relies on assumptions about the state of <code>x</code> (e.g., <code>x</code> must be 0 before <code>push</code> so <code>pop</code> can restore it).<ref name="Yokoyama-
▲** '''Loop:''' <code>from e1 do s1 loop s2 until e2</code>. Upon forward entry, assertion <code>e1</code> must be true. <code>s1</code> is executed. Then, test <code>e2</code> is evaluated. If true, the loop terminates. If false, <code>s2</code> is executed, after which assertion <code>e1</code> must now be false for the loop to continue back to <code>s1</code>. In reverse, <code>e2</code> is the entry assertion, s2<sup>−1</sup> is executed, <code>e1</code> is the test (loop continues if false, terminates if true), and s1<sup>−1</sup> is executed if the loop continues.<ref name="Yokoyama-71-81"/>
▲** '''Stack Operations:''' <code>push(x, stack)</code> and <code>pop(x, stack)</code>. Reversibility often relies on assumptions about the state of <code>x</code> (e.g., <code>x</code> must be 0 before <code>push</code> so <code>pop</code> can restore it).<ref name="Yokoyama-71-81"/>** '''Local Variables:''' <code>local t x = e in s delocal t x = e</code> This block introduces a local variable <code>x</code>, initializes it reversibly using <code>e</code>, executes <code>s</code>, and then uncomputes <code>x</code> back to its initial state (usually 0) using the inverse of <code>e</code> upon exit.<ref name="Yokoyama-71-81"/>
** '''Procedure Call:''' <code>call id</code> executes procedure <code>id</code> forwards; <code>uncall id</code> executes procedure <code>id</code> backwards.<ref name="Choudhury"/> Procedures operate via side effects on the global store.
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.
Line 189 ⟶ 149:
===Implementations and code examples===
Several online interpreters for Janus exist.<ref>{{cite web |url=https://topps.diku.dk/pirc/?id=janus |title=Janus: a reversible imperative programming language |website=University of Copenhagen (DIKU) |access-date=April 9, 2025}}</ref> Janus has been used to implement various algorithms reversibly, including computing Fibonacci pairs,<ref name="Yokoyama-
| last1 = Yokoyama
| first1 = Tetsuo
Line 211 ⟶ 171:
}}</ref>
The following fibpair procedure in Janus calculates a pair of consecutive Fibonacci numbers.<ref name="Glück-2022.06.010"/>
<pre>
Line 641 ⟶ 585:
| class = cs.PL
}}</ref>
* '''Flowchart Languages:''' Languages like R-CORE, R-WHILE, and SRL provide structured representations of reversible control flow, often serving as intermediate languages or theoretical models.<ref name="Palazzo-2501.05259"/> Their semantics can also be captured using categorical frameworks.<ref>{{cite
| last1 = Glück
| first1 = Robert
Line 787 ⟶ 719:
{| class="wikitable"
|+ Comparison of Reversible Programming Languages<ref name="Yokoyama-
| last1 = Haulund
| first1 = Tue
| |||