Abstract
The Böhm–Jacopini theorem (Böhm 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ashcroft, E., Manna, Z.: The translation of goto programs into while programs. In: Freiman, C.V., Griffith, J.E., Rosenfeld, J.L. (eds.) Proceedings of IFIP Congress 71, vol. 1, pp. 250–255. North-Holland, Amsterdam (1972)
Böhm, C., Jacopini, G.: Flow diagrams, Turing machines and languages with only two formation rules. In: Communications of the ACM, pp. 366–371 (May 1966)
Kaplan, D.M.: Regular expressions and the equivalence of programs. J. Comput. Syst. Sci. 3, 361–386 (1969)
Kosaraju, S.R.: Analysis of structured programs. In: Proc. 5th ACM Symp. Theory of Computing (STOC 1973), pp. 240–252. ACM, New York (1973)
Kozen, D.: Automata on guarded strings and applications. Matématica Contemporânea 24, 117–139 (2003)
D. Kozen.: Nonlocal flow of control and Kleene algebra with tests. Technical Report http://hdl.handle.net/1813/10595 Computing and Information Science, Cornell University (April 2008); Proc. 23rd IEEE Symp. Logic in Computer Science (LICS 2008) (to appear, June 2008)
Morris, P.H., Gray, R.A., Filman, R.E.: Goto removal based on regular expressions. J. Software Maintenance: Research and Practice 9(1), 47–66 (1997)
Oulsnam, G.: Unraveling unstructured programs. The Computer Journal 25(3), 379–387 (1982)
Peterson, W., Kasami, T., Tokura, N.: On the capabilities of while, repeat, and exit statements. Comm. Assoc. Comput. Mach. 16(8), 503–512 (1973)
Ramshaw, L.: Eliminating goto’s while preserving program structure. Journal of the ACM 35(4), 893–920 (1988)
Williams, M., Ossher, H.: Conversion of unstructured flow diagrams into structured form. The Computer Journal 21(2), 161–167 (1978)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kozen, D., Tseng, WL.D. (2008). The Böhm–Jacopini Theorem Is False, Propositionally. In: Audebaud, P., Paulin-Mohring, C. (eds) Mathematics of Program Construction. MPC 2008. Lecture Notes in Computer Science, vol 5133. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70594-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-70594-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70593-2
Online ISBN: 978-3-540-70594-9
eBook Packages: Computer ScienceComputer Science (R0)