Department of Computer Science and Technology

Technical reports

Structural induction in LCF

Lawrence Paulson

November 1983, 35 pages

DOI: 10.48456/tr-44

Abstract

The fixed-point theory of computation can express a variety of recursive data types, including lazy types, conventional first-order (strict) types, mutually recursive types, and types with equational constraints. Lazy types contain infinite objects, regarded as the limit of a chain of finite objects. Structural induction for all these types follows from fixed-point induction, though induction for lazy types is only sound for a certain class of formulas.

The paper presents the derivation of structural induction for each type, and justifies the necessary axioms by furnishing models for them. It presents example type definitions of lazy lists, strict lists, syntax trees for expressions and finite sets. Strict data types are proved to be flat in their partial ordering. Primitive recursion operators are introduced for each type, providing theoretical insights as well as a concise notation for defining total functions.

The research was done using LCF, an interactive theorem-prover for the fixed-point theory. The paper documents the theory of LCF data types, and surveys several LCF proofs involving structural induction. In order to be self-contained, it makes little reference to LCF details and includes a summary of the fixed point theory.

Full text

PDF (1.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-44,
  author =	 {Paulson, Lawrence},
  title = 	 {{Structural induction in LCF}},
  year = 	 1983,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-44.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-44},
  number = 	 {UCAM-CL-TR-44}
}