Böhm-Jacopini定理

Question

根据Böhm-Jacopini定理，一个算法只需使用三个语句即可编写：

- 顺序 - 选择 - 迭代

许多老师认为这个定理就像是信仰一样，他们教授时会建议不要使用（goto、jump、break、multiple return等）这些指令，因为这些指令都是邪恶的。

但是当我询问证明该定理的证据时，没有人能够提供。

个人认为该定理并非虚假，但实际应用时并不总是最佳选择。

因此，我进行了一些小型搜索，以下是我的疑虑：

1. 该定理已经在流程图结构归纳上得到证明，但它真的适用于计算机程序吗？ 根据维基百科，“Böhm和Jacopini的算法转换并不是真正的实用程序，因此为这个方向的其他研究打开了大门。”

2. 定理的一个推论是每个“goto”可以通过归纳转换为选择或迭代，但效率呢？ 我找不到任何证明表明每个算法都可以重写，保持相同的性能。

3. 递归，一个递归算法是否真的可以只使用顺序、选择和迭代来编写？ 我知道一些递归算法可以优化为循环（想想尾递归），但是否真的适用于所有情况？

4. 清晰的代码，我知道过多地使用跳转可能会创建一个庞大的代码，但我认为在某些情况下，在循环中正确使用break可以提高代码的可读性。

n = 0;
while (n < 1000 || (cond1 && cond2) || (cond3 && cond4) || (cond5 && cond6)) 
{  
   n++;  
   //The rest of code  
}   

可以重写为：

for (n = 0; n < 1000; n++)
{
   if (cond1 && cond2) break;
   elseif (cond2 && cond3) break;
   elseif (cond4 && cond5) break;
   elseif (cond6 && cond7) break;
   //The rest of code
}

个人认为，这个定理并非为了编写更好的代码而创立，认为清晰的代码必须遵循该定理，是由于一种奇怪的主观原因在世界上传播开来。

我发现了这篇有趣的文章：https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf，我认为这证明了真正的程序不必强制遵循Jaopini定理。您是否得出相同的结论？

总之，我想知道一个只使用（序列、选择和迭代）的程序是否真的比使用不同语句的其他程序更好，并且是否有证据或者说这只是主观看法？

- Stefano Balzarotti

---

由于几乎所有编程语言都有超出Böhm-Jacopini论文的结构，我不认为任何人“被迫遵循Jaopini定理”。自Dijkstra最初的长篇抨击以来，goto已经被反复讨论。共识是它们（或一些更结构化的版本，如break或continue）有其存在之处，但Dijkstra在很大程度上赢得了这场战争。 Böhm-Jacopini定理与此关系不大（除了对那些声称绝对需要goto的程序员提供回应）。结构化编程的成功是令人信服的。 - John Coleman

谢谢@JohnColeman，关于Dijkstra的长篇抨击，我发现了这篇有趣的文章，其中包含所有原始参考资料。特别是我发现Donald E. Knuth的这篇文章非常有趣，它展示了控制使用goto并不完全有害。 - Stefano Balzarotti

Answer 1

定理已经在流程图结构归纳上得到证明，但它是否实用于计算机程序呢？根据维基百科“Böhm和Jacopini的算法不太实用作为程序转换算法，因此打开了这个方向的进一步研究”的说法。

他们提供的操作和结构可以轻松地模拟图灵机的功能。因此，它是一个图灵等价的计算系统。根据Church-Turing论题，这被认为是我们所能做的全部计算：使用"goto"将不会增加任何不可能完成的任务。

定理的一个推论是每个“goto”都可以通过归纳转换为选择或迭代，但是效率如何呢？我找不到任何证明表明每个算法重写后保持相同的性能。

对许多算法而言，在没有使用计算的'goto'的情况下，性能很可能更差。您当然可以针对特定问题显示出这种情况。是否改变了渐近复杂度是另一个问题，但就我所知，这与Bohm和Jacopini无关。

递归算法真的可以仅使用序列、选择和迭代来编写吗？我知道一些递归算法可以优化为循环（想想尾递归），但是否可应用于所有算法呢？

