Monday, April
28, 2008 4:00 PM 5130 Upson Hall |
Theory Seminar Spring 2008 CS 789 |
|
---|---|---|
Dexter Kozen |
||
The Boehm-Jacopini Theorem is False, Propositionally |
||
The Boehm-Jacopini 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 three-state flowchart that is not equivalent to any
while program.
Joint work with Dustin Tseng.
|