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

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

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

   133 

   134   State of the art:

   161   \\

   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 

   964   %\begin{center}\small

   965   %\colorbox{cream}{

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

   967   %\end{center}

   968  

   969 

   970   leads to a more complicated notion of mgu.

   971   \end{itemize}

   972 

   973   \end{frame}}

   974   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   975 *}

   976 

   977 text_raw {*

   978   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   979   \mode<presentation>{

   980   \begin{frame}<1-3>

   981   \frametitle{Is it Useful?}

   982 

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

   984 

   985   \color{darkgray}

   986   \begin{tabular}{@ {}l}

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

   988   

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

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

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

   992   

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

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

   995   

   996   member X X::Tail.\\

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

   998   \end{tabular}

   999 

  1000   \only<2->{

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

  1002   \begin{tikzpicture}

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

  1004   {\color{darkgray}

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

  1006   {\bf Problem:} If we ask whether

  1007   

  1008   \begin{center}

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

  1010   \end{center}

  1011 

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

  1013 

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

  1015   in a program (clause).}

  1016   \end{minipage}};

  1017   \end{tikzpicture}

  1018   \end{textblock}}

  1019 

  1020   \end{frame}}

  1021   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1022 *}

  1023 

  1024 text_raw {*

  1025   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1026   \mode<presentation>{

  1027   \begin{frame}<1->

  1028   \frametitle{Equivariant Unification}

  1029 

  1030   James Cheney

  1031 

  1032   \begin{center}

  1033   \colorbox{cream}{

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

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

  1036   \end{center}\bigskip\bigskip

  1037   \pause

  1038 

  1039   He also showed that this is undecidable in general. :(

  1040 

  1041   \end{frame}}

  1042   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1043 *}

  1044 

  1045 text_raw {*

  1046   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1047   \mode<presentation>{

  1048   \begin{frame}<1->

  1049   \frametitle{Taking Atoms as Variables}

  1050 

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

  1052   \pause

  1053 

  1054   Unfortunately this breaks the mgu-property:

  1055 

  1056   \begin{center}

  1057   

  1058   \end{center}

  1059 

  1060   \end{frame}}

  1061   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1062 *}

  1063 

  1064 text_raw {*

  1065   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1066   \mode<presentation>{

  1067   \begin{frame}<1>

  1068   \frametitle{HOPU vs. NOMU}

  1069 

  1070   \begin{itemize}

  1071   \item James Cheney showed\bigskip

  1072   \begin{center}

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

  1074   \end{center}\bigskip

  1075 

  1076   \item Levi\bigskip

  1077   \begin{center}

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

  1079   \end{center}\bigskip

  1080   \end{itemize}

  1081 

  1082   The translations `explode' the problems quadratically.

  1083 

  1084   \end{frame}}

  1085   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1086 *}

  1087 

  1088 text_raw {*

  1089   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1090   \mode<presentation>{

  1091   \begin{frame}<1>

  1092   \small\tt

  1093   

  1094   \begin{minipage}{13cm}

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

  1096   \\

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

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

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

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

  1101   \\

  1102   Hi Christian,\\

  1103   \\

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

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

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

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

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

  1109   \ldots\\

  1110 

  1111   Thanks/Zhenyu

  1112   \end{tabular}

  1113   \end{minipage}

  1114 

  1115   \end{frame}}

  1116   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1117 *}

  1118 

  1119 text_raw {*

  1120   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1121   \mode<presentation>{

  1122   \begin{frame}<1>

  1123   \frametitle{Complexity}

  1124 

  1125   \begin{itemize}

  1126   \item Maribel Fernandez

  1127 

  1128   \item Levi 

  1129   

  1130   

  1131   \end{itemize}

  1132 

  1133   \end{frame}}

  1134   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1135 *}

  1136 

  1137 

  1138 text_raw {*

  1139   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1140   \mode<presentation>{

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

  1159 

  1160   \end{frame}}

  1161   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1162 *}

  1163 

  1164 text_raw {*

  1165   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1166   \mode<presentation>{

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

  1168   \frametitle{

  1169   \begin{tabular}{c}

  1170   \mbox{}\\[23mm]

  1171   \alert{\LARGE Thank you very much}\\

  1172   \alert{\Large Questions?}

  1173   \end{tabular}}

  1174   

  1175   \end{frame}}

  1176   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1177 *}

  1178 

  1179 text_raw {*

  1180   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1181   \mode<presentation>{

  1182   \begin{frame}<1-3>

  1183   \frametitle{Most General Unifiers}

  1184 

  1185   \underline{Definition}: For a unification problem

  1186   \smath{P}, a solution \smath{(\sigma_1,\nabla_1)} is

  1187   \alert{more general} than another solution

  1188   \smath{(\sigma_2,\nabla_2)}, iff~there exists a substitution

  1189   \smath{\tau} with

  1190 

  1191   \begin{center}

  1192   \begin{tabular}{ll}

  1193   \pgfuseshading{smallbluesphere} & 

  1194      \alt<2>{\smath{\alert{\nabla_2\vdash\tau(\nabla_1)}}}

  1195             {\smath{\nabla_2\vdash\tau(\nabla_1)}}\\

  1196   \pgfuseshading{smallbluesphere} & 

  1197      \alt<3>{\smath{\alert{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}}

  1198             {\smath{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}

  1199   \end{tabular}

  1200   \end{center}

  1201 

  1202   \only<2>{

  1203   \begin{textblock}{13}(1.5,10.5)

  1204   \smath{\nabla_2\vdash a\fresh \sigma(X)} holds for all

  1205   \smath{(a\fresh X)\in\nabla_1}

  1206   \end{textblock}}

  1207   

  1208   \only<3>{

  1209   \begin{textblock}{11}(1.5,10.5)

  1210   \smath{\nabla_2\vdash \sigma_2(X)\approx

  1211   \sigma(\sigma_1(X))}

  1212   holds for all

  1213   \smath{X\in\text{dom}(\sigma_2)\cup\text{dom}(\sigma\circ\sigma_1)}

  1214   \end{textblock}}