3162

1 
%process by latex inddefsslides; dvips Plime inddefsslides


2 
% ghostview magstep 2 landscape inddefsslides.ps


3 
% $Id$


4 
\documentclass[a4,slidesonly,semlayer]{seminar}


5 


6 
\usepackage{fancybox}


7 
\usepackage{semhelv}


8 
\usepackage{epsf}


9 
\def\printlandscape{\special{landscape}} % Works with dvips.


10 


11 
\slidesmag{5}\articlemag{2} %the difference is 3 instead of 4!


12 
\extraslideheight{30pt}


13 


14 
\renewcommand\slidefuzz{6pt}


15 
\sloppy\hfuzz2pt %sloppy defines \hfuzz0.5pt but it's mainly for text


16 


17 
\newcommand\sbs{\subseteq}


18 
\newcommand\Pow{{\cal P}}


19 
\newcommand\lfp{\hbox{\tt lfp}}


20 
\newcommand\gfp{\hbox{\tt gfp}}


21 
\newcommand\lst{\hbox{\tt list}}


22 
\newcommand\term{\hbox{\tt term}}


23 


24 
\newcommand\heading[1]{%


25 
\begin{center}\large\bf\shadowbox{#1}\end{center}


26 
\vspace{1ex minus 1ex}}


27 


28 
\newpagestyle{mine}%


29 
{L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil


30 
\thepage}%


31 
{\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=6


32 
hoffset=14}\hfil}


33 
\pagestyle{mine}


34 


35 


36 
\begin{document}


37 
\slidefonts


38 


39 
\begin{slide}\centering


40 
\shadowbox{%


41 
\begin{Bcenter}


42 
{\Large\bf A Fixedpoint Approach to}\\[2ex]


43 
{\Large\bf (Co)Inductive Definitions}


44 
\end{Bcenter}}


45 
\bigskip


46 


47 
\begin{Bcenter}


48 
Lawrence C. Paulson\\


49 
Computer Laboratory\\


50 
University of Cambridge\\


51 
England\\[1ex]


52 
\verblcp@cl.cam.ac.uk


53 
\end{Bcenter}


54 
\bigskip


55 


56 
{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453


57 
`Types'}


58 
\end{slide}


59 


60 


61 
\begin{slide}


62 
\heading{Inductive Definitions}


63 
\begin{itemize}


64 
\item {\bf datatypes}


65 
\begin{itemize}


66 
\item finite lists, trees


67 
\item syntax of expressions, \ldots


68 
\end{itemize}


69 
\item {\bf inference systems}


70 
\begin{itemize}


71 
\item transitive closure of a relation


72 
\item transition systems


73 
\item structural operational semantics


74 
\end{itemize}


75 
\end{itemize}


76 


77 
Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF


78 
\end{slide}


79 


80 


81 
\begin{slide}


82 
\heading{Coinductive Definitions}


83 
\begin{itemize}


84 
\item {\bf codatatypes}


85 
\begin{itemize}


86 
\item {\it infinite\/} lists, trees


87 
\item syntax of {\it infinite\/} expressions, \ldots


88 
\end{itemize}


89 
\item {\bf bisimulation relations}


90 
\begin{itemize}


91 
\item process equivalence


92 
\item uses in functional programming (Abramksy, Howe)


93 
\end{itemize}


94 
\end{itemize}


95 


96 
Supported by \ldots ?, \ldots, Isabelle/ZF


97 
\end{slide}


98 


99 


100 
\begin{slide}


101 
\heading{The KnasterTarksi Fixedpoint Theorem}


102 
$h$ a monotone function


103 


104 
$D$ a set such that $h(D)\sbs D$


105 


106 
The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions


107 


108 
The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions


109 


110 
{\it A general approach\/}:


111 
\begin{itemize}


112 
\item handles all provably monotone definitions


113 
\item works for set theory, higherorder logic, \ldots


114 
\end{itemize}


115 
\end{slide}


116 


117 


118 
\begin{slide}


119 
\heading{An Implementation in Isabelle/ZF}\centering


120 
\begin{itemize}


121 
\item {\bf Input}


122 
\begin{itemize}


123 
\item description of {\it introduction rules\/} \& tree's {\it


124 
constructors\/}


125 
\item {\it theorems\/} implying that the definition is {\it monotonic\/}


126 
\end{itemize}


127 
\item {\bf Output}


128 
\begin{itemize}


129 
\item (co)induction rules


130 
\item case analysis rule and {\it rule inversion\/} tools, \ldots


131 
\end{itemize}


132 
\end{itemize}


133 


134 
\vfill


135 
{\it flexible, secure, \ldots but fast\/}


136 
\end{slide}


137 


138 


139 
\begin{slide}


140 
\heading{Working Examples}


141 
\begin{itemize}


142 
\item lists


143 
\item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$


144 
\item primitive recursive functions


145 
\item lazy lists


146 
\item bisimulations for lazy lists


147 
\item combinator reductions; ChurchRosser Theorem


148 
\item mutually recursive trees \& forests


149 
\end{itemize}


150 
\end{slide}


151 


152 


153 
\begin{slide}


154 
\heading{Other Work Using Fixedpoints}


155 
{\bf The HOL system}:


156 
\begin{itemize}


157 
\item Melham's induction package: special case of Fixedpoint Theorem


158 
\item Andersen \& Petersen's induction package


159 
\item (no HOL datatype package uses fixedpoints)


160 
\end{itemize}


161 


162 
{\bf Coq and LEGO}:


163 
\begin{itemize}


164 
\item (Co)induction {\it almost\/} expressible in base logic (CoC)


165 
\item \ldots{} inductive definitions are builtin


166 
\end{itemize}


167 
\end{slide}


168 


169 


170 
\begin{slide}


171 
\heading{Limitations \& Future Developments}\centering


172 
\begin{itemize}


173 
\item {\bf infinitebranching trees}


174 
\begin{itemize}


175 
\item justification requires proof


176 
\item would be easier to {\it build them in\/}!


177 
\end{itemize}


178 
\item {\bf recursive function definitions}


179 
\begin{itemize}


180 
\item use {\it wellfounded\/} recursion


181 
\item distinct from datatype definitions


182 
\end{itemize}


183 
\item {\bf port to Isabelle/HOL}


184 
\end{itemize}


185 
\end{slide}


186 


187 
\end{document}


188 


189 


190 
{\it flat\/} ordered pairs used to define infinite lists, \ldots


191 


192 
\begin{slide}


193 
\heading{}\centering


194 
\end{slide}


195 
