The Böhm-Jacopini Theorem Is False, Propositionally

The Böhm-Jacopini Theorem Is False, Propositionally,10.1007/978-3-540-70594-9_11,Dexter Kozen,Wei-lung Dustin Tseng

The Böhm-Jacopini Theorem Is False, Propositionally   (Citations: 1)
BibTex | RIS | RefWorks Download
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 usu- ally 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 sucient to represent all determin- istic flowcharts without introducing auxiliary variables. Kosaraju (1973) established a strict hierarchy determined by the maximum depth of nest- ing 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 dis- tinguish 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.
Conference: Mathematics of Program Construction - MPC , pp. 177-192, 2008
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: