Tops: theory operationalization for program synthesis
S. Roach · 1998
Amphion is a real-world, domain-independent program synthesis system. It is specialized to specific applications through the creation of an operational domain theory. The Meta-Amphion system is being developed to empower domain experts to develop and maintain their own Amphion applications. This thesis describes technology for automatically transforming declarative domain theories into efficient, domain-specific program synthesis systems. A prototype of the system has been implemented in TOPS, Theory Operationalization for Program Synthesis. TOPS identifies axioms in the domain theory that are an instance of the theory of a procedure in a library of procedures. TOPS uses partial deduction to augment the procedure with the capability to construct ground terms for deductive synthesis. The synthesized procedure is interfaced to a resolution theorem prover. Axioms in the original domain theory that are implied by the synthesized procedure are removed. During deductive synthesis, the procedure is invoked to test the satisfiability of sets of literals in the language of the theory of the procedure. The procedure generates ground terms which are bound to existential variables in a problem specification. These terms are program fragments. Answers to deductive synthesis problem specifications can be generated using the procedure just in case they can be generated without using the procedures. Experiments show that the procedures synthesized by TOPS can reduce theorem proving search at least as much as hand tuning of the deductive synthesis system.