1 (*<*)

     2 theory Slides3

     3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"

     4 begin

     5 

     6 declare [[show_question_marks = false]]

     7 

     8 notation (latex output)

     9   set ("_") and

    10   Cons  ("_::/_" [66,65] 65) 

    11 

    12 (*>*)

    13 

    14 text_raw {*

    15   \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}

    16 

    17   \newcommand{\abst}[2]{#1.#2}% atom-abstraction

    18   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing

    19   \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions

    20   \newcommand{\unit}{\langle\rangle}% unit

    21   \newcommand{\app}[2]{#1\,#2}% application

    22   \newcommand{\eqprob}{\mathrel{{\approx}?}}

    23   \newcommand{\freshprob}{\mathrel{\#?}}

    24   \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction

    25   \newcommand{\id}{\varepsilon}% identity substitution

    26 

    27   \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%

    28   {rgb(0mm)=(0,0,0.9);

    29   rgb(0.9mm)=(0,0,0.7);

    30   rgb(1.3mm)=(0,0,0.5);

    31   rgb(1.4mm)=(1,1,1)}

    32 

    33   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    34   \mode<presentation>{

    35   \begin{frame}<1>[c]

    36   \frametitle{Quiz}

    37   

    38   Assuming that \smath{a} and \smath{b} are distinct variables,\\

    39   is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7} 

    40   that make the following pairs \alert{$\alpha$-equivalent}?

    41 

    42   \begin{tabular}{@ {\hspace{14mm}}p{12cm}}

    43   \begin{itemize}

    44   \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 

    45         \smath{\lambda b.\lambda a. (a\,M_1)\;}

    46 

    47   \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and 

    48         \smath{\lambda b.\lambda a. (a\,M_3)\;}

    49 

    50   \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and 

    51         \smath{\lambda b.\lambda a. (a\,M_5)\;}

    52 

    53   \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 

    54         \smath{\lambda a.\lambda a. (a\,M_7)\;}

    55   \end{itemize}

    56   \end{tabular}

    57 

    58   If there is one solution for a pair, can you describe all its solutions?

    59 

    60   \end{frame}}

    61   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    62 *}

    63 

    64 text_raw {*

    65   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    66   \mode<presentation>{

    67   \begin{frame}<1>[t]

    68   \frametitle{%

    69   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}

    70   \\

    71   \huge Nominal Unification\\[-2mm] 

    72   \Large Hitting a Sweet Spot\\[5mm]

    73   \end{tabular}}

    74   \begin{center}

    75   Christian Urban

    76   \end{center}

    77   \begin{center}

    78   \small initial spark from Roy Dyckhoff in November 2001\\[0mm] 

    79   \small joint work with Andy Pitts and Jamie Gabbay\\[0mm] 

    80   \end{center}

    81   \end{frame}}

    82   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    83 

    84 *}

    85 text_raw {*

    86   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    87   \mode<presentation>{

    88   \begin{frame}<1-4>[c]

    89   \frametitle{One Motivation}

    90 

    91   \onslide<2->{Typing implemented in Prolog \textcolor{darkgray}{(from a textbook)}}\bigskip\\

    92 

    93   \onslide<3->{\color{darkgray}

    94   \begin{tabular}{l}

    95   type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\

    96   

    97   type (Gamma, app(M, N), T') :-\\

    98   \hspace{3cm}type (Gamma, M, arrow(T, T')),\\ 

    99   \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\

   100   

   101   type (Gamma, lam(X, M), arrow(T, T')) :-\\

   102   \hspace{3cm}type ((X, T)::Gamma, M, T').\smallskip\medskip\\

   103   

   104   member X X::Tail.\\

   105   member X Y::Tail :- member X Tail.\\

   106   \end{tabular}}

   107  

   108   \only<4>{

   109   \begin{textblock}{6}(2.5,2)

   110   \begin{tikzpicture}

   111   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   112   {\color{darkgray}

   113   \begin{minipage}{8cm}\raggedright

   114   The problem is that \smath{\lambda x.\lambda x. (x\;x)}

   115   will have the types

   116   \begin{center}

   117   \begin{tabular}{l}

   118   \smath{T\rightarrow (T\rightarrow S) \rightarrow S} and\\ 

   119   \smath{(T\rightarrow S)\rightarrow T \rightarrow S}\\

   120   \end{tabular}

   121   \end{center}

   122   \end{minipage}};

   123   \end{tikzpicture}

   124   \end{textblock}}

   125   

   126   \end{frame}}

   127   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   128 *}

   129 

   130 text_raw {*

   131   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   132   \mode<presentation>{

   133   \begin{frame}<1>[c]

   134   \frametitle{Higher-Order Unification}

   135 

   136   State of the art at the time:

   137 

   138   \begin{itemize}

   139   \item Lambda Prolog with full Higher-Order Unification\\ 

   140   \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip

   141   \item Higher-Order Pattern Unification\\ 

   142   \textcolor{darkgray}{(has mgus, decidable, some restrictions, modulo $\alpha\beta_0$)}

   143   \end{itemize}

   144  

   145   \end{frame}}

   146   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   147 *}

   148 

   149 text_raw {*

   150   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   151   \mode<presentation>{

   152   \begin{frame}<1-10>[t]

   153   \frametitle{Underlying Ideas}

   154 

   155   \begin{itemize}

   156   \item<1-> Unification (\alert{only}) up to $\alpha$

   157 

   158   \item<2-> Swappings / Permutations

   159 

   160   \only<2-5>{

   161   \begin{center}

   162   \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{12mm}}r@ {\hspace{1mm}}l}

   163   \\

   164   \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%

   165   \only<3>{\smath{[b\!:=\!a]}}%

   166   \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} & 

   167   \onslide<2-5>{\smath{\lambda a.b}} &

   168   

   169   \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%

   170   \only<3>{\smath{[b\!:=\!a]}}%

   171   \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} &

   172   \onslide<2-5>{\smath{\lambda c.b}}\\

   173 

   174   \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda a.a}}\only<4-5>{\smath{\lambda b.a}} & 

   175   \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda c.a}}\only<4-5>{\smath{\lambda c.a}}\\

   176   \end{tabular}

   177   \end{center}\bigskip

   178 

   179   \onslide<4-5>{

   180   \begin{center}

   181   \begin{tikzpicture}

   182   \draw (0,0) node[inner sep=0mm,fill=cream, ultra thick, draw=cream] 

   183   {\begin{minipage}{8cm}

   184   \begin{tabular}{r@ {\hspace{3mm}}l}

   185   \smath{\swap{a}{b}\act t} $\;\dn$ & \alert{swap} {\bf all} occurrences of\\ 

   186                                   & \smath{b} and \smath{a} in \smath{t}

   187   \end{tabular}

   188   \end{minipage}};

   189   \end{tikzpicture}

   190   \end{center}}\bigskip

   191 

   192   \onslide<5>{

   193   Unlike for \smath{[b\!:=\!a]\act(-)}, for \smath{\swap{a}{b}\act (-)} we do

   194   have if \smath{t =_\alpha t'} then \smath{\pi \act t =_\alpha \pi \act t'.}}}

   195 

   196   \item<6-> Variables (or holes)\bigskip

   197 

   198   \begin{center}

   199   \onslide<7->{\mbox{}\hspace{-25mm}\smath{\lambda x\hspace{-0.5mm}s .}}

   200   \onslide<8-9>{\raisebox{-1.7mm}{\huge\smath{(}}}\raisebox{-4mm}{\begin{tikzpicture}

   201   \fill[blue] (0, 0) circle (5mm);

   202   \end{tikzpicture}}

   203   \onslide<8-9>{\smath{y\hspace{-0.5mm}s}{\raisebox{-1.7mm}{\huge\smath{)}}}}\bigskip

   204   \end{center}

   205 

   206   \only<8-9>{\smath{y\hspace{-0.5mm}s} are the parameters the hole can depend on\onslide<9->{, but 

   207   then you need $\beta_0$-reduction\medskip

   208   \begin{center}

   209   \smath{(\lambda x. t) y \longrightarrow_{\beta_0} t[x:=y]}

   210   \end{center}}}

   211 

   212   \only<10>{we will record the information about which parameters a hole 

   213   \alert{\bf cannot} depend on}

   214 

   215   \end{itemize}

   216   

   217   \end{frame}}

   218   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   219 *}

   220 

   221 text_raw {*

   222   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   223   \mode<presentation>{

   224   \begin{frame}<1-4>[c]

   225   \frametitle{Terms}

   226 

   227   \begin{tabular}{lll @ {\hspace{10mm}}lll}

   228 

   229   \onslide<1->{\pgfuseshading{smallbluesphere}} & 

   230   \onslide<1->{\colorbox{cream}{\smath{\unit}}} &

   231   \onslide<1->{Units} &

   232 

   233   \onslide<2->{\pgfuseshading{smallbluesphere}} &

   234   \onslide<2->{\colorbox{cream}{\smath{a}}} &

   235   \onslide<2->{Atoms} \\[5mm]

   236 

   237   \onslide<1->{\pgfuseshading{smallbluesphere}} & 

   238   \onslide<1->{\colorbox{cream}{\smath{\pair{t}{t'}}}} &

   239   \onslide<1->{Pairs} &

   240   

   241   \onslide<3->{\pgfuseshading{smallbluesphere}} &

   242   \onslide<3->{\colorbox{cream}{\smath{\abst{a}{t}}}} &

   243   \onslide<3->{Abstractions}\\[5mm]

   244 

   245   \onslide<1->{\pgfuseshading{smallbluesphere}} & 

   246   \onslide<1->{\colorbox{cream}{\smath{\app{F}{t}}}} &

   247   \onslide<1->{Funct.} &

   248 

   249   \onslide<4->{\pgfuseshading{smallbluesphere}} &

   250   \onslide<4->{\colorbox{cream}{\smath{\pi\susp X}}} &

   251   \onslide<4->{Suspensions}

   252   \end{tabular}

   253  

   254   \only<2>{

   255   \begin{textblock}{13}(1.5,12)

   256   \small Atoms are constants \textcolor{darkgray}{(infinitely many of them)}

   257   \end{textblock}}

   258 

   259   \only<3>{

   260   \begin{textblock}{13}(1.5,12)

   261   \small \smath{\ulcorner \lambda\abst{a}{a}\urcorner \mapsto \text{fn\ }\abst{a}{a}}\\

   262   \small constructions like \smath{\text{fn\ }\abst{X}{X}} are not allowed

   263   \end{textblock}}

   264 

   265   \only<4>{

   266   \begin{textblock}{13}(1.5,12)

   267   \small \smath{X} is a variable standing for a term\\

   268   \small \smath{\pi} is an explicit permutation \smath{\swap{a_1}{b_1}\ldots\swap{a_n}{b_n}},

   269   waiting to be applied to the term that is substituted for \smath{X}

   270   \end{textblock}}

   271 

   272   \end{frame}}

   273   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   274 *}

   275 

   276 text_raw {*

   277   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   278   \mode<presentation>{

   279   \begin{frame}<1-3>[c]

   280   \frametitle{Permutations}

   281 

   282   a permutation applied to a term

   283 

   284   \begin{center}

   285   \begin{tabular}{lrcl}

   286   \pgfuseshading{smallbluesphere} &

   287   \smath{[]\act c} & \smath{\dn} & \smath{c} \\

   288 

   289   \pgfuseshading{smallbluesphere} &

   290   \smath{\swap{a}{b}\!::\!\pi\act c} & \smath{\dn} & 

   291   \smath{\begin{cases} 

   292   a & \text{if}\;\pi\act c = b\\

   293   b & \text{if}\;\pi\act c = a\\

   294   \pi\act c & \text{otherwise}

   295   \end{cases}}\\

   296 

   297   \onslide<2->{\pgfuseshading{smallbluesphere}} &

   298   \onslide<2->{\smath{\pi\act\abst{a}{t}}} & \onslide<2->{\smath{\dn}} & 

   299   \onslide<2->{\smath{\abst{\pi\act a}{\pi\act t}}}\\ 

   300 

   301   \onslide<3->{\pgfuseshading{smallbluesphere}} &

   302   \onslide<3->{\smath{\pi\act\pi'\act X}} & \onslide<3->{\smath{\dn}} & 

   303   \onslide<3->{\smath{(\pi @ \pi')\act X}}\\

   304   \end{tabular}

   305   \end{center}

   306 

   307   \end{frame}}

   308   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   309 *}

   310 

   311 text_raw {*

   312   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   313   \mode<presentation>{

   314   \begin{frame}<1-3>[c]

   315   \frametitle{Freshness Constraints}

   316 

   317   Recall \smath{\lambda a. \raisebox{-0.7mm}{\tikz \fill[blue] (0, 0) circle (2.5mm);}}

   318   \bigskip\pause

   319 

   320   We therefore will identify

   321 

   322   \begin{center}

   323   \smath{\text{fn\ } a. X \;\approx\; \text{fn\ } b. \alert<3->{\swap{a}{b}}\act X}

   324   \end{center}

   325 

   326   provided that `\smath{b} is fresh for \smath{X} --- (\smath{b\fresh X})',

   327   i.e., does not occur freely in any ground term that might be substituted for

   328   \smath{X}.\bigskip\pause 

   329 

   330   If we know more about \smath{X}, e.g., if we knew that \smath{a\fresh X} and

   331   \smath{b\fresh X}, then we can replace\\ \smath{\swap{a}{b}\act X} by

   332   \smath{X}.

   333 

   334   \end{frame}}

   335   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   336 *}

   337 

   338 text_raw {*

   339   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   340   \mode<presentation>{

   341   \begin{frame}<1-4>[c]

   342   \frametitle{Equivalence Judgements}

   343 

   344   \alt<1>{Our equality is {\bf not} just}{but judgements}

   345 

   346   \begin{center}

   347   \begin{tabular}{rl}

   348   \colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} t \approx t'}} & \alert{$\alpha$-equivalence}\\[1mm]

   349   \onslide<4->{\colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} a \fresh t}}} & 

   350   \onslide<4->{\alert{freshness}}

   351   \end{tabular}

   352   \end{center}

   353 

   354   \onslide<2->{

   355   where

   356   \begin{center}

   357   \smath{\nabla = \{a_1\fresh X_1,\ldots, a_n\fresh X_n\}}

   358   \end{center}

   359   is a finite set of \alert{freshness assumptions}.}

   360 

   361   \onslide<3->{

   362   \begin{center}

   363   \smath{\{a\fresh X,b\fresh X\} \vdash \text{fn\ } a. X \approx \text{fn\ } b. X}

   364   \end{center}}

   365 

   366   \end{frame}}

   367   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   368 *}

   369 

   370 text_raw {*

   371   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   372   \mode<presentation>{

   373   \begin{frame}<1>[c]

   374   \frametitle{Rules for Equivalence}

   375 

   376   \begin{center}

   377   \begin{tabular}{c}

   378   Excerpt\\

   379   (i.e.~only the interesting rules)

   380   \end{tabular}

   381   \end{center}  

   382 

   383   \end{frame}}

   384   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   385 *}

   386 

   387 text_raw {*

   388   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   389   \mode<presentation>{

   390   \begin{frame}<1>[c]

   391   \frametitle{Rules for Equivalence}

   392 

   393   \begin{center}

   394   \begin{tabular}{c}

   395   \colorbox{cream}{\smath{\infer{\nabla \vdash a \approx a}{}}}\\[8mm]

   396 

   397   \colorbox{cream}{%

   398   \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{a}{t'}}

   399                {\nabla \vdash t \approx t'}}}\\[8mm]

   400  

   401   \colorbox{cream}{%

   402   \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{b}{t'}}

   403   {a\not=b\;\; & \nabla \vdash t \approx \swap{a}{b}\act t'\;\;& \nabla \vdash a\fresh t'}}}

   404   \end{tabular}

   405   \end{center}

   406 

   407   \end{frame}}

   408   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   409 *}

   410 

   411 text_raw {*

   412   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   413   \mode<presentation>{

   414   \begin{frame}<1-3>[c]

   415   \frametitle{Rules for Equivalence}

   416 

   417   \begin{center}

   418   \colorbox{cream}{%

   419   \smath{%

   420   \infer{\nabla \vdash \pi\act X \approx \pi'\act X}

   421   {\begin{array}{c}

   422   (a\fresh X)\in\nabla\\

   423   \text{for all}\; a \;\text{with}\;\pi\act a \not= \pi'\act a 

   424   \end{array}

   425   }}}

   426   \end{center}

   427 

   428   \onslide<2->{

   429   for example\\[4mm]

   430   

   431   \alt<2>{%

   432   \begin{center}

   433   \smath{\{a\fresh\!X, b\fresh\!X\} \vdash X \approx \swap{a}{b}\act X}

   434   \end{center}}

   435   {%

   436   \begin{center}

   437   \smath{\{a\fresh\!X, c\fresh\!X\} \vdash \swap{a}{c}\swap{a}{b}\act X \approx \swap{b}{c}\act X}

   438   \end{center}}

   439 

   440   \onslide<3->{

   441   \begin{tabular}{@ {}lllll@ {}}

   442   because & 

   443   \smath{\swap{a}{c}\swap{a}{b}}: & 

   444   \smath{a\mapsto b} &

   445   \smath{\swap{b}{c}}: &

   446   \smath{a\mapsto a}\\

   447   & & \smath{b\mapsto c} & & \smath{b\mapsto c}\\

   448   & & \smath{c\mapsto a} & & \smath{c\mapsto b}\\

   449   \end{tabular}

   450   disagree at \smath{a} and \smath{c}.}

   451   }

   452 

   453   \end{frame}}

   454   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   455 *}

   456 

   457 text_raw {*

   458   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   459   \mode<presentation>{

   460   \begin{frame}<1>[c]

   461   \frametitle{Rules for Freshness}

   462 

   463   \begin{center}

   464   \begin{tabular}{c}

   465   Excerpt\\

   466   (i.e.~only the interesting rules)

   467   \end{tabular}

   468   \end{center}  

   469 

   470   \end{frame}}

   471   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   472 *}

   473 

   474 text_raw {*

   475   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   476   \mode<presentation>{

   477   \begin{frame}<1>[c]

   478   \frametitle{Rules for Freshness}

   479 

   480   \begin{center}

   481   \begin{tabular}{c}

   482   \colorbox{cream}{%

   483   \smath{\infer{\nabla \vdash a\fresh b}{a\not= b}}}\\[5mm]

   484   

   485   \colorbox{cream}{%

   486   \smath{\infer{\nabla \vdash a\fresh\abst{a}{t}}{}}}\hspace{7mm}

   487   \colorbox{cream}{%

   488   \smath{\infer{\nabla \vdash a\fresh\abst{b}{t}}

   489   {a\not= b\;\; & \nabla \vdash a\fresh t}}}\\[5mm]

   490 

   491   \colorbox{cream}{%

   492   \smath{\infer{\nabla \vdash a\fresh \pi\act X}

   493   {(\pi^{-1}\act a\fresh X)\in\nabla}}}

   494   \end{tabular}

   495   \end{center}

   496 

   497   \end{frame}}

   498   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   499 *}

   500 

   501 text_raw {*

   502   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   503   \mode<presentation>{

   504   \begin{frame}<1-4>[t]

   505   \frametitle{$\approx$ is an Equivalence}

   506   \mbox{}\\[5mm]

   507 

   508   \begin{center}

   509   \colorbox{cream}{\alert{Theorem:}

   510   $\approx$ is an equivalence relation.}

   511   \end{center}\bigskip

   512 

   513   \only<1>{%

   514   \begin{tabular}{ll}

   515   (Reflexivity)  & $\smath{\nabla\vdash t\approx t}$\\[2mm]

   516   (Symmetry)     & if $\smath{\nabla\vdash t_1\approx t_2}\;$ 

   517                    then $\;\smath{\nabla\vdash t_2\approx t_1}$\\[2mm]

   518   (Transitivity) & if $\smath{\nabla\vdash t_1\approx t_2}\;$ and 

   519                    $\;\smath{\nabla\vdash t_2\approx t_3}$\\

   520                  & then $\smath{\nabla\vdash t_1\approx t_3}$\\

   521   \end{tabular}}

   522 

   523   \only<2->{%

   524   \begin{itemize}

   525   \item<2-> \smath{\nabla \vdash t\approx t'} then \smath{\nabla \vdash \pi\act t\approx \pi\act t'}

   526 

   527   \item<2-> \smath{\nabla \vdash a\fresh t} then 

   528   \smath{\nabla \vdash \pi\act a\fresh \pi\act t}

   529 

   530   \item<3-> \smath{\nabla \vdash t\approx \pi\act t'} then 

   531   \smath{\nabla \vdash (\pi^{-1})\act t\approx t'}

   532 

   533   \item<3-> \smath{\nabla \vdash a\fresh \pi\act t} then 

   534   \smath{\nabla \vdash (\pi^{-1})\act a\fresh t}

   535 

   536   \item<4-> \smath{\nabla \vdash a\fresh t} and \smath{\nabla \vdash t\approx t'} then

   537       \smath{\nabla \vdash a\fresh t'}

   538   \end{itemize}

   539   }

   540 

   541   \end{frame}}

   542   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   543 *}

   544 

   545 text_raw {*

   546   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   547   \mode<presentation>{

   548   \begin{frame}<1-4>

   549   \frametitle{Comparison $=_\alpha$}

   550 

   551   Traditionally \smath{=_\alpha} is defined as

   552 

   553   \begin{center}

   554   \colorbox{cream}{%

   555   \begin{minipage}{9cm}

   556   \raggedright least congruence which identifies \smath{\abst{a}{t}} 

   557   with \smath{\abst{b}{[a:=b]t}} provided \smath{b} is not free  

   558   in \smath{t}

   559   \end{minipage}}

   560   \end{center}

   561 

   562   where \smath{[a:=b]t} replaces all free occurrences of\\

   563   \smath{a} by \smath{b} in \smath{t}.

   564   \bigskip 

   565 

   566   \only<2>{%

   567   \begin{textblock}{13}(1.2,10)

   568   For \alert{ground} terms:

   569   

   570   \begin{center}

   571   \colorbox{cream}{%

   572   \begin{minipage}{9.0cm}

   573   \begin{tabular}{@ {}rl}

   574   \underline{Theorem:}

   575   & \smath{t=_\alpha t'\;\;}  if\hspace{-0.5mm}f~\smath{\;\;\emptyset \vdash t\approx t'}\\[2mm]

   576   & \smath{a\not\in F\hspace{-0.9mm}A(t)\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset\vdash a\fresh t} 

   577   \end{tabular}

   578   \end{minipage}}

   579   \end{center}

   580   \end{textblock}}

   581 

   582   \only<3>{%

   583   \begin{textblock}{13}(1.2,10)

   584   In general \smath{=_\alpha} and \smath{\approx} are distinct!

   585   \begin{center}

   586   \colorbox{cream}{%

   587   \begin{minipage}{6.0cm}

   588   \smath{\abst{a}{X}=_\alpha \abst{b}{X}\;} but not\\[2mm]

   589   \smath{\emptyset \vdash \abst{a}{X} \approx \abst{b}{X}\;} (\smath{a\not=b})

   590   \end{minipage}}

   591   \end{center}

   592   \end{textblock}}

   593 

   594   \only<4>{

   595   \begin{textblock}{6}(1,2)

   596   \begin{tikzpicture}

   597   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   598   {\color{darkgray}

   599   \begin{minipage}{10cm}\raggedright

   600   That is a crucial point: if we had\\[-2mm]

   601   \[\smath{\emptyset \vdash \abst{a}{X}\approx \abst{b}{X}}\mbox{,}\] 

   602   then applying $\smath{[X:=a]}$, $\smath{[X:=b]}$, $\ldots$\\

   603   give two terms that are {\bf not} $\alpha$-equivalent.\\[3mm] 

   604   The freshness constraints $\smath{a\fresh X}$ and $\smath{b\fresh X}$

   605   rule out the problematic substitutions. Therefore

   606 

   607   \[\smath{\{a\fresh X,b\fresh X\} \vdash \abst{a}{X}\approx \abst{b}{X}}\] 

   608   

   609   does hold.

   610   \end{minipage}};

   611   \end{tikzpicture}

   612   \end{textblock}}

   613 

   614   \end{frame}}

   615   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   616 *}

   617 

   618 text_raw {*

   619   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   620   \mode<presentation>{

   621   \begin{frame}<1-9>

   622   \frametitle{Substitution}

   623 

   624   \begin{tabular}{l@ {\hspace{8mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {}}

   625   \pgfuseshading{smallbluesphere} & 

   626   \smath{\sigma(\abst{a}{t})} & \smath{\dn} & \smath{\abst{a}{\sigma(t)}}\\[2mm]

   627 

   628   \pgfuseshading{smallbluesphere} & 

   629   \smath{\sigma(\pi\act X)} & \smath{\dn} & 

   630   \smath{\begin{cases}% 

   631   \pi\;\act\;\sigma(X) & \!\!\text{if\ } \sigma(X)\not=X\\

   632   \pi\act X & \!\!\text{otherwise}% 

   633   \end{cases}}\\[6mm]

   634   \end{tabular}\bigskip\bigskip

   635 

   636   \pause

   637   \only<2-5>{

   638   \only<2->{for example}

   639   \def\arraystretch{1.3}

   640   \begin{tabular}{@ {\hspace{14mm}}l@ {\hspace{3mm}}l}

   641   \onslide<2->{\textcolor{white}{$\Rightarrow$}} &

   642   \onslide<2->{\alt<3>{\smath{\underline{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}

   643                       {\smath{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}\\

   644   \onslide<3->{\smath{\Rightarrow}} &

   645   \onslide<3->{\alt<3,4>{\smath{\abst{a}{\underline{\swap{a}{b}\act X[X:=\pair{b}{Y}]}}}}

   646                         {\smath{\abst{a}{\swap{a}{b}\act X}[X:=\pair{b}{Y}]}}}\\

   647   \onslide<4->{\smath{\Rightarrow}} &

   648   \onslide<4->{\alt<4>{\smath{\abst{a}{\swap{a}{b}\act \underline{\pair{b}{Y}}}}}

   649                       {\smath{\abst{a}{\underline{\swap{a}{b}}\act \pair{b}{Y}}}}}\\

   650   \onslide<5->{\smath{\Rightarrow}} &

   651   \onslide<5->{\smath{\abst{a}{\pair{a}{\swap{a}{b}\act Y}}}}

   652   \end{tabular}}

   653 

   654   \only<6->

   655   {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}

   656   \pgfuseshading{smallbluesphere} &

   657   if \smath{\nabla\vdash t\approx t'} and\hspace{-2mm}\mbox{}

   658   \raisebox{-2.7mm}{

   659   \alt<7>{\begin{tikzpicture}

   660           \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=3mm] 

   661           {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};

   662           \end{tikzpicture}}

   663          {\begin{tikzpicture}

   664           \draw (0,0) node[inner sep=1mm,fill=white, very thick, draw=white, rounded corners=3mm] 

   665           {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};

   666           \end{tikzpicture}}}\\

   667   & then \smath{\nabla'\vdash\sigma(t)\approx\sigma(t')}

   668   \end{tabular}}

   669 

   670   \only<9>

   671   {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}

   672   \\[-4mm]

   673   \pgfuseshading{smallbluesphere} &

   674   \smath{\sigma(\pi\act t)=\pi\act\sigma(t)}

   675   \end{tabular}}

   676 

   677 

   678   \only<7>{

   679   \begin{textblock}{6}(10,10.5)

   680   \begin{tikzpicture}

   681   \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=2mm] 

   682   {\color{darkgray}

   683    \begin{minipage}{3.8cm}\raggedright

   684    this means\\[1mm]

   685    \smath{\nabla'\vdash a\fresh\sigma(X)}\\[1mm]

   686    holds for all\\[1mm]

   687    \smath{(a\fresh X)\in\nabla}

   688   \end{minipage}};

   689   \end{tikzpicture}

   690   \end{textblock}}

   691 

   692   \end{frame}}

   693   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   694 *}

   695 

   696 text_raw {*

   697   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   698   \mode<presentation>{

   699   \begin{frame}<1->

   700   \frametitle{Equational Problems}

   701 

   702   An equational problem 

   703   \[

   704     \colorbox{cream}{\smath{t \eqprob t'}}

   705   \]

   706   is \alert{solved} by

   707 

   708   \begin{center}

   709   \begin{tabular}{ll}

   710   \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma} (terms for variables)\\[3mm]

   711   \pgfuseshading{smallbluesphere} & {\bf and} a set of freshness assumptions \smath{\nabla}

   712   \end{tabular}

   713   \end{center}

   714 

   715   so that \smath{\nabla\vdash \sigma(t)\approx \sigma(t')}.

   716 

   717 

   718   \end{frame}}

   719   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   720 *}

   721 

   722 text_raw {*

   723   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   724   \mode<presentation>{

   725   \begin{frame}<1->

   726 

   727   Unifying equations may entail solving

   728   \alert{freshness problems}.

   729 

   730   \bigskip

   731   

   732   E.g.~assuming that \smath{a\not=a'}, then

   733   \[

   734   \smath{\abst{a}{t}\eqprob \abst{a'}{t'}} 

   735   \]

   736   can only be solved if 

   737   \[

   738   \smath{t\eqprob \swap{a}{a'}\act t'} \quad\text{\emph{and}}\quad

   739   \smath{a\freshprob t'}

   740   \]

   741   can be solved.

   742 

   743   \end{frame}}

   744   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   745 *}

   746 

   747 text_raw {*

   748   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   749   \mode<presentation>{

   750   \begin{frame}<1->

   751   \frametitle{Freshness Problems}

   752 

   753   A freshness problem

   754   \[

   755   \colorbox{cream}{\smath{a \freshprob t}}

   756   \]

   757   is \alert{solved} by

   758 

   759   \begin{center}

   760   \begin{tabular}{ll}

   761   \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma}\\[3mm]

   762   \pgfuseshading{smallbluesphere} & and a set of freshness assumptions \smath{\nabla}

   763   \end{tabular}

   764   \end{center}

   765 

   766   so that \smath{\nabla\vdash a \fresh \sigma(t)}.

   767 

   768   \end{frame}}

   769   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   770 *}

   771 

   772 text_raw {*

   773   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   774   \mode<presentation>{

   775   \begin{frame}<1-3>

   776   \frametitle{Existence of MGUs}

   777 

   778   \underline{Theorem}: There is an algorithm which, given a nominal

   779   unification problem \smath{P}, decides whether\\ 

   780   or not it has a solution \smath{(\sigma,\nabla)}, and returns a \\

   781   \alert{most general} one if it does.\bigskip\bigskip

   782 

   783   \only<3>{

   784   Proof: one can reduce all the equations to `solved form'

   785   first (creating a substitution), and then solve the freshness

   786   problems (easy).}

   787 

   788   \only<2>{

   789   \begin{textblock}{6}(2.5,9.5)

   790   \begin{tikzpicture}

   791   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   792   {\color{darkgray}

   793   \begin{minipage}{8cm}\raggedright

   794   \alert{most general:}\\

   795   straightforward definition\\

   796   ``if\hspace{-0.5mm}f there exists a \smath{\tau} such that \ldots''

   797   \end{minipage}};

   798   \end{tikzpicture}

   799   \end{textblock}}

   800 

   801   \end{frame}}

   802   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   803 *}

   804 

   805 text_raw {*

   806   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   807   \mode<presentation>{

   808   \begin{frame}<1>

   809   \frametitle{Remember the Quiz?}

   810 

   811   \textcolor{gray}{Assuming that $a$ and $b$ are distinct variables,\\

   812   is it possible to find $\lambda$-terms $M_1$ to $M_7$ 

   813   that make the following pairs $\alpha$-equivalent?}

   814 

   815   \begin{tabular}{@ {\hspace{14mm}}p{12cm}}

   816   \begin{itemize}

   817   \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 

   818         \smath{\lambda b.\lambda a. (a\,M_1)\;}

   819 

   820   \item \textcolor{gray}{$\lambda a.\lambda b. (M_2\,b)\;$ and 

   821         $\lambda b.\lambda a. (a\,M_3)\;$}

   822 

   823   \item \textcolor{gray}{$\lambda a.\lambda b. (b\,M_4)\;$ and 

   824         $\lambda b.\lambda a. (a\,M_5)\;$}

   825 

   826   \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 

   827         \smath{\lambda a.\lambda a. (a\,M_7)\;}

   828   \end{itemize}

   829   \end{tabular}

   830 

   831   \textcolor{gray}{If there is one solution for a pair, can you 

   832   describe all its solutions?}

   833 

   834 

   835   \end{frame}}

   836   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   837 *}

   838 

   839 text_raw {*

   840   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   841   \mode<presentation>{

   842   \begin{frame}<1->

   843   \frametitle{Answers to the Quiz}

   844   \small

   845   \def\arraystretch{1.6}

   846   \begin{tabular}{c@ {\hspace{2mm}}l}

   847   & \only<1>{\smath{\lambda a.\lambda b. (M_1\,b)\;} and \smath{\;\lambda b.\lambda a. (a\,M_1)}}%

   848     \only<2->{\smath{\abst{a}{\abst{b}{\pair{M_1}{b}}} \;\eqprob\; \abst{b}{\abst{a}{\pair{a}{M_1}}}}}\\

   849 

   850   \onslide<3->{\smath{\redu{\id}}} &

   851   \only<3>{\smath{\abst{b}{\pair{M_1}{b}} \eqprob

   852        \alert{\swap{a}{b}} \act \abst{a}{\pair{a}{M_1}}\;,\;a\freshprob \abst{a}{\pair{a}{M_1}}}}%

   853   \only<4->{\smath{\abst{b}{\pair{M_1}{b}} \eqprob \abst{b}{\pair{b}{\swap{a}{b}\act M_1}}\;,\

   854        a\freshprob \abst{a}{\pair{a}{M_1}}}}\\

   855 

   856   \onslide<5->{\smath{\redu{\id}}} &

   857   \only<5->{\smath{\pair{M_1}{b} \eqprob \pair{b}{\swap{a}{b}\act M_1}\;,\;%

   858        a\freshprob \abst{a}{\pair{a}{M_1}}}}\\

   859 

   860   \onslide<6->{\smath{\redu{\id}}} &

   861   \only<6->{\smath{M_1 \eqprob b \;,\; b \eqprob \swap{a}{b}\act M_1\;,\;%

   862        a\freshprob \abst{a}{\pair{a}{M_1}}}}\\

   863 

   864   \onslide<7->{\smath{\redu{[M_1:=b]}}} &

   865   \only<7>{\smath{b \eqprob \swap{a}{b}\act \alert{b}\;,\;%

   866        a\freshprob \abst{a}{\pair{a}{\alert{b}}}}}%

   867   \only<8->{\smath{b \eqprob a\;,\; a\freshprob \abst{a}{\pair{a}{b}}}}\\

   868 

   869   \onslide<9->{\smath{\redu{}}} &

   870   \only<9->{\smath{F\hspace{-0.5mm}AIL}}

   871   \end{tabular}

   872 

   873   \only<10>{

   874   \begin{textblock}{6}(2,11)

   875   \begin{tikzpicture}

   876   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   877   {\color{darkgray}

   878   \begin{minipage}{9cm}\raggedright

   879   \smath{\lambda a.\lambda b. (M_1\,b)} \smath{=_\alpha} 

   880   \smath{\lambda b.\lambda a. (a\,M_1)} has no solution

   881   \end{minipage}};

   882   \end{tikzpicture}

   883   \end{textblock}}

   884 

   885   \end{frame}}

   886   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   887 *}

   888 

   889 text_raw {*

   890   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   891   \mode<presentation>{

   892   \begin{frame}<1->

   893   \frametitle{Answers to the Quiz}

   894   \small

   895   \def\arraystretch{1.6}

   896   \begin{tabular}{c@ {\hspace{2mm}}l}

   897   & \only<1>{\smath{\lambda a.\lambda b. (b\,M_6)\;} and \smath{\;\lambda a.\lambda a. (a\,M_7)}}%

   898     \only<2->{\smath{\abst{a}{\abst{b}{\pair{b}{M_6}}} \;\eqprob\; \abst{a}{\abst{a}{\pair{a}{M_7}}}}}\\

   899 

   900   \onslide<3->{\smath{\redu{\id}}} &

   901   \only<3->{\smath{\abst{b}{\pair{b}{M_6}} \eqprob \abst{a}{\pair{a}{M_7}}}}\\

   902 

   903   \onslide<4->{\smath{\redu{\id}}} &

   904   \only<4->{\smath{\pair{b}{M_6} \eqprob \pair{b}{\swap{b}{a}\act M_7}\;,\;b\freshprob\pair{a}{M_7}}}\\

   905 

   906   \onslide<5->{\smath{\redu{\id}}} &

   907   \only<5->{\smath{b\eqprob b\;,\; M_6 \eqprob \swap{b}{a}\act M_7\;,\;%

   908        b\freshprob \pair{a}{M_7}}}\\

   909 

   910   \onslide<6->{\smath{\redu{\id}}} &

   911   \only<6->{\smath{M_6 \eqprob \swap{b}{a}\act M_7\;,\;%

   912        b\freshprob \pair{a}{M_7}}}\\

   913 

   914   \onslide<7->{\makebox[0mm]{\smath{\redu{[M_6:=\swap{b}{a}\act M_7]}}}} &

   915   \only<7->{\smath{\qquad b\freshprob \pair{a}{M_7}}}\\

   916 

   917   \onslide<8->{\smath{\redu{\varnothing}}} &

   918   \only<8->{\smath{b\freshprob a\;,\;b\freshprob M_7}}\\

   919   

   920   \onslide<9->{\smath{\redu{\varnothing}}} &

   921   \only<9->{\smath{b\freshprob M_7}}\\

   922  

   923   \onslide<10->{\makebox[0mm]{\smath{\redu{\{b\fresh M_7\}}}}} &

   924   \only<10->{\smath{\;\;\varnothing}}\\

   925 

   926   \end{tabular}

   927 

   928   \only<10>{

   929   \begin{textblock}{6}(6,9)

   930   \begin{tikzpicture}

   931   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   932   {\color{darkgray}

   933   \begin{minipage}{7cm}\raggedright

   934   \smath{\lambda a.\lambda b. (b\,M_6)\;} \smath{=_\alpha} 

   935   \smath{\;\lambda a.\lambda a. (a\,M_7)}\\[2mm]

   936   we can take \smath{M_7} to be any $\lambda$-term that does not

   937   contain free occurrences of \smath{b}, so long as we take \smath{M_6} to

   938   be the result of swapping all occurrences of \smath{b} and \smath{a}

   939   throughout \smath{M_7}

   940   \end{minipage}};

   941   \end{tikzpicture}

   942   \end{textblock}}

   943 

   944   \end{frame}}

   945   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   946 *}

   947 

   948 text_raw {*

   949   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   950   \mode<presentation>{

   951   \begin{frame}<1->

   952   \frametitle{Properties}

   953 

   954   \begin{itemize}

   955   \item An interesting feature of nominal unification is that it

   956   does not need to create new atoms.\bigskip

   957 

   958   \begin{center}\small

   959   \colorbox{cream}{

   960   \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id} \{t \eqprob \swap{a}{b}\act t', a \freshprob t'\} \cup P}}

   961   \end{center}\bigskip\bigskip

   962   \pause

   963 

   964   \item The alternative rule

   965 

   966   \begin{center}\small

   967   \colorbox{cream}{

   968   \begin{tabular}{@ {}l@ {}}

   969   \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id}}\\ 

   970   \mbox{}\hspace{2cm}\smath{\{\swap{a}{c}\act t \eqprob 

   971   \swap{b}{c}\act t', c \freshprob t, c \freshprob t'\} \cup P}

   972   \end{tabular}}

   973   \end{center}

   974  

   975   leads to a more complicated notion of mgu.\medskip\pause

   976   

   977   \footnotesize

   978   \smath{\{a.X \eqprob b.Y\} \redu{} (\{a\fresh Y, c\fresh Y\}, [X:=\swap{a}{c}\swap{b}{c}\act Y])}

   979   \end{itemize}

   980 

   981   \end{frame}}

   982   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   983 *}

   984 

   985 text_raw {*

   986   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   987   \mode<presentation>{

   988   \begin{frame}<1-3>

   989   \frametitle{Is it Useful?}

   990 

   991   Yes. $\alpha$Prolog by James Cheney (main developer)\bigskip\bigskip

   992 

   993   \color{darkgray}

   994   \begin{tabular}{@ {}l}

   995   type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\

   996   

   997   type (Gamma, app(M, N), T') :-\\

   998   \hspace{3cm}type (Gamma, M, arrow(T, T')),\\ 

   999   \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\

  1000   

  1001   type (Gamma, lam(\alert{x.M}), arrow(T, T')) / \alert{x \# Gamma} :-\\

  1002   \hspace{3cm}type ((x, T)::Gamma, M, T').\smallskip\medskip\\

  1003   

  1004   member X X::Tail.\\

  1005   member X Y::Tail :- member X Tail.\\

  1006   \end{tabular}

  1007 

  1008   \only<2->{

  1009   \begin{textblock}{6}(1.5,0.5)

  1010   \begin{tikzpicture}

  1011   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

  1012   {\color{darkgray}

  1013   \begin{minipage}{9cm}\raggedright

  1014   {\bf One problem:} If we ask whether

  1015   

  1016   \begin{center}

  1017   ?- type ([(x, T')], lam(x.Var(x)), T) 

  1018   \end{center}

  1019 

  1020   is typable, we expect an answer for T.\bigskip

  1021 

  1022   \onslide<3>{Solution: Before back-chaining freshen all variables and atoms

  1023   in a program (clause).}

  1024   \end{minipage}};

  1025   \end{tikzpicture}

  1026   \end{textblock}}

  1027 

  1028   \end{frame}}

  1029   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1030 *}

  1031 

  1032 text_raw {*

  1033   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1034   \mode<presentation>{

  1035   \begin{frame}<1->

  1036   \frametitle{Equivariant Unification}

  1037 

  1038   James Cheney proposed

  1039 

  1040   \begin{center}

  1041   \colorbox{cream}{

  1042   \smath{t \eqprob t'  \redu{\nabla, \sigma, \pi}   

  1043     \nabla \vdash \sigma(t) \approx \pi \act \sigma(t')}}

  1044   \end{center}\bigskip\bigskip

  1045   \pause

  1046 

  1047   But he also showed this problem is undecidable\\ in general. :(

  1048 

  1049   \end{frame}}

  1050   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1051 *}

  1052 

  1053 text_raw {*

  1054   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1055   \mode<presentation>{

  1056   \begin{frame}<1->

  1057   \frametitle{Taking Atoms as Variables}

  1058 

  1059   Instead of \smath{a.X}, have \smath{A.X}.\bigskip

  1060   \pause

  1061 

  1062   Unfortunately this breaks the mgu-property:

  1063 

  1064   \begin{center}

  1065   \smath{a.Z \eqprob X.Y.v(a)}

  1066   \end{center}

  1067 

  1068   can be solved by

  1069 

  1070   \begin{center}

  1071   \smath{[X:=a, Z:=Y.v(a)]} and

  1072   \smath{[Y:=a, Z:=Y.v(Y)]}

  1073   \end{center}

  1074 

  1075   \end{frame}}

  1076   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1077 *}

  1078 

  1079 text_raw {*

  1080   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1081   \mode<presentation>{

  1082   \begin{frame}<1>[c]

  1083   \frametitle{HOPU vs. NOMU}

  1084 

  1085   \begin{itemize}

  1086   \item James Cheney showed\bigskip

  1087   \begin{center}

  1088   \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}} 

  1089   \end{center}\bigskip

  1090 

  1091   \item Jordi Levy and Mateu Villaret established\bigskip

  1092   \begin{center}

  1093   \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}} 

  1094   \end{center}\bigskip

  1095   \end{itemize}

  1096 

  1097   The translations `explode' the problems quadratically.

  1098 

  1099   \end{frame}}

  1100   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1101 *}

  1102 

  1103 text_raw {*

  1104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1105   \mode<presentation>{

  1106   \begin{frame}<1>

  1107   \small\tt

  1108   

  1109   \begin{minipage}{13cm}

  1110   \begin{tabular}{@ {\hspace{-2mm}}p{11.5cm}}

  1111   \\

  1112   From: Zhenyu Qian <zhqian@microsoft.com>\\

  1113   To: Christian Urban <urbanc@in.tum.de>\\

  1114   Subject: RE: Linear Higher-Order Pattern Unification\\

  1115   Date: Mon, 14 Apr 2008 09:56:47 +0800\\

  1116   \\

  1117   Hi Christian,\\

  1118   \\

  1119   Thanks for your interests and asking. I know that that paper is complex. As

  1120   I told Tobias when we met last time, I have raised the question to myself 

  1121   many times whether the proof could have some flaws, and so making it through 

  1122   a theorem prover would definitely bring piece to my mind (no matter what 

  1123   the result would be). The only problem for me is the time.\\

  1124   \ldots\\

  1125 

  1126   Thanks/Zhenyu

  1127   \end{tabular}

  1128   \end{minipage}

  1129 

  1130   \end{frame}}

  1131   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1132 *}

  1133 

  1134 text_raw {*