wneuper/isa: doc-src/Inductive/ind-defs-slides.tex@20e3616b2d9c

     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}

     6 \usepackage{fancybox}

     7 \usepackage{semhelv}

     8 \usepackage{epsf}

     9 \def\printlandscape{\special{landscape}}    % Works with dvips.

    11 \slidesmag{5}\articlemag{2}    %the difference is 3 instead of 4!

    12 \extraslideheight{30pt}

    14 \renewcommand\slidefuzz{6pt}

    15 \sloppy\hfuzz2pt   %sloppy defines \hfuzz0.5pt but it's mainly for text

    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}}

    24 \newcommand\heading[1]{%

    25   \begin{center}\large\bf\shadowbox{#1}\end{center}

    26   \vspace{1ex minus 1ex}}

    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}

    36 \begin{document}

    37 \slidefonts

    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

    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

    56 {\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453

    57   `Types'}

    58 \end{slide}

    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}

    77 Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF

    78 \end{slide}

    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}

    96 Supported by \ldots ?, \ldots, Isabelle/ZF

    97 \end{slide}

   100 \begin{slide}

   101 \heading{The Knaster-Tarksi Fixedpoint Theorem}

   102 $h$ a monotone function

   104 $D$ a set such that $h(D)\sbs D$

   106 The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions

   108 The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions

   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}

   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}

   134 \vfill

   135 {\it flexible, secure, \ldots but fast\/}

   136 \end{slide}

   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}

   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}

   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}

   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}

   187 \end{document}

   190 {\it flat\/} ordered pairs used to define infinite lists, \ldots

   192 \begin{slide}

   193 \heading{}\centering

   194 \end{slide}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 3162	78fa85d44e68
child 43508	381fdcab0f36
permissions	-rw-r--r--