Editing Structured program theorem (section)

== 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 |last1=Böhm |first1=Corrado |author-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}}

=== Single-while-loop, folk version of the theorem ===
This version of the theorem replaces all the original program's control flow with a single global <code>while</code> loop that simulates a [[program counter]] going over all possible labels (flowchart boxes) in the original non-structured program. Harel traced the origin of this folk theorem to two papers marking the beginning of computing. One is the 1946 description of the [[von Neumann architecture]], which explains how a [[program counter]] operates in terms of a while loop. Harel notes that the single loop used by the folk version of the structured programming theorem basically just provides [[operational semantics]] for the execution of a flowchart on a von Neumann computer.<ref name="Harel"/>{{rp|383}} Another, even older source that Harel traced the folk version of the theorem is [[Stephen Kleene]]'s [[Kleene's T predicate|normal form theorem]] from 1936.<ref name="Harel"/>{{rp|383}}

[[Donald Knuth]] criticized this form of the proof, which results in [[pseudocode]] like the one below, by pointing out that the structure of the original program is completely lost in this transformation.<ref>{{cite journal
 |  author = Donald Knuth
 |   title = Structured Programming with go to Statements
 | journal = Computing Surveys
 |  volume = 6
 |   issue = 4
 |    year = 1974
 |   pages = 261–301
 |   doi = 10.1145/356635.356640
|   citeseerx = 10.1.1.103.6084
 | s2cid = 207630080
 }}</ref>{{rp|274}} Similarly, Bruce Ian Mills wrote about this approach that "The spirit of block structure is a style, not a language. By simulating a Von Neumann machine, we can produce the behavior of any spaghetti code within the confines of a block-structured language. This does not prevent it from being spaghetti."<ref name="Mills2005">{{cite book|author=Bruce Ian Mills|title=Theoretical Introduction to Programming|year=2005|publisher=Springer|isbn=978-1-84628-263-8|page=279}}</ref>

<syntaxhighlight lang="pascal">
p := 1
while p > 0 do
    if p = 1 then
        perform step 1 from the flowchart
        p := resulting successor step number of step 1 from the flowchart (0 if no successor)
    end if
    if p = 2 then
        perform step 2 from the flowchart
        p := resulting successor step number of step 2 from the flowchart (0 if no successor)
    end if
    ...
    if p = n then
        perform step n from the flowchart
        p := resulting successor step number of step n from the flowchart (0 if no successor)
    end if
end while
</syntaxhighlight>

=== Böhm and Jacopini's proof ===
{{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|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"/> 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.