Content deleted Content added
merged duplicate references |
m uncategorized |
||
| (3 intermediate revisions by 3 users not shown) | |||
Line 1:
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
== Core concepts and design principles ==
The fundamental goal of a reversible programming language is to support computation that is deterministic in both the forward and backward directions.
| last1 = Glück
| first1 = Robert
Line 14:
| 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 -->
| doi-access= free
}}</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.
Key in the design of many reversible languages is cleanliness or garbage-free computation.<ref>{{cite arXiv
Line 59 ⟶ 40:
| 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
| series = Lecture Notes in Computer Science
| volume = 7165
Line 67 ⟶ 48:
| 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 -->
| url-access= subscription
}}</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-
| last1 = Yokoyama
| first1 = Tetsuo
Line 90 ⟶ 69:
| 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
}}</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
| 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 name="Palazzo-2501.05259">{{cite arXiv
| last1 = Palazzo
| first1 = Matteo
Line 115 ⟶ 90:
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref name="Yokoyama-
* '''Procedure Calls:''' Languages need mechanisms to invoke procedures both forwards and backwards. This is often achieved through paired commands like <code>call</code> (forward execution) and <code>uncall</code> or <code>rcall</code> (backward execution).<ref name="Choudhury"/>
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref name="Yokoyama-
| last1 = Haulund
| first1 = Tue
Line 141 ⟶ 104:
| 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
| series = Lecture Notes in Computer Science
| volume = 10301
Line 149 ⟶ 112:
| 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 -->
| url-access= subscription
}}</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"/>
Line 158 ⟶ 119:
== Janus Language ==
[[Janus (time-reversible computing programming language)|Janus]] is widely recognized as the first structured, imperative programming language designed explicitly for reversible computation.<ref name="Yokoyama-
===Design philosophy===
Line 165 ⟶ 126:
===Syntax and semantics===
* ''Program Structure:'' A Janus program consists of global variable declarations followed by procedure declarations. The execution starts at a procedure named <code>main</code>, or the last procedure defined if <code>main</code> is absent.
* ''Data Types:'' Janus primarily uses 32-bit integers (interpreters may differ on signed vs. unsigned) and one-dimensional integer arrays of fixed size.<ref name="Yokoyama-
* ''Statements:''
** '''Assignment:''' Reversible updates <code>x op= e</code> or <code>x[e] op= e</code>, where <code>op</code> is <code>+</code>, <code>-</code>, or <code>^</code> (bitwise XOR). The variable <code>x</code> must not appear in the expression <code>e</code>.<ref name="Yokoyama-
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.
** '''Conditional:''' <code>if e1 then s1 else s2 fi e2</code>. The expression <code>e1</code> is the test evaluated upon forward entry. The expression <code>e2</code> is an assertion evaluated upon forward exit; it must be true if <code>s1</code> was executed and false if <code>s2</code> was executed. For backward execution (e.g., via <code>uncall</code>), <code>e2</code> acts as the test to determine which inverse branch (s1<sup>−1</sup> or s2<sup>−1</sup>) to take, and <code>e1</code> becomes the assertion checked upon exiting backward.<ref
** '''Loop:''' <code>from e1 do s1 loop s2 until e2</code>. Upon forward entry, assertion <code>e1</code> must be true. <code>s1</code> is executed. Then, test <code>e2</code> is evaluated. If true, the loop terminates. If false, <code>s2</code> is executed, after which assertion <code>e1</code> must now be false for the loop to continue back to <code>s1</code>. In reverse, <code>e2</code> is the entry assertion, s2<sup>−1</sup> is executed, <code>e1</code> is the test (loop continues if false, terminates if true), and s1<sup>−1</sup> is executed if the loop continues.<ref name="Yokoyama-2010.02.007"/>
** '''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"/>
** '''Procedure Call:''' <code>call id</code> executes procedure <code>id</code> forwards; <code>uncall id</code> executes procedure <code>id</code> backwards.<ref name="Choudhury"/> Procedures operate via side effects on the global store.
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.
Line 189 ⟶ 138:
===Implementations and code examples===
Several online interpreters for Janus exist.<ref>{{cite web |url=https://topps.diku.dk/pirc/?id=janus |title=Janus: a reversible imperative programming language |website=University of Copenhagen (DIKU) |access-date=April 9, 2025}}</ref> Janus has been used to implement various algorithms reversibly, including computing Fibonacci pairs,<ref name="Yokoyama-
| last1 = Yokoyama
| first1 = Tetsuo
Line 199 ⟶ 148:
| 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
| pages = 144–153
| publisher = ACM
Line 205 ⟶ 154:
| 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 -->
| url-access= subscription
}}</ref>
The following fibpair procedure in Janus calculates a pair of consecutive Fibonacci numbers.<ref name="Glück-2022.06.010"/>
<pre>
Line 245 ⟶ 176:
procedure main_fwd
n += 4
call fibpair
prodecure main_bwd
Line 284 ⟶ 215:
<!-- 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
Line 334 ⟶ 265:
** 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"/>
===Code examples===
The following PISA assembly code<ref>{{cite conference
Line 350 ⟶ 281:
| 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
| series = Lecture Notes in Computer Science
| volume = 4649
Line 358 ⟶ 289:
| 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 -->
| url-access= subscription
}}</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.
Line 570 ⟶ 499:
| 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
}}</ref>
* '''ROOPL:''' The first reversible object-oriented programming language.<ref>{{cite conference
Line 587 ⟶ 514:
| 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
| series = Lecture Notes in Computer Science
| volume = 10301
Line 595 ⟶ 522:
| 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 -->
| url-access= subscription
}}</ref> It extends the imperative reversible paradigm with features like user-defined data types (classes), inheritance, and subtype polymorphism.<ref>{{cite arXiv
| last1 = Haulund
Line 641 ⟶ 566:
| class = cs.PL
}}</ref>
* '''Flowchart Languages:''' Languages like R-CORE, R-WHILE, and SRL provide structured representations of reversible control flow, often serving as intermediate languages or theoretical models.<ref name="Palazzo-2501.05259"/> Their semantics can also be captured using categorical frameworks.<ref>{{cite
| last1 = Glück
| first1 = Robert
Line 661 ⟶ 574:
| 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
| series = Electronic Notes in Theoretical Computer Science
| volume = 341
Line 669 ⟶ 582:
| 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
| last1 = Matsuda
| first1 = Kazutaka
Line 686 ⟶ 596:
| 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 -->
| doi-access= free
}}</ref> Pi/Pi^o,<ref name="Choudhury"/> Inv,<ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
Line 703 ⟶ 610:
| 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 -->
| doi-access= free
}}</ref> Yarel,<ref>{{cite arXiv
| last1 = Grandi
| first1 = Claudio
Line 722 ⟶ 626:
<!-- timestamp: Tue, 21 May 2019 18:03:37 +0200 -->
| class = cs.PL
}}</ref>
| last1 = Matsuda
| first1 = Kazutaka
Line 734 ⟶ 638:
| 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 -->
| doi-access= free
}}</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
| last1 = Amy
| first1 = Matthew
Line 750 ⟶ 651:
| series = Lecture Notes in Computer Science
| arxiv = 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 -->
| volume = 10427
| pages = 3–21
Line 775 ⟶ 673:
| 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 -->
| hdl-access= free
}}</ref>
Line 787 ⟶ 682:
{| class="wikitable"
|+ Comparison of Reversible Programming Languages<ref name="Yokoyama-
| last1 = Haulund
| first1 = Tue
Line 841 ⟶ 736:
== References ==
{{reflist}}
{{uncategorized|date=August 2025}}
| |||