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