overheads for inductive definitions, originally for CADE-12
authorlcp
Wed Aug 17 10:42:41 1994 +0200 (1994-08-17 ago)
changeset 541be4c4ba87143
parent 540 e30c23731c2d
child 542 164be35c8a16
overheads for inductive definitions, originally for CADE-12
doc-src/ind-defs-slides.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ind-defs-slides.tex	Wed Aug 17 10:42:41 1994 +0200
     1.3 @@ -0,0 +1,195 @@
     1.4 +%process by     nlatex cade; dvips -o s.ps -Ppreview cade
     1.5 +%               ghostview -magstep -2 -landscape s.ps
     1.6 +\documentstyle[fancybox,newlfont,lcp,proof,semhelv,sem-a4,%
     1.7 +%  article,%
     1.8 +  slidesonly,%Try notes or notesonly instead
     1.9 +  semlayer%     This must be included, but you need the semcolor option to
    1.10 +  ]{seminar}                                  % actually see the overlays.
    1.11 +
    1.12 +\def\printlandscape{\special{landscape}}    % Works with dvips.
    1.13 +
    1.14 +\slidesmag{5}\articlemag{2}    %the difference is 3 instead of 4!
    1.15 +\extraslideheight{30pt}
    1.16 +
    1.17 +\renewcommand\slidefuzz{6pt}
    1.18 +\sloppy\hfuzz2pt   %sloppy defines \hfuzz0.5pt but it's mainly for text
    1.19 +
    1.20 +\newcommand\sbs{\subseteq}
    1.21 +\newcommand\Pow{{\cal P}}
    1.22 +\newcommand\lfp{\hbox{\tt lfp}}
    1.23 +\newcommand\gfp{\hbox{\tt gfp}}
    1.24 +\newcommand\lst{\hbox{\tt list}}
    1.25 +\newcommand\term{\hbox{\tt term}}
    1.26 +
    1.27 +\newcommand\heading[1]{%
    1.28 +  \begin{center}\large\bf\shadowbox{#1}\end{center}
    1.29 +  \vspace{1ex minus 1ex}}
    1.30 +
    1.31 +\newpagestyle{mine}%
    1.32 +  {L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil
    1.33 +      \thepage}%
    1.34 +  {\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6
    1.35 +      hoffset=-14}\hfil}
    1.36 +\pagestyle{mine}
    1.37 +
    1.38 +
    1.39 +\begin{document}
    1.40 +\slidefonts
    1.41 +
    1.42 +\begin{slide}\centering
    1.43 +\shadowbox{% 
    1.44 +    \begin{Bcenter}
    1.45 +    {\Large\bf A Fixedpoint Approach to}\\[2ex]
    1.46 +    {\Large\bf (Co)Inductive Definitions}
    1.47 +    \end{Bcenter}}
    1.48 +\bigskip
    1.49 +
    1.50 +    \begin{Bcenter}
    1.51 +    Lawrence C. Paulson\\
    1.52 +    Computer Laboratory\\
    1.53 +    University of Cambridge\\
    1.54 +    England\\[1ex]
    1.55 +    \verb|lcp@cl.cam.ac.uk|
    1.56 +    \end{Bcenter}
    1.57 +\bigskip
    1.58 +
    1.59 +{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453
    1.60 +  `Types'} 
    1.61 +\end{slide}
    1.62 +
    1.63 +
    1.64 +\begin{slide}
    1.65 +\heading{Inductive Definitions}
    1.66 +\begin{itemize}
    1.67 +  \item {\bf datatypes}
    1.68 +    \begin{itemize}
    1.69 +      \item finite lists, trees
    1.70 +      \item syntax of expressions, \ldots
    1.71 +    \end{itemize}
    1.72 +  \item {\bf inference systems}
    1.73 +    \begin{itemize}
    1.74 +      \item transitive closure of a relation
    1.75 +      \item transition systems
    1.76 +      \item structural operational semantics
    1.77 +    \end{itemize}
    1.78 +\end{itemize}
    1.79 +
    1.80 +Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF
    1.81 +\end{slide}
    1.82 +
    1.83 +
    1.84 +\begin{slide}
    1.85 +\heading{Coinductive Definitions}
    1.86 +\begin{itemize}
    1.87 +  \item {\bf codatatypes}
    1.88 +    \begin{itemize}
    1.89 +      \item {\it infinite\/} lists, trees
    1.90 +      \item  syntax of {\it infinite\/} expressions, \ldots
    1.91 +    \end{itemize}
    1.92 +  \item {\bf bisimulation relations}
    1.93 +    \begin{itemize}
    1.94 +      \item process equivalence
    1.95 +      \item uses in functional programming (Abramksy, Howe)
    1.96 +    \end{itemize}
    1.97 +\end{itemize}
    1.98 +
    1.99 +Supported by \ldots ?, \ldots, Isabelle/ZF
   1.100 +\end{slide}
   1.101 +
   1.102 +
   1.103 +\begin{slide}
   1.104 +\heading{The Knaster-Tarksi Fixedpoint Theorem}
   1.105 +$h$ a monotone function
   1.106 +
   1.107 +$D$ a set such that $h(D)\sbs D$
   1.108 +
   1.109 +The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions
   1.110 +
   1.111 +The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions
   1.112 +
   1.113 +{\it A general approach\/}:
   1.114 +\begin{itemize}
   1.115 +  \item handles all provably monotone definitions
   1.116 +  \item works for set theory, higher-order logic, \ldots
   1.117 +\end{itemize}
   1.118 +\end{slide}
   1.119 +
   1.120 +
   1.121 +\begin{slide}
   1.122 +\heading{An Implementation in Isabelle/ZF}\centering
   1.123 +\begin{itemize}
   1.124 +  \item {\bf Input} 
   1.125 +     \begin{itemize}
   1.126 +      \item description of {\it introduction rules\/} \& tree's {\it
   1.127 +          constructors\/} 
   1.128 +      \item {\it theorems\/} implying that the definition is {\it monotonic\/}
   1.129 +    \end{itemize}
   1.130 +  \item {\bf Output} 
   1.131 +     \begin{itemize}
   1.132 +      \item (co)induction rules
   1.133 +      \item case analysis rule and {\it rule inversion\/} tools, \ldots
   1.134 +    \end{itemize}
   1.135 +\end{itemize}
   1.136 +
   1.137 +\vfill
   1.138 +{\it flexible, secure, \ldots but fast\/}
   1.139 +\end{slide}
   1.140 +
   1.141 +
   1.142 +\begin{slide}
   1.143 +\heading{Working Examples}
   1.144 +\begin{itemize}
   1.145 +  \item lists
   1.146 +  \item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$
   1.147 +  \item primitive recursive functions
   1.148 +  \item lazy lists
   1.149 +  \item bisimulations for lazy lists
   1.150 +  \item combinator reductions; Church-Rosser Theorem
   1.151 +  \item mutually recursive trees \& forests
   1.152 +\end{itemize}
   1.153 +\end{slide}
   1.154 +
   1.155 +
   1.156 +\begin{slide}
   1.157 +\heading{Other Work Using Fixedpoints}
   1.158 +{\bf The HOL system}:
   1.159 +\begin{itemize}
   1.160 +  \item Melham's induction package: special case of Fixedpoint Theorem
   1.161 +  \item Andersen \& Petersen's induction package
   1.162 +  \item (no HOL datatype package uses fixedpoints)
   1.163 +\end{itemize}
   1.164 +
   1.165 +{\bf Coq and LEGO}:
   1.166 +\begin{itemize}
   1.167 +  \item (Co)induction {\it almost\/} expressible in base logic (CoC)
   1.168 +  \item \ldots{} inductive definitions are built-in
   1.169 +\end{itemize}
   1.170 +\end{slide}
   1.171 +
   1.172 +
   1.173 +\begin{slide}
   1.174 +\heading{Limitations \& Future Developments}\centering
   1.175 +\begin{itemize}
   1.176 +  \item {\bf infinite-branching trees}
   1.177 +    \begin{itemize}
   1.178 +      \item justification requires proof
   1.179 +      \item would be easier to {\it build them in\/}!
   1.180 +    \end{itemize}
   1.181 +  \item {\bf recursive function definitions}
   1.182 +    \begin{itemize}
   1.183 +      \item use {\it well-founded\/} recursion
   1.184 +      \item distinct from datatype definitions
   1.185 +    \end{itemize}
   1.186 +  \item {\bf port to Isabelle/HOL}
   1.187 +\end{itemize}
   1.188 +\end{slide}
   1.189 +
   1.190 +\end{document}
   1.191 +
   1.192 +
   1.193 +{\it flat\/} ordered pairs used to define infinite lists, \ldots
   1.194 +
   1.195 +\begin{slide}
   1.196 +\heading{}\centering
   1.197 +\end{slide}
   1.198 +