柏姆-雅可比尼定理

Böhm-Jacopini theorem

根据 Böhm-Jacopini 定理,可以仅使用三个语句编写算法:

很多老师认为该定理是一种信仰行为,他们教导不要使用(goto、jump、break、multiple return,等等...),因为这些指令是邪恶的。

但是当我要求解释时,没有人能够提供定理证明。

我个人不认为这个定理是错误的,但我认为它在现实世界中的适用性并不总是更好的选择。

所以我做了一点搜索,这些是我的疑惑:

  1. 这个定理在流程图的结构上已经被归纳证明了,但它真的适用于计算机程序吗?
    根据维基百科 "Böhm and Jacopini's was not really practical as a program transformation algorithm, and thus opened the door for additional research in this direction".

  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
}

我个人认为这个定理并不是为了写出更好的代码而创建的,干净的代码必须遵循这个定理的想法已经因为一个奇怪的主观原因传播到世界上。

  1. 我发现了这篇有趣的文章:https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf 我认为这证明了真正的程序不能被强制遵循 Jaopini 定理。
    你们有相同的结论吗?

总结一下这个问题,我需要知道一个只使用(序列、选择和迭代)的程序是否真的比使用不同语句的任何其他程序都好,是否有证据或者它是否都是主观的。

The theorem has been proven on induction on the structure of the flow chart, but it's really applicable in a computer program? According to wikipedia "Böhm and Jacopini's was not really practical as a program transformation algorithm, and thus opened the door for additional research in this direction".

他们给出的操作和结构可以很容易地显示能够复制图灵机的功能。因此,它是一个图灵等效的计算系统。根据 Church-Turing 论点,这被认为是我们所能做的尽可能多的计算:goto 不会添加任何不可能的东西。

A consequence of theorem prove that each "goto" can be translated into selection or iteration by induction, but what about efficiency? I can't find any proof shows that each algorithm can be rewritten preserving the same performance.

对于许多不使用计算 goto 的算法,性能很可能更差。你当然可以证明它是特定问题的情况。这是否会改变渐近复杂性是另一个问题,但据我所知,与 Bohm 和 Jacopini 无关。

Recursion, a recursive algorithm can really be written using only sequence, selection and iteration? I know that some recursive algorithms can be optimized as loops (think to tail recursion), but can really be applicable to all?

既然 Bohm 和 Jacopini 的系统是图灵等价的,那么你是对的,递归没有增加新的力量。它肯定会增加可读性。

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

According to Böhm-Jacopini theorem, an algorithm can be written using only three statements:

  • sequence
  • selection
  • iteration

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。我省略了其他结构。这些与过程抽象有关,它命名语句序列,即函数和过程。但我现在不想延长太多。

I found this interesting article : https://www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf I think this prove that real program must not be forced to follow the Jacopini Theorem. Do you share the same conclusions?

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

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

您可以使用 Böhm-Jacopini 定理,因为它产生了一个等价的程序。

Personally I don't think that the theorem is false, but I think that it's applicability in real world is not always the better choice.

该结果支持结构化编程。但是你不应该使用它,因为你不应该使用数据流图来设计程序。 你甚至不应该使用 While 伪代码来设计程序。

最佳做法是使用更能代表您要解决的问题的抽象规范语言。 证明您的解决方案,然后编写可以转换为您的编程语言代码的文档。 这就是文学编程背后的理念。准确解释你对问题领域的了解,说明你如何用抽象规范语言表示你的问题,并将其系统地转换为编程语言。所有的解释都应该用自然语言和数学公式,并且代码片段应该是可分离的以产生程序代码。为此,您可以使用 CWeb 和 LaTeX 等程序。

新的声明式语言非常接近规范语言,但最好坚持上述建议。尽管这些语言会推断类型,但有时数据结构中的细节会分散设计过程的注意力。稍后应该详细说明类型,以便在静态类型的编程语言中实现程序。 这是更好的编程习惯。

Personally I think that the theorem has not been created for write better code,

好吧,从来没有。 Theorem wasn't created (theorems aren't just created).该定理是作为一种计算模型被发现的,作为一种证明 GOTO 语句不是编码算法的绝对必要条件的方法。

我们需要了解首次提出该定理的背景。当时,程序员们相当野蛮地使用 GOTO 并且没有结构,坚信 GOTO 语句是必不可少的。

定理证明事实并非如此。现在,这个定理并不意味着由它构造的程序必然优越(因为在某些情况下,偏离建议的结构是 better/more elegant/efficient 的方法。)

该定理在当时的作用就像棺材上的钉子一样,证明了 GOTO 语句是创建复杂程序所必需的(它们不是。)

该定理的最大好处是它提供了一种新的(在一般情况下,更好的)方法来制定、分析和编码算法。

and the idea that a clean code must follow this theorem has been spread into world for a strange subjective reason.

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

我再说一遍,关于定理的全部内容是针对一般情况

  1. 时序逻辑不需要依赖 GOTO
  2. 时序逻辑可以用这种方法统一描述
  3. 可以正式分析由此产生的时序逻辑编码(尝试使用 GOTO soup。)

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