Reference. First-order unification by structural recursion
First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve counting the number of unsolved variables and showing that this total decreases each time a substitution enlarges the terms. There are many such proofs in the literature (Manna & Waldinger, 1981; Paulson, 1985; Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999). This paper shows how a dependent type can relate terms to the set of variables over which they are constructed. As a consequence, first-order unification becomes a structurally recursive program, and a termination proof is no longer required. Both the program and its correctness proof have been checked using the proof assistant LEGO (Luo & Pollack, 1992; McBride, 1999).
Cite
Cited by (1)
Everybody’s Got To Be Somewhere mcbrideEverybodysGotToBeSomewhere2018
The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly, those we discard. Standard de Bruijn representations delay discarding maximally till the leaves of terms where one is chosen from the variables in scope at the expense of the rest. Consequently, introducing new but unused variables requires term traversal. This paper introduces a nameless ‘co-de-Bruijn’ representation which makes the opposite canonical choice, delaying discarding minimally, as near as possible to the root. It is literate Agda: dependent types make it a practical joy to express and be driven by strong intrinsic invariants which ensure that scope is aggressively whittled down to just the support of each subterm, in which every remaining variable occurs somewhere. The construction is generic, delivering a universe of syntaxes with higher-order metavariables, for which the appropriate notion of substitution is hereditary. The implementation of simultaneous substitution exploits tight scope control to avoid busywork and shift terms without traversal. Surprisingly, it is also intrinsically terminating, by structural recursion alone.
Cites 22 works (0 here)
External (22)
- Proving First-Order Unification Correct (2003)
- Lego development of First-Order Unification (2003)
- Dependently Typed Functional Programs and their Proofs (2000)
- A Finite Axiomatization of Inductive-Recursive Definitions (1999)
- Programming in Martin-Löf Type Theory. Unification: A non-trivial Example (1999)
- Structured Type Theory (1999)
- Cayenne—a language with dependent types (1998)
- The Zipper (1997)
- Unification: a case study in transposition of formal properties (1997)
- Elementary strong functional programming (1995)
- Computation and Reasoning: A Type Theory for Computer Science (1994)
- The implementation of ALF : a proof editor based on Martin-Löf's monomorphic type theory with explicit substitution (1994)
- Inductive families (1994)
- Interactive Program Derivation (1992)
- LEGO Proof Development System: User's Manual (1992)
- Développement de l'algorithme d'unification dans le Calcul des Constructions avec types inductifs (1992)
- Inductively defined types in the Calculus of Constructions (1990)
- Inductively defined functions in functional programming languages (1987)
- Verifying the unification algorithm in LCF (1985)
- Deductive synthesis of the unification algorithm (1981)
- Proving Properties of Programs by Structural Induction (1969)
- A Machine-Oriented Logic Based on the Resolution Principle (1965)