Technical reports

Recent developments in LCF: examples of structural induction

Larry Paulson

January 1983, 15 pages

DOI: 10.48456/tr-34

Abstract

Manna and Waldinger have outlined a large proof that probably exceeds the power of current theorem-provers. The proof establishes the unification algorithm for terms composed of variables, constants, and other terms. Two theorems from this proof, involving structural induction, are performed in the LCF proof assistant. These theorems concern a function that searches for an occurrence of one term inside another, and a function that lists the variables in a term.

Formally, terms are regarded as abstract syntax trees. LCF automatically builds the first-order theory, with equality, of this recursive data structure.

The first theorem has a simple proof, induction followed by rewriting. The second theorem requires a cases split and substitution throughout the goal. Each theorem is proved by reducing the initial goal to simpler and simpler subgoals. LCF provides many standard proof strategies for attacking goals; the user can program additional ones in LCF’s meta-language, ML. This felxibility allows users to take ideas from such diverse fields as denotational semantics and logic programming.

Full text

PDF (0.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-34,
  author =	 {Paulson, Larry},
  title = 	 {{Recent developments in LCF: examples of structural
         	   induction}},
  year = 	 1983,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-34.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-34},
  number = 	 {UCAM-CL-TR-34}
}