The Böhm-Jacopini Theorem Is False, Propositionally
The Böhm-Jacopini Theorem Is False, Propositionally
复制标题
玻姆-雅可比尼定理在命题上是错误的
DOI：
10.1007/978-3-540-70594-9_11
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Wei
中科院分区：
文献类型：
--
作者：
D. Kozen;Wei
Bohm-Jacopini定理（BohmandJacopini，1966）是程序模式学的一个经典结果.它指出，任何确定性流程图程序都等效于while程序。该定理通常在一阶解释或一阶未解释（示意）层次上表述，因为构造需要引入辅助变量。Ashcroft和Manna（1972）以及Kemaju（1973）表明，这是不可避免的。正如许多作者所观察到的，一个稍微更强大的结构化编程构造，即具有多级中断的循环程序，足以表示所有确定性流程图，而无需引入辅助变量。1973年，Kaghaju建立了一个严格的等级制度，由允许的最大嵌套深度决定。在本文中，我们给出了一个纯粹的命题说明这些结果。我们重新制定的问题在命题层面上的自动机保护字符串，自动机理论对应的Kleene代数测试。而经典的方法不区分一阶和命题抽象层次，我们发现，纯粹的命题制定允许一个更精简的数学处理，使用代数和拓扑概念，如互模拟和coinduction。使用这些工具，我们可以给出更严格的数学公式和更简单，更有启发性的证明。
The Bohm---Jacopini theorem (Bohm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem is usually formulated at the first-order interpreted or first-order uninterpreted (schematic) level, because the construction requires the introduction of auxiliary variables. Ashcroft and Manna (1972) and Kosaraju (1973) showed that this is unavoidable. As observed by a number of authors, a slightly more powerful structured programming construct, namely loop programs with multi-level breaks, is sufficient to represent all deterministic flowcharts without introducing auxiliary variables. Kosaraju (1973) established a strict hierarchy determined by the maximum depth of nesting allowed. In this paper we give a purely propositional account of these results. We reformulate the problems at the propositional level in terms of automata on guarded strings, the automata-theoretic counterpart to Kleene algebra with tests. Whereas the classical approaches do not distinguish between first-order and propositional levels of abstraction, we find that the purely propositional formulation allows a more streamlined mathematical treatment, using algebraic and topological concepts such as bisimulation and coinduction. Using these tools, we can give more mathematically rigorous formulations and simpler and more revealing proofs.