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

CS 789
 

Dexter Kozen
Cornell University

 
 

 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.