--- 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