Avoid record-inner constants in polymorphic definitions in Bali
The Bali package needs to insert a record extension into a type
class and define an associated polymorphic constant. There is no
elegant way to do this.
The existing approach was to insert every record extension into
the type class, defining the polymorphic constant at each layer
using inner operations created by the record package. Some of
those operations have been removed. They can be replaced by use
of record_name.extend if necessary, but we can also sidestep
this altogether.
The simpler approach here is to use defs(overloaded) once to
provide a single definition for the composition of all the type
constructors, which seems to be permitted. This gets us exactly
the fact we need, with the cost that some types that were
admitted to the type class have no definition for the constant
at all.
%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}