Structured program theorem: Difference between revisions

Revision as of 19:59, 9 December 2024

Revision as of 10:37, 22 January 2025

Line 9:

The theorem forms the basis of [[structured programming]], a programming paradigm which eschews [[Goto|goto commands]] and exclusively uses subroutines, sequences, selection and iteration.[[File:Structured program patterns.svg|Graphical representation of the three basic patterns of the structured program theorem — sequence, selection, and repetition — using [[Nassi–Shneiderman diagram|NS diagrams]] (blue) and [[flow chart]]s (green).|thumb|center|border|700px]]

== Origin and variants ==

The theorem is typically credited<ref name="Harel"/>{{rp|381}} to a 1966 paper by [[Corrado Böhm]] and [[{{ill|Giuseppe Jacopini]]|it}}.<ref name="BohmJacopini">{{cite journal |lastlast1=BohmBöhm |firstfirst1=Corrado |author2author-link1= Corrado Böhm |last2= Jacopini |first2= Giuseppe |author-link2= :it:Giuseppe Jacopini |date=May 1966 |title=Flow Diagrams, Turing Machines and Languages with Only Two Formation Rules |journal=[[Communications of the ACM]] |volume=9 |issue=5 |pages=366–371 |doi=10.1145/355592.365646 |citeseerx=10.1.1.119.9119 |s2cid=10236439 }}</ref> [[David Harel]] wrote in 1980 that the Böhm–Jacopini paper enjoyed "universal popularity",<ref name="Harel"/>{{rp|381}} particularly with proponents of structured programming. Harel also noted that "due to its rather technical style [the 1966 Böhm–Jacopini paper] is apparently more often cited than read in detail"<ref name="Harel"/>{{rp|381}} and, after reviewing a large number of papers published up to 1980, Harel argued that the contents of the Böhm–Jacopini proof were usually misrepresented as a [[Mathematical folklore|folk theorem]] that essentially contains a simpler result, a result which itself can be traced to the inception of modern computing theory in the papers of [[John von Neumann|von Neumann]]<ref>{{Citation|last1= Burks|first1= Arthur W.|last2= Goldstine|first2= Herman|last3= von Neumann|first3= John|author-link= Arthur W. Burks|author2-link= Herman Goldstine|author3-link = John von Neumann|title= Preliminary discussion of the Logical Design of an Electronic Computing Instrument|publisher= Institute for Advanced Study|___location= Princeton, NJ|year= 1947}}</ref> and [[Stephen Cole Kleene|Kleene]].<ref name="Harel"/>{{rp|383}}

Harel also writes that the more generic name was proposed by [[Harlan Mills|H.D. Mills]] as "The Structure Theorem" in the early 1970s.<ref name="Harel">{{cite journal|last=Harel|first=David|author-link=David Harel|year=1980|title=On Folk Theorems|journal=Communications of the ACM|volume=23|issue=7|pages=379–389|doi=10.1145/358886.358892|s2cid=16300625 |url=http://www.wisdom.weizmann.ac.il/~dharel/SCANNED.PAPERS/OnFolkTheorems.pdf}}</ref>{{rp|381}}

Line 55:

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|doi-access=free}}</ref> is an important concept in the field of [[reversible computing]]. It posits that any computation achievable by a reversible program can also be accomplished through a reversible program using only a structured combination of control flow constructs such as sequences, selections, and iterations. Any computation achievable by a traditional, irreversible program can also be accomplished through a reversible program, but with the additional constraint that each step must be reversible and some extra output.<ref>{{cite journal |last1=Bennett |first1=C. H. |title=Logical Reversibility of Computation |journal=IBM Journal of Research and Development |date=November 1973 |volume=17 |issue=6 |pages=525–532 |doi=10.1147/rd.176.0525}}</ref> Furthermore, any reversible unstructured program can also be accomplished through a structured reversible program with only one iteration without any extra output. This theorem lays the foundational principles for constructing reversible algorithms within a structured programming framework.

For the Structured Program Theorem, both local<ref name="BohmJacopini"/> and global<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> methods of proof are known. However, for its reversible version, while a global method of proof is recognized, a local approach similar to that undertaken by Böhm and Jacopini<ref name="BohmJacopini">{{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 ==