[Prev][Next][Index][Thread]
paper available
The following report is available by anonymous ftp from the University of
Cambridge.
A Fixedpoint Approach to Implementing (Co)Inductive Definitions
by Lawrence C. Paulson
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 provably 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.
FTP 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 reports (by typing "cd reports")
* "get" the file TR320-lcp-isabelle-ind-defs.dvi.gz from that directory.
This is a gzip'ed dvi file. It should be unpacked using the Gnu utility
gunzip.
Larry Paulson