由于Bohm和Jacopini的系统是图灵等价的，因此您是正确的，递归不会增加新的能力。它可能会增加可读性。

- Patrick87

---

谢谢@Patrick87，我会等几天再接受这个答案，看看是否有人能提供更完整的解释。 - Stefano Balzarotti

Answer 2

根据Böhm-Jacopini定理，一个算法只需要使用三种语句：顺序、选择和迭代。 While语言具有以下结构：

1. 赋值，V := E 2. 空程序，skip 3. 顺序，S1;S2 4. 选择，if B then S1 [elsif Si] else Sn fi 5. 迭代，while B do S od 你省略了赋值和skip，这是一个中性元素，就像算术中的0一样。还有其他我省略的结构，这些与过程抽象有关，即命名语句序列，即函数和过程。但我现在不想扩展它太多。

我发现了这篇有趣的文章: https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf。我认为这证明了真实的程序不必遵循Jacopini定理。你是否得出了相同的结论？

Kozen是一个非常好的作者，他严谨而清晰。

Kozen展示了命题演算在证明Böhm-Jacopini定理时存在的局限性。原始文章使用谓词演算。他使用1960年代不可用的技术给出了正确的定理证明。问题出现在变换中使用变量，这是命题演算无法处理的事情。 其他变换存在，可以使用带有break的循环而不是While语言。所有关于GOTO的讨论现在都很清楚。这篇文章很有趣，因为它是如何在一个老问题中使用新技术的例子。

您可以使用Böhm-Jacopini定理，因为它会产生等效的程序。

个人认为该定理并非错误，但在现实世界中不一定总是更好的选择。该结果支持结构化编程，但您不应使用数据流图来设计程序，甚至不应使用“While”伪代码来设计程序。最佳实践是使用更适合表示要解决问题的抽象规范语言。证明您的解决方案，然后编写一个可以转换为编程语言代码的文档。这就是文学编程背后的思想。精确阐述您对问题域的了解，说明如何用抽象规范语言表示问题，并将其系统地转换为编程语言。所有说明都应使用自然语言和数学公式，代码片段应可分开以生成程序代码。为此，您可以使用类似CWeb和LaTeX的程序。新的声明性语言非常接近规范语言，但最好坚持上述建议。尽管这些语言推断类型，但有时数据结构中的细节会在设计过程中分散注意力。后来应详细说明类型，以便在静态类型的编程语言中实现程序。这是更好的编程实践。

- guest

Answer 3

任何看起来像Type 1/2/3的程序都可以转换为：

- Achraf

Answer 4

个人认为，这个定理并不是为了编写更好的代码而创造的。

实际上，它从来都不是。这个定理并不是被“创造”的（定理并不只是“创造”出来的）。这个定理是作为计算模型被发现的，是为了证明编写算法时 GOTO 语句并非绝对必要的一种方式。

我们需要了解该定理最初提出的背景。当时，程序员们在使用 GOTO 语句时相当野蛮和缺乏结构，坚信 GOTO 语句是必不可少的。

该定理证明了这并不是事实。现在，该定理并不意味着按照它所提出的结构编写的程序必然优越（因为有些情况下，偏离所提出的结构是更好/更优雅/更高效的方法）。

该定理当时的最大好处是它为 GOTO 语句是创建复杂程序的必需品的争论画上了句号（它们并不是必需品）。

该定理最大的好处是它提供了一种新的（通常更好的）方式来阐述、分析和编码算法。

“一个干净的代码必须遵循这个定理”的想法已经因为奇怪的主观原因而传播到了全世界。

一般情况下，这是正确的，并且没有主观原因。该定理是结构化编程的基础，在一般情况下，这比其前任替代方案要好得多。

我再重复一遍，关于该定理的整个问题在于对于一般情况：

1. 您不需要依赖GOTO进行顺序逻辑
2. 顺序逻辑可以通过此方法统一描述
3. 顺序逻辑的结果编码可以被正式分析（尝试使用GOTO soup进行分析）

客观地说，这就是该定理应该被看待的方式。

- luis.espinal