Wie kann man den Satz des strukturierten Programms beweisen?

Wikipedia :

Das strukturierte Programm [...] besagt, dass [...] jeder Algorithmus mit nur drei Kontrollstrukturen ausgedrückt werden kann. Sie sind

• Ausführen eines Unterprogramms und dann eines anderen Unterprogramms (Sequenz)
• Ausführen eines von zwei Unterprogrammen gemäß dem Wert eines booleschen Ausdrucks (Auswahl)
• Ausführen eines Unterprogramms, bis ein boolescher Ausdruck wahr ist (Iteration)

Dieser Satz wird in den folgenden Abhandlungen entwickelt:

• C. Böhm, "Über eine Familie von Turing-Maschinen und die zugehörige Programmiersprache", ICC Bull., 3, 185–194, Juli 1964.
• C. Böhm, G. Jacopini, "Flussdiagramme, Turingmaschinen und Sprachen mit nur zwei Formationsregeln", Comm. of the ACM, 9 (5): 366–371,1966.

Leider ist der erste praktisch nicht verfügbar, und der zweite ist nicht nur ein bisschen kryptisch (zumindest für mich), sondern bezieht sich auch auf den ersten, sodass ich Probleme habe, den Beweis zu verstehen. Kann mir jemand helfen? Gibt es ein modernes Papier oder Buch, das den Beweis darstellt? Vielen Dank.

AKTUALISIEREN

Um genau zu sein, möchte ich den zweiten Teil des CACM-Papiers (Abschnitt 3) verstehen . Die Autoren schreiben in Abschnitt 1 Folgendes:

Im zweiten Teil des Papiers (von C. Böhm) werden einige Ergebnisse eines früheren Papiers berichtet [8], und die Ergebnisse des ersten Teils dieses Papiers werden dann verwendet, um zu beweisen, dass jede Turing-Maschine in oder in reduzierbar ist Ein entschlossener Sinn ist gleichbedeutend mit einem Programm, das in einer Sprache geschrieben ist, die als Formation nur Komposition und Iteration zulässt.

Hier bezieht sich [8] auf das nicht verfügbare ICC Bulletin Paper. Es ist leicht zu erkennen, dass sich das obige Zitat aus Wikipedia auf diesen zweiten Teil des CACM-Papiers bezieht (die Turing-Maschine dient als genaue Definition von Algorithmen; "Komposition" bedeutet Sequenz; eine Iteration kann eine Auswahl ersetzen).

Das Böhm-Jacopini-Theorem besagt im Wesentlichen, dass ein auf 'goto' basierendes Programm eine Funktionalität ist, die einer aus 'while' und 'if' besteht.

Beweisskizze anhand folgender Vorlesungsunterlagen :

Angenommen, Sie haben ein Programm, das aus einer Folge von Anweisungen besteht $S_i$;; Stellen Sie jeder Anweisung ein Label voran$S_i^{\prime} \gets L_i: S_i$und aktualisieren Sie vorhandene goto-Anweisungen, um auf die richtigen Positionen zu verweisen. Deklarieren Sie eine Standortvariable.$l \gets 1$und schließen Sie die vorangestellten Anweisungen in eine while-Schleife ein, die fortgesetzt wird, bis die letzte Anweisung erreicht ist. $\textbf{while} (l \neq M) \ \textbf{do} \ S^{\prime}$.

Wenden Sie die folgenden Umschreiberegeln auf an $S^{\prime}$::

• Gehe zu Regel: Ersetzen $L_i \ \textbf{goto} \ L_j$ mit $\textbf{if} \ (l = i) \ \textbf{then} \ l \gets j$
• If-goto-Regel: Ersetzen $L_i : \textbf{if} \ \text{(cond)} \ \textbf{then} \ \textbf{goto} \ L_j$ mit $\textbf{if} \ (l = i \land \text{(cond)}) \ \textbf{then} \ l \gets j \ \textbf{else} \ l \gets l + 1$
• Ansonsten Regel: Ersetzen $L_i : S_i$ mit $\textbf{if} \ l = i \ \textbf{then} \ S_i, \quad l \gets l + 1$

Das resultierende Programm ist dann frei von goto-Anweisungen, die die Entsprechung zwischen den beiden Paradigmen zeigen.

Ein formellerer Beweis ist in Ihrer zweiten Referenz enthalten .

Aktualisieren

Nachdem ich die Arbeit genauer studiert habe, ist dies meine Interpretation:

Basierend auf den Definitionen in CACM, lassen Sie $\mathcal{B}^{\prime} = \mathcal{D}(\alpha, \lbrace \lambda, R \rbrace)$ sei die Klasse der Turing-Maschinen, die durch die Sprache repräsentiert werden $\mathcal{P}^{\prime}$das umfasst Flussdiagramme. Lassen$\mathcal{B}^{\prime \prime} = \mathcal{E}(\alpha, \lbrace \lambda, R \rbrace)$ sei die Klasse der Turing-Maschinen, die durch die Sprache repräsentiert werden $\mathcal{P}^{\prime \prime}$ das deckt die oben behandelte Transformation ab.

Laut CACM möchte der Autor nachweisen, dass eine Turingmaschine in der von beschriebenen Turingmaschinenfamilie existiert $M \in \mathcal{B}^{\prime}$, dann gibt es eine entsprechende Turingmaschine in der Familie der von beschriebenen Turingmaschinen $M^{*} \in \mathcal{B}^{\prime \prime}$.

Skizze des Beweises des Autors: Er tut dies, indem er aus der abgeleiteten Beziehung schöpft $M \in \mathcal{B}^{\prime}$ und $M \in \mathcal{E}(\cdots)$ (Definition (5)) und richtet dann die Beziehung ein $M^{*} \in \mathcal{E}^{*}(\cdots)$. Für jede Komponente von$\mathcal{E}(\cdots)$ er zeichnet eine Eins-zu-Eins-Zuordnung mit denen von $\mathcal{E}^*(\cdots)$. So durch die Herstellung der Brücke zwischen$M$ und $M^{*}$ durch $\mathcal{E}(\cdots)$ der Autor beweist $M \in \mathcal{B}^{\prime} \implies M^{*} \in \mathcal{B}^{\prime\prime}$.