Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||The Boehm-Jacopini Theorem is False, Propositionally|
|Authors: ||Kozen, Dexter|
Tseng, Wei-Lung (Dustin)
|Keywords: ||Boehm-Jacopini theorem|
|Issue Date: ||23-Jan-2008|
|Abstract: ||The Boehm-Jacopini theorem (Boehm 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 level of the multi-level breaks that are allowed.
In this paper we give 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 the first-order and propositional level 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.|
|Appears in Collections:||Computing and Information Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.