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