doc-src/ind-defs-slides.tex
author oheimb
Sat Feb 15 16:10:00 1997 +0100 (1997-02-15)
changeset 2628 1fe7c9f599c2
parent 1144 5a62ecf80126
permissions -rw-r--r--
description of del(eq)congs, safe and unsafe solver
lcp@1144
     1
%process by     latex ind-defs-slides; dvips -Plime ind-defs-slides
lcp@1144
     2
%               ghostview -magstep -2 -landscape ind-defs-slides.ps
lcp@1144
     3
%  $Id$
lcp@1144
     4
\documentclass[a4,slidesonly,semlayer]{seminar}
lcp@541
     5
lcp@1144
     6
\usepackage{fancybox}
lcp@1144
     7
\usepackage{semhelv}
lcp@1144
     8
\usepackage{epsf}
lcp@541
     9
\def\printlandscape{\special{landscape}}    % Works with dvips.
lcp@541
    10
lcp@541
    11
\slidesmag{5}\articlemag{2}    %the difference is 3 instead of 4!
lcp@541
    12
\extraslideheight{30pt}
lcp@541
    13
lcp@541
    14
\renewcommand\slidefuzz{6pt}
lcp@541
    15
\sloppy\hfuzz2pt   %sloppy defines \hfuzz0.5pt but it's mainly for text
lcp@541
    16
lcp@541
    17
\newcommand\sbs{\subseteq}
lcp@541
    18
\newcommand\Pow{{\cal P}}
lcp@541
    19
\newcommand\lfp{\hbox{\tt lfp}}
lcp@541
    20
\newcommand\gfp{\hbox{\tt gfp}}
lcp@541
    21
\newcommand\lst{\hbox{\tt list}}
lcp@541
    22
\newcommand\term{\hbox{\tt term}}
lcp@541
    23
lcp@541
    24
\newcommand\heading[1]{%
lcp@541
    25
  \begin{center}\large\bf\shadowbox{#1}\end{center}
lcp@541
    26
  \vspace{1ex minus 1ex}}
lcp@541
    27
lcp@541
    28
\newpagestyle{mine}%
lcp@541
    29
  {L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil
lcp@541
    30
      \thepage}%
lcp@541
    31
  {\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6
lcp@541
    32
      hoffset=-14}\hfil}
lcp@541
    33
\pagestyle{mine}
lcp@541
    34
lcp@541
    35
lcp@541
    36
\begin{document}
lcp@541
    37
\slidefonts
lcp@541
    38
lcp@541
    39
\begin{slide}\centering
lcp@541
    40
\shadowbox{% 
lcp@541
    41
    \begin{Bcenter}
lcp@541
    42
    {\Large\bf A Fixedpoint Approach to}\\[2ex]
lcp@541
    43
    {\Large\bf (Co)Inductive Definitions}
lcp@541
    44
    \end{Bcenter}}
lcp@541
    45
\bigskip
lcp@541
    46
lcp@541
    47
    \begin{Bcenter}
lcp@541
    48
    Lawrence C. Paulson\\
lcp@541
    49
    Computer Laboratory\\
lcp@541
    50
    University of Cambridge\\
lcp@541
    51
    England\\[1ex]
lcp@541
    52
    \verb|lcp@cl.cam.ac.uk|
lcp@541
    53
    \end{Bcenter}
lcp@541
    54
\bigskip
lcp@541
    55
