Content deleted Content added
Citation bot (talk | contribs) Alter: template type, title. Add: hdl, bibcode, isbn, doi, pages, volume, arxiv, series, chapter, class, article-number. Removed parameters. Some additions/deletions were parameter name changes. Upgrade ISBN10 to 13. | Use this bot. Report bugs. | Suggested by Folkezoft | #UCB_toolbar |
|||
Line 11:
| journal = Theoretical Computer Science
| volume = 953
|
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
Line 27:
| journal = Theoretical Computer Science
| volume = 953
|
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
Line 37:
}}</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
| last1 = Thomsen
| first1 = Michael Kirkedal
Line 46:
<!-- 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
Line 121 ⟶ 122:
<!-- 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
| last1 = Palazzo
| first1 = Matteo
Line 132 ⟶ 133:
<!-- 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
| last1 = Yokoyama
Line 151 ⟶ 153:
<!-- 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
| last1 = Palazzo
| first1 = Matteo
Line 162 ⟶ 164:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</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
Line 366 ⟶ 369:
}}</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
| last1 = Palazzo
| first1 = Matteo
Line 377 ⟶ 380:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</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
Line 519 ⟶ 523:
| journal = Theoretical Computer Science
| volume = 953
|
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
Line 664 ⟶ 668:
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/9464
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/9464
Line 678 ⟶ 683:
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
Line 691 ⟶ 697:
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
Line 724 ⟶ 731:
| ___location = Cambridge, MA, USA
| year = 1999
| hdl = 1721.1/80144
| type = PhD thesis
| url = https://hdl.handle.net/1721.1/80144
Line 914 ⟶ 922:
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
| last1 = Tyagi
| first1 = Nirvan
Line 927 ⟶ 935:
<!-- 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
| last1 = Tyagi
| first1 = Nirvan
Line 940 ⟶ 949:
<!-- 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
| last1 = Tyagi
| first1 = Nirvan
Line 953 ⟶ 963:
<!-- 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
| last1 = Tyagi
| first1 = Nirvan
Line 966 ⟶ 977:
<!-- 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
Line 1,011 ⟶ 1,023:
<!-- 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
| last1 = Haulund
| first1 = Tue
Line 1,020 ⟶ 1,032:
<!-- 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
| last1 = Haulund
| first1 = Tue
Line 1,029 ⟶ 1,042:
<!-- 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
| last1 = Thomsen
| first1 = Michael Kirkedal
Line 1,039 ⟶ 1,053:
<!-- 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
| last1 = Thomsen
| first1 = Michael Kirkedal
Line 1,048 ⟶ 1,063:
<!-- 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>{{cite
| last1 = Palazzo
| first1 = Matteo
Line 1,060 ⟶ 1,076:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Their semantics can also be captured using categorical frameworks.<ref>{{cite conference
| last1 = Glück
Line 1,090 ⟶ 1,107:
| volume = 34
| year = 2024
| article-number = e2
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
Line 1,114 ⟶ 1,132:
| volume = 34
| year = 2024
| article-number = e2
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
Line 1,121 ⟶ 1,140:
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Yarel <ref>{{cite
| last1 = Grandi
| first1 = Claudio
Line 1,134 ⟶ 1,153:
<!-- 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
| last1 = Matsuda
Line 1,143 ⟶ 1,163:
| volume = 34
| year = 2024
| article-number = e2
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
Line 1,150 ⟶ 1,171:
<!-- 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
| last1 = Amy
| first1 = Matthew
Line 1,157 ⟶ 1,178:
| last3 = Svore
| first3 = Krysta M.
| title =
| chapter = Verified Compilation of Space-Efficient Reversible Circuits
| eprint = 1603.01635▼
| series = Lecture Notes in Computer Science
| 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
| 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
Line 1,177 ⟶ 1,204:
| 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}}
Line 1,217 ⟶ 1,246:
<!-- 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
| last1 = Haulund
| first1 = Tue
Line 1,226 ⟶ 1,255:
<!-- 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
| |||