[Prev][Next][Index][Thread]
paper available (draft)
The following paper is available by anonymous ftp from the University of
Cambridge. Instructions:
* Connect to host ftp.cl.cam.ac.uk [128.232.0.56]
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary")
* go to directory ml (by typing "cd ml")
* "get" the file final.ps.gz from that directory.
Lawrence C Paulson, University Lecturer
Computer Laboratory, University of Cambridge,
Pembroke Street, Cambridge CB2 3QG, England
Tel: +44(0)223 334623 Fax: +44(0)223 334678
A Concrete Final Coalgebra Theorem for ZF Set Theory
by Lawrence C. Paulson
A special final coalgebra theorem, in the style of Aczel's, 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.
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.
The theorem, like Aczel's, applies only to functors that are uniform on
maps. This property is discussed and it is noted that the identity functor is
not uniform on maps, a point omitted from previous literature.