Wikipedia

Reversible programming language: Difference between revisions

Browse history interactively
Next edit →
Content deleted Content added
VisualWikitext
Mgr829 (talk | contribs)
16 edits
Tag: New redirect
 
Mgr829 (talk | contribs)
16 edits
Tags: Removed redirect Possible self promotion in userspace
Line 1:
Reversible programming languages are designed to bridge the gap between the theoretical models of reversible computation and practical software development. They provide constructs that allow programmers to write code that is guaranteed, by the language's syntax and semantics, to be executable both forwards and backwards deterministically.
#REDIRECT [[Program Inversion, Interpretation, and Injectivization]]
 
=== Core Concepts and Design Principles ===
{{Redirect category shell|
 
{{R from move}}
The fundamental goal of a reversible programming language is to support computation that is deterministic in both the forward and backward directions. <ref>{{cite journal
}}
| last1 = Glück
| first1 = Robert
| last2 = Yokoyama
| first2 = Tetsuo
| title = Reversible computing from a programming language perspective
| journal = Theoretical Computer Science
| volume = 953
| pages = 113429
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- 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. <ref>{{cite journal
| last1 = Glück
| first1 = Robert
| last2 = Yokoyama
| first2 = Tetsuo
| title = Reversible computing from a programming language perspective
| journal = Theoretical Computer Science
| volume = 953
| pages = 113429
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> Local invertibility means that each basic computational step has a well-defined inverse, and the inverse of a sequence of steps is the sequence of inverse steps performed in reverse order.
 
Key in the design of many reversible languages is cleanliness or garbage-free computation.<ref>{{cite arxiv
| last1 = Thomsen
| first1 = Michael Kirkedal
| title = Design of Reversible Computing Systems; Large Logic, Languages, and Circuits
| eprint = 2309.11832
| year = 2023
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2309-11832.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
}}</ref> This means avoiding the accumulation of auxiliary information (like computation histories or ancilla bits) that is generated solely for the purpose of enabling reversibility but is not part of the desired output.<ref>{{cite conference
| last1 = Thomsen
| first1 = Michael Kirkedal
| last2 = Axelsen
| first2 = Holger Bock
| last3 = Glück
| first3 = Robert
| editor-last1 = De Vos
| editor-first1= Alexis
| editor-last2 = Wille
| editor-first2= Robert
| title = A Reversible Processor Architecture and Its Reversible Logic Design
| book-title = Reversible Computation - Third International Workshop, RC 2011, Gent, Belgium, July 4-5, 2011. Revised Papers
| series = Lecture Notes in Computer Science
| volume = 7165
| pages = 30–42
| publisher = Springer
| year = 2011
| url = https://doi.org/10.1007/978-3-642-29517-1_3
| doi = 10.1007/978-3-642-29517-1_3
| id = {{DBLP|conf/rc/ThomsenAG11}}
<!-- biburl: https://dblp.org/rec/conf/rc/ThomsenAG11.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Sun, 02 Jun 2019 21:17:32 +0200 -->
}}</ref> Clean reversible languages aim to perform computations and their reversals using only the specified input and output variables.
 
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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- 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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> The swap operation (<code>x <=> y</code>), which exchanges the values of two variables, is another fundamental reversible update.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- 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>{{cite arxiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> These additional predicates store the necessary information to determine the execution path uniquely during backward execution, where the roles of tests and assertions are typically swapped.<ref>{{cite arxiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
}}</ref> This explicit management of control flow information is a significant difference from conventional programming.
* '''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>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Handling dynamic data structures like stacks requires careful semantic design to maintain reversibility, such as assuming variables are zero-cleared before being pushed onto a stack, ensuring <code>pop</code> can perfectly reverse <code>push</code>.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> More recent research has explored reversible object-oriented features, including user-defined types, inheritance, and polymorphism.<ref>{{cite conference
| last1 = Haulund
| first1 = Tue
| last2 = Mogensen
| first2 = Torben Ægidius
| last3 = Glück
| first3 = Robert
| editor-last1 = Phillips
| editor-first1= Iain
| editor-last2 = Rahaman
| editor-first2= Hafizur
| title = Implementing Reversible Object-Oriented Language Features on Reversible Machines
| book-title = Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| pages = 66–73
| publisher = Springer
| year = 2017
| url = https://doi.org/10.1007/978-3-319-59936-6_5
| doi = 10.1007/978-3-319-59936-6_5
| id = {{DBLP|conf/rc/HaulundMG17}}
<!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
}}</ref>
* '''Computational Power:''' A common benchmark for the power of a reversible language is [[Turing completeness|r-Turing completeness]], which means the language can simulate any Reversible Turing Machine cleanly (without garbage accumulation).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
 
=== 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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Originally conceived by Christopher Lutz and Howard Derby at Caltech in the 1980s<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>, it was later rediscovered, formalized, and extended, notably by Tetsuo Yokoyama and Robert Glück.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
 
'''Design Philosophy:''' Janus embodies the principle of local invertibility. It operates on a global store of variables (no heap allocation or local procedure scope in early versions) and ensures that every statement has a unique inverse.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
 
'''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.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
* ''Data Types:'' Janus primarily uses 32-bit integers (interpreters may differ on signed vs. unsigned) and one-dimensional integer arrays of fixed size.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Some versions include stacks.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> All variables and array elements are initialized to zero.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
* ''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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
** '''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>{{cite arxiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
}}</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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Procedure Call:''' <code>call id</code> executes procedure <code>id</code> forwards; <code>uncall id</code> executes procedure <code>id</code> backwards.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> Procedures operate via side effects on the global store.
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
** '''Sequence:''' <code>s1; s2</code>. The inverse is <code>s2<sup>−1</sup>; s1<sup>−1</sup></code>.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
 
'''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>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>, simulating RTMs<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>, Fast Fourier Transform (FFT)<ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref>, graph algorithms <ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref>, and simulating the Schrödinger wave equation.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| last2 = Glück
| first2 = Robert
| editor-last1 = Ramalingam
| editor-first1= G.
| editor-last2 = Visser
| editor-first2= Eelco
| title = A reversible programming language and its invertible self-interpreter
| book-title = Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2007, Nice, France, January 15-16, 2007
| pages = 144–153
| publisher = ACM
| year = 2007
| url = https://doi.org/10.1145/1244381.1244404
| doi = 10.1145/1244381.1244404
| id = {{DBLP|conf/pepm/YokoyamaG07}}
<!-- biburl: https://dblp.org/rec/conf/pepm/YokoyamaG07.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Sun, 02 Jun 2019 21:16:05 +0200 -->
}}</ref>
 
The following fibpair procedure in Janus calculates a pair of consecutive Fibonacci numbers.<ref>{{cite journal
| last1 = Glück
| first1 = Robert
| last2 = Yokoyama
| first2 = Tetsuo
| title = Reversible computing from a programming language perspective
| journal = Theoretical Computer Science
| volume = 953
| pages = 113429
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> Given an input <code>n</code>, it sets <code>x1</code> to <code>F(n)</code> and <code>x2</code> to <code>F(n+1)</code>, assuming <code>x1</code> and <code>x2</code> are initially <code>0</code>:
 
<pre>
int n x1 x2 // variable declarations
 
procedure fibpair
if n=0 then x1 += 1
x2 += 1
else n -= 1
call fibpair
x1 += x2
x1 <=> x2
fi x1=x2
</pre>
For calling and uncalling the Fibonacci-pair procedure we use
<pre>
procedure main_fwd
n += 4
call fibpair
 
prodecure main_bwd
x1 += 5
x2 += 8
uncall fibpair
</pre>
 
=== R Language (MIT) ===
 
The R language (distinct from the [[R (programming language)|statistical language R]]) was developed by Michael P. Frank at [[MIT]] in the late 1990s as part of the Reversible Computing project.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> It is an imperative, compiled language featuring an S-expression (Lisp-like) syntax.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> A key aspect of R's design was its close integration with hardware development; it was designed to target the Pendulum reversible instruction set architecture (PISA), developed concurrently at MIT for an adiabatic CMOS processor.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
 
'''Syntax and Semantics:'''
* ''Program Structure:'' Programs are defined using <code>(defmain ...)</code> for the main routine and <code>(defsub ...)</code> for subroutines. Global variables and arrays are declared with <code>(defword ...)</code> and <code>(defarray ...)</code>.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* ''Data Types:'' R primarily supports integers and integer arrays.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* ''Statements:''
** '''Assignment/Update:''' Includes increment (<code>loc ++</code>), negation (<code>- loc</code>), swap (<code>loc <-> loc</code>), and reversible updates (<code>loc op= e</code>) using operators like <code>+=</code>, <code>-=</code>, <code>^=</code>, and specialized comparison-updates (<code><=<</code>, <code>>=></code>).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> Similar restrictions to Janus apply regarding variable dependencies.
** '''Conditional:''' <code>(if e then s*)</code>. To ensure reversibility, the language requires that the value of the conditional expression <code>e</code> must be the same before and after the execution of the <code>then</code> block (<code>s*</code>).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> This acts as an implicit invariant assertion, similar in function to Janus's explicit exit assertion.
** '''Loop:''' <code>(for name = e_start to e_end s*)</code>. Reversibility requires that the loop iteration variable (<code>name</code>) must have the same value before entering and after exiting the loop.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Local Binding:''' <code>(let ((name <- e)) s*)</code>. Introduces a local variable <code>name</code> initialized with <code>e</code>. Reversibility is ensured by requiring the variable to be returned to a known state (e.g., zero-cleared) before the scope is exited, analogous to Janus's <code>local/delocal</code>.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Procedure Call:''' Explicit forward <code>(call subname e*)</code> and reverse <code>(rcall subname e*)</code> calls are provided.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Output:''' <code>(printword e)</code> and <code>(println)</code> are included for output.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> These are inherently irreversible operations.
 
'''Pendulum/PISA Target Architecture:''' The R language was designed with a specific hardware target: the Pendulum processor.<ref>{{cite thesis
| last1 = Frank
| first1 = Michael P.
| title = Reversibility for efficient computing
| publisher = Massachusetts Institute of Technology
| ___location = Cambridge, MA, USA
| year = 1999
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/9464
| id = {{DBLP|phd/ndltd/Frank99}}
<!-- biburl: https://dblp.org/rec/phd/ndltd/Frank99.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 04 May 2022 12:58:38 +0200 -->
}}</ref>
* ''Architecture:'' Pendulum is a 12-bit, [[RISC]]-inspired, fully reversible microprocessor implemented in 0.5µm CMOS.<ref>{{cite thesis
| last1 = Vieri
| first1 = Carlin
| title = Reversible computer engineering and architecture
| publisher = Massachusetts Institute of Technology
| ___location = Cambridge, MA, USA
| year = 1999
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
| id = {{DBLP|phd/ndltd/Vieri99}}
<!-- biburl: https://dblp.org/rec/phd/ndltd/Vieri99.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 04 May 2022 12:58:32 +0200 -->
}}</ref> It features general-purpose registers and fixed-length instructions.<ref>{{cite thesis
| last1 = Vieri
| first1 = Carlin
| title = Reversible computer engineering and architecture
| publisher = Massachusetts Institute of Technology
| ___location = Cambridge, MA, USA
| year = 1999
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
| id = {{DBLP|phd/ndltd/Vieri99}}
<!-- biburl: https://dblp.org/rec/phd/ndltd/Vieri99.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 04 May 2022 12:58:32 +0200 -->
}}</ref>
* ''PISA Features:'' The instruction set includes several features tailored for reversibility:
** A Direction Bit (DIR) register tracks forward/backward execution mode.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** A Branch Bit (BR) register assists with reversible control flow.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** Branch instructions (e.g., <code>BEZ</code>, <code>BLTZ</code>) are conditional and require careful pairing. Reverse branches (<code>RBEZ</code>, <code>RBLTZ</code>) also toggle the DIR bit.<ref>{{cite thesis
| last1 = Vieri
| first1 = Carlin
| title = Reversible computer engineering and architecture
| publisher = Massachusetts Institute of Technology
| ___location = Cambridge, MA, USA
| year = 1999
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
| id = {{DBLP|phd/ndltd/Vieri99}}
<!-- biburl: https://dblp.org/rec/phd/ndltd/Vieri99.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 04 May 2022 12:58:32 +0200 -->
}}</ref>
** Memory access uses a reversible <code>EXCH</code> (exchange) instruction that swaps register and memory contents.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** Arithmetic and logic instructions (e.g., <code>ADD</code>, <code>ANDX</code>, <code>XOR</code>, <code>SLLX</code>, <code>RL</code>) are designed to be reversible, with some operations' behavior (like addition/subtraction or rotation direction) dependent on the DIR bit.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
 
'''Code Examples:'''
 
The following PISA assembly code<ref>{{cite conference
| last1 = Axelsen
| first1 = Holger Bock
| last2 = Glück
| first2 = Robert
| last3 = Yokoyama
| first3 = Tetsuo
| editor-last1 = Diekert
| editor-first1= Volker
| editor-last2 = Volkov
| editor-first2= Mikhail V.
| editor-last3 = Voronkov
| editor-first3= Andrei
| title = Reversible Machine Code and Its Abstract Processor Architecture
| book-title = Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings
| series = Lecture Notes in Computer Science
| volume = 4649
| pages = 56–69
| publisher = Springer
| year = 2007
| url = https://doi.org/10.1007/978-3-540-74510-5_9
| doi = 10.1007/978-3-540-74510-5_9
| id = {{DBLP|conf/csr/AxelsenGY07}}
<!-- biburl: https://dblp.org/rec/conf/csr/AxelsenGY07.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:01:20 +0100 -->
}}</ref> simulates a free-falling object. It includes a main section to call and "uncall" (reverse) a subroutine named Fall, which contains the core simulation logic.
 
<pre>
Call Fall:
10: ADDI h 1000
11: ADDI tend 5
12: BRA 16 ; call
 
Uncall Fall:
18: ADDI v 40
19: ADDI t 4
20: ADDI tend 4
21: RBRA 7 ; uncall
 
Subroutine Fall:
27: BRA 9
28: SWAPBR rtn ; br <=> rtn
29: NEG rtn ; rtn=-rtn
30: BGTZ t 5 ; t > 0?
31: ADDI v 10 ; v += 10
32: ADDI h 5 ; h += 5
33: SUB h v ; h -= v
34: ADDI t 1 ; t += 1
35: BNE t tend -5 ; t != tend?
36: BRA -9
</pre>
 
The R program defines global variables for height (h), end time (tend), velocity (v), and current time (t). The core logic is encapsulated in the Fall subroutine, which simulates the object's motion. The main routine initializes parameters, calls Fall to simulate forward motion, then modifies parameters and calls Fall in reverse (rcall Fall), mirroring the structure of the PISA example's "Call Fall" and "Uncall Fall" sections.
 
A key feature of R's <code>if</code> statement is that the conditional expression must evaluate to the same truth value before and after the execution of its then block. The Fall subroutine in PISA (lines 30-36) effectively has a loop that runs as long as <code>t</code> is not equal to <code>tend</code>, but this loop is only entered if an initial condition (implied by <code>BGTZ t 5</code> meaning skip if <code>t > 0</code>, so run if <code>t <= 0</code>) is met. To translate this faithfully and handle R's <code>if</code> semantics, the R code for Fall uses a let binding to capture the state of the initial condition (<code>t <= 0</code>) before the loop. The <code>if</code> then operates on this captured, unchanging boolean value. The loop itself is represented by R's for construct, iterating tend times, which corresponds to the PISA loop structure (<code>BNE t tend -5</code>).
 
<pre>
;; Global variable declarations
(defword h)
(defword tend)
(defword v)
(defword t)
 
;; Subroutine to simulate falling
;; Corresponds to PISA "Subroutine Fall" (lines 27-36)
(defsub Fall ()
;; The PISA code at line 30 (BGTZ t 5) skips the main simulation
;; if t > 0. This means the simulation loop runs if t <= 0.
;; We use 'let' to capture this condition, and 'if' operates on the captured value.
(let ((do_run <- (<= t 0))) ;; Capture condition: t must be <= 0 to run.
;; 'do_run' is a local temporary.
(if do_run ;; If the condition was true (t was <= 0 initially)
then
(progn ;; Execute the simulation loop
;; The PISA loop (lines 31-35) effectively iterates 'tend' times,
;; incrementing 't' each time, starting from its initial value (which is 0
;; when 'do_run' is true). The BNE t tend -5 continues as long as t != tend.
;; R's 'for' loop is a suitable high-level representation.
;; We assume 'tend' represents the number of iterations *from t=0*.
(for i = 1 to tend ;; Loop 'tend' times
(progn
(+= v 10) ;; PISA: ADDI v 10
(+= h 5) ;; PISA: ADDI h 5
(-= h v) ;; PISA: SUB h v
(++ t) ;; PISA: ADDI t 1
)
)
)
;; else (if 'do_run' is false, meaning t was > 0 initially), do nothing,
;; mimicking the PISA BGTZ t 5 branch.
)
;; Upon exiting 'let', 'do_run' is restored/cleared, satisfying R's rules
;; for 'let' and ensuring the 'if do_run' invariant holds for 'do_run'.
)
)
 
;; Main program routine
(defmain ()
;; Initialize global variables to 0.
;; While PISA doesn't show explicit zeroing, R programs often start clean.
;; These are reversible assignments.
(-= h h) ;; h = 0
(-= tend tend) ;; tend = 0
(-= v v) ;; v = 0
(-= t t) ;; t = 0
 
;; --- "Call Fall" section from PISA ---
;; Set initial parameters for forward simulation
(+= h 1000) ; PISA: ADDI h 1000
(+= tend 5) ; PISA: ADDI tend 5
; t and v are 0 from initialization.
 
;; Call the Fall subroutine to simulate forward motion
;; PISA: BRA 16 (relative branch to call setup, actual call is implicit)
(call Fall)
 
;; State after (call Fall) with h_initial=1000, tend_initial=5, t_initial=0, v_initial=0:
;; Inside Fall: do_run = (<= 0 0) = true. Loop runs 5 times.
;; t becomes 0 + 5 = 5.
;; v becomes 0 + 5*10 = 50.
;; h becomes 1000 + 5*5 - (10+20+30+40+50) = 1000 + 25 - 150 = 875.
;; tend remains 5 (Fall does not modify the 'tend' global it uses for loop count).
 
;; (printword h) (printword v) (printword t) (printword tend) (println)
;; Expected: h=875, v=50, t=5, tend=5
 
;; --- "Uncall Fall" section from PISA ---
;; The PISA code modifies v, t, and tend before the reverse call.
;; Current state from R perspective: h=875, v=50, t=5, tend=5.
(+= v 40) ; PISA: ADDI v 40. v = 50 + 40 = 90
(+= t 4) ; PISA: ADDI t 4. t = 5 + 4 = 9
(+= tend 4) ; PISA: ADDI tend 4. global 'tend' becomes 5 + 4 = 9
;; h remains 875.
 
;; Perform the reverse call to Fall
;; PISA: RBRA 7 (relative branch to uncall setup)
(rcall Fall)
 
;; Behavior of (rcall Fall):
;; 'rcall Fall' executes the inverse of 'Fall'.
;; Inside 'Fall' (conceptually, during rcall):
;; The (let ((do_run <- (<= t 0))) ...) block is reversed.
;; The (<= t 0) condition is evaluated with current t=9. (<= 9 0) is false.
;; So, 'do_run' (if we consider its "uncomputed" state) would correspond to 'false'.
;; The 'if do_run' block's 'then' part (the loop) was not executed in the forward
;; direction corresponding to this 'false' condition. Thus, its reverse also does nothing.
;; The net effect, matching PISA's BGTZ t 5, is that if t > 0, the main body of Fall
;; (and its reverse) is skipped.
;; Final state after (rcall Fall): h=875, v=90, t=9, tend=9.
;; This is because 'Fall' was effectively a no-op due to t=9 > 0.
;; The 'rcall' correctly reverses this no-op.
 
;; (printword h) (printword v) (printword t) (printword tend) (println)
;; Expected: h=875, v=90, t=9, tend=9
)
</pre>
 
=== Overview of Other Reversible Languages ===
 
Research has continued beyond Janus and R, exploring different paradigms and features:
 
* '''Eel (Energy-Efficient Language):''' Notable for supporting partially reversible computation. It allows mixing reversible operations with irreversible ones.<ref>{{cite arxiv
| last1 = Tyagi
| first1 = Nirvan
| last2 = Lynch
| first2 = Jayson
| last3 = Demaine
| first3 = Erik D.
| title = Toward an Energy Efficient Language and Compiler for (Partially) Reversible Algorithms
| eprint = 1605.08475
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/TyagiLD16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
}}</ref> To handle irreversible steps during reversal, Eel uses a "log stack" to save the necessary information (e.g., overwritten values), explicitly trading increased space complexity for the ability to reverse irreversible actions, while associating an energy cost with these actions based on Landauer's principle.<ref>{{cite arxiv
| last1 = Tyagi
| first1 = Nirvan
| last2 = Lynch
| first2 = Jayson
| last3 = Demaine
| first3 = Erik D.
| title = Toward an Energy Efficient Language and Compiler for (Partially) Reversible Algorithms
| eprint = 1605.08475
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/TyagiLD16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
}}</ref> It features advanced control logic constructs (protected/general conditionals and loops) offering different points on the energy-space trade-off spectrum.<ref>{{cite arxiv
| last1 = Tyagi
| first1 = Nirvan
| last2 = Lynch
| first2 = Jayson
| last3 = Demaine
| first3 = Erik D.
| title = Toward an Energy Efficient Language and Compiler for (Partially) Reversible Algorithms
| eprint = 1605.08475
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/TyagiLD16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
}}</ref> This makes Eel distinct from fully reversible languages like Janus, aiming for more flexibility in algorithm design.<ref>{{cite arxiv
| last1 = Tyagi
| first1 = Nirvan
| last2 = Lynch
| first2 = Jayson
| last3 = Demaine
| first3 = Erik D.
| title = Toward an Energy Efficient Language and Compiler for (Partially) Reversible Algorithms
| eprint = 1605.08475
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/TyagiLD16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
}}</ref>
* '''Rfun:''' A reversible functional programming language.<ref>{{cite web |url=https://aubert.perso.math.cnrs.fr/notes/exemples_cand_tt/ASU/cp.pdf |title=Reversible Computation |website= Classroom Presentation at Appalachian State University |access-date=April 9, 2025}}</ref> Its semantics have been modeled using categorical structures like join inverse rig categories, highlighting the connection between functional programming and abstract algebraic models of reversibility.<ref>{{cite conference
| last1 = Kaarsgaard
| first1 = Robin
| last2 = Rennela
| first2 = Mathys
| editor-last1 = Sokolova
| editor-first1= Ana
| title = Join inverse rig categories for reversible functional programming, and beyond
| book-title = Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021
| series = EPTCS
| volume = 351
| pages = 152–167
| year = 2021
| url = https://doi.org/10.4204/EPTCS.351.10
| doi = 10.4204/EPTCS.351.10
| id = {{DBLP|journals/corr/abs-2105-09929}}
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2105-09929.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:31:45 +0100 -->
}}</ref>
* '''ROOPL:''' The first reversible object-oriented programming language.<ref>{{cite conference
| last1 = Haulund
| first1 = Tue
| last2 = Mogensen
| first2 = Torben Ægidius
| last3 = Glück
| first3 = Robert
| editor-last1 = Phillips
| editor-first1= Iain
| editor-last2 = Rahaman
| editor-first2= Hafizur
| title = Implementing Reversible Object-Oriented Language Features on Reversible Machines
| book-title = Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| pages = 66–73
| publisher = Springer
| year = 2017
| url = https://doi.org/10.1007/978-3-319-59936-6_5
| doi = 10.1007/978-3-319-59936-6_5
| id = {{DBLP|conf/rc/HaulundMG17}}
<!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
}}</ref> It extends the imperative reversible paradigm with features like user-defined data types (classes), inheritance, and subtype polymorphism.<ref>{{cite arxiv
| last1 = Haulund
| first1 = Tue
| title = Design and Implementation of a Reversible Object-Oriented Programming Language
| eprint = 1707.07845
| year = 2017
<!-- biburl: https://dblp.org/rec/journals/corr/Haulund17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
}}</ref> ROOPL demonstrates that higher-level object-oriented abstractions can be integrated into a reversible framework while maintaining local invertibility and r-Turing completeness. It was designed for garbage-free translation to the PISA assembly language.<ref>{{cite arxiv
| last1 = Haulund
| first1 = Tue
| title = Design and Implementation of a Reversible Object-Oriented Programming Language
| eprint = 1707.07845
| year = 2017
<!-- biburl: https://dblp.org/rec/journals/corr/Haulund17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
}}</ref>
* '''Reversible HDLs:''' To aid in the complex task of designing reversible logic circuits, specialized [[Hardware Description Language]]s have been developed.<ref>{{cite arxiv
| last1 = Thomsen
| first1 = Michael Kirkedal
| title = Design of Reversible Computing Systems; Large Logic, Languages, and Circuits
| eprint = 2309.11832
| year = 2023
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2309-11832.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
}}</ref> These are often functional in nature and may include features like [[Linear type system|linear types]] to manage resources and ensure garbage-free designs. They facilitate a design flow from high-level descriptions to gate-level implementations.<ref>{{cite arxiv
| last1 = Thomsen
| first1 = Michael Kirkedal
| title = Design of Reversible Computing Systems; Large Logic, Languages, and Circuits
| eprint = 2309.11832
| year = 2023
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2309-11832.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
}}</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>{{cite arxiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
}}</ref> Their semantics can also be captured using categorical frameworks.<ref>{{cite conference
| last1 = Glück
| first1 = Robert
| last2 = Kaarsgaard
| first2 = Robin
| editor-last1 = Staton
| editor-first1= Sam
| title = A Categorical Foundation for Structured Reversible Flowchart Languages
| book-title = Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018
| series = Electronic Notes in Theoretical Computer Science
| volume = 341
| pages = 155–171
| publisher = Elsevier
| year = 2018
| url = https://doi.org/10.1016/j.entcs.2018.03.021
| doi = 10.1016/J.ENTCS.2018.03.021
| id = {{DBLP|journals/entcs/GluckK18}}
<!-- biburl: https://dblp.org/rec/journals/entcs/GluckK18.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Feb 2020 15:57:36 +0100 -->
}}</ref>
* '''Other Languages:''' A variety of other languages have been proposed, including Psi-Lisp <ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| last2 = Wang
| first2 = Meng
| title = Sparcl: A language for partially invertible computation
| journal = Journal of Functional Programming
| volume = 34
| year = 2024
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}}
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Pi/Pi^o <ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>, Inv <ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| last2 = Wang
| first2 = Meng
| title = Sparcl: A language for partially invertible computation
| journal = Journal of Functional Programming
| volume = 34
| year = 2024
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}}
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Yarel <ref>{{cite arxiv
| last1 = Grandi
| first1 = Claudio
| last2 = Moshiri
| first2 = Dariush
| last3 = Roversi
| first3 = Luca
| title = Introducing Yet Another REversible Language
| eprint = 1902.05369
| year = 2019
<!-- biburl: https://dblp.org/rec/journals/corr/abs-1902-05369.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 21 May 2019 18:03:37 +0200 -->
}}</ref>, SPARCL <ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| last2 = Wang
| first2 = Meng
| title = Sparcl: A language for partially invertible computation
| journal = Journal of Functional Programming
| volume = 34
| year = 2024
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}}
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Hermes (focused on cryptography) <ref>{{cite web |url=https://reversible-computation-2020.github.io/slides/day-1-session-2-torben-mogensen.pdf |title=Hermes: A Language for Lightweight Encryption |website=Reversible Computation (RC) Lecture |access-date=April 9, 2025}}</ref>, and Revs (compiling F# subset to circuits).<ref>{{cite arxiv
| last1 = Amy
| first1 = Matthew
| last2 = Roetteler
| first2 = Martin
| last3 = Svore
| first3 = Krysta M.
| title = Verified compilation of space-efficient reversible circuits
| eprint = 1603.01635
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/AmyRS16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 17 Sep 2019 14:15:13 +0200 -->
}}</ref> Reversibility has also been studied in the context of existing languages like [[Erlang (programming language)|Erlang]].<ref>{{cite journal
| last1 = Lanese
| first1 = Ivan
| last2 = Schultz
| first2 = Ulrik Pagh
| last3 = Ulidowski
| first3 = Irek
| title = Reversible Computing in Debugging of Erlang Programs
| journal = IT Professional
| volume = 24
| issue = 1
| pages = 74–80
| year = 2022
| doi = 10.1109/MITP.2021.3117920
| url = https://doi.org/10.1109/MITP.2021.3117920
| id = {{DBLP|journals/itpro/LaneseSUS22}}
<!-- bibtex source: DBLP:journals/itpro/LaneseSUS22 -->
<!-- biburl: https://dblp.org/rec/journals/itpro/LaneseSUS22.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Fri, 01 Apr 2022 11:23:39 +0200 -->
}}</ref>
 
=== Comparison of Reversible Programming Languages ===
 
The following table summarizes key characteristics of some prominent reversible programming languages discussed:
 
{| class="wikitable"
|+ Comparison of Reversible Programming Languages<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> <ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> <ref>{{cite arxiv
| last1 = Haulund
| first1 = Tue
| title = Design and Implementation of a Reversible Object-Oriented Programming Language
| eprint = 1707.07845
| year = 2017
<!-- biburl: https://dblp.org/rec/journals/corr/Haulund17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
}}</ref>
! Feature !! [[Janus (time-reversible computing programming language)|Janus]] !! R (MIT) !! Eel !! ROOPL
|-
! Paradigm
| Imperative, Procedural
| Imperative, Compiled
| Imperative, Partially Reversible
| Imperative, Object-Oriented
|-
! Reversibility Model
| Full (Locally Invertible)
| Full (Locally Invertible)
| Partial (Allows Irreversible Ops)
| Full (Locally Invertible)
|-
! Key Control Flow
| <code>if..fi</code> (test+assert),<br /><code>from..until</code> (assert+test)
| <code>(if..)</code> (invariant),<br /><code>(for..)</code> (invariant)
| Protected/General if/loop,<br />Log/Unroll blocks
| Reversible if, loop (similar to Janus),<br />Method Calls
|-
! Data Types
| Integers, Arrays, Stacks
| Integers, Arrays
| Integers, Arrays, Log Stack
| Integers, Arrays, User-defined Classes (Objects), Inheritance
|-
! Inversion Mechanism
| <code>uncall</code> statement,<br />Local Inversion
| <code>rcall</code> statement,<br />Local Inversion
| <code>Unroll</code> statement<br />(uses Log Stack)
| <code>uncall</code> (for methods),<br />Local Inversion
|-
! Target/Compiler
| Interpreters,<br />Partial Evaluator,<br />Self-Interpreter
| PISA (Pendulum ISA) Compiler
| Compiler & Interpreter (Java-based),<br />Energy Simulation
| PISA Compiler<br />(Garbage-free)
|}
 
This comparison highlights the different design choices made. Janus and R enforce full reversibility through language constructs, differing primarily in syntax (C-like vs S-expression) and target (interpretation vs PISA compilation). Eel introduces partial reversibility, allowing irreversible operations at the cost of using a log stack for reversal information and incurring a conceptual energy cost, aiming for greater flexibility. ROOPL extends the fully reversible imperative model with object-oriented features, demonstrating the applicability of higher-level abstractions.
 
== References ==
Retrieved from "https://en.wikipedia.org/wiki/Reversible_programming_language"