Technical reports

A concrete final coalgebra theorem for ZF set theory

Lawrence C. Paulson

May 1994, 21 pages

DOI: 10.48456/tr-334

Abstract

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel’s Solution and Substitution Lemmas are proved in the style of Rutten and Turi (1993).

The approach is less general than Aczel’s; non-well-founded objects can be modelled only using the variant tuples and functions. But the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. The theory is intended for machine implementation and a simple case of it is already implemented using the theorem prover Isabelle.

Full text

PDF (0.2 MB)
PS (0.1 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-334,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{A concrete final coalgebra theorem for ZF set theory}},
  year = 	 1994,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-334.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-334},
  number = 	 {UCAM-CL-TR-334}
}