# HG changeset patch
# User paulson
# Date 861293412 -7200
# Node ID bb55cab416af79b7de5a9f0854684037f627365f
# Parent  184c7cd8043d6dcdbd0fca2d57fbc28947a5326b
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?

diff -r 184c7cd8043d -r bb55cab416af doc-src/ind-defs.tex
--- a/doc-src/ind-defs.tex	Thu Apr 17 17:54:21 1997 +0200
+++ b/doc-src/ind-defs.tex	Thu Apr 17 18:10:12 1997 +0200
@@ -4,10 +4,9 @@
 
 \title{A Fixedpoint Approach to\\ 
   (Co)Inductive and (Co)Datatype Definitions%
-\thanks{J. Grundy and S. Thompson made detailed
-    comments; the referees were also helpful.  Research funded by
-    SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453
-    ``Types''.}}
+  \thanks{J. Grundy and S. Thompson made detailed comments.  Mads Tofte and
+    the referees were also helpful.  The research was funded by the SERC
+    grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}
 
 \author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
         Computer Laboratory, University of Cambridge, England}
@@ -138,20 +137,23 @@
 Some logics take datatypes as primitive; consider Boyer and Moore's shell
 principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
 
-A datatype is but one example of an \defn{inductive definition}.  This
-specifies the least set closed under given rules~\cite{aczel77}.  The
-collection of theorems in a logic is inductively defined.  A structural
-operational semantics~\cite{hennessy90} is an inductive definition of a
-reduction or evaluation relation on programs.  A few theorem provers
-provide commands for formalizing inductive definitions; these include
-Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}.
+A datatype is but one example of an \defn{inductive definition}.  Such a
+definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}
+given rules: applying a rule to elements of~$R$ yields a result within~$R$.
+Inductive definitions have many applications.  The collection of theorems in a
+logic is inductively defined.  A structural operational
+semantics~\cite{hennessy90} is an inductive definition of a reduction or
+evaluation relation on programs.  A few theorem provers provide commands for
+formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and
+again the \textsc{hol} system~\cite{camilleri92}.
 
-The dual notion is that of a \defn{coinductive definition}.  This specifies
-the greatest set closed under given rules.  Important examples include
-using bisimulation relations to formalize equivalence of
-processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}.
-Other examples include lazy lists and other infinite data structures; these
-are called \defn{codatatypes} below.
+The dual notion is that of a \defn{coinductive definition}.  Such a definition
+specifies the greatest set~$R$ \defn{consistent with} given rules: every
+element of~$R$ can be seen as arising by applying a rule to elements of~$R$.
+Important examples include using bisimulation relations to formalize
+equivalence of processes~\cite{milner89} or lazy functional
+programs~\cite{abramsky90}.  Other examples include lazy lists and other
+infinite data structures; these are called \defn{codatatypes} below.
 
 Not all inductive definitions are meaningful.  \defn{Monotone} inductive
 definitions are a large, well-behaved class.  Monotonicity can be enforced
@@ -219,7 +221,7 @@
 These equations are instances of the Knaster-Tarski theorem, which states
 that every monotonic function over a complete lattice has a
 fixedpoint~\cite{davey&priestley}.  It is obvious from their definitions
-that  $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
+that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
 
 This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
 prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
@@ -472,7 +474,7 @@
 refinements such as those for the induction rules.  (Experience may suggest
 refinements later.)  Consider the codatatype of lazy lists as an example.  For
 suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
-greatest fixedpoint satisfying the rules
+greatest set consistent with the rules
 \[  \LNil\in\llist(A)  \qquad 
     \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
 \]