--- a/Slides/Slides3.thy Tue Jul 13 14:37:28 2010 +0100
+++ b/Slides/Slides3.thy Tue Jul 13 23:39:39 2010 +0100
@@ -131,7 +131,7 @@
\begin{frame}<1>[c]
\frametitle{Higher-Order Unification}
- State of the art:
+ State of the art at the time:
\begin{itemize}
\item Lambda Prolog with full Higher-Order Unification\\
@@ -961,13 +961,19 @@
\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}
+ \begin{center}\small
+ \colorbox{cream}{
+ \begin{tabular}{@ {}l@ {}}
+ \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id}}\\
+ \mbox{}\hspace{2cm}\smath{\{\swap{a}{c}\act t \eqprob
+ \swap{b}{c}\act t', c \freshprob t, c \freshprob t'\} \cup P}
+ \end{tabular}}
+ \end{center}
-
- leads to a more complicated notion of mgu.
+ leads to a more complicated notion of mgu.\medskip\pause
+
+ \footnotesize
+ \smath{\{a.X \eqprob b.Y\} \redu{} (\{a\fresh Y, c\fresh Y\}, [X:=\swap{a}{c}\swap{b}{c}\act Y])}
\end{itemize}
\end{frame}}
@@ -1003,7 +1009,7 @@
\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
+ {\bf One problem:} If we ask whether
\begin{center}
?- type ([(x, T')], lam(x.Var(x)), T)
@@ -1027,7 +1033,7 @@
\begin{frame}<1->
\frametitle{Equivariant Unification}
- James Cheney
+ James Cheney proposed
\begin{center}
\colorbox{cream}{
@@ -1036,7 +1042,7 @@
\end{center}\bigskip\bigskip
\pause
- He also showed that this is undecidable in general. :(
+ But he also showed this problem is undecidable\\ in general. :(
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1054,7 +1060,14 @@
Unfortunately this breaks the mgu-property:
\begin{center}
-
+ \smath{a.Z \eqprob X.Y.v(a)}
+ \end{center}
+
+ can be solved by
+
+ \begin{center}
+ \smath{[X:=a, Z:=Y.v(a)]} and
+ \smath{[Y:=a, Z:=Y.v(Y)]}
\end{center}
\end{frame}}
@@ -1064,7 +1077,7 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1>
+ \begin{frame}<1>[c]
\frametitle{HOPU vs. NOMU}
\begin{itemize}
@@ -1073,7 +1086,7 @@
\colorbox{cream}{\smath{HOPU \Rightarrow NOMU}}
\end{center}\bigskip
- \item Levi\bigskip
+ \item Jordi Levy and Mateu Villaret established\bigskip
\begin{center}
\colorbox{cream}{\smath{HOPU \Leftarrow NOMU}}
\end{center}\bigskip
@@ -1123,10 +1136,12 @@
\frametitle{Complexity}
\begin{itemize}
- \item Maribel Fernandez
+ \item Christiopher Calves and Maribel Fernandez showed first that
+ it is polynomial and then also quadratic
- \item Levi
-
+ \item Jordi Levy and Mateu Villaret showed that it is quadratic
+ by a translation into a subset of NOMU and using ideas from
+ Martelli/Montenari.
\end{itemize}
@@ -1143,14 +1158,18 @@
\begin{itemize}
\item Nominal Unification is a completely first-order
- language, but implements unification modulo $\alpha$.\medskip\pause
+ language, but implements unification modulo $\alpha$.
+ \textcolor{gray}{(verification\ldots Ramana Kumar and Michael Norrish)}
+ \medskip\pause
\item NOMU has been applied in term-rewriting and
- logic programming. I hope it will also be used in typing
+ logic programming. \textcolor{gray}{(Maribel Fernandez et
+ al has a KB-completion procedure.)}
+ 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
+ and considerable research to find this out).\medskip\pause
\item The question about complexity is still an ongoing
story.\medskip
@@ -1168,7 +1187,7 @@
\frametitle{
\begin{tabular}{c}
\mbox{}\\[23mm]
- \alert{\LARGE Thank you very much}\\
+ \alert{\LARGE Thank you very much!}\\
\alert{\Large Questions?}
\end{tabular}}