Reference. First-order unification by structural recursion

Conor McBride · · unification · PDF · DOI · pldb
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

Cite as @mcbrideFirstorderUnification2003 (helia, typst) · \cite{mcbrideFirstorderUnification2003} (LaTeX)
BibTeX
bibtex · 10 lines
@article{mcbrideFirstorderUnification2003,
 title = {First-order unification by structural recursion},
 author = {McBride, Conor},
 year = {2003},
 journal = {Journal of Functional Programming},
 volume = {13},
 number = {6},
 pages = {1061--1075},
 doi = {10.1017/S0956796803004957}
}
hayagriva YAML (typst)
yaml · 13 lines
mcbrideFirstorderUnification2003:
  type: article
  title: First-order unification by structural recursion
  author: McBride, Conor
  date: 2003
  page-range: 1061-1075
  serial-number:
    doi: 10.1017/S0956796803004957
  parent:
    type: periodical
    title: Journal of Functional Programming
    issue: 6
    volume: 13
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.
DOI
Cites 22 works (0 here)
External (22)
mcbrideFirstorderUnification2003 reference entries/refs/mcbrideFirstorderUnification2003/mcbrideFirstorderUnification2003.hel