Content deleted Content added
added Wayback link for "page not found" link |
|||
Line 51:
{{expand section|date=July 2014}}
The proof in Böhm and Jacopini's paper proceeds by [[structural induction|induction on the structure]] of the flow chart.<ref name="Harel"/>{{rp|381}} Because it employed [[Subgraph isomorphism problem|pattern matching in graphs]], the proof of Böhm and Jacopini's was not really practical as a [[program transformation]] algorithm, and thus opened the door for additional research in this direction.<ref name="amma92"/>
=== Reversible version ===
The Reversible Structured Program Theorem<ref>{{cite journal |last1=Yokoyama |first1=Tetsuo |last2=Axelsen |first2=Holger Bock |last3=Glück |first3=Robert |title=Fundamentals of reversible flowchart languages |journal=Theoretical Computer Science |date=January 2016 |volume=611 |pages=87–115 |doi=10.1016/j.tcs.2015.07.046}}</ref> is an important concept in the field of reversible computing. It posits that any computation achievable by a traditional, irreversible program can also be accomplished through a reversible program using only a structured combination of control flow constructs such as sequences, selections, and iterations, but with the additional constraint that each step must be reversible and some extra output. Furthermore, any reversible unstructured program can also be accomplished through a structured reversible program with only one iteration without any extra output. This theorem not only demonstrates the theoretical possibility of reversible computing matching the computational power of conventional computing but also lays the foundational principles for constructing reversible algorithms within a structured programming framework.
For the Structured Program Theorem, both local and global methods of proof are known. However, for its reversible version, while a global method of proof is recognized,<ref>{{cite journal |last1=Cooper |first1=David C. |title=Böhm and Jacopini's reduction of flow charts |journal=Communications of the ACM |date=August 1967 |volume=10 |issue=8 |pages=463 |doi=10.1145/363534.363539}}</ref> a local approach similar to that undertaken by Böhm and Jacopini<ref>{{cite journal |last1=Böhm |first1=Corrado |last2=Jacopini |first2=Giuseppe |title=Flow diagrams, turing machines and languages with only two formation rules |journal=Communications of the ACM |date=May 1966 |volume=9 |issue=5 |pages=366–371 |doi=10.1145/355592.365646}}</ref> is not yet known. This distinction is an example that underscores the challenges and nuances in establishing the foundations of reversible computing compared to traditional computing paradigms.
== Implications and refinements ==
| |||