|
3121
|
1 |
(*<*)
|
|
|
2 |
theory SlidesA
|
|
|
3 |
imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
|
|
|
4 |
begin
|
|
|
5 |
|
|
|
6 |
notation (latex output)
|
|
|
7 |
set ("_") and
|
|
|
8 |
Cons ("_::/_" [66,65] 65)
|
|
|
9 |
|
|
|
10 |
(*>*)
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
text_raw {*
|
|
|
14 |
%% was \begin{colormixin}{20!averagebackgroundcolor}
|
|
|
15 |
%%
|
|
|
16 |
%% is \begin{colormixin}{50!averagebackgroundcolor}
|
|
|
17 |
\renewcommand{\slidecaption}{Warsaw, 9 February 2012}
|
|
|
18 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
19 |
\mode<presentation>{
|
|
|
20 |
\begin{frame}
|
|
|
21 |
\frametitle{%
|
|
|
22 |
\begin{tabular}{@ {}c@ {}}
|
|
|
23 |
\Huge Nominal Techniques\\[0mm]
|
|
|
24 |
\Huge in Isabelle\\
|
|
|
25 |
\Large or, How Not to be Intimidated by the\\[-3mm]
|
|
|
26 |
\Large Variable Convention\\[-5mm]
|
|
|
27 |
\end{tabular}}
|
|
|
28 |
|
|
|
29 |
\begin{center}
|
|
|
30 |
Christian Urban\\[1mm]
|
|
|
31 |
King's College London\\[-6mm]\mbox{}
|
|
|
32 |
\end{center}
|
|
|
33 |
|
|
|
34 |
\begin{center}
|
|
|
35 |
\begin{block}{}
|
|
|
36 |
\color{gray}
|
|
|
37 |
\small
|
|
|
38 |
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm]
|
|
|
39 |
If $M_1,\ldots,M_n$ occur in a certain mathematical context
|
|
|
40 |
(e.g. definition, proof), then in these terms all bound variables
|
|
|
41 |
are chosen to be different from the free variables.\\[2mm]
|
|
|
42 |
|
|
|
43 |
\footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
|
|
|
44 |
\end{block}
|
|
|
45 |
\end{center}
|
|
|
46 |
|
|
|
47 |
\end{frame}}
|
|
|
48 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
49 |
|
|
|
50 |
*}
|
|
|
51 |
|
|
|
52 |
text_raw {*
|
|
|
53 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
54 |
\mode<presentation>{
|
|
|
55 |
\begin{frame}<1->[c]
|
|
|
56 |
\frametitle{Nominal Techniques}
|
|
|
57 |
|
|
|
58 |
\begin{itemize}
|
|
|
59 |
\item Andy Pitts found out that permutations\\ preserve $\alpha$-equivalence:
|
|
|
60 |
\begin{center}
|
|
|
61 |
\smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2}
|
|
|
62 |
\end{center}
|
|
|
63 |
|
|
|
64 |
\item also permutations and substitutions commute, if you suspend permutations
|
|
|
65 |
in front of variables
|
|
|
66 |
\begin{center}
|
|
|
67 |
\smath{\pi\act\sigma(t) = \sigma(\pi\act t)}
|
|
|
68 |
\end{center}\medskip\medskip
|
|
|
69 |
|
|
|
70 |
\item this allowed us to define Nominal Unification\medskip
|
|
|
71 |
\begin{center}
|
|
|
72 |
\smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}
|
|
|
73 |
\smath{\nabla \vdash a \fresh^? t}
|
|
|
74 |
\end{center}
|
|
|
75 |
\end{itemize}
|
|
|
76 |
|
|
|
77 |
\begin{textblock}{3}(13.1,1.1)
|
|
|
78 |
\includegraphics[scale=0.26]{andrewpitts.jpg}
|
|
|
79 |
\end{textblock}
|
|
|
80 |
|
|
|
81 |
\end{frame}}
|
|
|
82 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
83 |
*}
|
|
|
84 |
|
|
|
85 |
text_raw {*
|
|
|
86 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
87 |
\mode<presentation>{
|
|
|
88 |
\begin{frame}[c]
|
|
|
89 |
\frametitle{Nominal Isabelle}
|
|
|
90 |
|
|
|
91 |
\begin{itemize}
|
|
|
92 |
\item a theory about atoms and permutations\medskip
|
|
|
93 |
|
|
|
94 |
\item support and freshness
|
|
|
95 |
\begin{center}
|
|
|
96 |
\smath{\text{supp}(x) \dn \{ a \mid \text{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}
|
|
|
97 |
\end{center}\bigskip\pause
|
|
|
98 |
|
|
|
99 |
\item $\alpha$-equivalence
|
|
|
100 |
\begin{center}
|
|
|
101 |
\begin{tabular}{l}
|
|
|
102 |
\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]
|
|
|
103 |
\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\
|
|
|
104 |
\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\
|
|
|
105 |
\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}
|
|
|
106 |
\end{tabular}
|
|
|
107 |
\end{center}
|
|
|
108 |
\end{itemize}
|
|
|
109 |
|
|
|
110 |
\end{frame}}
|
|
|
111 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
112 |
*}
|
|
|
113 |
|
|
|
114 |
text_raw {*
|
|
|
115 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
116 |
\mode<presentation>{
|
|
|
117 |
\begin{frame}<1-6>
|
|
|
118 |
\frametitle{New Types in HOL}
|
|
|
119 |
|
|
|
120 |
\begin{center}
|
|
|
121 |
\begin{tikzpicture}[scale=1.5]
|
|
|
122 |
%%%\draw[step=2mm] (-4,-1) grid (4,1);
|
|
|
123 |
|
|
|
124 |
\onslide<2-4,6>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
|
|
|
125 |
\onslide<1-4,6>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
|
|
|
126 |
\onslide<3-5,6>{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
|
|
|
127 |
|
|
|
128 |
\onslide<3-4,6>{\draw (-2.0, 0.845) -- (0.7,0.845);}
|
|
|
129 |
\onslide<3-4,6>{\draw (-2.0,-0.045) -- (0.7,-0.045);}
|
|
|
130 |
|
|
|
131 |
\onslide<4-4,6>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
|
|
|
132 |
\onslide<4-5,6>{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
|
|
|
133 |
\onslide<1-4,6>{\draw (1.8, 0.48) node[right=-0.1mm]
|
|
|
134 |
{\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6>{\alert{(sets of raw terms)}}\end{tabular}};}
|
|
|
135 |
\onslide<2-4,6>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
|
|
|
136 |
\onslide<3-5,6>{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
|
|
|
137 |
|
|
|
138 |
\onslide<3-4,6>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
|
|
|
139 |
\onslide<3-4,6>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
|
|
|
140 |
|
|
|
141 |
\onslide<6>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
|
|
|
142 |
\end{tikzpicture}
|
|
|
143 |
\end{center}
|
|
|
144 |
|
|
|
145 |
\begin{center}
|
|
|
146 |
\textcolor{red}{\large\bf\onslide<6>{define $\alpha$-equivalence}}
|
|
|
147 |
\end{center}
|
|
|
148 |
|
|
|
149 |
\end{frame}}
|
|
|
150 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
151 |
*}
|
|
|
152 |
|
|
|
153 |
text_raw {*
|
|
|
154 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
155 |
\mode<presentation>{
|
|
|
156 |
\begin{frame}<1-3>[c]
|
|
|
157 |
\frametitle{HOL vs.~Nominal}
|
|
|
158 |
|
|
|
159 |
\begin{itemize}
|
|
|
160 |
\item Nominal logic / nominal sets by Pitts are incompatible
|
|
|
161 |
with choice principles\medskip
|
|
|
162 |
|
|
|
163 |
\item HOL includes Hilbert's epsilon\pause\bigskip
|
|
|
164 |
|
|
|
165 |
\item Solution: Do not require that everything has finite support\medskip
|
|
|
166 |
|
|
|
167 |
\begin{center}
|
|
|
168 |
\smath{\onslide<1-2>{\text{finite}(\text{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x}
|
|
|
169 |
\end{center}
|
|
|
170 |
\end{itemize}
|
|
|
171 |
|
|
|
172 |
\end{frame}}
|
|
|
173 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
174 |
*}
|
|
|
175 |
|
|
|
176 |
text_raw {*
|
|
|
177 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
178 |
\mode<presentation>{
|
|
|
179 |
\begin{frame}[c]
|
|
|
180 |
\frametitle{}
|
|
|
181 |
|
|
|
182 |
\begin{tabular}{c@ {\hspace{2mm}}c}
|
|
|
183 |
\\[6mm]
|
|
|
184 |
\begin{tabular}{c}
|
|
|
185 |
\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
|
|
|
186 |
{\footnotesize Bob Harper}\\[-2.5mm]
|
|
|
187 |
{\footnotesize (CMU)}
|
|
|
188 |
\end{tabular}
|
|
|
189 |
\begin{tabular}{c}
|
|
|
190 |
\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
|
|
|
191 |
{\footnotesize Frank Pfenning}\\[-2.5mm]
|
|
|
192 |
{\footnotesize (CMU)}
|
|
|
193 |
\end{tabular} &
|
|
|
194 |
|
|
|
195 |
\begin{tabular}{p{6cm}}
|
|
|
196 |
\raggedright
|
|
|
197 |
\color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
|
|
|
198 |
$\sim$31pp}
|
|
|
199 |
\end{tabular}\\
|
|
|
200 |
|
|
|
201 |
\pause
|
|
|
202 |
\\[0mm]
|
|
|
203 |
|
|
|
204 |
\begin{tabular}{c}
|
|
|
205 |
\includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
|
|
|
206 |
{\footnotesize Andrew Appel}\\[-2.5mm]
|
|
|
207 |
{\footnotesize (Princeton)}
|
|
|
208 |
\end{tabular} &
|
|
|
209 |
|
|
|
210 |
\begin{tabular}{p{6cm}}
|
|
|
211 |
\raggedright
|
|
|
212 |
\color{gray}{relied on their proof in a\\ {\bf security} critical application}
|
|
|
213 |
\end{tabular}
|
|
|
214 |
\end{tabular}\medskip\pause
|
|
|
215 |
|
|
|
216 |
\small
|
|
|
217 |
\begin{minipage}{1.0\textwidth}
|
|
|
218 |
(I also found an {\bf error} in my Ph.D.-thesis about cut-elimination
|
|
|
219 |
examined by Henk Barendregt and Andy Pitts.)
|
|
|
220 |
\end{minipage}
|
|
|
221 |
|
|
|
222 |
\end{frame}}
|
|
|
223 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
224 |
*}
|
|
|
225 |
|
|
|
226 |
|
|
|
227 |
|
|
|
228 |
text_raw {*
|
|
|
229 |
|
|
|
230 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
231 |
\mode<presentation>{
|
|
|
232 |
\begin{frame}<1,2,3,4>[squeeze]
|
|
|
233 |
\frametitle{Formalisation of LF}
|
|
|
234 |
|
|
|
235 |
|
|
|
236 |
\begin{center}
|
|
|
237 |
\begin{tabular}{@ {\hspace{-16mm}}lc}
|
|
|
238 |
\mbox{}\\[-6mm]
|
|
|
239 |
|
|
|
240 |
\textcolor{white}{\raisebox{4mm}{1.~Solution}} &
|
|
|
241 |
\begin{tikzpicture}
|
|
|
242 |
[node distance=25mm,
|
|
|
243 |
text height=1.5ex,
|
|
|
244 |
text depth=.25ex,
|
|
|
245 |
node1/.style={
|
|
|
246 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
247 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
248 |
]
|
|
|
249 |
|
|
|
250 |
\node (proof) [node1] {\large Proof};
|
|
|
251 |
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
|
|
|
252 |
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
|
|
|
253 |
|
|
|
254 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
255 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
256 |
|
|
|
257 |
\onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);}
|
|
|
258 |
\end{tikzpicture}
|
|
|
259 |
\\[2mm]
|
|
|
260 |
|
|
|
261 |
\onslide<3->{%
|
|
|
262 |
\raisebox{4mm}{\textcolor{white}{1st Solution}} &
|
|
|
263 |
\begin{tikzpicture}
|
|
|
264 |
[node distance=25mm,
|
|
|
265 |
text height=1.5ex,
|
|
|
266 |
text depth=.25ex,
|
|
|
267 |
node1/.style={
|
|
|
268 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
269 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
270 |
node2/.style={
|
|
|
271 |
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
|
|
272 |
draw=red!70, top color=white, bottom color=red!50!black!20}
|
|
|
273 |
]
|
|
|
274 |
|
|
|
275 |
\node (proof) [node1] {\large Proof};
|
|
|
276 |
\node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$};
|
|
|
277 |
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
|
|
|
278 |
|
|
|
279 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
280 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
281 |
|
|
|
282 |
\end{tikzpicture}
|
|
|
283 |
\\[2mm]}
|
|
|
284 |
|
|
|
285 |
\end{tabular}
|
|
|
286 |
\end{center}
|
|
|
287 |
|
|
|
288 |
\begin{textblock}{3}(13.2,5.1)
|
|
|
289 |
\onslide<3->{
|
|
|
290 |
\begin{tikzpicture}
|
|
|
291 |
\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
|
|
|
292 |
\end{tikzpicture}
|
|
|
293 |
}
|
|
|
294 |
\end{textblock}
|
|
|
295 |
|
|
|
296 |
|
|
|
297 |
\begin{textblock}{11}(1.4,14.3)
|
|
|
298 |
\only<1->{\footnotesize (one needs to check $\sim$31pp~of informal paper proofs from
|
|
|
299 |
ACM Transactions on Computational Logic, 2005)}
|
|
|
300 |
\end{textblock}
|
|
|
301 |
|
|
|
302 |
\only<4->{
|
|
|
303 |
\begin{textblock}{9}(10,11.5)
|
|
|
304 |
\begin{tikzpicture}[remember picture, overlay]
|
|
|
305 |
\draw (0,0) node[fill=cream, text width=5.3cm, thick, draw=red, rounded corners=1mm] (n2)
|
|
|
306 |
{\raggedright I also found \mbox{(fixable)} mistakes in my Ph.D.~thesis.
|
|
|
307 |
};
|
|
|
308 |
\end{tikzpicture}
|
|
|
309 |
\end{textblock}}
|
|
|
310 |
|
|
|
311 |
\end{frame}}
|
|
|
312 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
313 |
|
|
|
314 |
*}
|
|
|
315 |
|
|
|
316 |
text_raw {*
|
|
|
317 |
|
|
|
318 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
319 |
\mode<presentation>{
|
|
|
320 |
\begin{frame}[c]
|
|
|
321 |
\frametitle{\LARGE\begin{tabular}{c}Nominal Isabelle\end{tabular}}
|
|
|
322 |
|
|
|
323 |
|
|
|
324 |
\begin{itemize}
|
|
|
325 |
\item \ldots{}is a tool on top of the theorem prover
|
|
|
326 |
Isabelle; bound variables have names (no de Bruijn
|
|
|
327 |
indices).\medskip
|
|
|
328 |
|
|
|
329 |
\item It can be used to, for example, represent lambda terms
|
|
|
330 |
|
|
|
331 |
\begin{center}
|
|
|
332 |
\smath{M ::= x\;\mid\; M\,N \;\mid\; \lambda x.M}
|
|
|
333 |
\end{center}
|
|
|
334 |
\end{itemize}
|
|
|
335 |
|
|
|
336 |
\end{frame}}
|
|
|
337 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
338 |
|
|
|
339 |
*}
|
|
|
340 |
|
|
|
341 |
text_raw {*
|
|
|
342 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
343 |
\mode<presentation>{
|
|
|
344 |
\begin{frame}
|
|
|
345 |
\small
|
|
|
346 |
\begin{beamercolorbox}[sep=1mm, wd=11cm]{boxcolor}
|
|
|
347 |
{\bf Substitution Lemma:}
|
|
|
348 |
If \smath{x\not\equiv y} and
|
|
|
349 |
\smath{x\not\in \text{fv}(L)}, then\\
|
|
|
350 |
\mbox{}\hspace{5mm}\smath{M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]}
|
|
|
351 |
\end{beamercolorbox}
|
|
|
352 |
|
|
|
353 |
{\bf Proof:} \alert<4>{By induction on the structure of \smath{M}.}
|
|
|
354 |
\begin{itemize}
|
|
|
355 |
\item {\bf Case 1:} \smath{M} is a variable.
|
|
|
356 |
|
|
|
357 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}p{9cm}@ {}}
|
|
|
358 |
Case 1.1. & \smath{M\equiv x}. Then both sides \alert<3,4>{equal}
|
|
|
359 |
\smath{N[y:=L]} since \smath{x\not\equiv y}.\\[1mm]
|
|
|
360 |
Case 1.2. & \smath{M\equiv y}. Then both sides \alert<3,4>{equal}
|
|
|
361 |
\smath{L}, for \smath{x\not\in \text{fv}(L)}\\
|
|
|
362 |
& implies \smath{L[x:=\ldots]\equiv L}.\\[1mm]
|
|
|
363 |
Case 1.3. & \smath{M\equiv z\not\equiv x,y}. Then both sides \alert<3,4>{equal} \smath{z}.\\[1mm]
|
|
|
364 |
\end{tabular}
|
|
|
365 |
|
|
|
366 |
\item {\bf Case 2:} \smath{M\equiv \lambda z.M_1}.
|
|
|
367 |
\alert<2>{By the variable convention we may assume that \smath{z\not\equiv x,y}
|
|
|
368 |
and \smath{z} is not free in \smath{N,L}.}
|
|
|
369 |
|
|
|
370 |
\begin{tabular}{@ {}r@ {\hspace{1mm}}l@ {}}
|
|
|
371 |
\smath{(\lambda z.M_1)[x\!:=\!N][y\!:=\!L]}
|
|
|
372 |
\smath{\equiv} & \smath{\lambda z.(M_1[x\!:=\!N][y\!:=\!L])}\\
|
|
|
373 |
\smath{\equiv} & \smath{\lambda z.(M_1[y\!:=\!L][x\!:=\!N[y\!:=\!L]])}\\
|
|
|
374 |
\smath{\equiv} & \smath{(\lambda z.M_1)[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}.\\
|
|
|
375 |
\end{tabular}
|
|
|
376 |
|
|
|
377 |
\item {\bf Case 3:} \smath{M\equiv M_1 M_2}.
|
|
|
378 |
The statement follows again from the induction hypothesis. \hfill$\,\Box\,$
|
|
|
379 |
\end{itemize}
|
|
|
380 |
|
|
|
381 |
\begin{textblock}{11}(4,3)
|
|
|
382 |
\begin{block}<5>{}
|
|
|
383 |
Remember only if \smath{y\not=x} and \smath{x\not\in \text{fv}(N)} then\\[2mm]
|
|
|
384 |
\smath{\quad(\lambda y.M)[x:=N]=\lambda y.(M[x:=N])}\\[4mm]
|
|
|
385 |
|
|
|
386 |
\begin{tabular}{c@ {\hspace{2mm}}l@ {\hspace{2mm}}l@ {}}
|
|
|
387 |
& \smath{(\lambda z.M_1)[x:=N][y:=L]}\\[1.3mm]
|
|
|
388 |
\smath{\equiv} & \smath{(\lambda z.(M_1[x:=N]))[y:=L]} & $\stackrel{1}{\leftarrow}$\\[1.3mm]
|
|
|
389 |
\smath{\equiv} & \smath{\lambda z.(M_1[x:=N][y:=L])} & $\stackrel{2}{\leftarrow}$\\[1.3mm]
|
|
|
390 |
\smath{\equiv} & \smath{\lambda z.(M_1[y:=L][x:=N[y:=L]])} & IH\\[1.3mm]
|
|
|
391 |
\smath{\equiv} & \smath{(\lambda z.(M_1[y:=L]))[x:=N[y:=L]])}
|
|
|
392 |
& $\stackrel{2}{\rightarrow}$ \alert{\bf\;!}\\[1.3mm]
|
|
|
393 |
\smath{\equiv} & \smath{(\lambda z.M_1)[y:=L][x:=N[y:=L]]}. &
|
|
|
394 |
$\stackrel{1}{\rightarrow}$\\[1.3mm]
|
|
|
395 |
\end{tabular}
|
|
|
396 |
\end{block}
|
|
|
397 |
\end{textblock}
|
|
|
398 |
|
|
|
399 |
\end{frame}}
|
|
|
400 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
401 |
*}
|
|
|
402 |
|
|
|
403 |
text_raw {*
|
|
|
404 |
|
|
|
405 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
406 |
\mode<presentation>{
|
|
|
407 |
\begin{frame}
|
|
|
408 |
\frametitle{Nominal Isabelle}
|
|
|
409 |
|
|
|
410 |
\begin{itemize}
|
|
|
411 |
\item Define lambda-terms as:
|
|
|
412 |
\end{itemize}
|
|
|
413 |
*}
|
|
|
414 |
|
|
|
415 |
atom_decl name text_raw {*\medskip\isanewline *}
|
|
|
416 |
nominal_datatype lam =
|
|
|
417 |
Var "name"
|
|
|
418 |
| App "lam" "lam"
|
|
|
419 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam _._")
|
|
|
420 |
|
|
|
421 |
|
|
|
422 |
text_raw {*
|
|
|
423 |
\mbox{}\bigskip
|
|
|
424 |
|
|
|
425 |
\begin{itemize}
|
|
|
426 |
\item These are \underline{\bf named} alpha-equivalence classes, for example
|
|
|
427 |
\end{itemize}
|
|
|
428 |
|
|
|
429 |
\begin{center}
|
|
|
430 |
\gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}
|
|
|
431 |
\end{center}
|
|
|
432 |
|
|
|
433 |
\end{frame}}
|
|
|
434 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
435 |
|
|
|
436 |
*}
|
|
|
437 |
|
|
|
438 |
(*<*)
|
|
|
439 |
|
|
|
440 |
nominal_primrec
|
|
|
441 |
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
|
|
|
442 |
where
|
|
|
443 |
"(Var x)[y::=s] = (if x=y then s else (Var x))"
|
|
|
444 |
| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
|
|
|
445 |
| "x\<sharp>(y,s) \<Longrightarrow> (SlidesA.Lam x t)[y::=s] = SlidesA.Lam x (t[y::=s])"
|
|
|
446 |
apply(finite_guess)+
|
|
|
447 |
apply(rule TrueI)+
|
|
|
448 |
apply(simp add: abs_fresh)+
|
|
|
449 |
apply(fresh_guess)+
|
|
|
450 |
done
|
|
|
451 |
|
|
|
452 |
(*>*)
|
|
|
453 |
|
|
|
454 |
text_raw {*
|
|
|
455 |
|
|
|
456 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
457 |
\mode<presentation>{
|
|
|
458 |
\begin{frame}
|
|
|
459 |
%%\frametitle{\large Formal Proof of the Substitution Lemma}
|
|
|
460 |
|
|
|
461 |
\small
|
|
|
462 |
\begin{tabular}{@ {\hspace{-4mm}}c @ {}}
|
|
|
463 |
\begin{minipage}{1.1\textwidth}
|
|
|
464 |
*}
|
|
|
465 |
|
|
|
466 |
lemma forget:
|
|
|
467 |
assumes a: "x \<sharp> L"
|
|
|
468 |
shows "L[x::=P] = L"
|
|
|
469 |
using a by (nominal_induct L avoiding: x P rule: lam.strong_induct)
|
|
|
470 |
(auto simp add: abs_fresh fresh_atm)
|
|
|
471 |
|
|
|
472 |
lemma fresh_fact:
|
|
|
473 |
fixes z::"name"
|
|
|
474 |
assumes a: "z \<sharp> N" "z \<sharp> L"
|
|
|
475 |
shows "z \<sharp> N[y::=L]"
|
|
|
476 |
using a by (nominal_induct N avoiding: z y L rule: lam.strong_induct)
|
|
|
477 |
(auto simp add: abs_fresh fresh_atm)
|
|
|
478 |
|
|
|
479 |
lemma substitution_lemma:
|
|
|
480 |
assumes a: "x \<noteq> y" "x \<sharp> L" -- {* \mbox{}\hspace{-2mm}\tikz[remember picture] \node (n1) {}; *}
|
|
|
481 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
|
|
|
482 |
using a
|
|
|
483 |
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
|
|
|
484 |
(auto simp add: fresh_fact forget)
|
|
|
485 |
|
|
|
486 |
text_raw {*
|
|
|
487 |
\end{minipage}
|
|
|
488 |
\end{tabular}
|
|
|
489 |
|
|
|
490 |
\begin{textblock}{6}(11,9)
|
|
|
491 |
\only<2>{
|
|
|
492 |
\begin{tikzpicture}[remember picture, overlay]
|
|
|
493 |
\draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (n2)
|
|
|
494 |
{\setlength\leftmargini{6mm}%
|
|
|
495 |
\begin{itemize}
|
|
|
496 |
\item stands for \smath{x\not\in \text{fv}(L)}\\[-2mm]
|
|
|
497 |
\item reads as ``\smath{x} fresh for \smath{L}''
|
|
|
498 |
\end{itemize}
|
|
|
499 |
};
|
|
|
500 |
|
|
|
501 |
\path[overlay, ->, very thick, red] (n2) edge[out=-90, in=0] (n1);
|
|
|
502 |
\end{tikzpicture}}
|
|
|
503 |
\end{textblock}
|
|
|
504 |
|
|
|
505 |
\only<1-3>{}
|
|
|
506 |
\end{frame}}
|
|
|
507 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
508 |
|
|
|
509 |
*}
|
|
|
510 |
|
|
|
511 |
text_raw {*
|
|
|
512 |
|
|
|
513 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
514 |
\mode<presentation>{
|
|
|
515 |
\begin{frame}
|
|
|
516 |
\frametitle{\LARGE (Weak) Induction Principles}
|
|
|
517 |
|
|
|
518 |
\begin{itemize}
|
|
|
519 |
\item The usual induction principle for lambda-terms is as follows:
|
|
|
520 |
|
|
|
521 |
\begin{center}
|
|
|
522 |
\mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}
|
|
|
523 |
\centering\smath{%
|
|
|
524 |
\infer{P\,t}
|
|
|
525 |
{\begin{array}{l}
|
|
|
526 |
\forall x.\;P\,x\\[2mm]
|
|
|
527 |
\forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]
|
|
|
528 |
\forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\
|
|
|
529 |
\end{array}
|
|
|
530 |
}}
|
|
|
531 |
\end{beamercolorbox}
|
|
|
532 |
\end{center}
|
|
|
533 |
|
|
|
534 |
\item It requires us in the lambda-case to show the property \smath{P} for
|
|
|
535 |
all binders \smath{x}.\smallskip\\
|
|
|
536 |
|
|
|
537 |
(This nearly always requires renamings and they can be
|
|
|
538 |
tricky to automate.)
|
|
|
539 |
\end{itemize}
|
|
|
540 |
|
|
|
541 |
\end{frame}}
|
|
|
542 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
543 |
|
|
|
544 |
*}
|
|
|
545 |
|
|
|
546 |
|
|
|
547 |
text_raw {*
|
|
|
548 |
|
|
|
549 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
550 |
\mode<presentation>{
|
|
|
551 |
\begin{frame}
|
|
|
552 |
\frametitle{\LARGE Strong Induction Principles}
|
|
|
553 |
|
|
|
554 |
\begin{itemize}
|
|
|
555 |
\item Therefore we will use the following strong induction principle:
|
|
|
556 |
|
|
|
557 |
\begin{center}
|
|
|
558 |
\mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
|
|
|
559 |
\centering\smath{%
|
|
|
560 |
\infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%
|
|
|
561 |
\tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%
|
|
|
562 |
\tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}
|
|
|
563 |
{\begin{array}{l}
|
|
|
564 |
\forall x\,c.\;P\,c\;x\\[2mm]
|
|
|
565 |
\forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
|
|
|
566 |
\Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
|
|
|
567 |
\forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}}
|
|
|
568 |
\wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
|
|
|
569 |
\end{array}
|
|
|
570 |
}}
|
|
|
571 |
\end{beamercolorbox}
|
|
|
572 |
\end{center}
|
|
|
573 |
\end{itemize}
|
|
|
574 |
|
|
|
575 |
\begin{textblock}{11}(0.9,10.9)
|
|
|
576 |
\only<2>{
|
|
|
577 |
\begin{tikzpicture}[remember picture]
|
|
|
578 |
\draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)
|
|
|
579 |
{ The variable over which the induction proceeds:\\[2mm]
|
|
|
580 |
\hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};
|
|
|
581 |
|
|
|
582 |
\path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);
|
|
|
583 |
\end{tikzpicture}}
|
|
|
584 |
|
|
|
585 |
\only<3>{
|
|
|
586 |
\begin{tikzpicture}[remember picture]
|
|
|
587 |
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)
|
|
|
588 |
{The {\bf context} of the induction; i.e.~what the binder should be fresh for
|
|
|
589 |
$\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]
|
|
|
590 |
``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}}
|
|
|
591 |
and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};
|
|
|
592 |
|
|
|
593 |
\path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);
|
|
|
594 |
\end{tikzpicture}}
|
|
|
595 |
|
|
|
596 |
\only<4>{
|
|
|
597 |
\begin{tikzpicture}[remember picture]
|
|
|
598 |
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)
|
|
|
599 |
{The property to be proved by induction:\\[-3mm]
|
|
|
600 |
\begin{center}\small
|
|
|
601 |
\begin{tabular}{l}
|
|
|
602 |
\smath{\!\!\lambda
|
|
|
603 |
(x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]
|
|
|
604 |
\hspace{8mm}
|
|
|
605 |
\smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}
|
|
|
606 |
\end{tabular}
|
|
|
607 |
\end{center}};
|
|
|
608 |
|
|
|
609 |
\path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);
|
|
|
610 |
\end{tikzpicture}}
|
|
|
611 |
\end{textblock}
|
|
|
612 |
|
|
|
613 |
\end{frame}}
|
|
|
614 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
615 |
|
|
|
616 |
*}
|
|
|
617 |
|
|
|
618 |
|
|
|
619 |
text_raw {*
|
|
|
620 |
|
|
|
621 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
622 |
\mode<presentation>{
|
|
|
623 |
\begin{frame}
|
|
|
624 |
\frametitle{\LARGE Strong Induction Principles}
|
|
|
625 |
|
|
|
626 |
\begin{center}
|
|
|
627 |
\mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
|
|
|
628 |
\centering\smath{%
|
|
|
629 |
\infer{P\,\alert{c}\;t}
|
|
|
630 |
{\begin{array}{l}
|
|
|
631 |
\forall x\,c.\;P\,c\;x\\[2mm]
|
|
|
632 |
\forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
|
|
|
633 |
\Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
|
|
|
634 |
\forall x\,t\,c.\;x\fresh c \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
|
|
|
635 |
\end{array}
|
|
|
636 |
}}
|
|
|
637 |
\end{beamercolorbox}
|
|
|
638 |
\end{center}
|
|
|
639 |
|
|
|
640 |
|
|
|
641 |
\only<1>{
|
|
|
642 |
\begin{textblock}{14}(1.2,9.2)
|
|
|
643 |
\begin{itemize}
|
|
|
644 |
\item There is a condition for when Barendregt's variable convention
|
|
|
645 |
is applicable---it is almost always satisfied, but not always:\\[2mm]
|
|
|
646 |
|
|
|
647 |
The induction context \smath{c} needs to be finitely supported
|
|
|
648 |
(is not allowed to mention all names as free).
|
|
|
649 |
\end{itemize}
|
|
|
650 |
\end{textblock}}
|
|
|
651 |
|
|
|
652 |
\only<2>{
|
|
|
653 |
\begin{itemize}
|
|
|
654 |
\item In the case of the substitution lemma:\\[2mm]
|
|
|
655 |
|
|
|
656 |
\begin{textblock}{16.5}(0.7,11.5)
|
|
|
657 |
\small
|
|
|
658 |
*}
|
|
|
659 |
|
|
|
660 |
(*<*)
|
|
|
661 |
lemma
|
|
|
662 |
assumes a: "x\<noteq>y" "x \<sharp> L"
|
|
|
663 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
|
|
|
664 |
using a
|
|
|
665 |
(*>*)
|
|
|
666 |
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
|
|
|
667 |
txt_raw {* \isanewline$\ldots$ *}
|
|
|
668 |
(*<*)oops(*>*)
|
|
|
669 |
|
|
|
670 |
text_raw {*
|
|
|
671 |
\end{textblock}
|
|
|
672 |
\end{itemize}}
|
|
|
673 |
|
|
|
674 |
\end{frame}}
|
|
|
675 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
676 |
|
|
|
677 |
*}
|
|
|
678 |
|
|
|
679 |
|
|
|
680 |
text_raw {*
|
|
|
681 |
|
|
|
682 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
683 |
\mode<presentation>{
|
|
|
684 |
\begin{frame}
|
|
|
685 |
\frametitle{\Large \mbox{Same Problem with Rule Inductions}}
|
|
|
686 |
|
|
|
687 |
\begin{itemize}
|
|
|
688 |
\item We can specify typing-rules for lambda-terms as:
|
|
|
689 |
|
|
|
690 |
\begin{center}
|
|
|
691 |
\begin{tabular}{@ {\hspace{-6mm}}c@ {}}
|
|
|
692 |
\colorbox{cream}{
|
|
|
693 |
\smath{\infer{\Gamma\vdash x:\tau}{(x\!:\!\tau)\in\Gamma\;\;\text{valid}\;\Gamma}}}
|
|
|
694 |
\;\;
|
|
|
695 |
\colorbox{cream}{
|
|
|
696 |
\smath{\infer{\Gamma\vdash t_1\;t_2:\tau}
|
|
|
697 |
{\Gamma\vdash t_1:\sigma\!\rightarrow\!\tau & \Gamma\vdash t_2:\sigma}}}\\[4mm]
|
|
|
698 |
|
|
|
699 |
\colorbox{cream}{
|
|
|
700 |
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
|
|
|
701 |
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}\\[6mm]
|
|
|
702 |
|
|
|
703 |
\colorbox{cream}{
|
|
|
704 |
\smath{\infer{\text{valid}\;[]}{}}}
|
|
|
705 |
\;\;\;\;
|
|
|
706 |
\colorbox{cream}{
|
|
|
707 |
\smath{\infer{\text{valid}\;(x\!:\!\tau)\!::\!\Gamma}{x\fresh\Gamma & \text{valid}\;\Gamma}}}\\[8mm]
|
|
|
708 |
\end{tabular}
|
|
|
709 |
\end{center}
|
|
|
710 |
|
|
|
711 |
\item If \smath{\Gamma_1\vdash t:\tau} and \smath{\text{valid}\;\Gamma_2},
|
|
|
712 |
\smath{\Gamma_1\subseteq \Gamma_2} then \smath{\Gamma_2\vdash t:\tau}.$\!\!\!\!\!$
|
|
|
713 |
|
|
|
714 |
\end{itemize}
|
|
|
715 |
|
|
|
716 |
|
|
|
717 |
\begin{textblock}{11}(1.3,4)
|
|
|
718 |
\only<2>{
|
|
|
719 |
\begin{tikzpicture}
|
|
|
720 |
\draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (nn)
|
|
|
721 |
{The proof of the weakening lemma is said to be trivial / obvious / routine
|
|
|
722 |
/\ldots{} in many places.\\[2mm]
|
|
|
723 |
|
|
|
724 |
(I am actually still looking for a place in the literature where a
|
|
|
725 |
trivial / obvious / routine /\ldots{} proof is spelled out --- I know of
|
|
|
726 |
proofs by Gallier, McKinna \& Pollack and Pitts, but I would not
|
|
|
727 |
call them trivial / obvious / routine /\ldots)};
|
|
|
728 |
\end{tikzpicture}}
|
|
|
729 |
\end{textblock}
|
|
|
730 |
|
|
|
731 |
\end{frame}}
|
|
|
732 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
733 |
*}
|
|
|
734 |
|
|
|
735 |
text_raw {*
|
|
|
736 |
|
|
|
737 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
738 |
\mode<presentation>{
|
|
|
739 |
\begin{frame}[c]
|
|
|
740 |
\frametitle{Recall: Rule Inductions}
|
|
|
741 |
|
|
|
742 |
\begin{center}\large
|
|
|
743 |
\colorbox{cream}{
|
|
|
744 |
\smath{\infer[\text{rule}]{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}}
|
|
|
745 |
\end{center}\bigskip
|
|
|
746 |
|
|
|
747 |
\begin{tabular}[t]{l}
|
|
|
748 |
Rule Inductions:\\[1mm]
|
|
|
749 |
\begin{tabular}{l@ {\hspace{2mm}}p{8.4cm}}
|
|
|
750 |
1.) & Assume the property for the premises. Assume the side-conditions.\\[1mm]
|
|
|
751 |
2.) & Show the property for the conclusion.\\
|
|
|
752 |
\end{tabular}
|
|
|
753 |
\end{tabular}
|
|
|
754 |
|
|
|
755 |
\end{frame}}
|
|
|
756 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
757 |
|
|
|
758 |
*}
|
|
|
759 |
|
|
|
760 |
text_raw {*
|
|
|
761 |
|
|
|
762 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
763 |
\mode<presentation>{
|
|
|
764 |
\begin{frame}
|
|
|
765 |
\frametitle{\LARGE\mbox{Induction Principle for Typing}}
|
|
|
766 |
|
|
|
767 |
\begin{itemize}
|
|
|
768 |
\item The induction principle that comes with the typing definition is as follows:\\[-13mm]
|
|
|
769 |
\mbox{}
|
|
|
770 |
\end{itemize}
|
|
|
771 |
|
|
|
772 |
\begin{center}
|
|
|
773 |
\begin{tabular}{@ {\hspace{-5mm}}c@ {}}
|
|
|
774 |
\colorbox{cream}{
|
|
|
775 |
\smath{
|
|
|
776 |
\infer{\Gamma\vdash t:\tau \Rightarrow P\,\Gamma\,t\,\tau}
|
|
|
777 |
{\begin{array}{l}
|
|
|
778 |
\forall \Gamma\,x\,\tau.\,\;(x\!:\!\tau)\in\Gamma\wedge
|
|
|
779 |
\text{valid}\,\Gamma\Rightarrow P\,\Gamma\,(x)\,\tau\\[4mm]
|
|
|
780 |
\forall \Gamma\,t_1\,t_2\,\sigma\,\tau.\\
|
|
|
781 |
P\,\Gamma\,t_1\,(\sigma\!\rightarrow\!\tau)\wedge
|
|
|
782 |
P\,\Gamma\,t_2\,\sigma
|
|
|
783 |
\Rightarrow P\,\Gamma\,(t_1\,t_2)\,\tau\\[4mm]
|
|
|
784 |
\forall \Gamma\,x\,t\,\sigma\,\tau.\\
|
|
|
785 |
x\fresh\Gamma\wedge
|
|
|
786 |
P\,((x\!:\!\sigma)\!::\!\Gamma)\,t\,\tau
|
|
|
787 |
\Rightarrow P\,\Gamma (\lambda x.t)\,(\sigma\!\rightarrow\!\tau)\\[2mm]
|
|
|
788 |
\end{array}
|
|
|
789 |
}
|
|
|
790 |
}}
|
|
|
791 |
\end{tabular}
|
|
|
792 |
\end{center}
|
|
|
793 |
|
|
|
794 |
\begin{textblock}{4}(9,13.8)
|
|
|
795 |
\begin{tikzpicture}
|
|
|
796 |
\draw (0,0) node[fill=cream, text width=3.9cm, thick, draw=red, rounded corners=1mm] (nn)
|
|
|
797 |
{\small Note the quantifiers!};
|
|
|
798 |
\end{tikzpicture}
|
|
|
799 |
\end{textblock}
|
|
|
800 |
|
|
|
801 |
\end{frame}}
|
|
|
802 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
803 |
|
|
|
804 |
*}
|
|
|
805 |
|
|
|
806 |
text_raw {*
|
|
|
807 |
|
|
|
808 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
809 |
\mode<presentation>{
|
|
|
810 |
\begin{frame}
|
|
|
811 |
\frametitle{\LARGE \mbox{Proof of Weakening Lemma}}
|
|
|
812 |
\mbox{}\\[-18mm]\mbox{}
|
|
|
813 |
|
|
|
814 |
\begin{center}
|
|
|
815 |
\colorbox{cream}{
|
|
|
816 |
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
|
|
|
817 |
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}
|
|
|
818 |
\end{center}
|
|
|
819 |
|
|
|
820 |
\begin{minipage}{1.1\textwidth}
|
|
|
821 |
\begin{itemize}
|
|
|
822 |
\item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then
|
|
|
823 |
\smath{\alert<1>{\forall \Gamma_2}.\,\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!
|
|
|
824 |
\Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}
|
|
|
825 |
\end{itemize}
|
|
|
826 |
|
|
|
827 |
\pause
|
|
|
828 |
|
|
|
829 |
\mbox{}\hspace{-5mm}
|
|
|
830 |
\underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:
|
|
|
831 |
|
|
|
832 |
\begin{itemize}
|
|
|
833 |
\item We know:\\
|
|
|
834 |
\smath{\forall \alert<4->{\Gamma_2}.\,\text{valid}\,\alert<4->{\Gamma_2} \wedge
|
|
|
835 |
(x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \alert<4->{\Gamma_2} \Rightarrow \!\!
|
|
|
836 |
\tikz[remember picture, baseline=(ea.base)]
|
|
|
837 |
\node (ea) {\smath{\alert<4->{\Gamma_2}}};\!\vdash\! t\!:\!\tau}\\
|
|
|
838 |
\smath{x\fresh\Gamma_1}\\
|
|
|
839 |
\onslide<3->{\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2
|
|
|
840 |
\only<6->{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\!
|
|
|
841 |
(x\!:\!\sigma)\!::\!\Gamma_2}}}\\
|
|
|
842 |
\onslide<3->{\smath{\textcolor{white}{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2
|
|
|
843 |
\Rightarrow} \only<7->{\;\alert{\text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2\;\;\text{\bf ???}}}}}
|
|
|
844 |
|
|
|
845 |
\item We have to show:\\
|
|
|
846 |
\only<2>{
|
|
|
847 |
\smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge
|
|
|
848 |
\Gamma_1\!\subseteq\!\Gamma_2 \Rightarrow \Gamma_2\!\vdash\!
|
|
|
849 |
\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}
|
|
|
850 |
\only<3->{
|
|
|
851 |
\smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}
|
|
|
852 |
|
|
|
853 |
\end{itemize}
|
|
|
854 |
\end{minipage}
|
|
|
855 |
|
|
|
856 |
\begin{textblock}{4}(10,6.5)
|
|
|
857 |
\only<5->{
|
|
|
858 |
\begin{tikzpicture}[remember picture]
|
|
|
859 |
\draw (0,0) node[fill=cream, text width=4cm, thick, draw=red, rounded corners=1mm] (eb)
|
|
|
860 |
{\smath{\Gamma_2\mapsto (x\!:\!\sigma)\!::\!\Gamma_2}};
|
|
|
861 |
|
|
|
862 |
\path[overlay, ->, ultra thick, red] (eb) edge[out=-90, in=80] (ea);
|
|
|
863 |
\end{tikzpicture}}
|
|
|
864 |
\end{textblock}
|
|
|
865 |
|
|
|
866 |
\end{frame}}
|
|
|
867 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
868 |
|
|
|
869 |
*}
|
|
|
870 |
|
|
|
871 |
text_raw {*
|
|
|
872 |
|
|
|
873 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
874 |
\mode<presentation>{
|
|
|
875 |
\begin{frame}
|
|
|
876 |
|
|
|
877 |
\begin{textblock}{14.8}(0.7,0.5)
|
|
|
878 |
\begin{itemize}
|
|
|
879 |
\item The usual proof of strong normalisation for simply- typed lambda-terms
|
|
|
880 |
establishes first:\\[1mm]
|
|
|
881 |
|
|
|
882 |
\colorbox{cream}{%
|
|
|
883 |
\begin{tabular}{@ {}p{11cm}}
|
|
|
884 |
Lemma: If for all reducible \smath{s}, \smath{t[x\!:=\!s]} is reducible, then
|
|
|
885 |
\smath{\lambda x.t} is reducible.
|
|
|
886 |
\end{tabular}}\smallskip
|
|
|
887 |
|
|
|
888 |
\item Then one shows for a closing (simultaneous) substitution:\\[2mm]
|
|
|
889 |
|
|
|
890 |
\colorbox{cream}{%
|
|
|
891 |
\begin{tabular}{@ {}p{11cm}}
|
|
|
892 |
Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing
|
|
|
893 |
substitutions \smath{\theta} containing reducible terms only,
|
|
|
894 |
\smath{\theta(t)} is reducible.
|
|
|
895 |
\end{tabular}}
|
|
|
896 |
|
|
|
897 |
\mbox{}\\[1mm]
|
|
|
898 |
|
|
|
899 |
Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)}
|
|
|
900 |
is reducible with \smath{s} being reducible. This is equal\alert{$^*$} to
|
|
|
901 |
\smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get \smath{\lambda
|
|
|
902 |
x.(\theta(t))} is reducible. Because this is equal\alert{$^*$} to
|
|
|
903 |
\smath{\theta(\lambda x.t)}, we are done.
|
|
|
904 |
\hfill\footnotesize\alert{$^*$}you have to take a deep breath
|
|
|
905 |
\end{itemize}
|
|
|
906 |
\end{textblock}
|
|
|
907 |
|
|
|
908 |
\end{frame}}
|
|
|
909 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
910 |
|
|
|
911 |
*}
|
|
|
912 |
|
|
|
913 |
|
|
|
914 |
text_raw {*
|
|
|
915 |
|
|
|
916 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
917 |
\mode<presentation>{
|
|
|
918 |
\begin{frame}
|
|
|
919 |
\frametitle{\LARGE \mbox{Proof of Weakening Lemma}}
|
|
|
920 |
\mbox{}\\[-18mm]\mbox{}
|
|
|
921 |
|
|
|
922 |
\begin{center}
|
|
|
923 |
\colorbox{cream}{
|
|
|
924 |
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
|
|
|
925 |
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}
|
|
|
926 |
\end{center}
|
|
|
927 |
|
|
|
928 |
\begin{minipage}{1.1\textwidth}
|
|
|
929 |
\begin{itemize}
|
|
|
930 |
\item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then
|
|
|
931 |
\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!
|
|
|
932 |
\Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}
|
|
|
933 |
\end{itemize}
|
|
|
934 |
|
|
|
935 |
\mbox{}\hspace{-5mm}
|
|
|
936 |
\underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:
|
|
|
937 |
|
|
|
938 |
\begin{itemize}
|
|
|
939 |
\item We know:\\
|
|
|
940 |
\smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge
|
|
|
941 |
(x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \Gamma_2 \Rightarrow \!\!
|
|
|
942 |
\Gamma_2\!\vdash\! t\!:\!\tau}\\
|
|
|
943 |
\smath{x\fresh\Gamma_1}\\
|
|
|
944 |
\begin{tabular}{@ {}ll@ {}}
|
|
|
945 |
\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2} &
|
|
|
946 |
\only<2->{\smath{\alert{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\!
|
|
|
947 |
(x\!:\!\sigma)\!::\!\Gamma_2}}}\\
|
|
|
948 |
\smath{\alert{x\fresh\Gamma_2}} &
|
|
|
949 |
\only<2->{\smath{\alert{\Rightarrow \text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2}}}
|
|
|
950 |
\end{tabular}
|
|
|
951 |
|
|
|
952 |
\item We have to show:\\
|
|
|
953 |
\smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}
|
|
|
954 |
|
|
|
955 |
\end{itemize}
|
|
|
956 |
\end{minipage}
|
|
|
957 |
|
|
|
958 |
|
|
|
959 |
\end{frame}}
|
|
|
960 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
961 |
|
|
|
962 |
*}
|
|
|
963 |
|
|
|
964 |
|
|
|
965 |
|
|
|
966 |
text_raw {*
|
|
|
967 |
|
|
|
968 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
969 |
\mode<presentation>{
|
|
|
970 |
\begin{frame}
|
|
|
971 |
\frametitle{SN (Again)}
|
|
|
972 |
\mbox{}\\[-8mm]
|
|
|
973 |
|
|
|
974 |
\colorbox{cream}{%
|
|
|
975 |
\begin{tabular}{@ {}p{10.5cm}}
|
|
|
976 |
Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing
|
|
|
977 |
substitutions \smath{\theta} containing reducible terms only,
|
|
|
978 |
\smath{\theta(t)} is reducible.
|
|
|
979 |
\end{tabular}}\medskip
|
|
|
980 |
|
|
|
981 |
\begin{itemize}
|
|
|
982 |
\item
|
|
|
983 |
Since we say that the strong induction should avoid \smath{\theta}, we
|
|
|
984 |
get the assumption \alert{$x\fresh\theta$} then:\\[2mm]
|
|
|
985 |
|
|
|
986 |
\begin{tabular}{@ {}p{10.5cm}}\raggedright
|
|
|
987 |
Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)} is reducible
|
|
|
988 |
with
|
|
|
989 |
\smath{s} being reducible. This is {\bf equal} to
|
|
|
990 |
\smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get
|
|
|
991 |
\smath{\lambda x.(\theta(t))} is reducible. Because this is {\bf equal} to
|
|
|
992 |
\smath{\theta(\lambda x.t)}, we are done.
|
|
|
993 |
\end{tabular}\smallskip
|
|
|
994 |
|
|
|
995 |
\begin{center}
|
|
|
996 |
\begin{tabular}{rl}
|
|
|
997 |
\smath{x\fresh\theta\Rightarrow} &
|
|
|
998 |
\smath{(x\!\mapsto\! s\cup\theta)(t) \;\alert{=}\;(\theta(t))[x\!:=\!s]}\\[1mm]
|
|
|
999 |
&
|
|
|
1000 |
\smath{\theta(\lambda x.t) \;\alert{=}\; \lambda x.(\theta(t))}
|
|
|
1001 |
\end{tabular}
|
|
|
1002 |
\end{center}
|
|
|
1003 |
\end{itemize}
|
|
|
1004 |
|
|
|
1005 |
\end{frame}}
|
|
|
1006 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1007 |
|
|
|
1008 |
*}
|
|
|
1009 |
|
|
|
1010 |
text_raw {*
|
|
|
1011 |
|
|
|
1012 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1013 |
\mode<presentation>{
|
|
|
1014 |
\begin{frame}
|
|
|
1015 |
\frametitle{So Far So Good}
|
|
|
1016 |
|
|
|
1017 |
\begin{itemize}
|
|
|
1018 |
\item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}
|
|
|
1019 |
\end{itemize}
|
|
|
1020 |
|
|
|
1021 |
\begin{center}
|
|
|
1022 |
\begin{block}{}
|
|
|
1023 |
\color{gray}
|
|
|
1024 |
\small%
|
|
|
1025 |
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm]
|
|
|
1026 |
If $M_1,\ldots,M_n$ occur in a certain mathematical context
|
|
|
1027 |
(e.g. definition, proof), then in these terms all bound variables
|
|
|
1028 |
are chosen to be different from the free variables.\\[2mm]
|
|
|
1029 |
|
|
|
1030 |
\footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
|
|
|
1031 |
\end{block}
|
|
|
1032 |
\end{center}
|
|
|
1033 |
|
|
|
1034 |
\mbox{}\\[-18mm]\mbox{}
|
|
|
1035 |
|
|
|
1036 |
\begin{columns}
|
|
|
1037 |
\begin{column}[t]{4.7cm}
|
|
|
1038 |
Inductive Definitions:\\
|
|
|
1039 |
\begin{center}
|
|
|
1040 |
\smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}
|
|
|
1041 |
\end{center}
|
|
|
1042 |
\end{column}
|
|
|
1043 |
\begin{column}[t]{7cm}
|
|
|
1044 |
Rule Inductions:\\[2mm]
|
|
|
1045 |
\begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}
|
|
|
1046 |
1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]
|
|
|
1047 |
2.) & Show the property for\\ & the conclusion.\\
|
|
|
1048 |
\end{tabular}
|
|
|
1049 |
\end{column}
|
|
|
1050 |
\end{columns}
|
|
|
1051 |
|
|
|
1052 |
\end{frame}}
|
|
|
1053 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1054 |
|
|
|
1055 |
*}
|
|
|
1056 |
|
|
|
1057 |
text_raw {*
|
|
|
1058 |
|
|
|
1059 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1060 |
\mode<presentation>{
|
|
|
1061 |
\setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
|
|
|
1062 |
\begin{frame}[sqeeze]
|
|
|
1063 |
\frametitle{Faulty Reasoning}
|
|
|
1064 |
|
|
|
1065 |
%\mbox{}
|
|
|
1066 |
|
|
|
1067 |
\begin{itemize}
|
|
|
1068 |
\item Consider the two-place relation \smath{\text{foo}}:\medskip
|
|
|
1069 |
\begin{center}
|
|
|
1070 |
\begin{tabular}{ccc}
|
|
|
1071 |
\raisebox{2.5mm}{\colorbox{cream}{%
|
|
|
1072 |
\smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}
|
|
|
1073 |
&
|
|
|
1074 |
\raisebox{2mm}{\colorbox{cream}{%
|
|
|
1075 |
\smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}
|
|
|
1076 |
&
|
|
|
1077 |
\colorbox{cream}{%
|
|
|
1078 |
\smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]
|
|
|
1079 |
\end{tabular}
|
|
|
1080 |
\end{center}
|
|
|
1081 |
|
|
|
1082 |
\pause
|
|
|
1083 |
|
|
|
1084 |
\item The lemma we going to prove:\smallskip
|
|
|
1085 |
\begin{center}
|
|
|
1086 |
Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.
|
|
|
1087 |
\end{center}\bigskip
|
|
|
1088 |
|
|
|
1089 |
\only<3>{
|
|
|
1090 |
\item Cases 1 and 2 are trivial:\medskip
|
|
|
1091 |
\begin{itemize}
|
|
|
1092 |
\item If \smath{y\fresh x} then \smath{y\fresh x}.
|
|
|
1093 |
\item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.
|
|
|
1094 |
\end{itemize}
|
|
|
1095 |
}
|
|
|
1096 |
|
|
|
1097 |
\only<4->{
|
|
|
1098 |
\item Case 3:
|
|
|
1099 |
\begin{itemize}
|
|
|
1100 |
\item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.};
|
|
|
1101 |
We have to show \smath{y\fresh t'}.$\!\!\!\!$
|
|
|
1102 |
\item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.
|
|
|
1103 |
\item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!
|
|
|
1104 |
\end{itemize}
|
|
|
1105 |
}
|
|
|
1106 |
\end{itemize}
|
|
|
1107 |
|
|
|
1108 |
\begin{textblock}{11.3}(0.7,0.6)
|
|
|
1109 |
\only<5-7>{
|
|
|
1110 |
\begin{tikzpicture}
|
|
|
1111 |
\draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)
|
|
|
1112 |
{{\bf Variable Convention:}\\[2mm]
|
|
|
1113 |
\small
|
|
|
1114 |
If $M_1,\ldots,M_n$ occur in a certain mathematical context
|
|
|
1115 |
(e.g. definition, proof), then in these terms all bound variables
|
|
|
1116 |
are chosen to be different from the free variables.\smallskip
|
|
|
1117 |
|
|
|
1118 |
\normalsize
|
|
|
1119 |
{\bf In our case:}\\[2mm]
|
|
|
1120 |
The free variables are \smath{y} and \smath{t'}; the bound one is
|
|
|
1121 |
\smath{x}.\medskip
|
|
|
1122 |
|
|
|
1123 |
By the variable convention we conclude that \smath{x\not= y}.
|
|
|
1124 |
};
|
|
|
1125 |
\end{tikzpicture}}
|
|
|
1126 |
\end{textblock}
|
|
|
1127 |
|
|
|
1128 |
\begin{textblock}{9.2}(3.6,9)
|
|
|
1129 |
\only<6,7>{
|
|
|
1130 |
\begin{tikzpicture}[remember picture]
|
|
|
1131 |
\draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)
|
|
|
1132 |
{\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow
|
|
|
1133 |
y\!\not\in\! \text{fv}(t)\!-\!\{x\}
|
|
|
1134 |
\stackrel{x\not=y}{\Longleftrightarrow}
|
|
|
1135 |
y\!\not\in\! \text{fv}(t)}};
|
|
|
1136 |
|
|
|
1137 |
\path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);
|
|
|
1138 |
\end{tikzpicture}}
|
|
|
1139 |
\end{textblock}
|
|
|
1140 |
|
|
|
1141 |
\end{frame}}
|
|
|
1142 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1143 |
|
|
|
1144 |
*}
|
|
|
1145 |
|
|
|
1146 |
text_raw {*
|
|
|
1147 |
|
|
|
1148 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1149 |
\mode<presentation>{
|
|
|
1150 |
\setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
|
|
|
1151 |
\begin{frame}
|
|
|
1152 |
\frametitle{VC-Compatibility}
|
|
|
1153 |
|
|
|
1154 |
\begin{itemize}
|
|
|
1155 |
\item We introduced two conditions that make the VC safe to use in rule inductions:
|
|
|
1156 |
|
|
|
1157 |
\begin{itemize}
|
|
|
1158 |
\item the relation needs to be \alert{\bf equivariant}, and
|
|
|
1159 |
\item the binder is not allowed to occur in the \alert{\bf support} of
|
|
|
1160 |
the conclusion (not free in the conclusion)\bigskip
|
|
|
1161 |
\end{itemize}
|
|
|
1162 |
|
|
|
1163 |
\item Once a relation satisfies these two conditions, then Nominal
|
|
|
1164 |
Isabelle derives the strong induction principle automatically.
|
|
|
1165 |
\end{itemize}
|
|
|
1166 |
|
|
|
1167 |
\begin{textblock}{11.3}(0.7,6)
|
|
|
1168 |
\only<2>{
|
|
|
1169 |
\begin{tikzpicture}
|
|
|
1170 |
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (nn)
|
|
|
1171 |
{A relation \smath{R} is {\bf equivariant} iff
|
|
|
1172 |
%
|
|
|
1173 |
\begin{center}
|
|
|
1174 |
\smath{%
|
|
|
1175 |
\begin{array}[t]{l}
|
|
|
1176 |
\forall \pi\,t_1\ldots t_n\\[1mm]
|
|
|
1177 |
\;\;\;\;R\,t_1\ldots t_n \Rightarrow R (\pi\act t_1)\ldots(\pi\act t_n)
|
|
|
1178 |
\end{array}}
|
|
|
1179 |
\end{center}
|
|
|
1180 |
%
|
|
|
1181 |
This means the relation has to be invariant under permutative renaming of
|
|
|
1182 |
variables.\smallskip
|
|
|
1183 |
|
|
|
1184 |
\small
|
|
|
1185 |
(This property can be checked automatically if the inductive definition is composed of
|
|
|
1186 |
equivariant ``things''.)
|
|
|
1187 |
};
|
|
|
1188 |
\end{tikzpicture}}
|
|
|
1189 |
\end{textblock}
|
|
|
1190 |
|
|
|
1191 |
\only<3>{}
|
|
|
1192 |
|
|
|
1193 |
\end{frame}}
|
|
|
1194 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1195 |
|
|
|
1196 |
*}
|
|
|
1197 |
|
|
|
1198 |
text_raw {*
|
|
|
1199 |
|
|
|
1200 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1201 |
\mode<presentation>{
|
|
|
1202 |
\begin{frame}
|
|
|
1203 |
\frametitle{\mbox{Honest Toil, No Theft!}}
|
|
|
1204 |
|
|
|
1205 |
\begin{itemize}
|
|
|
1206 |
\item The \underline{sacred} principle of HOL:
|
|
|
1207 |
|
|
|
1208 |
\begin{block}{}
|
|
|
1209 |
``The method of `postulating' what we want has many advantages; they are
|
|
|
1210 |
the same as the advantages of theft over honest toil.''\\[2mm]
|
|
|
1211 |
\hfill{}\footnotesize B.~Russell, Introduction of Mathematical Philosophy
|
|
|
1212 |
\end{block}\bigskip\medskip
|
|
|
1213 |
|
|
|
1214 |
\item I will show next that the \underline{weak} structural induction
|
|
|
1215 |
principle implies the \underline{strong} structural induction principle.\\[3mm]
|
|
|
1216 |
|
|
|
1217 |
\textcolor{gray}{(I am only going to show the lambda-case.)}
|
|
|
1218 |
\end{itemize}
|
|
|
1219 |
|
|
|
1220 |
\end{frame}}
|
|
|
1221 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1222 |
|
|
|
1223 |
*}
|
|
|
1224 |
|
|
|
1225 |
text_raw {*
|
|
|
1226 |
|
|
|
1227 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1228 |
\mode<presentation>{
|
|
|
1229 |
\begin{frame}
|
|
|
1230 |
\frametitle{Permutations}
|
|
|
1231 |
|
|
|
1232 |
A permutation \alert{\bf acts} on variable names as follows:
|
|
|
1233 |
|
|
|
1234 |
\begin{center}
|
|
|
1235 |
\begin{tabular}{rcl}
|
|
|
1236 |
$\smath{{[]}\act a}$ & $\smath{\dn}$ & $\smath{a}$\\
|
|
|
1237 |
$\smath{(\swap{a_1}{a_2}\!::\!\pi)\act a}$ & $\smath{\dn}$ &
|
|
|
1238 |
$\smath{\begin{cases}
|
|
|
1239 |
a_1 &\text{if $\pi\act a = a_2$}\\
|
|
|
1240 |
a_2 &\text{if $\pi\act a = a_1$}\\
|
|
|
1241 |
\pi\act a &\text{otherwise}
|
|
|
1242 |
\end{cases}}$
|
|
|
1243 |
\end{tabular}
|
|
|
1244 |
\end{center}
|
|
|
1245 |
|
|
|
1246 |
\begin{itemize}
|
|
|
1247 |
\item $\smath{[]}$ stands for the empty list (the identity permutation), and\smallskip
|
|
|
1248 |
\item $\smath{\swap{a_1}{a_2}\!::\!\pi}$ stands for the permutation $\smath{\pi}$
|
|
|
1249 |
followed by the swapping $\smath{\swap{a_1}{a_2}}$.
|
|
|
1250 |
\end{itemize}
|
|
|
1251 |
|
|
|
1252 |
\end{frame}}
|
|
|
1253 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1254 |
|
|
|
1255 |
*}
|
|
|
1256 |
|
|
|
1257 |
text_raw {*
|
|
|
1258 |
|
|
|
1259 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1260 |
\mode<presentation>{
|
|
|
1261 |
\begin{frame}
|
|
|
1262 |
\frametitle{\Large\mbox{Permutations on Lambda-Terms}}
|
|
|
1263 |
|
|
|
1264 |
\begin{itemize}
|
|
|
1265 |
\item Permutations act on lambda-terms as follows:
|
|
|
1266 |
|
|
|
1267 |
\begin{center}
|
|
|
1268 |
\begin{tabular}{rcl}
|
|
|
1269 |
$\smath{\pi\act\,x}$ & $\smath{\dn}$ & ``action on variables''\\
|
|
|
1270 |
$\smath{\pi\act\, (t_1~t_2)}$ & $\smath{\dn}$ & $\smath{(\pi\act t_1)~(\pi\act t_2)}$\\
|
|
|
1271 |
$\smath{\pi\act(\lambda x.t)}$ & $\smath{\dn}$ & $\smath{\lambda (\pi\act x).(\pi\act t)}$\\
|
|
|
1272 |
\end{tabular}
|
|
|
1273 |
\end{center}\medskip
|
|
|
1274 |
|
|
|
1275 |
\item Alpha-equivalence can be defined as:
|
|
|
1276 |
|
|
|
1277 |
\begin{center}
|
|
|
1278 |
\begin{tabular}{c}
|
|
|
1279 |
\colorbox{cream}{\smath{\infer{\lambda x.t_1 = \lambda x.t_2}{t_1=t_2}}}\\[3mm]
|
|
|
1280 |
\colorbox{cream}{\smath{\infer{\lambda x.t_1
|
|
|
1281 |
\tikz[baseline=-3pt,remember picture] \node (e1) {\alert<2>{$=$}};
|
|
|
1282 |
\lambda y.t_2}
|
|
|
1283 |
{x\not=y & t_1 = \swap{x}{y}\act t_2 & x\fresh t_2}}}
|
|
|
1284 |
\end{tabular}
|
|
|
1285 |
\end{center}
|
|
|
1286 |
|
|
|
1287 |
\end{itemize}
|
|
|
1288 |
|
|
|
1289 |
|
|
|
1290 |
\begin{textblock}{4}(8.3,14.2)
|
|
|
1291 |
\only<2>{
|
|
|
1292 |
\begin{tikzpicture}[remember picture]
|
|
|
1293 |
\draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (e2)
|
|
|
1294 |
{\small Notice, I wrote equality here!};
|
|
|
1295 |
|
|
|
1296 |
\path[overlay, ->, ultra thick, red] (e2) edge[out=180, in=-90] (e1);
|
|
|
1297 |
\end{tikzpicture}}
|
|
|
1298 |
\end{textblock}
|
|
|
1299 |
|
|
|
1300 |
\end{frame}}
|
|
|
1301 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1302 |
|
|
|
1303 |
*}
|
|
|
1304 |
|
|
|
1305 |
text_raw {*
|
|
|
1306 |
|
|
|
1307 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1308 |
\mode<presentation>{
|
|
|
1309 |
\begin{frame}
|
|
|
1310 |
\frametitle{My Claim}
|
|
|
1311 |
|
|
|
1312 |
\begin{center}
|
|
|
1313 |
\colorbox{cream}{%
|
|
|
1314 |
\smath{%
|
|
|
1315 |
\infer{P\;t}
|
|
|
1316 |
{\begin{array}{l}
|
|
|
1317 |
\forall x.\;P\;x\\[2mm]
|
|
|
1318 |
\forall t_1\,t_2.\;P\;t_1\wedge P\;t_2\Rightarrow P\;(t_1\;t_2)\\[2mm]
|
|
|
1319 |
\forall x\,t.\;P\;t\Rightarrow P\;(\lambda x.t)\\
|
|
|
1320 |
\end{array}
|
|
|
1321 |
}}}\medskip
|
|
|
1322 |
|
|
|
1323 |
\begin{tikzpicture}
|
|
|
1324 |
\node at (0,0) [single arrow, single arrow tip angle=140,
|
|
|
1325 |
shape border rotate=270, fill=red,text=white]{implies};
|
|
|
1326 |
\end{tikzpicture}\medskip
|
|
|
1327 |
|
|
|
1328 |
\colorbox{cream}{%
|
|
|
1329 |
\smath{%
|
|
|
1330 |
\infer{P c\,t}%
|
|
|
1331 |
{\begin{array}{@ {}l@ {}}
|
|
|
1332 |
\forall x\,c.\;P c\,x\\[2mm]
|
|
|
1333 |
\forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d.\,P d\,t_2)
|
|
|
1334 |
\Rightarrow P c\,(t_1\,t_2)\\[2mm]
|
|
|
1335 |
\forall x\,t\,c.\;
|
|
|
1336 |
x\fresh c \wedge (\forall d.\,P d\,t)\Rightarrow P c\,(\lambda x.t)
|
|
|
1337 |
\end{array}}}}
|
|
|
1338 |
|
|
|
1339 |
\end{center}
|
|
|
1340 |
|
|
|
1341 |
\end{frame}}
|
|
|
1342 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1343 |
|
|
|
1344 |
*}
|
|
|
1345 |
|
|
|
1346 |
text_raw {*
|
|
|
1347 |
|
|
|
1348 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1349 |
\mode<presentation>{
|
|
|
1350 |
\begin{frame}
|
|
|
1351 |
\frametitle{\large\mbox{Proof for the Strong Induction Principle}}
|
|
|
1352 |
|
|
|
1353 |
\begin{textblock}{14}(1.2,1.7)
|
|
|
1354 |
\begin{itemize}
|
|
|
1355 |
\item<1-> We prove \alt<1>{\smath{P c\,t}}{\smath{\forall \pi\,c.\;P c\,(\pi\act t)}}
|
|
|
1356 |
by induction on \smath{t}.
|
|
|
1357 |
|
|
|
1358 |
\item<3-> I.e., we have to show \alt<3>{\smath{P c\,(\pi\act(\lambda x.t))}}
|
|
|
1359 |
{\smath{P c\,\lambda(\pi\act x).(\pi\act t)}}.
|
|
|
1360 |
|
|
|
1361 |
\item<5-> We have \smath{\forall \pi\,c.\;P c\,(\pi\act t)} by induction.
|
|
|
1362 |
|
|
|
1363 |
|
|
|
1364 |
\item<6-> Our weaker precondition says that:\\
|
|
|
1365 |
\begin{center}
|
|
|
1366 |
\smath{\forall x\,t\,c.\,x\fresh c \wedge (\forall c.\,P c\,t) \Rightarrow P c\,(\lambda x.t)}
|
|
|
1367 |
\end{center}
|
|
|
1368 |
|
|
|
1369 |
\item<7-> We choose a fresh \smath{y} such that \smath{y\fresh (\pi\act x,\pi\act t,c)}.
|
|
|
1370 |
|
|
|
1371 |
\item<8-> Now we can use
|
|
|
1372 |
\alt<8>{\smath{\forall c.\;P c\,((\swap{y}{\,\pi\act x}\!::\!\pi)\act t)}}
|
|
|
1373 |
{\smath{\forall c.\;P c\,(\swap{y}{\,\pi\act x}\act\pi\act t)}} \only<10->{to infer}
|
|
|
1374 |
|
|
|
1375 |
\only<10->{
|
|
|
1376 |
\begin{center}
|
|
|
1377 |
\smath{P\,c\,\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t)}
|
|
|
1378 |
\end{center}}
|
|
|
1379 |
|
|
|
1380 |
\item<11-> However
|
|
|
1381 |
\begin{center}
|
|
|
1382 |
\smath{\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t)
|
|
|
1383 |
\textcolor{red}{\;=\;}\lambda (\pi\act x).(\pi\act t)}
|
|
|
1384 |
\end{center}
|
|
|
1385 |
|
|
|
1386 |
\item<12> Therefore \smath{P\,c\,\lambda (\pi\act x).(\pi\act t)} and we are done.
|
|
|
1387 |
\end{itemize}
|
|
|
1388 |
\end{textblock}
|
|
|
1389 |
|
|
|
1390 |
\only<11->{
|
|
|
1391 |
\begin{textblock}{9}(7,6)
|
|
|
1392 |
\begin{tikzpicture}[remember picture, overlay]
|
|
|
1393 |
\draw (0,0) node[fill=cream, text width=7cm, thick, draw=red, rounded corners=1mm] (n2)
|
|
|
1394 |
{\centering
|
|
|
1395 |
\smath{\infer{\lambda y.t_1=\lambda x.t_2}{x\not=y & t_1=\swap{x}{y}\act t_2 &
|
|
|
1396 |
y\fresh t_2}}
|
|
|
1397 |
};
|
|
|
1398 |
\end{tikzpicture}
|
|
|
1399 |
\end{textblock}}
|
|
|
1400 |
|
|
|
1401 |
\end{frame}}
|
|
|
1402 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1403 |
|
|
|
1404 |
*}
|
|
|
1405 |
|
|
|
1406 |
text_raw {*
|
|
|
1407 |
|
|
|
1408 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1409 |
\mode<presentation>{
|
|
|
1410 |
\begin{frame}<3->[squeeze]
|
|
|
1411 |
\frametitle{Formalisation of LF}
|
|
|
1412 |
|
|
|
1413 |
|
|
|
1414 |
\begin{center}
|
|
|
1415 |
\begin{tabular}{@ {\hspace{-16mm}}lc}
|
|
|
1416 |
\mbox{}\\[-6mm]
|
|
|
1417 |
|
|
|
1418 |
\textcolor{white}{\raisebox{4mm}{1.~Solution}} &
|
|
|
1419 |
\begin{tikzpicture}
|
|
|
1420 |
[node distance=25mm,
|
|
|
1421 |
text height=1.5ex,
|
|
|
1422 |
text depth=.25ex,
|
|
|
1423 |
node1/.style={
|
|
|
1424 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
1425 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
1426 |
]
|
|
|
1427 |
|
|
|
1428 |
\node (proof) [node1] {\large Proof};
|
|
|
1429 |
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
|
|
|
1430 |
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
|
|
|
1431 |
|
|
|
1432 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
1433 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
1434 |
|
|
|
1435 |
\onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);}
|
|
|
1436 |
\end{tikzpicture}
|
|
|
1437 |
\\[2mm]
|
|
|
1438 |
|
|
|
1439 |
\onslide<3->{%
|
|
|
1440 |
\raisebox{4mm}{1st Solution} &
|
|
|
1441 |
\begin{tikzpicture}
|
|
|
1442 |
[node distance=25mm,
|
|
|
1443 |
text height=1.5ex,
|
|
|
1444 |
text depth=.25ex,
|
|
|
1445 |
node1/.style={
|
|
|
1446 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
1447 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
1448 |
node2/.style={
|
|
|
1449 |
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
|
|
1450 |
draw=red!70, top color=white, bottom color=red!50!black!20}
|
|
|
1451 |
]
|
|
|
1452 |
|
|
|
1453 |
\node (proof) [node1] {\large Proof};
|
|
|
1454 |
\node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$};
|
|
|
1455 |
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
|
|
|
1456 |
|
|
|
1457 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
1458 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
1459 |
|
|
|
1460 |
\end{tikzpicture}
|
|
|
1461 |
\\[2mm]}
|
|
|
1462 |
|
|
|
1463 |
\onslide<4->{%
|
|
|
1464 |
\raisebox{4mm}{\hspace{-1mm}2nd Solution} &
|
|
|
1465 |
\begin{tikzpicture}
|
|
|
1466 |
[node distance=25mm,
|
|
|
1467 |
text height=1.5ex,
|
|
|
1468 |
text depth=.25ex,
|
|
|
1469 |
node1/.style={
|
|
|
1470 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
1471 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
1472 |
node2/.style={
|
|
|
1473 |
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
|
|
1474 |
draw=red!70, top color=white, bottom color=red!50!black!20}
|
|
|
1475 |
]
|
|
|
1476 |
|
|
|
1477 |
\node (proof) [node1] {\large Proof};
|
|
|
1478 |
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
|
|
|
1479 |
\node (alg) [node2, right of=proof] {\large Alg.$\!^\text{-ex}$};
|
|
|
1480 |
|
|
|
1481 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
1482 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
1483 |
|
|
|
1484 |
\end{tikzpicture}
|
|
|
1485 |
\\[2mm]}
|
|
|
1486 |
|
|
|
1487 |
\onslide<5->{%
|
|
|
1488 |
\raisebox{4mm}{\hspace{-1mm}3rd Solution} &
|
|
|
1489 |
\begin{tikzpicture}
|
|
|
1490 |
[node distance=25mm,
|
|
|
1491 |
text height=1.5ex,
|
|
|
1492 |
text depth=.25ex,
|
|
|
1493 |
node1/.style={
|
|
|
1494 |
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
|
|
|
1495 |
draw=black!50, top color=white, bottom color=black!20},
|
|
|
1496 |
node2/.style={
|
|
|
1497 |
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
|
|
1498 |
draw=red!70, top color=white, bottom color=red!50!black!20}
|
|
|
1499 |
]
|
|
|
1500 |
|
|
|
1501 |
\node (proof) [node2] {\large Proof};
|
|
|
1502 |
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
|
|
|
1503 |
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
|
|
|
1504 |
|
|
|
1505 |
\draw[->,black!50,line width=2mm] (proof) -- (def);
|
|
|
1506 |
\draw[->,black!50,line width=2mm] (proof) -- (alg);
|
|
|
1507 |
|
|
|
1508 |
\end{tikzpicture}
|
|
|
1509 |
\\}
|
|
|
1510 |
|
|
|
1511 |
\end{tabular}
|
|
|
1512 |
\end{center}
|
|
|
1513 |
|
|
|
1514 |
\begin{textblock}{3}(13.2,5.1)
|
|
|
1515 |
\onslide<3->{
|
|
|
1516 |
\begin{tikzpicture}
|
|
|
1517 |
\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
|
|
|
1518 |
\end{tikzpicture}
|
|
|
1519 |
}
|
|
|
1520 |
\end{textblock}
|
|
|
1521 |
|
|
|
1522 |
|
|
|
1523 |
\begin{textblock}{13}(1.4,15)
|
|
|
1524 |
\only<3->{\footnotesize (each time one needs to check $\sim$31pp~of informal paper proofs)}
|
|
|
1525 |
\end{textblock}
|
|
|
1526 |
|
|
|
1527 |
\end{frame}}
|
|
|
1528 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1529 |
|
|
|
1530 |
*}
|
|
|
1531 |
|
|
|
1532 |
|
|
|
1533 |
text_raw {*
|
|
|
1534 |
|
|
|
1535 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1536 |
\mode<presentation>{
|
|
|
1537 |
\begin{frame}
|
|
|
1538 |
\frametitle{Conclusions}
|
|
|
1539 |
|
|
|
1540 |
\begin{itemize}
|
|
|
1541 |
\item The Nominal Isabelle automatically derives the strong structural
|
|
|
1542 |
induction principle for \underline{\bf all} nominal datatypes (not just the
|
|
|
1543 |
lambda-calculus);
|
|
|
1544 |
|
|
|
1545 |
\item also for rule inductions (though they have to satisfy the vc-condition).
|
|
|
1546 |
|
|
|
1547 |
\item They are easy to use: you just have to think carefully what the variable
|
|
|
1548 |
convention should be.
|
|
|
1549 |
|
|
|
1550 |
\item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners
|
|
|
1551 |
of the variable convention: when and where it can be used safely.
|
|
|
1552 |
|
|
|
1553 |
\item<2> \alert{\bf Main Point:} Actually these proofs using the
|
|
|
1554 |
variable convention are all trivial / obvious / routine\ldots {\bf provided}
|
|
|
1555 |
you use Nominal Isabelle. ;o)
|
|
|
1556 |
|
|
|
1557 |
\end{itemize}
|
|
|
1558 |
|
|
|
1559 |
|
|
|
1560 |
\end{frame}}
|
|
|
1561 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1562 |
|
|
|
1563 |
*}
|
|
|
1564 |
|
|
|
1565 |
text_raw {*
|
|
|
1566 |
|
|
|
1567 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1568 |
\mode<presentation>{
|
|
|
1569 |
\begin{frame}
|
|
|
1570 |
\frametitle{\begin{tabular}{c}Nominal Meets\\[-2mm] Automata Theory\end{tabular}}
|
|
|
1571 |
|
|
|
1572 |
\begin{itemize}
|
|
|
1573 |
\item<1-> So what?\bigskip\medskip
|
|
|
1574 |
|
|
|
1575 |
\item<2-> I can give you a good argument why regular expressions
|
|
|
1576 |
are much, much better than automata. \textcolor{darkgray}{(over dinner?)}\medskip
|
|
|
1577 |
|
|
|
1578 |
\item<3-> Nominal automata?\bigskip\bigskip\medskip
|
|
|
1579 |
\end{itemize}
|
|
|
1580 |
|
|
|
1581 |
|
|
|
1582 |
\onslide<2->{
|
|
|
1583 |
\footnotesize\textcolor{darkgray}{A Formalisation of the Myhill-Nerode Theorem based on
|
|
|
1584 |
Regular Expressions (by Wu, Zhang and Urban)}
|
|
|
1585 |
}
|
|
|
1586 |
|
|
|
1587 |
\end{frame}}
|
|
|
1588 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1589 |
|
|
|
1590 |
*}
|
|
|
1591 |
|
|
|
1592 |
|
|
|
1593 |
|
|
|
1594 |
text_raw {*
|
|
|
1595 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1596 |
\mode<presentation>{
|
|
|
1597 |
\begin{frame}
|
|
|
1598 |
\frametitle{Quiz}
|
|
|
1599 |
%%%\small
|
|
|
1600 |
\mbox{}\\[-9mm]
|
|
|
1601 |
|
|
|
1602 |
Imagine\ldots\\[2mm]
|
|
|
1603 |
|
|
|
1604 |
\begin{tabular}{@ {\hspace{1cm}}l}
|
|
|
1605 |
\textcolor{blue}{Var\;``name''} \\
|
|
|
1606 |
\textcolor{blue}{App\;``lam''\;''lam''}\\
|
|
|
1607 |
\textcolor{blue}{Lam\;``\flqq{}name\frqq{}lam''} \\
|
|
|
1608 |
\textcolor{red}{Foo\;``\flqq{}name\frqq{}\flqq{}name\frqq{}lam''\;``
|
|
|
1609 |
\flqq{}name\frqq{}\flqq{}name\frqq{}lam''}\\[2mm]
|
|
|
1610 |
\end{tabular}
|
|
|
1611 |
|
|
|
1612 |
That means roughly:\\[2mm]
|
|
|
1613 |
|
|
|
1614 |
\begin{tabular}{@ {\hspace{1cm}}l}
|
|
|
1615 |
\alert{Foo\;($\lambda x.y.t_1$)\;($\lambda z.u.t_2$)}
|
|
|
1616 |
\end{tabular}
|
|
|
1617 |
|
|
|
1618 |
\begin{itemize}
|
|
|
1619 |
\item What does the variable convention look like for \alert{Foo}?
|
|
|
1620 |
\item What does the clause for capture-avoiding substitution look like?
|
|
|
1621 |
\end{itemize}
|
|
|
1622 |
|
|
|
1623 |
\footnotesize
|
|
|
1624 |
Answers: Download Nominal Isabelle and try it out\\
|
|
|
1625 |
\textcolor{white}{Answers:} http://isabelle.in.tum.de/nominal\\
|
|
|
1626 |
\end{frame}}
|
|
|
1627 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1628 |
*}
|
|
|
1629 |
|
|
|
1630 |
text_raw {*
|
|
|
1631 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1632 |
\mode<presentation>{
|
|
|
1633 |
\begin{frame}<1>[b]
|
|
|
1634 |
\frametitle{
|
|
|
1635 |
\begin{tabular}{c}
|
|
|
1636 |
\mbox{}\\[13mm]
|
|
|
1637 |
\alert{\LARGE Thank you very much!}\\
|
|
|
1638 |
\alert{\Large Questions?}
|
|
|
1639 |
\end{tabular}}
|
|
|
1640 |
|
|
|
1641 |
|
|
|
1642 |
\end{frame}}
|
|
|
1643 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
1644 |
*}
|
|
|
1645 |
|
|
|
1646 |
(*<*)
|
|
|
1647 |
end
|
|
|
1648 |
(*>*) |