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
     1 %process by     latex ind-defs-slides; dvips -Plime ind-defs-slides
     2 %               ghostview -magstep -2 -landscape ind-defs-slides.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     \verb|lcp@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 Knaster-Tarksi 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, higher-order 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; Church-Rosser 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 built-in
   166 \end{itemize}
   167 \end{slide}
   168 
   169 
   170 \begin{slide}
   171 \heading{Limitations \& Future Developments}\centering
   172 \begin{itemize}
   173   \item {\bf infinite-branching 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 well-founded\/} 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