
diff -r 840a857354f2 -r 7aec0986b229 Slides/Slides3.thy
--- a/Slides/Slides3.thy	Mon Jul 12 21:48:39 2010 +0100
+++ b/Slides/Slides3.thy	Tue Jul 13 14:37:28 2010 +0100
@@ -18,6 +18,9 @@
   \newcommand{\unit}{\langle\rangle}% unit
   \newcommand{\app}[2]{#1\,#2}% application
   \newcommand{\eqprob}{\mathrel{{\approx}?}}
+  \newcommand{\freshprob}{\mathrel{\#?}}
+  \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
+  \newcommand{\id}{\varepsilon}% identity substitution
 
   \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
   {rgb(0mm)=(0,0,0.9);
@@ -70,7 +73,8 @@
   Christian Urban
   \end{center}
   \begin{center}
-  \small initial work with Andy Pitts and Jamie Gabbay\\[0mm] 
+  \small initial spark from Roy Dyckhoff in November 2001\\[0mm] 
+  \small joint work with Andy Pitts and Jamie Gabbay\\[0mm] 
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -84,7 +88,7 @@
 
   \onslide<2->{Typing implemented in Prolog \textcolor{darkgray}{(from a textbook)}}\bigskip\\
 
-  \onslide<3->{
+  \onslide<3->{\color{darkgray}
   \begin{tabular}{l}
   type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\
   
@@ -106,7 +110,7 @@
   {\color{darkgray}
   \begin{minipage}{8cm}\raggedright
   The problem is that \smath{\lambda x.\lambda x. (x\;x)}
-  gets the types
+  will have the types
   \begin{center}
   \begin{tabular}{l}
   \smath{T\rightarrow (T\rightarrow S) \rightarrow S} and\\ 
@@ -127,6 +131,8 @@
   \begin{frame}<1>[c]
   \frametitle{Higher-Order Unification}
 
+  State of the art:
+
   \begin{itemize}
   \item Lambda Prolog with full Higher-Order Unification\\ 
   \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip
@@ -152,6 +158,7 @@
   \only<2-5>{
   \begin{center}
   \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{12mm}}r@ {\hspace{1mm}}l}
+  \\
   \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%
   \only<3>{\smath{[b\!:=\!a]}}%
   \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} & 
@@ -173,7 +180,7 @@
   \draw (0,0) node[inner sep=0mm,fill=cream, ultra thick, draw=cream] 
   {\begin{minipage}{8cm}
   \begin{tabular}{r@ {\hspace{3mm}}l}
-  \smath{\swap{a}{b}\act t} $\;\dn$ & \alert{swap} {\bf all} occurences of\\ 
+  \smath{\swap{a}{b}\act t} $\;\dn$ & \alert{swap} {\bf all} occurrences of\\ 
                                   & \smath{b} and \smath{a} in \smath{t}
   \end{tabular}
   \end{minipage}};
@@ -311,7 +318,7 @@
   We therefore will identify
 
   \begin{center}
-  \smath{\mathtt{fn\ } a. X \;\approx\; \mathtt{fn\ } b. \alert<3->{\swap{a}{b}}\act X}
+  \smath{\text{fn\ } a. X \;\approx\; \text{fn\ } b. \alert<3->{\swap{a}{b}}\act X}
   \end{center}
 
   provided that `\smath{b} is fresh for \smath{X} --- (\smath{b\fresh X})',
@@ -564,7 +571,7 @@
   \begin{tabular}{@ {}rl}
   \underline{Theorem:}
   & \smath{t=_\alpha t'\;\;}  if\hspace{-0.5mm}f~\smath{\;\;\emptyset \vdash t\approx t'}\\[2mm]
-  & \smath{a\not\in FA(t)\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset\vdash a\fresh t} 
+  & \smath{a\not\in F\hspace{-0.9mm}A(t)\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset\vdash a\fresh t} 
   \end{tabular}
   \end{minipage}}
   \end{center}
@@ -714,19 +721,439 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1->
+
+  Unifying equations may entail solving
+  \alert{freshness problems}.
+
+  \bigskip
+  
+  E.g.~assuming that \smath{a\not=a'}, then
+  \[
+  \smath{\abst{a}{t}\eqprob \abst{a'}{t'}} 
+  \]
+  can only be solved if 
+  \[
+  \smath{t\eqprob \swap{a}{a'}\act t'} \quad\text{\emph{and}}\quad
+  \smath{a\freshprob t'}
+  \]
+  can be solved.
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Freshness Problems}
+
+  A freshness problem
+  \[
+  \colorbox{cream}{\smath{a \freshprob t}}
+  \]
+  is \alert{solved} by
+
+  \begin{center}
+  \begin{tabular}{ll}
+  \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma}\\[3mm]
+  \pgfuseshading{smallbluesphere} & and a set of freshness assumptions \smath{\nabla}
+  \end{tabular}
+  \end{center}
+
+  so that \smath{\nabla\vdash a \fresh \sigma(t)}.
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{Existence of MGUs}
+
+  \underline{Theorem}: There is an algorithm which, given a nominal
+  unification problem \smath{P}, decides whether\\ 
+  or not it has a solution \smath{(\sigma,\nabla)}, and returns a \\
+  \alert{most general} one if it does.\bigskip\bigskip
+
+  \only<3>{
+  Proof: one can reduce all the equations to `solved form'
+  first (creating a substitution), and then solve the freshness
+  problems (easy).}
+
+  \only<2>{
+  \begin{textblock}{6}(2.5,9.5)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{8cm}\raggedright
+  \alert{most general:}\\
+  straightforward definition\\
+  ``if\hspace{-0.5mm}f there exists a \smath{\tau} such that \ldots''
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{Remember the Quiz?}
+
+  \textcolor{gray}{Assuming that $a$ and $b$ are distinct variables,\\
+  is it possible to find $\lambda$-terms $M_1$ to $M_7$ 
+  that make the following pairs $\alpha$-equivalent?}
+
+  \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
+  \begin{itemize}
+  \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 
+        \smath{\lambda b.\lambda a. (a\,M_1)\;}
+
+  \item \textcolor{gray}{$\lambda a.\lambda b. (M_2\,b)\;$ and 
+        $\lambda b.\lambda a. (a\,M_3)\;$}
+
+  \item \textcolor{gray}{$\lambda a.\lambda b. (b\,M_4)\;$ and 
+        $\lambda b.\lambda a. (a\,M_5)\;$}
+
+  \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 
+        \smath{\lambda a.\lambda a. (a\,M_7)\;}
+  \end{itemize}
+  \end{tabular}
+
+  \textcolor{gray}{If there is one solution for a pair, can you 
+  describe all its solutions?}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Answers to the Quiz}
+  \small
+  \def\arraystretch{1.6}
+  \begin{tabular}{c@ {\hspace{2mm}}l}
+  & \only<1>{\smath{\lambda a.\lambda b. (M_1\,b)\;} and \smath{\;\lambda b.\lambda a. (a\,M_1)}}%
+    \only<2->{\smath{\abst{a}{\abst{b}{\pair{M_1}{b}}} \;\eqprob\; \abst{b}{\abst{a}{\pair{a}{M_1}}}}}\\
+
+  \onslide<3->{\smath{\redu{\id}}} &
+  \only<3>{\smath{\abst{b}{\pair{M_1}{b}} \eqprob
+       \alert{\swap{a}{b}} \act \abst{a}{\pair{a}{M_1}}\;,\;a\freshprob \abst{a}{\pair{a}{M_1}}}}%
+  \only<4->{\smath{\abst{b}{\pair{M_1}{b}} \eqprob \abst{b}{\pair{b}{\swap{a}{b}\act M_1}}\;,\
+       a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+
+  \onslide<5->{\smath{\redu{\id}}} &
+  \only<5->{\smath{\pair{M_1}{b} \eqprob \pair{b}{\swap{a}{b}\act M_1}\;,\;%
+       a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+
+  \onslide<6->{\smath{\redu{\id}}} &
+  \only<6->{\smath{M_1 \eqprob b \;,\; b \eqprob \swap{a}{b}\act M_1\;,\;%
+       a\freshprob \abst{a}{\pair{a}{M_1}}}}\\
+
+  \onslide<7->{\smath{\redu{[M_1:=b]}}} &
+  \only<7>{\smath{b \eqprob \swap{a}{b}\act \alert{b}\;,\;%
+       a\freshprob \abst{a}{\pair{a}{\alert{b}}}}}%
+  \only<8->{\smath{b \eqprob a\;,\; a\freshprob \abst{a}{\pair{a}{b}}}}\\
+
+  \onslide<9->{\smath{\redu{}}} &
+  \only<9->{\smath{F\hspace{-0.5mm}AIL}}
+  \end{tabular}
+
+  \only<10>{
+  \begin{textblock}{6}(2,11)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{9cm}\raggedright
+  \smath{\lambda a.\lambda b. (M_1\,b)} \smath{=_\alpha} 
+  \smath{\lambda b.\lambda a. (a\,M_1)} has no solution
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Answers to the Quiz}
+  \small
+  \def\arraystretch{1.6}
+  \begin{tabular}{c@ {\hspace{2mm}}l}
+  & \only<1>{\smath{\lambda a.\lambda b. (b\,M_6)\;} and \smath{\;\lambda a.\lambda a. (a\,M_7)}}%
+    \only<2->{\smath{\abst{a}{\abst{b}{\pair{b}{M_6}}} \;\eqprob\; \abst{a}{\abst{a}{\pair{a}{M_7}}}}}\\
+
+  \onslide<3->{\smath{\redu{\id}}} &
+  \only<3->{\smath{\abst{b}{\pair{b}{M_6}} \eqprob \abst{a}{\pair{a}{M_7}}}}\\
+
+  \onslide<4->{\smath{\redu{\id}}} &
+  \only<4->{\smath{\pair{b}{M_6} \eqprob \pair{b}{\swap{b}{a}\act M_7}\;,\;b\freshprob\pair{a}{M_7}}}\\
+
+  \onslide<5->{\smath{\redu{\id}}} &
+  \only<5->{\smath{b\eqprob b\;,\; M_6 \eqprob \swap{b}{a}\act M_7\;,\;%
+       b\freshprob \pair{a}{M_7}}}\\
+
+  \onslide<6->{\smath{\redu{\id}}} &
+  \only<6->{\smath{M_6 \eqprob \swap{b}{a}\act M_7\;,\;%
+       b\freshprob \pair{a}{M_7}}}\\
+
+  \onslide<7->{\makebox[0mm]{\smath{\redu{[M_6:=\swap{b}{a}\act M_7]}}}} &
+  \only<7->{\smath{\qquad b\freshprob \pair{a}{M_7}}}\\
+
+  \onslide<8->{\smath{\redu{\varnothing}}} &
+  \only<8->{\smath{b\freshprob a\;,\;b\freshprob M_7}}\\
+  
+  \onslide<9->{\smath{\redu{\varnothing}}} &
+  \only<9->{\smath{b\freshprob M_7}}\\
+ 
+  \onslide<10->{\makebox[0mm]{\smath{\redu{\{b\fresh M_7\}}}}} &
+  \only<10->{\smath{\;\;\varnothing}}\\
+
+  \end{tabular}
+
+  \only<10>{
+  \begin{textblock}{6}(6,9)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{7cm}\raggedright
+  \smath{\lambda a.\lambda b. (b\,M_6)\;} \smath{=_\alpha} 
+  \smath{\;\lambda a.\lambda a. (a\,M_7)}\\[2mm]
+  we can take \smath{M_7} to be any $\lambda$-term that does not
+  contain free occurrences of \smath{b}, so long as we take \smath{M_6} to
+  be the result of swapping all occurrences of \smath{b} and \smath{a}
+  throughout \smath{M_7}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Properties}
+
+  \begin{itemize}
+  \item An interesting feature of nominal unification is that it
+  does not need to create new atoms.\bigskip
+
+  \begin{center}\small
+  \colorbox{cream}{
+  \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id} \{t \eqprob \swap{a}{b}\act t', a \freshprob t'\} \cup P}}
+  \end{center}\bigskip\bigskip
+  \pause
+
+  \item The alternative rule
+
+  %\begin{center}\small
+  %\colorbox{cream}{
+  %\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}}
+  %\end{center}
+ 
+
+  leads to a more complicated notion of mgu.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{Is it Useful?}
+
+  Yes. $\alpha$Prolog by James Cheney (main developer)\bigskip\bigskip
+
+  \color{darkgray}
+  \begin{tabular}{@ {}l}
+  type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\
+  
+  type (Gamma, app(M, N), T') :-\\
+  \hspace{3cm}type (Gamma, M, arrow(T, T')),\\ 
+  \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\
+  
+  type (Gamma, lam(\alert{x.M}), arrow(T, T')) / \alert{x \# Gamma} :-\\
+  \hspace{3cm}type ((x, T)::Gamma, M, T').\smallskip\medskip\\
+  
+  member X X::Tail.\\
+  member X Y::Tail :- member X Tail.\\
+  \end{tabular}
+
+  \only<2->{
+  \begin{textblock}{6}(1.5,0.5)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{9cm}\raggedright
+  {\bf Problem:} If we ask whether
+  
+  \begin{center}
+  ?- type ([(x, T')], lam(x.Var(x)), T) 
+  \end{center}
+
+  is typable, we expect an answer for T.\bigskip
+
+  \onslide<3>{Solution: Before back-chaining freshen all variables and atoms
+  in a program (clause).}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Equivariant Unification}
+
+  James Cheney
+
+  \begin{center}
+  \colorbox{cream}{
+  \smath{t \eqprob t'  \redu{\nabla, \sigma, \pi}   
+    \nabla \vdash \sigma(t) \approx \pi \act \sigma(t')}}
+  \end{center}\bigskip\bigskip
+  \pause
+
+  He also showed that this is undecidable in general. :(
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->
+  \frametitle{Taking Atoms as Variables}
+
+  Instead of \smath{a.X}, have \smath{A.X}.\bigskip
+  \pause
+
+  Unfortunately this breaks the mgu-property:
+
+  \begin{center}
+  
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{HOPU vs. NOMU}
+
+  \begin{itemize}
+  \item James Cheney showed\bigskip
+  \begin{center}
+  \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}} 
+  \end{center}\bigskip
+
+  \item Levi\bigskip
+  \begin{center}
+  \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}} 
+  \end{center}\bigskip
+  \end{itemize}
+
+  The translations `explode' the problems quadratically.
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \small\tt
+  
+  \begin{minipage}{13cm}
+  \begin{tabular}{@ {\hspace{-2mm}}p{11.5cm}}
+  \\
+  From: Zhenyu Qian <zhqian@microsoft.com>\\
+  To: Christian Urban <urbanc@in.tum.de>\\
+  Subject: RE: Linear Higher-Order Pattern Unification\\
+  Date: Mon, 14 Apr 2008 09:56:47 +0800\\
+  \\
+  Hi Christian,\\
+  \\
+  Thanks for your interests and asking. I know that that paper is complex. As
+  I told Tobias when we met last time, I have raised the question to myself 
+  many times whether the proof could have some flaws, and so making it through 
+  a theorem prover would definitely bring piece to my mind (no matter what 
+  the result would be). The only problem for me is the time.\\
+  \ldots\\
+
+  Thanks/Zhenyu
+  \end{tabular}
+  \end{minipage}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{Complexity}
+
+  \begin{itemize}
+  \item Maribel Fernandez
+
+  \item Levi 
+  
+  
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
   \frametitle{Conclusion}
 
   \begin{itemize}
-  \item the user does not see anything of the raw level\medskip
-  \only<1>{\begin{center}
-  Lam a (Var a) \alert{$=$} Lam b (Var b)
-  \end{center}\bigskip}
+  \item Nominal Unification is a completely first-order 
+  language, but implements unification modulo $\alpha$.\medskip\pause
 
-  \item<2-> we have not yet done function definitions (will come soon and
-  we hope to make improvements over the old way there too)\medskip
-  \item<3-> it took quite some time to get here, but it seems worthwhile 
-  (Barendregt's variable convention is unsound in general, 
-  found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
+  \item NOMU has been applied in term-rewriting and
+  logic programming. I hope it will also be used in typing
+  systems.\medskip\pause
+
+  \item NOMU and HOPU are `equivalent' (it took a long time
+  and considerable time to find this out).\medskip\pause
+  
+  \item The question about complexity is still an ongoing 
+  story.\medskip 
   \end{itemize}
 
 
@@ -734,6 +1161,62 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[23mm]
+  \alert{\LARGE Thank you very much}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{Most General Unifiers}
+
+  \underline{Definition}: For a unification problem
+  \smath{P}, a solution \smath{(\sigma_1,\nabla_1)} is
+  \alert{more general} than another solution
+  \smath{(\sigma_2,\nabla_2)}, iff~there exists a substitution
+  \smath{\tau} with
+
+  \begin{center}
+  \begin{tabular}{ll}
+  \pgfuseshading{smallbluesphere} & 
+     \alt<2>{\smath{\alert{\nabla_2\vdash\tau(\nabla_1)}}}
+            {\smath{\nabla_2\vdash\tau(\nabla_1)}}\\
+  \pgfuseshading{smallbluesphere} & 
+     \alt<3>{\smath{\alert{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}}
+            {\smath{\nabla_2\vdash\sigma_2\approx \tau\circ\sigma_1}}
+  \end{tabular}
+  \end{center}
+
+  \only<2>{
+  \begin{textblock}{13}(1.5,10.5)
+  \smath{\nabla_2\vdash a\fresh \sigma(X)} holds for all
+  \smath{(a\fresh X)\in\nabla_1}
+  \end{textblock}}
+  
+  \only<3>{
+  \begin{textblock}{11}(1.5,10.5)
+  \smath{\nabla_2\vdash \sigma_2(X)\approx
+  \sigma(\sigma_1(X))}
+  holds for all
+  \smath{X\in\text{dom}(\sigma_2)\cup\text{dom}(\sigma\circ\sigma_1)}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file




