11
$\begingroup$

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).

Improve this question
$\endgroup$
7
  • $\begingroup$ You may want to read the Wikipedia entry on the primitive language P'' described in the first paper. $\endgroup$
    – r.e.s.
    Oct 12, 2013 at 2:27
  • 1
    $\begingroup$ BTW, in that first paper, Böhm actually provided an explicit P'' program for each of a set of basic functions that together serve to compute any computable function. (The quote in your "update" is referring to language P''.) $\endgroup$
    – r.e.s.
    Oct 12, 2013 at 2:44
  • 1
    $\begingroup$ @r.e.s. Yes, I could find info on P'', but I still would like to read the original ICC Bulletin paper. Martin Davis wrote a brief review about it: "The author proves that every partial recursive function can be computed by a Turing machine of a particularly simple kind. The proof, making use of programming language techniques is neat and brief." This makes me curious :) $\endgroup$
    – kol
    Oct 12, 2013 at 7:12
  • 1
    $\begingroup$ If it's of any use, here's a UCLA/SRLF WorldCat link (click the "Worldwide libraries" item on that page) showing many libraries -- including some in Europe -- that own copies of the International Computation Centre Bulletin. (I created that Wikipedia article on P'' after chancing upon Böhm's 1964 paper during research at the SRLF about ten years ago.) $\endgroup$
    – r.e.s.
    Oct 12, 2013 at 14:08
  • 1
    $\begingroup$ I see a link to the result of Kleene: finite state automata are equivalent to regular expressions. While finite state automata are very much "goto", the regular expressions consist of concatenation (sequence), union (selection) and star (iteration). $\endgroup$
    – Hendrik Jan
    Dec 19, 2022 at 11:47

1 Answer 1

Reset to default
14
$\begingroup$

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}$.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you very much! In the second part of the CACM paper (section 3) the authors connect these results with the P'' language (defined in the ICC Bulletin paper) and Turing machines. Would you plese write a few words about this connection too? $\endgroup$
    – kol
    Oct 10, 2013 at 18:08
  • $\begingroup$ They write "In the second part of the paper [...] the results of the first part [...] are 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." The above quote from Wikipedia refers to this second part, and this is the part of the CACM paper what I would like to understand. $\endgroup$
    – kol
    Oct 10, 2013 at 19:24

Not the answer you're looking for? Browse other questions tagged or ask your own question.