Como provar o teorema do programa estruturado?

Wikipedia :

O teorema do programa estruturado [...] afirma que qualquer [...] algoritmo pode ser expresso usando apenas três estruturas de controle. Eles são

• Executando um subprograma e depois outro subprograma (sequência)
• Executando um dos dois subprogramas de acordo com o valor de uma expressão booleana (seleção)
• Executando um subprograma até que uma expressão booleana seja verdadeira (iteração)

Este teorema é desenvolvido nos seguintes artigos:

• C. Böhm, "Em uma família de máquinas de Turing e a linguagem de programação relacionada", ICC Bull., 3, 185-194, julho de 1964.
• C. Böhm, G. Jacopini, "Diagramas de fluxo, máquinas de Turing e idiomas com apenas duas regras de formação", Comm. of the ACM, 9 (5): 366-371,1966.

Infelizmente, o primeiro está praticamente indisponível, e o segundo, além de um pouco enigmático (pelo menos para mim), refere-se ao primeiro, por isso tenho problemas para entender a prova. Alguém pode me ajudar? Existe um papel ou livro moderno que apresente a prova? Obrigado.

ATUALIZAR

Para ser exato, eu gostaria de entender a segunda parte do documento do CACM (seção 3). Os autores escrevem na seção 1 o seguinte:

Na segunda parte do artigo (por C. Böhm), ​​alguns resultados de um artigo anterior são relatados [8] e os resultados da primeira parte deste artigo são usados ​​para provar que toda máquina de Turing é redutível em, ou em um sentido determinado é equivalente a um programa escrito em um idioma que admite como formação rege apenas composição e iteração.

Aqui [8] refere-se ao documento indisponível do ICC Bulletin. É fácil ver que a citação acima da Wikipedia se refere a esta segunda parte do artigo do CACM (a máquina de Turing serve como uma definição precisa de algoritmos; "composição" significa sequência; uma iteração pode substituir uma seleção).

O teorema de Böhm-Jacopini diz essencialmente que um programa baseado em 'goto' é uma funcionalidade equivalente a um composto por 'while' e 'if'.

Esboço da prova com base nas seguintes notas de aula :

Digamos que você tenha um programa que consiste em uma sequência de instruções ; prefixe cada instrução com um rótulo e atualize as instruções goto existentes para apontar para os locais corretos. Declare uma variável de local, e agrupe as instruções prefixadas em um loop while que continuará até a última instrução ser alcançada, .$S_i$$S_i^{\prime} \gets L_i: S_i$$l \gets 1$$\textbf{while} (l \neq M) \ \textbf{do} \ S^{\prime}$

Aplique as seguintes regras de reescrita em :$S^{\prime}$

• Regra Goto: Substitua por$L_i \ \textbf{goto} \ L_j$$\textbf{if} \ (l = i) \ \textbf{then} \ l \gets j$
• Regra If-goto: Substitua por$L_i : \textbf{if} \ \text{(cond)} \ \textbf{then} \ \textbf{goto} \ L_j$$\textbf{if} \ (l = i \land \text{(cond)}) \ \textbf{then} \ l \gets j \ \textbf{else} \ l \gets l + 1$
• Caso contrário, regra: Substitua por$L_i : S_i$$\textbf{if} \ l = i \ \textbf{then} \ S_i, \quad l \gets l + 1$

O programa resultante fica então livre de declarações goto mostrando a correspondência entre os dois paradigmas.

Uma prova mais formal é fornecida em sua segunda referência .

Atualizar

Depois de estudar o artigo com mais detalhes, esta é minha interpretação:

Com base nas definições do CACM, permita que seja a classe de máquinas de Turing representadas pelo idioma que abrange os diagramas de fluxo. Seja seja a classe de máquinas de Turing representada pela linguagem que cobre a transformação coberta acima.$\mathcal{B}^{\prime} = \mathcal{D}(\alpha, \lbrace \lambda, R \rbrace)$$\mathcal{P}^{\prime}$$\mathcal{B}^{\prime \prime} = \mathcal{E}(\alpha, \lbrace \lambda, R \rbrace)$$\mathcal{P}^{\prime \prime}$

De acordo com o CACM, o autor deseja provar que, se uma máquina de Turing existe na família de máquinas de Turing descrita por , existe uma máquina de Turing correspondente na família de máquinas de Turing descrito por .$M \in \mathcal{B}^{\prime}$$M^{*} \in \mathcal{B}^{\prime \prime}$

Esboço da prova do autor: Ele faz isso usando o relacionamento derivado e (definição (5)) e depois define o relacionamento . Para cada componente de ele desenha um mapeamento individual com os de . Assim, ao estabelecer a ponte entre e através de o autor comprova .$M \in \mathcal{B}^{\prime}$$M \in \mathcal{E}(\cdots)$$M^{*} \in \mathcal{E}^{*}(\cdots)$$\mathcal{E}(\cdots)$$\mathcal{E}^*(\cdots)$$M$$M^{*}$$\mathcal{E}(\cdots)$$M \in \mathcal{B}^{\prime} \implies M^{*} \in \mathcal{B}^{\prime\prime}$