Automating the Derivation of Unification Algorithms. A Case Study in Deductive Program Synthesis

Abstract

The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal. In deductive program synthesis, computer programming is phrased as a task in theorem proving; a declarative specification is expressed in logical form and presented to an automatic theorem prover, and a program meeting the specification is extracted from the proof. The correctness of the program is supported by the proof, which also provides an explanation of how the program works. The proof is conducted in an appropriate axiomatic subject-domain theory, which defines the concepts in the specification and the constructs in the target programming language and provides the background knowledge necessary to connect them. For the unification proof, we generalize and automate the manual proof presented in [Manna and Waldinger, 1981]. The new program unifies two given symbolic expressions (s-expressions) relative to a given “environment” substitution. The proof establishes the existence of an output substitution that is a most-general idempotent unifier of the given expressions and is an “extension” of the environment substitution. If no such substitution exists and the expressions are not unifiable, the program is to produce a failure indicator. Initially the environment substitution is the empty substitution, which makes no replacements at all; during execution of recursive calls, the environment substitution records the replacements that have been found so far. snark’s own unification algorithm employs an environment, and such algorithms appear in the literature [e.g., Luger and Stubblefield, 1997]. In addition to being more efficient, we believe the three-argument algorithm with an environment is easier to synthesize automatically than the two-argument version from the Manna-Waldinger paper. The proof is conducted relative to an axiomatic theory of expressions and substitutions. The structure of the derived program reflects the proof from which it was extracted. Conditional expressions in the program are obtained from case analysis in the proof; recursion is introduced using well-founded induction, with respect to a well-founded relation axiomatized in the theory. The proof was obtained automatically by the first-order resolution theorem prover snark [Stickel et al., 2001]. The extracted program, as we remarked, improves on Manna and Waldinger’s and contains some novel elements.