Richard Waldinger

Abstract

Deductive program synthesis uses automatic theorem-proving technology to construct programs that meet given specifications.  These specifications express the purpose of the program but may give no indication of a method for achieving that purpose.  In a deductive approach, the specification is phrased as a theorem in mathematical logic, which is submitted to a theorem prover. For an applicative program, the theorem expresses the existence of an output entity that satisfies the specified conditions. The proof is conducted in a subject domain theory that defines the concepts of the specification language and the constructs of the target programming language and provides the background knowledge that connects them.  The proof is restricted to be sufficiently constructive to provide a method for finding the desired output entity; that method is the basis for an algorithm that is extracted automatically from the proof.  The proof provides a justification for the correctness of the extracted program, and the rationale of the algorithm.  The structure of the algorithm reflects the structure of the proof.  Conditional expressions result from the use of case analysis; recursive calls are obtained from application of the mathematical induction principle.
As an example, we consider the synthesis of the unification algorithm.  Unification is the problem of finding a substitution that makes two logical expressions identical.  Unification was identified by Herbrand and later by Robinson as a key process in automatic theorem proving.  It has subsequently also found application in such areas as natural language understanding, programming language design, and question answering.   The algorithm served as an early target for program synthesis research, and partial, manual, or interactive derivations have been constructed, but full automation has eluded those efforts.  In this talk we show an automatic proof discovered by Stickel’s first-order-logic theorem prover SNARK.  The algorithm extracted from the proof contains some novel elements.
Theorem provers already surpass us in pure reasoning ability.  With continuing improvements in deductive technology, it is timely to ask when automatic program synthesis will have an impact on software practice.

Biography

Richard Waldinger is a Principal Scientist at the Artificial Intelligence Center of SRI International, in Menlo Park, California.  He has worked on the application of automatic theorem proving to program synthesis and verification, planning, and question answering. He is coauthor (with Zohar Manna) of a series of books on the relationship between mathematical logic and computer programs.