Corrected the informal description of coinductive definition in sections 1
authorpaulson
Thu Apr 17 18:10:12 1997 +0200 (1997-04-17)
changeset 2974bb55cab416af
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?
doc-src/ind-defs.tex
     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  \]