Monday, April
28, 2008 4:00 PM 5130 Upson Hall 
Theory Seminar Spring 2008 CS 789 


Dexter Kozen 

The BoehmJacopini Theorem is False, Propositionally 

The BoehmJacopini theorem (Boehm and
Jacopini, 1966) is a classical result of program schematology. It states
that any deterministic flowchart is equivalent to a while program. The
theorem is false at the propositional level, as shown by Ashcroft and
Manna (1972) and Kosaraju (1973), although their counterexamples have
some technical drawbacks: Kosaraju's is based on an unreasonable
assumption (it is not a counterexample without that assumption), and
Ashcroft and Manna's is overly complex, requiring 13 states. In this
talk I will show how to reformulate the problem in terms of automata
theory and give a threestate flowchart that is not equivalent to any
while program.
Joint work with Dustin Tseng.
