Computer Laboratory

Technical reports

Verifying the unification algorithm in LCF

Lawrence Paulson

March 1984, 28 pages

Abstract

Manna and Waldinger’s theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail, as an example of interaction with LCF. Translating the theory into LCF’s domain-theoretic logic is largely straightforward. Well-founded induction on a complex ordering is translated into nested structural inductions. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. The verification is presented as a series of lemmas. The LCF proofs are compared with the original ones, and with other approaches. It appears difficult to find a logic that is both simple and flexible, especially for proving termination.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-50,
  author =	 {Paulson, Lawrence},
  title = 	 {{Verifying the unification algorithm in LCF}},
  year = 	 1984,
  month = 	 mar,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-50.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-50}
}