2351
+ − 1 (*<*)
+ − 2 theory Slides3
+ − 3 imports "LaTeXsugar" "Nominal"
+ − 4 begin
+ − 5
+ − 6 notation (latex output)
+ − 7 set ("_") and
+ − 8 Cons ("_::/_" [66,65] 65)
+ − 9
+ − 10 (*>*)
+ − 11
2355
+ − 12 text_raw {*
+ − 13 \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}
2356
+ − 14
+ − 15 \newcommand{\abst}[2]{#1.#2}% atom-abstraction
+ − 16 \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
+ − 17 \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
+ − 18 \newcommand{\unit}{\langle\rangle}% unit
+ − 19 \newcommand{\app}[2]{#1\,#2}% application
+ − 20 \newcommand{\eqprob}{\mathrel{{\approx}?}}
2357
+ − 21 \newcommand{\freshprob}{\mathrel{\#?}}
+ − 22 \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
+ − 23 \newcommand{\id}{\varepsilon}% identity substitution
2356
+ − 24
+ − 25 \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
+ − 26 {rgb(0mm)=(0,0,0.9);
+ − 27 rgb(0.9mm)=(0,0,0.7);
+ − 28 rgb(1.3mm)=(0,0,0.5);
+ − 29 rgb(1.4mm)=(1,1,1)}
+ − 30
2355
+ − 31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 32 \mode<presentation>{
+ − 33 \begin{frame}<1>[c]
+ − 34 \frametitle{Quiz}
+ − 35
+ − 36 Assuming that \smath{a} and \smath{b} are distinct variables,\\
+ − 37 is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7}
+ − 38 that make the following pairs \alert{$\alpha$-equivalent}?
+ − 39
+ − 40 \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
+ − 41 \begin{itemize}
+ − 42 \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and
+ − 43 \smath{\lambda b.\lambda a. (a\,M_1)\;}
+ − 44
+ − 45 \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and
+ − 46 \smath{\lambda b.\lambda a. (a\,M_3)\;}
+ − 47
+ − 48 \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and
+ − 49 \smath{\lambda b.\lambda a. (a\,M_5)\;}
+ − 50
+ − 51 \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and
+ − 52 \smath{\lambda a.\lambda a. (a\,M_7)\;}
+ − 53 \end{itemize}
+ − 54 \end{tabular}
+ − 55
+ − 56 If there is one solution for a pair, can you describe all its solutions?
+ − 57
+ − 58 \end{frame}}
+ − 59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 60 *}
2351
+ − 61
+ − 62 text_raw {*
+ − 63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 64 \mode<presentation>{
+ − 65 \begin{frame}<1>[t]
+ − 66 \frametitle{%
+ − 67 \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+ − 68 \\
2355
+ − 69 \huge Nominal Unification\\[-2mm]
+ − 70 \Large Hitting a Sweet Spot\\[5mm]
2351
+ − 71 \end{tabular}}
+ − 72 \begin{center}
+ − 73 Christian Urban
+ − 74 \end{center}
+ − 75 \begin{center}
2357
+ − 76 \small initial spark from Roy Dyckhoff in November 2001\\[0mm]
+ − 77 \small joint work with Andy Pitts and Jamie Gabbay\\[0mm]
2351
+ − 78 \end{center}
+ − 79 \end{frame}}
+ − 80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 81
+ − 82 *}
+ − 83 text_raw {*
+ − 84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 85 \mode<presentation>{
2356
+ − 86 \begin{frame}<1-4>[c]
+ − 87 \frametitle{One Motivation}
+ − 88
+ − 89 \onslide<2->{Typing implemented in Prolog \textcolor{darkgray}{(from a textbook)}}\bigskip\\
2351
+ − 90
2357
+ − 91 \onslide<3->{\color{darkgray}
2356
+ − 92 \begin{tabular}{l}
+ − 93 type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\
+ − 94
+ − 95 type (Gamma, app(M, N), T') :-\\
+ − 96 \hspace{3cm}type (Gamma, M, arrow(T, T')),\\
+ − 97 \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\
2351
+ − 98
2356
+ − 99 type (Gamma, lam(X, M), arrow(T, T')) :-\\
+ − 100 \hspace{3cm}type ((X, T)::Gamma, M, T').\smallskip\medskip\\
+ − 101
+ − 102 member X X::Tail.\\
+ − 103 member X Y::Tail :- member X Tail.\\
+ − 104 \end{tabular}}
+ − 105
+ − 106 \only<4>{
+ − 107 \begin{textblock}{6}(2.5,2)
+ − 108 \begin{tikzpicture}
+ − 109 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 110 {\color{darkgray}
+ − 111 \begin{minipage}{8cm}\raggedright
+ − 112 The problem is that \smath{\lambda x.\lambda x. (x\;x)}
2357
+ − 113 will have the types
2351
+ − 114 \begin{center}
2356
+ − 115 \begin{tabular}{l}
+ − 116 \smath{T\rightarrow (T\rightarrow S) \rightarrow S} and\\
+ − 117 \smath{(T\rightarrow S)\rightarrow T \rightarrow S}\\
2351
+ − 118 \end{tabular}
2356
+ − 119 \end{center}
+ − 120 \end{minipage}};
+ − 121 \end{tikzpicture}
2351
+ − 122 \end{textblock}}
+ − 123
+ − 124 \end{frame}}
+ − 125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 126 *}
+ − 127
+ − 128 text_raw {*
+ − 129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 130 \mode<presentation>{
2356
+ − 131 \begin{frame}<1>[c]
+ − 132 \frametitle{Higher-Order Unification}
2351
+ − 133
2358
+ − 134 State of the art at the time:
2357
+ − 135
2351
+ − 136 \begin{itemize}
2356
+ − 137 \item Lambda Prolog with full Higher-Order Unification\\
+ − 138 \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip
+ − 139 \item Higher-Order Pattern Unification\\
+ − 140 \textcolor{darkgray}{(has mgus, decidable, some restrictions, modulo $\alpha\beta_0$)}
2351
+ − 141 \end{itemize}
2356
+ − 142
2351
+ − 143 \end{frame}}
+ − 144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 145 *}
+ − 146
+ − 147 text_raw {*
+ − 148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 149 \mode<presentation>{
2356
+ − 150 \begin{frame}<1-10>[t]
+ − 151 \frametitle{Underlying Ideas}
2351
+ − 152
+ − 153 \begin{itemize}
2356
+ − 154 \item<1-> Unification (\alert{only}) up to $\alpha$
+ − 155
+ − 156 \item<2-> Swappings / Permutations
+ − 157
+ − 158 \only<2-5>{
+ − 159 \begin{center}
+ − 160 \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{12mm}}r@ {\hspace{1mm}}l}
2357
+ − 161 \\
2356
+ − 162 \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%
+ − 163 \only<3>{\smath{[b\!:=\!a]}}%
+ − 164 \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} &
+ − 165 \onslide<2-5>{\smath{\lambda a.b}} &
2351
+ − 166
2356
+ − 167 \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%
+ − 168 \only<3>{\smath{[b\!:=\!a]}}%
+ − 169 \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} &
+ − 170 \onslide<2-5>{\smath{\lambda c.b}}\\
+ − 171
+ − 172 \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda a.a}}\only<4-5>{\smath{\lambda b.a}} &
+ − 173 \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda c.a}}\only<4-5>{\smath{\lambda c.a}}\\
+ − 174 \end{tabular}
+ − 175 \end{center}\bigskip
+ − 176
+ − 177 \onslide<4-5>{
+ − 178 \begin{center}
+ − 179 \begin{tikzpicture}
+ − 180 \draw (0,0) node[inner sep=0mm,fill=cream, ultra thick, draw=cream]
+ − 181 {\begin{minipage}{8cm}
+ − 182 \begin{tabular}{r@ {\hspace{3mm}}l}
2357
+ − 183 \smath{\swap{a}{b}\act t} $\;\dn$ & \alert{swap} {\bf all} occurrences of\\
2356
+ − 184 & \smath{b} and \smath{a} in \smath{t}
2351
+ − 185 \end{tabular}
2356
+ − 186 \end{minipage}};
+ − 187 \end{tikzpicture}
+ − 188 \end{center}}\bigskip
+ − 189
+ − 190 \onslide<5>{
+ − 191 Unlike for \smath{[b\!:=\!a]\act(-)}, for \smath{\swap{a}{b}\act (-)} we do
+ − 192 have if \smath{t =_\alpha t'} then \smath{\pi \act t =_\alpha \pi \act t'.}}}
+ − 193
+ − 194 \item<6-> Variables (or holes)\bigskip
+ − 195
+ − 196 \begin{center}
+ − 197 \onslide<7->{\mbox{}\hspace{-25mm}\smath{\lambda x\hspace{-0.5mm}s .}}
+ − 198 \onslide<8-9>{\raisebox{-1.7mm}{\huge\smath{(}}}\raisebox{-4mm}{\begin{tikzpicture}
+ − 199 \fill[blue] (0, 0) circle (5mm);
+ − 200 \end{tikzpicture}}
+ − 201 \onslide<8-9>{\smath{y\hspace{-0.5mm}s}{\raisebox{-1.7mm}{\huge\smath{)}}}}\bigskip
+ − 202 \end{center}
+ − 203
+ − 204 \only<8-9>{\smath{y\hspace{-0.5mm}s} are the parameters the hole can depend on\onslide<9->{, but
+ − 205 then you need $\beta_0$-reduction\medskip
+ − 206 \begin{center}
+ − 207 \smath{(\lambda x. t) y \longrightarrow_{\beta_0} t[x:=y]}
+ − 208 \end{center}}}
+ − 209
+ − 210 \only<10>{we will record the information about which parameters a hole
+ − 211 \alert{\bf cannot} depend on}
2351
+ − 212
+ − 213 \end{itemize}
2356
+ − 214
+ − 215 \end{frame}}
+ − 216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 217 *}
+ − 218
+ − 219 text_raw {*
+ − 220 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 221 \mode<presentation>{
+ − 222 \begin{frame}<1-4>[c]
+ − 223 \frametitle{Terms}
+ − 224
+ − 225 \begin{tabular}{lll @ {\hspace{10mm}}lll}
+ − 226
+ − 227 \onslide<1->{\pgfuseshading{smallbluesphere}} &
+ − 228 \onslide<1->{\colorbox{cream}{\smath{\unit}}} &
+ − 229 \onslide<1->{Units} &
+ − 230
+ − 231 \onslide<2->{\pgfuseshading{smallbluesphere}} &
+ − 232 \onslide<2->{\colorbox{cream}{\smath{a}}} &
+ − 233 \onslide<2->{Atoms} \\[5mm]
+ − 234
+ − 235 \onslide<1->{\pgfuseshading{smallbluesphere}} &
+ − 236 \onslide<1->{\colorbox{cream}{\smath{\pair{t}{t'}}}} &
+ − 237 \onslide<1->{Pairs} &
+ − 238
+ − 239 \onslide<3->{\pgfuseshading{smallbluesphere}} &
+ − 240 \onslide<3->{\colorbox{cream}{\smath{\abst{a}{t}}}} &
+ − 241 \onslide<3->{Abstractions}\\[5mm]
+ − 242
+ − 243 \onslide<1->{\pgfuseshading{smallbluesphere}} &
+ − 244 \onslide<1->{\colorbox{cream}{\smath{\app{F}{t}}}} &
+ − 245 \onslide<1->{Funct.} &
+ − 246
+ − 247 \onslide<4->{\pgfuseshading{smallbluesphere}} &
+ − 248 \onslide<4->{\colorbox{cream}{\smath{\pi\susp X}}} &
+ − 249 \onslide<4->{Suspensions}
+ − 250 \end{tabular}
+ − 251
+ − 252 \only<2>{
+ − 253 \begin{textblock}{13}(1.5,12)
+ − 254 \small Atoms are constants \textcolor{darkgray}{(infinitely many of them)}
+ − 255 \end{textblock}}
+ − 256
+ − 257 \only<3>{
+ − 258 \begin{textblock}{13}(1.5,12)
+ − 259 \small \smath{\ulcorner \lambda\abst{a}{a}\urcorner \mapsto \text{fn\ }\abst{a}{a}}\\
+ − 260 \small constructions like \smath{\text{fn\ }\abst{X}{X}} are not allowed
+ − 261 \end{textblock}}
+ − 262
+ − 263 \only<4>{
+ − 264 \begin{textblock}{13}(1.5,12)
+ − 265 \small \smath{X} is a variable standing for a term\\
+ − 266 \small \smath{\pi} is an explicit permutation \smath{\swap{a_1}{b_1}\ldots\swap{a_n}{b_n}},
+ − 267 waiting to be applied to the term that is substituted for \smath{X}
+ − 268 \end{textblock}}
2351
+ − 269
+ − 270 \end{frame}}
+ − 271 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 272 *}
+ − 273
+ − 274 text_raw {*
+ − 275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 276 \mode<presentation>{
2356
+ − 277 \begin{frame}<1-3>[c]
+ − 278 \frametitle{Permutations}
+ − 279
+ − 280 a permutation applied to a term
+ − 281
+ − 282 \begin{center}
+ − 283 \begin{tabular}{lrcl}
+ − 284 \pgfuseshading{smallbluesphere} &
+ − 285 \smath{[]\act c} & \smath{\dn} & \smath{c} \\
2351
+ − 286
2356
+ − 287 \pgfuseshading{smallbluesphere} &
+ − 288 \smath{\swap{a}{b}\!::\!\pi\act c} & \smath{\dn} &
+ − 289 \smath{\begin{cases}
+ − 290 a & \text{if}\;\pi\act c = b\\
+ − 291 b & \text{if}\;\pi\act c = a\\
+ − 292 \pi\act c & \text{otherwise}
+ − 293 \end{cases}}\\
+ − 294
+ − 295 \onslide<2->{\pgfuseshading{smallbluesphere}} &
+ − 296 \onslide<2->{\smath{\pi\act\abst{a}{t}}} & \onslide<2->{\smath{\dn}} &
+ − 297 \onslide<2->{\smath{\abst{\pi\act a}{\pi\act t}}}\\
+ − 298
+ − 299 \onslide<3->{\pgfuseshading{smallbluesphere}} &
+ − 300 \onslide<3->{\smath{\pi\act\pi'\act X}} & \onslide<3->{\smath{\dn}} &
+ − 301 \onslide<3->{\smath{(\pi @ \pi')\act X}}\\
2351
+ − 302 \end{tabular}
+ − 303 \end{center}
+ − 304
+ − 305 \end{frame}}
+ − 306 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 307 *}
+ − 308
+ − 309 text_raw {*
+ − 310 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 311 \mode<presentation>{
2356
+ − 312 \begin{frame}<1-3>[c]
+ − 313 \frametitle{Freshness Constraints}
+ − 314
+ − 315 Recall \smath{\lambda a. \raisebox{-0.7mm}{\tikz \fill[blue] (0, 0) circle (2.5mm);}}
+ − 316 \bigskip\pause
+ − 317
+ − 318 We therefore will identify
+ − 319
+ − 320 \begin{center}
2357
+ − 321 \smath{\text{fn\ } a. X \;\approx\; \text{fn\ } b. \alert<3->{\swap{a}{b}}\act X}
2356
+ − 322 \end{center}
+ − 323
+ − 324 provided that `\smath{b} is fresh for \smath{X} --- (\smath{b\fresh X})',
+ − 325 i.e., does not occur freely in any ground term that might be substituted for
+ − 326 \smath{X}.\bigskip\pause
+ − 327
+ − 328 If we know more about \smath{X}, e.g., if we knew that \smath{a\fresh X} and
+ − 329 \smath{b\fresh X}, then we can replace\\ \smath{\swap{a}{b}\act X} by
+ − 330 \smath{X}.
2351
+ − 331
2356
+ − 332 \end{frame}}
+ − 333 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 334 *}
+ − 335
+ − 336 text_raw {*
+ − 337 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 338 \mode<presentation>{
+ − 339 \begin{frame}<1-4>[c]
+ − 340 \frametitle{Equivalence Judgements}
2351
+ − 341
2356
+ − 342 \alt<1>{Our equality is {\bf not} just}{but judgements}
+ − 343
+ − 344 \begin{center}
+ − 345 \begin{tabular}{rl}
+ − 346 \colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} t \approx t'}} & \alert{$\alpha$-equivalence}\\[1mm]
+ − 347 \onslide<4->{\colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} a \fresh t}}} &
+ − 348 \onslide<4->{\alert{freshness}}
+ − 349 \end{tabular}
+ − 350 \end{center}
2351
+ − 351
+ − 352 \onslide<2->{
2356
+ − 353 where
2351
+ − 354 \begin{center}
2356
+ − 355 \smath{\nabla = \{a_1\fresh X_1,\ldots, a_n\fresh X_n\}}
+ − 356 \end{center}
+ − 357 is a finite set of \alert{freshness assumptions}.}
+ − 358
+ − 359 \onslide<3->{
+ − 360 \begin{center}
+ − 361 \smath{\{a\fresh X,b\fresh X\} \vdash \text{fn\ } a. X \approx \text{fn\ } b. X}
2351
+ − 362 \end{center}}
+ − 363
+ − 364 \end{frame}}
+ − 365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 366 *}
+ − 367
+ − 368 text_raw {*
+ − 369 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 370 \mode<presentation>{
2356
+ − 371 \begin{frame}<1>[c]
+ − 372 \frametitle{Rules for Equivalence}
+ − 373
+ − 374 \begin{center}
+ − 375 \begin{tabular}{c}
+ − 376 Excerpt\\
+ − 377 (i.e.~only the interesting rules)
+ − 378 \end{tabular}
+ − 379 \end{center}
+ − 380
+ − 381 \end{frame}}
+ − 382 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 383 *}
2351
+ − 384
2356
+ − 385 text_raw {*
+ − 386 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 387 \mode<presentation>{
+ − 388 \begin{frame}<1>[c]
+ − 389 \frametitle{Rules for Equivalence}
+ − 390
+ − 391 \begin{center}
+ − 392 \begin{tabular}{c}
+ − 393 \colorbox{cream}{\smath{\infer{\nabla \vdash a \approx a}{}}}\\[8mm]
+ − 394
+ − 395 \colorbox{cream}{%
+ − 396 \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{a}{t'}}
+ − 397 {\nabla \vdash t \approx t'}}}\\[8mm]
+ − 398
+ − 399 \colorbox{cream}{%
+ − 400 \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{b}{t'}}
+ − 401 {a\not=b\;\; & \nabla \vdash t \approx \swap{a}{b}\act t'\;\;& \nabla \vdash a\fresh t'}}}
2351
+ − 402 \end{tabular}
2356
+ − 403 \end{center}
2351
+ − 404
+ − 405 \end{frame}}
+ − 406 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 407 *}
+ − 408
+ − 409 text_raw {*
+ − 410 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 411 \mode<presentation>{
2356
+ − 412 \begin{frame}<1-3>[c]
+ − 413 \frametitle{Rules for Equivalence}
2351
+ − 414
+ − 415 \begin{center}
2356
+ − 416 \colorbox{cream}{%
+ − 417 \smath{%
+ − 418 \infer{\nabla \vdash \pi\act X \approx \pi'\act X}
+ − 419 {\begin{array}{c}
+ − 420 (a\fresh X)\in\nabla\\
+ − 421 \text{for all}\; a \;\text{with}\;\pi\act a \not= \pi'\act a
+ − 422 \end{array}
+ − 423 }}}
2351
+ − 424 \end{center}
+ − 425
2356
+ − 426 \onslide<2->{
+ − 427 for example\\[4mm]
+ − 428
+ − 429 \alt<2>{%
+ − 430 \begin{center}
+ − 431 \smath{\{a\fresh\!X, b\fresh\!X\} \vdash X \approx \swap{a}{b}\act X}
+ − 432 \end{center}}
+ − 433 {%
2351
+ − 434 \begin{center}
2356
+ − 435 \smath{\{a\fresh\!X, c\fresh\!X\} \vdash \swap{a}{c}\swap{a}{b}\act X \approx \swap{b}{c}\act X}
+ − 436 \end{center}}
2351
+ − 437
2356
+ − 438 \onslide<3->{
+ − 439 \begin{tabular}{@ {}lllll@ {}}
+ − 440 because &
+ − 441 \smath{\swap{a}{c}\swap{a}{b}}: &
+ − 442 \smath{a\mapsto b} &
+ − 443 \smath{\swap{b}{c}}: &
+ − 444 \smath{a\mapsto a}\\
+ − 445 & & \smath{b\mapsto c} & & \smath{b\mapsto c}\\
+ − 446 & & \smath{c\mapsto a} & & \smath{c\mapsto b}\\
+ − 447 \end{tabular}
+ − 448 disagree at \smath{a} and \smath{c}.}
+ − 449 }
+ − 450
+ − 451 \end{frame}}
+ − 452 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 453 *}
+ − 454
+ − 455 text_raw {*
+ − 456 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 457 \mode<presentation>{
+ − 458 \begin{frame}<1>[c]
+ − 459 \frametitle{Rules for Freshness}
+ − 460
2351
+ − 461 \begin{center}
2356
+ − 462 \begin{tabular}{c}
+ − 463 Excerpt\\
+ − 464 (i.e.~only the interesting rules)
2351
+ − 465 \end{tabular}
2356
+ − 466 \end{center}
2351
+ − 467
+ − 468 \end{frame}}
+ − 469 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 470 *}
+ − 471
+ − 472 text_raw {*
+ − 473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 474 \mode<presentation>{
2356
+ − 475 \begin{frame}<1>[c]
+ − 476 \frametitle{Rules for Freshness}
2351
+ − 477
2356
+ − 478 \begin{center}
+ − 479 \begin{tabular}{c}
+ − 480 \colorbox{cream}{%
+ − 481 \smath{\infer{\nabla \vdash a\fresh b}{a\not= b}}}\\[5mm]
2351
+ − 482
2356
+ − 483 \colorbox{cream}{%
+ − 484 \smath{\infer{\nabla \vdash a\fresh\abst{a}{t}}{}}}\hspace{7mm}
+ − 485 \colorbox{cream}{%
+ − 486 \smath{\infer{\nabla \vdash a\fresh\abst{b}{t}}
+ − 487 {a\not= b\;\; & \nabla \vdash a\fresh t}}}\\[5mm]
+ − 488
+ − 489 \colorbox{cream}{%
+ − 490 \smath{\infer{\nabla \vdash a\fresh \pi\act X}
+ − 491 {(\pi^{-1}\act a\fresh X)\in\nabla}}}
2351
+ − 492 \end{tabular}
+ − 493 \end{center}
+ − 494
+ − 495 \end{frame}}
+ − 496 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 497 *}
+ − 498
+ − 499 text_raw {*
+ − 500 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 501 \mode<presentation>{
2356
+ − 502 \begin{frame}<1-4>[t]
+ − 503 \frametitle{$\approx$ is an Equivalence}
+ − 504 \mbox{}\\[5mm]
2351
+ − 505
+ − 506 \begin{center}
2356
+ − 507 \colorbox{cream}{\alert{Theorem:}
+ − 508 $\approx$ is an equivalence relation.}
+ − 509 \end{center}\bigskip
2351
+ − 510
2356
+ − 511 \only<1>{%
+ − 512 \begin{tabular}{ll}
+ − 513 (Reflexivity) & $\smath{\nabla\vdash t\approx t}$\\[2mm]
+ − 514 (Symmetry) & if $\smath{\nabla\vdash t_1\approx t_2}\;$
+ − 515 then $\;\smath{\nabla\vdash t_2\approx t_1}$\\[2mm]
+ − 516 (Transitivity) & if $\smath{\nabla\vdash t_1\approx t_2}\;$ and
+ − 517 $\;\smath{\nabla\vdash t_2\approx t_3}$\\
+ − 518 & then $\smath{\nabla\vdash t_1\approx t_3}$\\
+ − 519 \end{tabular}}
2351
+ − 520
2356
+ − 521 \only<2->{%
+ − 522 \begin{itemize}
+ − 523 \item<2-> \smath{\nabla \vdash t\approx t'} then \smath{\nabla \vdash \pi\act t\approx \pi\act t'}
2351
+ − 524
2356
+ − 525 \item<2-> \smath{\nabla \vdash a\fresh t} then
+ − 526 \smath{\nabla \vdash \pi\act a\fresh \pi\act t}
2351
+ − 527
2356
+ − 528 \item<3-> \smath{\nabla \vdash t\approx \pi\act t'} then
+ − 529 \smath{\nabla \vdash (\pi^{-1})\act t\approx t'}
+ − 530
+ − 531 \item<3-> \smath{\nabla \vdash a\fresh \pi\act t} then
+ − 532 \smath{\nabla \vdash (\pi^{-1})\act a\fresh t}
2351
+ − 533
2356
+ − 534 \item<4-> \smath{\nabla \vdash a\fresh t} and \smath{\nabla \vdash t\approx t'} then
+ − 535 \smath{\nabla \vdash a\fresh t'}
+ − 536 \end{itemize}
+ − 537 }
+ − 538
2351
+ − 539 \end{frame}}
+ − 540 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 541 *}
+ − 542
+ − 543 text_raw {*
+ − 544 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 545 \mode<presentation>{
2356
+ − 546 \begin{frame}<1-4>
+ − 547 \frametitle{Comparison $=_\alpha$}
2351
+ − 548
2356
+ − 549 Traditionally \smath{=_\alpha} is defined as
2351
+ − 550
+ − 551 \begin{center}
2356
+ − 552 \colorbox{cream}{%
+ − 553 \begin{minipage}{9cm}
+ − 554 \raggedright least congruence which identifies \smath{\abst{a}{t}}
+ − 555 with \smath{\abst{b}{[a:=b]t}} provided \smath{b} is not free
+ − 556 in \smath{t}
+ − 557 \end{minipage}}
+ − 558 \end{center}
2351
+ − 559
2356
+ − 560 where \smath{[a:=b]t} replaces all free occurrences of\\
+ − 561 \smath{a} by \smath{b} in \smath{t}.
+ − 562 \bigskip
2351
+ − 563
2356
+ − 564 \only<2>{%
+ − 565 \begin{textblock}{13}(1.2,10)
+ − 566 For \alert{ground} terms:
2351
+ − 567
2356
+ − 568 \begin{center}
+ − 569 \colorbox{cream}{%
+ − 570 \begin{minipage}{9.0cm}
+ − 571 \begin{tabular}{@ {}rl}
+ − 572 \underline{Theorem:}
+ − 573 & \smath{t=_\alpha t'\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset \vdash t\approx t'}\\[2mm]
2357
+ − 574 & \smath{a\not\in F\hspace{-0.9mm}A(t)\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset\vdash a\fresh t}
2351
+ − 575 \end{tabular}
2356
+ − 576 \end{minipage}}
+ − 577 \end{center}
2351
+ − 578 \end{textblock}}
2356
+ − 579
+ − 580 \only<3>{%
+ − 581 \begin{textblock}{13}(1.2,10)
+ − 582 In general \smath{=_\alpha} and \smath{\approx} are distinct!
+ − 583 \begin{center}
+ − 584 \colorbox{cream}{%
+ − 585 \begin{minipage}{6.0cm}
+ − 586 \smath{\abst{a}{X}=_\alpha \abst{b}{X}\;} but not\\[2mm]
+ − 587 \smath{\emptyset \vdash \abst{a}{X} \approx \abst{b}{X}\;} (\smath{a\not=b})
+ − 588 \end{minipage}}
+ − 589 \end{center}
+ − 590 \end{textblock}}
+ − 591
+ − 592 \only<4>{
+ − 593 \begin{textblock}{6}(1,2)
2351
+ − 594 \begin{tikzpicture}
2356
+ − 595 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 596 {\color{darkgray}
+ − 597 \begin{minipage}{10cm}\raggedright
+ − 598 That is a crucial point: if we had\\[-2mm]
+ − 599 \[\smath{\emptyset \vdash \abst{a}{X}\approx \abst{b}{X}}\mbox{,}\]
+ − 600 then applying $\smath{[X:=a]}$, $\smath{[X:=b]}$, $\ldots$\\
+ − 601 give two terms that are {\bf not} $\alpha$-equivalent.\\[3mm]
+ − 602 The freshness constraints $\smath{a\fresh X}$ and $\smath{b\fresh X}$
+ − 603 rule out the problematic substitutions. Therefore
+ − 604
+ − 605 \[\smath{\{a\fresh X,b\fresh X\} \vdash \abst{a}{X}\approx \abst{b}{X}}\]
+ − 606
+ − 607 does hold.
2351
+ − 608 \end{minipage}};
+ − 609 \end{tikzpicture}
+ − 610 \end{textblock}}
+ − 611
+ − 612 \end{frame}}
+ − 613 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 614 *}
+ − 615
+ − 616 text_raw {*
+ − 617 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 618 \mode<presentation>{
2356
+ − 619 \begin{frame}<1-9>
+ − 620 \frametitle{Substitution}
+ − 621
+ − 622 \begin{tabular}{l@ {\hspace{8mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {}}
+ − 623 \pgfuseshading{smallbluesphere} &
+ − 624 \smath{\sigma(\abst{a}{t})} & \smath{\dn} & \smath{\abst{a}{\sigma(t)}}\\[2mm]
2351
+ − 625
2356
+ − 626 \pgfuseshading{smallbluesphere} &
+ − 627 \smath{\sigma(\pi\act X)} & \smath{\dn} &
+ − 628 \smath{\begin{cases}%
+ − 629 \pi\;\act\;\sigma(X) & \!\!\text{if\ } \sigma(X)\not=X\\
+ − 630 \pi\act X & \!\!\text{otherwise}%
+ − 631 \end{cases}}\\[6mm]
+ − 632 \end{tabular}\bigskip\bigskip
2351
+ − 633
2356
+ − 634 \pause
+ − 635 \only<2-5>{
+ − 636 \only<2->{for example}
+ − 637 \def\arraystretch{1.3}
+ − 638 \begin{tabular}{@ {\hspace{14mm}}l@ {\hspace{3mm}}l}
+ − 639 \onslide<2->{\textcolor{white}{$\Rightarrow$}} &
+ − 640 \onslide<2->{\alt<3>{\smath{\underline{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}
+ − 641 {\smath{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}\\
+ − 642 \onslide<3->{\smath{\Rightarrow}} &
+ − 643 \onslide<3->{\alt<3,4>{\smath{\abst{a}{\underline{\swap{a}{b}\act X[X:=\pair{b}{Y}]}}}}
+ − 644 {\smath{\abst{a}{\swap{a}{b}\act X}[X:=\pair{b}{Y}]}}}\\
+ − 645 \onslide<4->{\smath{\Rightarrow}} &
+ − 646 \onslide<4->{\alt<4>{\smath{\abst{a}{\swap{a}{b}\act \underline{\pair{b}{Y}}}}}
+ − 647 {\smath{\abst{a}{\underline{\swap{a}{b}}\act \pair{b}{Y}}}}}\\
+ − 648 \onslide<5->{\smath{\Rightarrow}} &
+ − 649 \onslide<5->{\smath{\abst{a}{\pair{a}{\swap{a}{b}\act Y}}}}
+ − 650 \end{tabular}}
2351
+ − 651
2356
+ − 652 \only<6->
+ − 653 {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}
+ − 654 \pgfuseshading{smallbluesphere} &
+ − 655 if \smath{\nabla\vdash t\approx t'} and\hspace{-2mm}\mbox{}
+ − 656 \raisebox{-2.7mm}{
+ − 657 \alt<7>{\begin{tikzpicture}
+ − 658 \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=3mm]
+ − 659 {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};
+ − 660 \end{tikzpicture}}
+ − 661 {\begin{tikzpicture}
+ − 662 \draw (0,0) node[inner sep=1mm,fill=white, very thick, draw=white, rounded corners=3mm]
+ − 663 {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};
+ − 664 \end{tikzpicture}}}\\
+ − 665 & then \smath{\nabla'\vdash\sigma(t)\approx\sigma(t')}
+ − 666 \end{tabular}}
2351
+ − 667
2356
+ − 668 \only<9>
+ − 669 {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}
+ − 670 \\[-4mm]
+ − 671 \pgfuseshading{smallbluesphere} &
+ − 672 \smath{\sigma(\pi\act t)=\pi\act\sigma(t)}
+ − 673 \end{tabular}}
2351
+ − 674
+ − 675
2356
+ − 676 \only<7>{
+ − 677 \begin{textblock}{6}(10,10.5)
2351
+ − 678 \begin{tikzpicture}
2356
+ − 679 \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=2mm]
+ − 680 {\color{darkgray}
+ − 681 \begin{minipage}{3.8cm}\raggedright
+ − 682 this means\\[1mm]
+ − 683 \smath{\nabla'\vdash a\fresh\sigma(X)}\\[1mm]
+ − 684 holds for all\\[1mm]
+ − 685 \smath{(a\fresh X)\in\nabla}
2351
+ − 686 \end{minipage}};
+ − 687 \end{tikzpicture}
+ − 688 \end{textblock}}
+ − 689
+ − 690 \end{frame}}
+ − 691 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 692 *}
+ − 693
+ − 694 text_raw {*
+ − 695 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 696 \mode<presentation>{
2356
+ − 697 \begin{frame}<1->
+ − 698 \frametitle{Equational Problems}
2351
+ − 699
2356
+ − 700 An equational problem
+ − 701 \[
+ − 702 \colorbox{cream}{\smath{t \eqprob t'}}
+ − 703 \]
+ − 704 is \alert{solved} by
2351
+ − 705
+ − 706 \begin{center}
2356
+ − 707 \begin{tabular}{ll}
+ − 708 \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma} (terms for variables)\\[3mm]
+ − 709 \pgfuseshading{smallbluesphere} & {\bf and} a set of freshness assumptions \smath{\nabla}
+ − 710 \end{tabular}
2351
+ − 711 \end{center}
+ − 712
2356
+ − 713 so that \smath{\nabla\vdash \sigma(t)\approx \sigma(t')}.
2351
+ − 714
+ − 715
+ − 716 \end{frame}}
+ − 717 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 718 *}
+ − 719
+ − 720 text_raw {*
+ − 721 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 722 \mode<presentation>{
+ − 723 \begin{frame}<1->
2357
+ − 724
+ − 725 Unifying equations may entail solving
+ − 726 \alert{freshness problems}.
+ − 727
+ − 728 \bigskip
+ − 729
+ − 730 E.g.~assuming that \smath{a\not=a'}, then
+ − 731 \[
+ − 732 \smath{\abst{a}{t}\eqprob \abst{a'}{t'}}
+ − 733 \]
+ − 734 can only be solved if
+ − 735 \[
+ − 736 \smath{t\eqprob \swap{a}{a'}\act t'} \quad\text{\emph{and}}\quad
+ − 737 \smath{a\freshprob t'}
+ − 738 \]
+ − 739 can be solved.
+ − 740
+ − 741 \end{frame}}
+ − 742 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 743 *}
+ − 744
+ − 745 text_raw {*
+ − 746 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 747 \mode<presentation>{
+ − 748 \begin{frame}<1->
+ − 749 \frametitle{Freshness Problems}
+ − 750
+ − 751 A freshness problem
+ − 752 \[
+ − 753 \colorbox{cream}{\smath{a \freshprob t}}
+ − 754 \]
+ − 755 is \alert{solved} by
+ − 756
+ − 757 \begin{center}
+ − 758 \begin{tabular}{ll}
+ − 759 \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma}\\[3mm]
+ − 760 \pgfuseshading{smallbluesphere} & and a set of freshness assumptions \smath{\nabla}
+ − 761 \end{tabular}
+ − 762 \end{center}
+ − 763
+ − 764 so that \smath{\nabla\vdash a \fresh \sigma(t)}.
+ − 765
+ − 766 \end{frame}}
+ − 767 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 768 *}
+ − 769
+ − 770 text_raw {*
+ − 771 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 772 \mode<presentation>{
+ − 773 \begin{frame}<1-3>
+ − 774 \frametitle{Existence of MGUs}
+ − 775
+ − 776 \underline{Theorem}: There is an algorithm which, given a nominal
+ − 777 unification problem \smath{P}, decides whether\\
+ − 778 or not it has a solution \smath{(\sigma,\nabla)}, and returns a \\
+ − 779 \alert{most general} one if it does.\bigskip\bigskip
+ − 780
+ − 781 \only<3>{
+ − 782 Proof: one can reduce all the equations to `solved form'
+ − 783 first (creating a substitution), and then solve the freshness
+ − 784 problems (easy).}
+ − 785
+ − 786 \only<2>{
+ − 787 \begin{textblock}{6}(2.5,9.5)
+ − 788 \begin{tikzpicture}
+ − 789 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 790 {\color{darkgray}
+ − 791 \begin{minipage}{8cm}\raggedright
+ − 792 \alert{most general:}\\
+ − 793 straightforward definition\\
+ − 794 ``if\hspace{-0.5mm}f there exists a \smath{\tau} such that \ldots''
+ − 795 \end{minipage}};
+ − 796 \end{tikzpicture}
+ − 797 \end{textblock}}
+ − 798
+ − 799 \end{frame}}
+ − 800 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 801 *}
+ − 802
+ − 803 text_raw {*
+ − 804 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 805 \mode<presentation>{
+ − 806 \begin{frame}<1>
+ − 807 \frametitle{Remember the Quiz?}
+ − 808
+ − 809 \textcolor{gray}{Assuming that $a$ and $b$ are distinct variables,\\
+ − 810 is it possible to find $\lambda$-terms $M_1$ to $M_7$
+ − 811 that make the following pairs $\alpha$-equivalent?}
+ − 812
+ − 813 \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
+ − 814 \begin{itemize}
+ − 815 \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and
+ − 816 \smath{\lambda b.\lambda a. (a\,M_1)\;}
+ − 817
+ − 818 \item \textcolor{gray}{$\lambda a.\lambda b. (M_2\,b)\;$ and
+ − 819 $\lambda b.\lambda a. (a\,M_3)\;$}
+ − 820
+ − 821 \item \textcolor{gray}{$\lambda a.\lambda b. (b\,M_4)\;$ and
+ − 822 $\lambda b.\lambda a. (a\,M_5)\;$}
+ − 823
+ − 824 \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and
+ − 825 \smath{\lambda a.\lambda a. (a\,M_7)\;}
+ − 826 \end{itemize}
+ − 827 \end{tabular}
+ − 828
+ − 829 \textcolor{gray}{If there is one solution for a pair, can you
+ − 830 describe all its solutions?}
+ − 831
+ − 832
+ − 833 \end{frame}}
+ − 834 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 835 *}
+ − 836
+ − 837 text_raw {*
+ − 838 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 839 \mode<presentation>{
+ − 840 \begin{frame}<1->
+ − 841 \frametitle{Answers to the Quiz}
+ − 842 \small
+ − 843 \def\arraystretch{1.6}
+ − 844 \begin{tabular}{c@ {\hspace{2mm}}l}
+ − 845 & \only<1>{\smath{\lambda a.\lambda b. (M_1\,b)\;} and \smath{\;\lambda b.\lambda a. (a\,M_1)}}%
+ − 846 \only<2->{\smath{\abst{a}{\abst{b}{\pair{M_1}{b}}} \;\eqprob\; \abst{b}{\abst{a}{\pair{a}{M_1}}}}}\\
+ − 847
+ − 848 \onslide<3->{\smath{\redu{\id}}} &
+ − 849 \only<3>{\smath{\abst{b}{\pair{M_1}{b}} \eqprob
+ − 850 \alert{\swap{a}{b}} \act \abst{a}{\pair{a}{M_1}}\;,\;a\freshprob \abst{a}{\pair{a}{M_1}}}}%
+ − 851 \only<4->{\smath{\abst{b}{\pair{M_1}{b}} \eqprob \abst{b}{\pair{b}{\swap{a}{b}\act M_1}}\;,\
+ − 852 a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+ − 853
+ − 854 \onslide<5->{\smath{\redu{\id}}} &
+ − 855 \only<5->{\smath{\pair{M_1}{b} \eqprob \pair{b}{\swap{a}{b}\act M_1}\;,\;%
+ − 856 a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+ − 857
+ − 858 \onslide<6->{\smath{\redu{\id}}} &
+ − 859 \only<6->{\smath{M_1 \eqprob b \;,\; b \eqprob \swap{a}{b}\act M_1\;,\;%
+ − 860 a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+ − 861
+ − 862 \onslide<7->{\smath{\redu{[M_1:=b]}}} &
+ − 863 \only<7>{\smath{b \eqprob \swap{a}{b}\act \alert{b}\;,\;%
+ − 864 a\freshprob \abst{a}{\pair{a}{\alert{b}}}}}%
+ − 865 \only<8->{\smath{b \eqprob a\;,\; a\freshprob \abst{a}{\pair{a}{b}}}}\\
+ − 866
+ − 867 \onslide<9->{\smath{\redu{}}} &
+ − 868 \only<9->{\smath{F\hspace{-0.5mm}AIL}}
+ − 869 \end{tabular}
+ − 870
+ − 871 \only<10>{
+ − 872 \begin{textblock}{6}(2,11)
+ − 873 \begin{tikzpicture}
+ − 874 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 875 {\color{darkgray}
+ − 876 \begin{minipage}{9cm}\raggedright
+ − 877 \smath{\lambda a.\lambda b. (M_1\,b)} \smath{=_\alpha}
+ − 878 \smath{\lambda b.\lambda a. (a\,M_1)} has no solution
+ − 879 \end{minipage}};
+ − 880 \end{tikzpicture}
+ − 881 \end{textblock}}
+ − 882
+ − 883 \end{frame}}
+ − 884 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 885 *}
+ − 886
+ − 887 text_raw {*
+ − 888 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 889 \mode<presentation>{
+ − 890 \begin{frame}<1->
+ − 891 \frametitle{Answers to the Quiz}
+ − 892 \small
+ − 893 \def\arraystretch{1.6}
+ − 894 \begin{tabular}{c@ {\hspace{2mm}}l}
+ − 895 & \only<1>{\smath{\lambda a.\lambda b. (b\,M_6)\;} and \smath{\;\lambda a.\lambda a. (a\,M_7)}}%
+ − 896 \only<2->{\smath{\abst{a}{\abst{b}{\pair{b}{M_6}}} \;\eqprob\; \abst{a}{\abst{a}{\pair{a}{M_7}}}}}\\
+ − 897
+ − 898 \onslide<3->{\smath{\redu{\id}}} &
+ − 899 \only<3->{\smath{\abst{b}{\pair{b}{M_6}} \eqprob \abst{a}{\pair{a}{M_7}}}}\\
+ − 900
+ − 901 \onslide<4->{\smath{\redu{\id}}} &
+ − 902 \only<4->{\smath{\pair{b}{M_6} \eqprob \pair{b}{\swap{b}{a}\act M_7}\;,\;b\freshprob\pair{a}{M_7}}}\\
+ − 903
+ − 904 \onslide<5->{\smath{\redu{\id}}} &
+ − 905 \only<5->{\smath{b\eqprob b\;,\; M_6 \eqprob \swap{b}{a}\act M_7\;,\;%
+ − 906 b\freshprob \pair{a}{M_7}}}\\
+ − 907
+ − 908 \onslide<6->{\smath{\redu{\id}}} &
+ − 909 \only<6->{\smath{M_6 \eqprob \swap{b}{a}\act M_7\;,\;%
+ − 910 b\freshprob \pair{a}{M_7}}}\\
+ − 911
+ − 912 \onslide<7->{\makebox[0mm]{\smath{\redu{[M_6:=\swap{b}{a}\act M_7]}}}} &
+ − 913 \only<7->{\smath{\qquad b\freshprob \pair{a}{M_7}}}\\
+ − 914
+ − 915 \onslide<8->{\smath{\redu{\varnothing}}} &
+ − 916 \only<8->{\smath{b\freshprob a\;,\;b\freshprob M_7}}\\
+ − 917
+ − 918 \onslide<9->{\smath{\redu{\varnothing}}} &
+ − 919 \only<9->{\smath{b\freshprob M_7}}\\
+ − 920
+ − 921 \onslide<10->{\makebox[0mm]{\smath{\redu{\{b\fresh M_7\}}}}} &
+ − 922 \only<10->{\smath{\;\;\varnothing}}\\
+ − 923
+ − 924 \end{tabular}
+ − 925
+ − 926 \only<10>{
+ − 927 \begin{textblock}{6}(6,9)
+ − 928 \begin{tikzpicture}
+ − 929 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 930 {\color{darkgray}
+ − 931 \begin{minipage}{7cm}\raggedright
+ − 932 \smath{\lambda a.\lambda b. (b\,M_6)\;} \smath{=_\alpha}
+ − 933 \smath{\;\lambda a.\lambda a. (a\,M_7)}\\[2mm]
+ − 934 we can take \smath{M_7} to be any $\lambda$-term that does not
+ − 935 contain free occurrences of \smath{b}, so long as we take \smath{M_6} to
+ − 936 be the result of swapping all occurrences of \smath{b} and \smath{a}
+ − 937 throughout \smath{M_7}
+ − 938 \end{minipage}};
+ − 939 \end{tikzpicture}
+ − 940 \end{textblock}}
+ − 941
+ − 942 \end{frame}}
+ − 943 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 944 *}
+ − 945
+ − 946 text_raw {*
+ − 947 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 948 \mode<presentation>{
+ − 949 \begin{frame}<1->
+ − 950 \frametitle{Properties}
+ − 951
+ − 952 \begin{itemize}
+ − 953 \item An interesting feature of nominal unification is that it
+ − 954 does not need to create new atoms.\bigskip
+ − 955
+ − 956 \begin{center}\small
+ − 957 \colorbox{cream}{
+ − 958 \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id} \{t \eqprob \swap{a}{b}\act t', a \freshprob t'\} \cup P}}
+ − 959 \end{center}\bigskip\bigskip
+ − 960 \pause
+ − 961
+ − 962 \item The alternative rule
+ − 963
2358
+ − 964 \begin{center}\small
+ − 965 \colorbox{cream}{
+ − 966 \begin{tabular}{@ {}l@ {}}
+ − 967 \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id}}\\
+ − 968 \mbox{}\hspace{2cm}\smath{\{\swap{a}{c}\act t \eqprob
+ − 969 \swap{b}{c}\act t', c \freshprob t, c \freshprob t'\} \cup P}
+ − 970 \end{tabular}}
+ − 971 \end{center}
2357
+ − 972
2358
+ − 973 leads to a more complicated notion of mgu.\medskip\pause
+ − 974
+ − 975 \footnotesize
+ − 976 \smath{\{a.X \eqprob b.Y\} \redu{} (\{a\fresh Y, c\fresh Y\}, [X:=\swap{a}{c}\swap{b}{c}\act Y])}
2357
+ − 977 \end{itemize}
+ − 978
+ − 979 \end{frame}}
+ − 980 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 981 *}
+ − 982
+ − 983 text_raw {*
+ − 984 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 985 \mode<presentation>{
+ − 986 \begin{frame}<1-3>
+ − 987 \frametitle{Is it Useful?}
+ − 988
+ − 989 Yes. $\alpha$Prolog by James Cheney (main developer)\bigskip\bigskip
+ − 990
+ − 991 \color{darkgray}
+ − 992 \begin{tabular}{@ {}l}
+ − 993 type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\
+ − 994
+ − 995 type (Gamma, app(M, N), T') :-\\
+ − 996 \hspace{3cm}type (Gamma, M, arrow(T, T')),\\
+ − 997 \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\
+ − 998
+ − 999 type (Gamma, lam(\alert{x.M}), arrow(T, T')) / \alert{x \# Gamma} :-\\
+ − 1000 \hspace{3cm}type ((x, T)::Gamma, M, T').\smallskip\medskip\\
+ − 1001
+ − 1002 member X X::Tail.\\
+ − 1003 member X Y::Tail :- member X Tail.\\
+ − 1004 \end{tabular}
+ − 1005
+ − 1006 \only<2->{
+ − 1007 \begin{textblock}{6}(1.5,0.5)
+ − 1008 \begin{tikzpicture}
+ − 1009 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 1010 {\color{darkgray}
+ − 1011 \begin{minipage}{9cm}\raggedright
2358
+ − 1012 {\bf One problem:} If we ask whether
2357
+ − 1013
+ − 1014 \begin{center}
+ − 1015 ?- type ([(x, T')], lam(x.Var(x)), T)
+ − 1016 \end{center}
+ − 1017
+ − 1018 is typable, we expect an answer for T.\bigskip
+ − 1019
+ − 1020 \onslide<3>{Solution: Before back-chaining freshen all variables and atoms
+ − 1021 in a program (clause).}
+ − 1022 \end{minipage}};
+ − 1023 \end{tikzpicture}
+ − 1024 \end{textblock}}
+ − 1025
+ − 1026 \end{frame}}
+ − 1027 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1028 *}
+ − 1029
+ − 1030 text_raw {*
+ − 1031 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1032 \mode<presentation>{
+ − 1033 \begin{frame}<1->
+ − 1034 \frametitle{Equivariant Unification}
+ − 1035
2358
+ − 1036 James Cheney proposed
2357
+ − 1037
+ − 1038 \begin{center}
+ − 1039 \colorbox{cream}{
+ − 1040 \smath{t \eqprob t' \redu{\nabla, \sigma, \pi}
+ − 1041 \nabla \vdash \sigma(t) \approx \pi \act \sigma(t')}}
+ − 1042 \end{center}\bigskip\bigskip
+ − 1043 \pause
+ − 1044
2358
+ − 1045 But he also showed this problem is undecidable\\ in general. :(
2357
+ − 1046
+ − 1047 \end{frame}}
+ − 1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1049 *}
+ − 1050
+ − 1051 text_raw {*
+ − 1052 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1053 \mode<presentation>{
+ − 1054 \begin{frame}<1->
+ − 1055 \frametitle{Taking Atoms as Variables}
+ − 1056
+ − 1057 Instead of \smath{a.X}, have \smath{A.X}.\bigskip
+ − 1058 \pause
+ − 1059
+ − 1060 Unfortunately this breaks the mgu-property:
+ − 1061
+ − 1062 \begin{center}
2358
+ − 1063 \smath{a.Z \eqprob X.Y.v(a)}
+ − 1064 \end{center}
+ − 1065
+ − 1066 can be solved by
+ − 1067
+ − 1068 \begin{center}
+ − 1069 \smath{[X:=a, Z:=Y.v(a)]} and
+ − 1070 \smath{[Y:=a, Z:=Y.v(Y)]}
2357
+ − 1071 \end{center}
+ − 1072
+ − 1073 \end{frame}}
+ − 1074 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1075 *}
+ − 1076
+ − 1077 text_raw {*
+ − 1078 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1079 \mode<presentation>{
2358
+ − 1080 \begin{frame}<1>[c]
2357
+ − 1081 \frametitle{HOPU vs. NOMU}
+ − 1082
+ − 1083 \begin{itemize}
+ − 1084 \item James Cheney showed\bigskip
+ − 1085 \begin{center}
+ − 1086 \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}}
+ − 1087 \end{center}\bigskip
+ − 1088
2358
+ − 1089 \item Jordi Levy and Mateu Villaret established\bigskip
2357
+ − 1090 \begin{center}
+ − 1091 \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}}
+ − 1092 \end{center}\bigskip
+ − 1093 \end{itemize}
+ − 1094
+ − 1095 The translations `explode' the problems quadratically.
+ − 1096
+ − 1097 \end{frame}}
+ − 1098 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1099 *}
+ − 1100
+ − 1101 text_raw {*
+ − 1102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1103 \mode<presentation>{
+ − 1104 \begin{frame}<1>
+ − 1105 \small\tt
+ − 1106
+ − 1107 \begin{minipage}{13cm}
+ − 1108 \begin{tabular}{@ {\hspace{-2mm}}p{11.5cm}}
+ − 1109 \\
+ − 1110 From: Zhenyu Qian <zhqian@microsoft.com>\\
+ − 1111 To: Christian Urban <urbanc@in.tum.de>\\
+ − 1112 Subject: RE: Linear Higher-Order Pattern Unification\\
+ − 1113 Date: Mon, 14 Apr 2008 09:56:47 +0800\\
+ − 1114 \\
+ − 1115 Hi Christian,\\
+ − 1116 \\
+ − 1117 Thanks for your interests and asking. I know that that paper is complex. As
+ − 1118 I told Tobias when we met last time, I have raised the question to myself
+ − 1119 many times whether the proof could have some flaws, and so making it through
+ − 1120 a theorem prover would definitely bring piece to my mind (no matter what
+ − 1121 the result would be). The only problem for me is the time.\\
+ − 1122 \ldots\\
+ − 1123
+ − 1124 Thanks/Zhenyu
+ − 1125 \end{tabular}
+ − 1126 \end{minipage}
+ − 1127
+ − 1128 \end{frame}}
+ − 1129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1130 *}
+ − 1131
+ − 1132 text_raw {*
+ − 1133 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1134 \mode<presentation>{
+ − 1135 \begin{frame}<1>
+ − 1136 \frametitle{Complexity}
+ − 1137
+ − 1138 \begin{itemize}
2358
+ − 1139 \item Christiopher Calves and Maribel Fernandez showed first that
+ − 1140 it is polynomial and then also quadratic
2357
+ − 1141
2358
+ − 1142 \item Jordi Levy and Mateu Villaret showed that it is quadratic
+ − 1143 by a translation into a subset of NOMU and using ideas from
+ − 1144 Martelli/Montenari.
2357
+ − 1145
+ − 1146 \end{itemize}
+ − 1147
+ − 1148 \end{frame}}
+ − 1149 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1150 *}
+ − 1151
+ − 1152
+ − 1153 text_raw {*
+ − 1154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1155 \mode<presentation>{
+ − 1156 \begin{frame}<1->[c]
2356
+ − 1157 \frametitle{Conclusion}
2351
+ − 1158
+ − 1159 \begin{itemize}
2357
+ − 1160 \item Nominal Unification is a completely first-order
2358
+ − 1161 language, but implements unification modulo $\alpha$.
+ − 1162 \textcolor{gray}{(verification\ldots Ramana Kumar and Michael Norrish)}
+ − 1163 \medskip\pause
2351
+ − 1164
2357
+ − 1165 \item NOMU has been applied in term-rewriting and
2358
+ − 1166 logic programming. \textcolor{gray}{(Maribel Fernandez et
+ − 1167 al has a KB-completion procedure.)}
+ − 1168 I hope it will also be used in typing
2357
+ − 1169 systems.\medskip\pause
+ − 1170
+ − 1171 \item NOMU and HOPU are `equivalent' (it took a long time
2358
+ − 1172 and considerable research to find this out).\medskip\pause
2357
+ − 1173
+ − 1174 \item The question about complexity is still an ongoing
+ − 1175 story.\medskip
2351
+ − 1176 \end{itemize}
+ − 1177
+ − 1178
+ − 1179 \end{frame}}
+ − 1180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1181 *}
+ − 1182
2357
+ − 1183 text_raw {*
+ − 1184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1185 \mode<presentation>{
+ − 1186 \begin{frame}<1>[c]
+ − 1187 \frametitle{
+ − 1188 \begin{tabular}{c}
+ − 1189 \mbox{}\\[23mm]
2358
+ − 1190 \alert{\LARGE Thank you very much!}\\
2357
+ − 1191 \alert{\Large Questions?}
+ − 1192 \end{tabular}}
+ − 1193
+ − 1194 \end{frame}}
+ − 1195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1196 *}
+ − 1197
+ − 1198 text_raw {*
+ − 1199 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1200 \mode<presentation>{
+ − 1201 \begin{frame}<1-3>
+ − 1202 \frametitle{Most General Unifiers}
+ − 1203
+ − 1204 \underline{Definition}: For a unification problem
+ − 1205 \smath{P}, a solution \smath{(\sigma_1,\nabla_1)} is
+ − 1206 \alert{more general} than another solution
+ − 1207 \smath{(\sigma_2,\nabla_2)}, iff~there exists a substitution
+ − 1208 \smath{\tau} with
+ − 1209
+ − 1210 \begin{center}
+ − 1211 \begin{tabular}{ll}
+ − 1212 \pgfuseshading{smallbluesphere} &
+ − 1213 \alt<2>{\smath{\alert{\nabla_2\vdash\tau(\nabla_1)}}}
+ − 1214 {\smath{\nabla_2\vdash\tau(\nabla_1)}}\\
+ − 1215 \pgfuseshading{smallbluesphere} &
+ − 1216 \alt<3>{\smath{\alert{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}}
+ − 1217 {\smath{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}
+ − 1218 \end{tabular}
+ − 1219 \end{center}
+ − 1220
+ − 1221 \only<2>{
+ − 1222 \begin{textblock}{13}(1.5,10.5)
+ − 1223 \smath{\nabla_2\vdash a\fresh \sigma(X)} holds for all
+ − 1224 \smath{(a\fresh X)\in\nabla_1}
+ − 1225 \end{textblock}}
+ − 1226
+ − 1227 \only<3>{
+ − 1228 \begin{textblock}{11}(1.5,10.5)
+ − 1229 \smath{\nabla_2\vdash \sigma_2(X)\approx
+ − 1230 \sigma(\sigma_1(X))}
+ − 1231 holds for all
+ − 1232 \smath{X\in\text{dom}(\sigma_2)\cup\text{dom}(\sigma\circ\sigma_1)}
+ − 1233 \end{textblock}}
+ − 1234
+ − 1235 \end{frame}}
+ − 1236 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1237 *}
+ − 1238
2351
+ − 1239 (*<*)
+ − 1240 end
+ − 1241 (*>*)