|
A '''reversible programming language''' is designed to bridge the gap between the theoretical models of [[reversible computing]] and practical [[software development]]. They provide constructs that allow programmers to write [[source code |code]] that is guaranteed, by the language's [[Syntax (programming languages)|syntax]] and [[Semantics (computer science)|semantics]], to be [[Execution (computing)|executable]] both forwards and backwards [[Deterministic system|deterministically]].
== 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. <ref name="Glück-2022.06.010">{{cite journal
| last1 = Glück
| first1 = Robert
| journal = Theoretical Computer Science
| volume = 953
| pagesarticle-number = 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 -->
| url = https://doi.org/10.1016/j.tcs.2022.06.010
| doi-access= free
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
}}</ref> This is typically achieved by ensuring that every primitive operation and composite statement within the language is locally invertible.<ref name="Glück-2022.06.010"/> 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.
<!-- 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 arxivarXiv
| last1 = Thomsen
| first1 = Michael Kirkedal
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
| class = cs.PL
}}</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
| 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-54–5, 2011. Revised Papers
| series = Lecture Notes in Computer Science
| volume = 7165
| 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 -->
| id = {{DBLP|conf/rc/ThomsenAG11}}
| url-access= subscription
<!-- 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 name="Yokoyama-2010.02.007">{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| 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 -->
| doi-access= free
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
}}</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-2010.02.007"/> The swap operation (<code>x <=> y</code>), which exchanges the values of two variables, is another fundamental reversible update.<ref name="Choudhury">{{cite web
<!-- 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=... -->
<!-- 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 name="Palazzo-2501.05259">{{cite arxivarXiv
| last1 = Palazzo
| first1 = Matteo
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref>{{cite conference
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref name="Yokoyama-2010.02.007"/> 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 name="Palazzo-2501.05259"/> This explicit management of control flow information is a significant difference from conventional programming.
| last1 = 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"/>
| first1 = Tetsuo
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref name="Yokoyama-2010.02.007"/> 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 name="Choudhury"/> More recent research has explored reversible object-oriented features, including user-defined types, inheritance, and polymorphism.<ref>{{cite conference
| 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
| 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-76–7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| 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 -->
| id = {{DBLP|conf/rc/HaulundMG17}}
| url-access= subscription
<!-- 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>
* '''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 name="Choudhury"/>
== 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-2010.02.007"/>{{cite conferenceOriginally conceived by Christopher Lutz and Howard Derby at [[Caltech]] in the 1980s,<ref name="Choudhury"/> it was later rediscovered, formalized, and extended, notably by Tetsuo Yokoyama and Robert Glück.<ref name="Choudhury"/>
| 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 webname="Choudhury"/>
| 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 name="Yokoyama-2010.02.007"/>{{cite conferenceSome versions include stacks.<ref name="Yokoyama-2010.02.007"/> All variables and array elements are initialized to zero.<ref name="Yokoyama-2010.02.007"/>
| 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 conferencename="Yokoyama-2010.02.007"/>
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.
| last1 = Yokoyama
** '''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 name="Palazzo-2501.05259"/>
| first1 = Tetsuo
** '''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-2010.02.007"/>
| editor-last1 = Ulidowski
** '''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-2010.02.007"/>** '''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-2010.02.007"/>
| editor-first1= Irek
** '''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.
| title = Reversible Computation and Reversible Programming Languages
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
** '''Sequence:''' <code>s1; s2</code>. The inverse is <code>s2<sup>−1</sup>; s1<sup>−1</sup></code>.
| 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 name="Yokoyama-2010.02.007"/> simulating RTMs,<ref name="Yokoyama-2010.02.007"/> 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
| 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
| 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-1615–16, 2007
| pages = 144–153
| publisher = ACM
| 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 -->
| id = {{DBLP|conf/pepm/YokoyamaG07}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/pepm/YokoyamaG07.bib -->
}}</ref>
<!-- 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 name="Glück-2022.06.010"/>{{cite journalGiven 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>:
| 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>
procedure main_fwd
n += 4
call fibpair
prodecure main_bwd
== 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 name="Choudhury"/>{{cite webIt is an imperative, compiled language featuring an S-expression (Lisp-like) syntax.<ref name="Choudhury"/> 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 name="Choudhury"/>
| 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 webname="Choudhury"/>
* ''Data Types:'' R primarily supports integers and integer arrays.<ref name="Choudhury"/>
| 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 name="Choudhury"/>{{cite webSimilar 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 name="Choudhury"/> This acts as an implicit invariant assertion, similar in function to Janus's explicit exit assertion.
| last1 = Choudhury
** '''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 name="Choudhury"/>
| first1 = Vikraman
** '''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 name="Choudhury"/>
| title = Reversible Programming Languages
** '''Procedure Call:''' Explicit forward <code>(call subname e*)</code> and reverse <code>(rcall subname e*)</code> calls are provided.<ref name="Choudhury"/>
| date = April 2018
** '''Output:''' <code>(printword e)</code> and <code>(println)</code> are included for output.<ref name="Choudhury"/> These are inherently irreversible operations.
| 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===
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/9464
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/9464
<!-- 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
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
}}</ref>
* ''PISA Features:'' The instruction set includes several features tailored for reversibility:
** A Direction Bit (DIR) register tracks forward/backward execution mode.<ref>{{cite webname="Choudhury"/>
** A Branch Bit (BR) register assists with reversible control flow.<ref name="Choudhury"/>
| 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
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
<!-- 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 webname="Choudhury"/>
** 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 name="Choudhury"/>
| 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
| 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-73–7, 2007, Proceedings
| series = Lecture Notes in Computer Science
| volume = 4649
| 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 -->
| id = {{DBLP|conf/csr/AxelsenGY07}}
| url-access= subscription
<!-- 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.
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 arxivarXiv
| last1 = Tyagi
| first1 = Nirvan
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
| class = cs.PL
}}</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
}}</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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
| class = cs.PL
}}</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
}}</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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
| class = cs.PL
}}</ref> This makes Eel distinct from fully reversible languages like Janus, aiming for more flexibility in algorithm design.<ref>{{cite arxiv
}}</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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:25 +0200 -->
| class = cs.PL
}}</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
| 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 -->
| arxiv= 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
| 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-76–7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| 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 -->
| id = {{DBLP|conf/rc/HaulundMG17}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib -->
}}</ref> It extends the imperative reversible paradigm with features like user-defined data types (classes), inheritance, and subtype polymorphism.<ref>{{cite arXiv
<!-- 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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
| class = cs.PL
}}</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
}}</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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
| class = cs.PL
}}</ref>
* '''Reversible HDLs:''' To aid in the complex task of designing reversible logic circuits, specialized [[Hardware Description Language]]s have been developed.<ref>{{cite arxivarXiv
| last1 = Thomsen
| first1 = Michael Kirkedal
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
| class = cs.PL
}}</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
}}</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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 25 Sep 2023 15:34:00 +0200 -->
| 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 arxivconference
| 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
| 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-96–9, 2018
| series = Electronic Notes in Theoretical Computer Science
| volume = 341
| 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 -->
<!-- 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
| volume = 34
| year = 2024
| article-number = e2
| 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 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</ref> Pi/Pi^o,<ref name="Choudhury"/> Inv,<ref>{{cite journal
<!-- 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
| volume = 34
| year = 2024
| article-number = e2
| 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 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</ref> Yarel,<ref>{{cite arXiv
<!-- 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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 21 May 2019 18:03:37 +0200 -->
| class = cs.PL
}}</ref>, SPARCL <ref>{{cite journal
}}</ref> SPARCL,<ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| volume = 34
| year = 2024
| article-number = e2
| 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 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</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 book
<!-- 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
| last3 = Svore
| first3 = Krysta M.
| title = VerifiedComputer compilationAided of space-efficient reversible circuitsVerification
| chapter = Verified Compilation of Space-Efficient Reversible Circuits
| eprint = 1603.01635
| series = Lecture Notes in Computer Science
| year = 2016
| arxiv = 1603.01635
<!-- biburl: https://dblp.org/rec/journals/corr/AmyRS16.bib -->
| 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 -->
| volume = 10427
<!-- timestamp: Tue, 17 Sep 2019 14:15:13 +0200 -->
| pages = 3–21
| doi = 10.1007/978-3-319-63390-9_1
| isbn = 978-3-319-63389-3
}}</ref> Reversibility has also been studied in the context of existing languages like [[Erlang (programming language)|Erlang]].<ref>{{cite journal
| last1 = Lanese
| year = 2022
| doi = 10.1109/MITP.2021.3117920
| bibcode = 2022ITPro..24a..74L
| hdl = 11585/884503
| 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 -->
| id = {{DBLP|journals/itpro/LaneseSUS22}}
| hdl-access= free
<!-- 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>
{| class="wikitable"
|+ Comparison of Reversible Programming Languages<ref name="Yokoyama-2010.02.007"/><ref name="Choudhury"/><ref>{{cite conferencearXiv
| 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
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 13 Aug 2018 16:48:32 +0200 -->
| class = cs.PL
}}</ref>
! Feature !! [[Janus (time-reversible computing programming language)|Janus]] !! R (MIT) !! Eel !! ROOPL
== References ==
{{reflist}}
{{uncategorized|date=August 2025}}
| 