Technical reports
Structural induction in LCF
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} }