author | paulson |

Thu Apr 17 18:10:12 1997 +0200 (1997-04-17) | |

changeset 2974 | bb55cab416af |

parent 2973 | 184c7cd8043d |

child 2975 | 230f456956a2 |

Corrected the informal description of coinductive definition in sections 1

and 4.3, introducing the notion of "consistent with" a set of rules.

Final version for Milner Festschrift?

and 4.3, introducing the notion of "consistent with" a set of rules.

Final version for Milner Festschrift?

1.1 --- a/doc-src/ind-defs.tex Thu Apr 17 17:54:21 1997 +0200 1.2 +++ b/doc-src/ind-defs.tex Thu Apr 17 18:10:12 1997 +0200 1.3 @@ -4,10 +4,9 @@ 1.4 1.5 \title{A Fixedpoint Approach to\\ 1.6 (Co)Inductive and (Co)Datatype Definitions% 1.7 -\thanks{J. Grundy and S. Thompson made detailed 1.8 - comments; the referees were also helpful. Research funded by 1.9 - SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 1.10 - ``Types''.}} 1.11 + \thanks{J. Grundy and S. Thompson made detailed comments. Mads Tofte and 1.12 + the referees were also helpful. The research was funded by the SERC 1.13 + grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}} 1.14 1.15 \author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\ 1.16 Computer Laboratory, University of Cambridge, England} 1.17 @@ -138,20 +137,23 @@ 1.18 Some logics take datatypes as primitive; consider Boyer and Moore's shell 1.19 principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}. 1.20 1.21 -A datatype is but one example of an \defn{inductive definition}. This 1.22 -specifies the least set closed under given rules~\cite{aczel77}. The 1.23 -collection of theorems in a logic is inductively defined. A structural 1.24 -operational semantics~\cite{hennessy90} is an inductive definition of a 1.25 -reduction or evaluation relation on programs. A few theorem provers 1.26 -provide commands for formalizing inductive definitions; these include 1.27 -Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}. 1.28 +A datatype is but one example of an \defn{inductive definition}. Such a 1.29 +definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under} 1.30 +given rules: applying a rule to elements of~$R$ yields a result within~$R$. 1.31 +Inductive definitions have many applications. The collection of theorems in a 1.32 +logic is inductively defined. A structural operational 1.33 +semantics~\cite{hennessy90} is an inductive definition of a reduction or 1.34 +evaluation relation on programs. A few theorem provers provide commands for 1.35 +formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and 1.36 +again the \textsc{hol} system~\cite{camilleri92}. 1.37 1.38 -The dual notion is that of a \defn{coinductive definition}. This specifies 1.39 -the greatest set closed under given rules. Important examples include 1.40 -using bisimulation relations to formalize equivalence of 1.41 -processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. 1.42 -Other examples include lazy lists and other infinite data structures; these 1.43 -are called \defn{codatatypes} below. 1.44 +The dual notion is that of a \defn{coinductive definition}. Such a definition 1.45 +specifies the greatest set~$R$ \defn{consistent with} given rules: every 1.46 +element of~$R$ can be seen as arising by applying a rule to elements of~$R$. 1.47 +Important examples include using bisimulation relations to formalize 1.48 +equivalence of processes~\cite{milner89} or lazy functional 1.49 +programs~\cite{abramsky90}. Other examples include lazy lists and other 1.50 +infinite data structures; these are called \defn{codatatypes} below. 1.51 1.52 Not all inductive definitions are meaningful. \defn{Monotone} inductive 1.53 definitions are a large, well-behaved class. Monotonicity can be enforced 1.54 @@ -219,7 +221,7 @@ 1.55 These equations are instances of the Knaster-Tarski theorem, which states 1.56 that every monotonic function over a complete lattice has a 1.57 fixedpoint~\cite{davey&priestley}. It is obvious from their definitions 1.58 -that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. 1.59 +that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. 1.60 1.61 This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to 1.62 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must 1.63 @@ -472,7 +474,7 @@ 1.64 refinements such as those for the induction rules. (Experience may suggest 1.65 refinements later.) Consider the codatatype of lazy lists as an example. For 1.66 suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the 1.67 -greatest fixedpoint satisfying the rules 1.68 +greatest set consistent with the rules 1.69 \[ \LNil\in\llist(A) \qquad 1.70 \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} 1.71 \]