[Solved]: How to prove the structured program theorem?

Problem Detail: 

Wikipedia:

The structured program theorem [...] states that [...] any algorithm can be expressed using only three control structures. They are

• Executing one subprogram, and then another subprogram (sequence)
• Executing one of two subprograms according to the value of a boolean expression (selection)
• Executing a subprogram until a boolean expression is true (iteration)

This theorem is developed in the following papers:

• C. Böhm, "On a family of Turing machines and the related programming language", ICC Bull., 3, 185–194, July 1964.
• C. Böhm, G. Jacopini, "Flow diagrams, Turing Machines and Languages with only Two Formation Rules", Comm. of the ACM, 9(5): 366–371,1966.

Unfortunately, the first one is practically unavailable, and the second one, in addition to being a bit cryptic (at least for me), refers to the first, so I have problems to understand the proof. Can anyone help me? Is there a modern paper or book which presents the proof? Thanks.

---

UPDATE

To be exact, I would like to understand the second part of the CACM paper (section 3). The authors write in section 1 the following:

In the second part of the paper (by C. Böhm), some results of a previous paper are reported [8] and the results of the first part of this paper are then used to prove that every Turing machine is reducible into, or in a determined sense is equivalent to, a program written in a language which admits as formation rules only composition and iteration.

Here [8] refers to the unavailable ICC Bulletin paper. It is easy to see that the above quote from Wikipedia refers to this second part of the CACM paper (the Turing machine serves as a precise definition of algorithms; "composition" means sequence; an iteration can replace a selection).

Asked By : kol

Answered By : GEL

The Böhm-Jacopini theorem essentially says that a program based on 'goto' is functionality equivalent to one consisting of 'while' and 'if'.

Sketch of proof based on the following lecture notes:

Say you have a program that consists of a sequence of statements $S_i$; prefix each statement with a label $S_i^{\prime} \gets L_i: S_i$ and update existing goto statements to point to the right locations. Declare a location variable, $l \gets 1$, and wrap the prefixed statements in a while loop that will continue until the last statement is reached, $\textbf{while} (l \neq M) \ \textbf{do} \ S^{\prime}$.

Apply the following rewrite rules to $S^{\prime}$:

• Goto rule: Replace $L_i \ \textbf{goto} \ L_j$ with $\textbf{if} \ (l = i) \ \textbf{then} \ l \gets j$
• If-goto rule: Replace $L_i : \textbf{if} \ \text{(cond)} \ \textbf{then} \ \textbf{goto} \ L_j$ with $\textbf{if} \ (l = i \land \text{(cond)}) \ \textbf{then} \ l \gets j \ \textbf{else} \ l \gets l + 1$
• Otherwise rule: Replace $L_i : S_i$ with $\textbf{if} \ l = i \ \textbf{then} \ S_i, \quad l \gets l + 1$

The resulting program is then free of goto statements showing the correspondence between the two paradigms.

A more formal proof is provided in your second reference.

Update

After studying the paper in greater detail, this is my interpretation:

Based on the definitions in CACM, let $\mathcal{B}^{\prime} = \mathcal{D}(\alpha, \lbrace \lambda, R \rbrace)$ be the class of Turing machines represented by the language $\mathcal{P}^{\prime}$ that covers flow diagrams. Let $\mathcal{B}^{\prime \prime} = \mathcal{E}(\alpha, \lbrace \lambda, R \rbrace)$ be the class of Turing machines represented by the language $\mathcal{P}^{\prime \prime}$ that covers the transformation covered above.

According to CACM, the author wants to prove that if a Turing machine exists in the family of Turing machines described by $M \in \mathcal{B}^{\prime}$, then there exists a corresponding Turing machine in the family of Turing machines described by $M^{*} \in \mathcal{B}^{\prime \prime}$.

Sketch of the author's proof: He does this by drawing from the derived relationship $M \in \mathcal{B}^{\prime}$ and $M \in \mathcal{E}(\cdots)$ (definition (5)) and then sets up the relationship $M^{*} \in \mathcal{E}^{*}(\cdots)$. For each component of $\mathcal{E}(\cdots)$ he draws a one-to-one mapping with those of $\mathcal{E}^*(\cdots)$. Thus by establishing the bridge between $M$ and $M^{*}$ through $\mathcal{E}(\cdots)$ the author proves $M \in \mathcal{B}^{\prime} \implies M^{*} \in \mathcal{B}^{\prime\prime}$.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/14983