Computer Laboratory

Technical reports

A fixedpoint approach to implementing (co)inductive definitions (updated version)

Lawrence C. Paulson

July 1995, 29 pages

Abstract

Several theorem provers provide commands for formalizing recursive datatypes or inductively defined sets. This paper presents a new approach, based on fixedpoint definitions. It is unusually general: it admits all monotone inductive definitions. It is conceptually simple, which has allowed the easy implementation of mutual recursion and other conveniences. It also handles coinductive definitions: simply replace the least fixedpoint by a greatest fixedpoint. This represents the first automated support for coinductive definitions.

The method has been implemented in Isabelle’s formalization of ZF set theory. It should be applicable to any logic in which the Knaster-Tarski Theorem can be proved. The paper briefly describes a method of formalizing non-well-founded data structures in standard ZF set theory.

Examples include lists of n elements, the accessible part of a relation and the set of primitive recursive functions. One example of a coinductive definition is bisimulations for lazy lists. Recursive datatypes are examined in detail, as well as one example of a “codatatype”: lazy lists. The appendices are simple user’s manuals for this Isabelle/ZF package.

Full text

PDF (0.2 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-320,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{A fixedpoint approach to implementing (co)inductive
         	   definitions (updated version)}},
  year = 	 1995,
  month = 	 jul,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-320.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-320}
}