lcp@541
    56
{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453
lcp@541
    57
  `Types'} 
lcp@541
    58
\end{slide}
lcp@541
    59
lcp@541
    60
lcp@541
    61
\begin{slide}
lcp@541
    62
\heading{Inductive Definitions}
lcp@541
    63
\begin{itemize}
lcp@541
    64
  \item {\bf datatypes}
lcp@541
    65
    \begin{itemize}
lcp@541
    66
      \item finite lists, trees
lcp@541
    67
      \item syntax of expressions, \ldots
lcp@541
    68
    \end{itemize}
lcp@541
    69
  \item {\bf inference systems}
lcp@541
    70
    \begin{itemize}
lcp@541
    71
      \item transitive closure of a relation
lcp@541
    72
      \item transition systems
lcp@541
    73
      \item structural operational semantics
lcp@541
    74
    \end{itemize}
lcp@541
    75
\end{itemize}
lcp@541
    76
lcp@541
    77
Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF
lcp@541
    78
\end{slide}
lcp@541
    79
lcp@541
    80
lcp@541
    81
\begin{slide}
lcp@541
    82
\heading{Coinductive Definitions}
lcp@541
    83
\begin{itemize}
lcp@541
    84
  \item {\bf codatatypes}
lcp@541
    85
    \begin{itemize}
lcp@541
    86
      \item {\it infinite\/} lists, trees
lcp@541
    87
      \item  syntax of {\it infinite\/} expressions, \ldots
lcp@541
    88
    \end{itemize}
lcp@541
    89
  \item {\bf bisimulation relations}
lcp@541
    90
    \begin{itemize}
lcp@541
    91
      \item process equivalence
lcp@541
    92
      \item uses in functional programming (Abramksy, Howe)
lcp@541
    93
    \end{itemize}
lcp@541
    94
\end{itemize}
lcp@541
    95
lcp@541
    96
Supported by \ldots ?, \ldots, Isabelle/ZF
lcp@541
    97
\end{slide}
lcp@541
    98
lcp@541
    99
lcp@541
   100
\begin{slide}
lcp@541
   101
\heading{The Knaster-Tarksi Fixedpoint Theorem}
lcp@541
   102
$h$ a monotone function
lcp@541
   103
lcp@541
   104
$D$ a set such that $h(D)\sbs D$
lcp@541
   105
lcp@541
   106
The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions
lcp@541
   107
lcp@541
   108
The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions
lcp@541
   109
lcp@541
   110
{\it A general approach\/}:
lcp@541
   111
\begin{itemize}
lcp@541
   112
  \item handles all provably monotone definitions
lcp@541
   113
  \item works for set theory, higher-order logic, \ldots
lcp@541
   114
\end{itemize}
lcp@541
   115
\end{slide}
lcp@541
   116
lcp@541
   117
lcp@541
   118
\begin{slide}
lcp@541
   119
\heading{An Implementation in Isabelle/ZF}\centering
lcp@541
   120
\begin{itemize}
lcp@541
   121
  \item {\bf Input} 
lcp@541
   122
     \begin{itemize}
lcp@541
   123
      \item description of {\it introduction rules\/} \& tree's {\it
lcp@541
   124
          constructors\/} 
lcp@541
   125
      \item {\it theorems\/} implying that the definition is {\it monotonic\/}
lcp@541
   126
    \end{itemize}
lcp@541
   127
  \item {\bf Output} 
lcp@541
   128
     \begin{itemize}
lcp@541
   129
      \item (co)induction rules
lcp@541
   130
      \item case analysis rule and {\it rule inversion\/} tools, \ldots
lcp@541
   131
    \end{itemize}
lcp@541
   132
\end{itemize}
lcp@541
   133
lcp@541
   134
\vfill
lcp@541
   135
{\it flexible, secure, \ldots but fast\/}
lcp@541
   136
\end{slide}
lcp@541
   137
lcp@541
   138
lcp@541
   139
\begin{slide}
lcp@541
   140
\heading{Working Examples}
lcp@541
   141
\begin{itemize}
lcp@541
   142
  \item lists
lcp@541
   143
  \item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$
lcp@541
   144
  \item primitive recursive functions
lcp@541
   145
  \item lazy lists
lcp@541
   146
  \item bisimulations for lazy lists
lcp@541
   147
  \item combinator reductions; Church-Rosser Theorem
lcp@541
   148
  \item mutually recursive trees \& forests
lcp@541
   149
\end{itemize}
lcp@541
   150
\end{slide}
lcp@541
   151
lcp@541
   152
lcp@541
   153
\begin{slide}
lcp@541
   154
\heading{Other Work Using Fixedpoints}
lcp@541
   155
{\bf The HOL system}:
lcp@541
   156
\begin{itemize}
lcp@541
   157
  \item Melham's induction package: special case of Fixedpoint Theorem
lcp@541
   158
  \item Andersen \& Petersen's induction package
lcp@541
   159
  \item (no HOL datatype package uses fixedpoints)
lcp@541
   160
\end{itemize}
lcp@541
   161
lcp@541
   162
{\bf Coq and LEGO}:
lcp@541
   163
\begin{itemize}
lcp@541
   164
  \item (Co)induction {\it almost\/} expressible in base logic (CoC)
lcp@541
   165
  \item \ldots{} inductive definitions are built-in
lcp@541
   166
\end{itemize}
lcp@541
   167
\end{slide}
lcp@541
   168
lcp@541
   169
lcp@541
   170
\begin{slide}
lcp@541
   171
\heading{Limitations \& Future Developments}\centering
lcp@541
   172
\begin{itemize}
lcp@541
   173
  \item {\bf infinite-branching trees}
lcp@541
   174
    \begin{itemize}
lcp@541
   175
      \item justification requires proof
lcp@541
   176
      \item would be easier to {\it build them in\/}!
lcp@541
   177
    \end{itemize}
lcp@541
   178
  \item {\bf recursive function definitions}
lcp@541
   179
    \begin{itemize}
lcp@541
   180
      \item use {\it well-founded\/} recursion
lcp@541
   181
      \item distinct from datatype definitions
lcp@541
   182
    \end{itemize}
lcp@541
   183
  \item {\bf port to Isabelle/HOL}
lcp@541
   184
\end{itemize}
lcp@541
   185
\end{slide}
lcp@541
   186
lcp@541
   187
\end{document}
lcp@541
   188
lcp@541
   189
lcp@541
   190
{\it flat\/} ordered pairs used to define infinite lists, \ldots
lcp@541
   191
lcp@541
   192
\begin{slide}
lcp@541
   193
\heading{}\centering
lcp@541
   194
\end{slide}
lcp@541
   195