%process by latex ind-defs-slides; dvips -Plime ind-defs-slides
% ghostview -magstep -2 -landscape ind-defs-slides.ps
% $Id$
\documentclass[a4,slidesonly,semlayer]{seminar}
\usepackage{fancybox}
\usepackage{semhelv}
\usepackage{epsf}
\def\printlandscape{\special{landscape}} % Works with dvips.
\slidesmag{5}\articlemag{2} %the difference is 3 instead of 4!
\extraslideheight{30pt}
\renewcommand\slidefuzz{6pt}
\sloppy\hfuzz2pt %sloppy defines \hfuzz0.5pt but it's mainly for text
\newcommand\sbs{\subseteq}
\newcommand\Pow{{\cal P}}
\newcommand\lfp{\hbox{\tt lfp}}
\newcommand\gfp{\hbox{\tt gfp}}
\newcommand\lst{\hbox{\tt list}}
\newcommand\term{\hbox{\tt term}}
\newcommand\heading[1]{%
\begin{center}\large\bf\shadowbox{#1}\end{center}
\vspace{1ex minus 1ex}}
\newpagestyle{mine}%
{L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil
\thepage}%
{\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6
hoffset=-14}\hfil}
\pagestyle{mine}
\begin{document}
\slidefonts
\begin{slide}\centering
\shadowbox{%
\begin{Bcenter}
{\Large\bf A Fixedpoint Approach to}\\[2ex]
{\Large\bf (Co)Inductive Definitions}
\end{Bcenter}}
\bigskip
\begin{Bcenter}
Lawrence C. Paulson\\
Computer Laboratory\\
University of Cambridge\\
England\\[1ex]
\verb|lcp@cl.cam.ac.uk|
\end{Bcenter}
\bigskip
{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453
`Types'}
\end{slide}
\begin{slide}
\heading{Inductive Definitions}
\begin{itemize}
\item {\bf datatypes}
\begin{itemize}
\item finite lists, trees
\item syntax of expressions, \ldots
\end{itemize}
\item {\bf inference systems}
\begin{itemize}
\item transitive closure of a relation
\item transition systems
\item structural operational semantics
\end{itemize}
\end{itemize}
Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF
\end{slide}
\begin{slide}
\heading{Coinductive Definitions}
\begin{itemize}
\item {\bf codatatypes}
\begin{itemize}
\item {\it infinite\/} lists, trees
\item syntax of {\it infinite\/} expressions, \ldots
\end{itemize}
\item {\bf bisimulation relations}
\begin{itemize}
\item process equivalence
\item uses in functional programming (Abramksy, Howe)
\end{itemize}
\end{itemize}
Supported by \ldots ?, \ldots, Isabelle/ZF
\end{slide}
\begin{slide}
\heading{The Knaster-Tarksi Fixedpoint Theorem}
$h$ a monotone function
$D$ a set such that $h(D)\sbs D$
The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions
The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions
{\it A general approach\/}:
\begin{itemize}
\item handles all provably monotone definitions
\item works for set theory, higher-order logic, \ldots
\end{itemize}
\end{slide}
\begin{slide}
\heading{An Implementation in Isabelle/ZF}\centering
\begin{itemize}
\item {\bf Input}
\begin{itemize}
\item description of {\it introduction rules\/} \& tree's {\it
constructors\/}
\item {\it theorems\/} implying that the definition is {\it monotonic\/}
\end{itemize}
\item {\bf Output}
\begin{itemize}
\item (co)induction rules
\item case analysis rule and {\it rule inversion\/} tools, \ldots
\end{itemize}
\end{itemize}
\vfill
{\it flexible, secure, \ldots but fast\/}
\end{slide}
\begin{slide}
\heading{Working Examples}
\begin{itemize}
\item lists
\item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$
\item primitive recursive functions
\item lazy lists
\item bisimulations for lazy lists
\item combinator reductions; Church-Rosser Theorem
\item mutually recursive trees \& forests
\end{itemize}
\end{slide}
\begin{slide}
\heading{Other Work Using Fixedpoints}
{\bf The HOL system}:
\begin{itemize}
\item Melham's induction package: special case of Fixedpoint Theorem
\item Andersen \& Petersen's induction package
\item (no HOL datatype package uses fixedpoints)
\end{itemize}
{\bf Coq and LEGO}:
\begin{itemize}
\item (Co)induction {\it almost\/} expressible in base logic (CoC)
\item \ldots{} inductive definitions are built-in
\end{itemize}
\end{slide}
\begin{slide}
\heading{Limitations \& Future Developments}\centering
\begin{itemize}
\item {\bf infinite-branching trees}
\begin{itemize}
\item justification requires proof
\item would be easier to {\it build them in\/}!
\end{itemize}
\item {\bf recursive function definitions}
\begin{itemize}
\item use {\it well-founded\/} recursion
\item distinct from datatype definitions
\end{itemize}
\item {\bf port to Isabelle/HOL}
\end{itemize}
\end{slide}
\end{document}
{\it flat\/} ordered pairs used to define infinite lists, \ldots
\begin{slide}
\heading{}\centering
\end{slide}