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{ \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \begin{frame}<1> + \small\tt + + \begin{minipage}{13cm} + \begin{tabular}{@ {\hspace{-2mm}}p{11.5cm}} + \\ + From: Zhenyu Qian \\ + To: Christian Urban \\ + 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{ + \begin{frame}<1> + \frametitle{Complexity} + + \begin{itemize} + \item Maribel Fernandez + + \item Levi + + + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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{ + \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{ + \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