# HG changeset patch # User Christian Urban # Date 1278967719 -3600 # Node ID 840a857354f2786e9fcc3bcce96e3b7ddb8b0a21 # Parent b38f8d5e0b093ff5f3aa1ef7115f4e932b811788 more on slides diff -r b38f8d5e0b09 -r 840a857354f2 Slides/Slides2.thy --- a/Slides/Slides2.thy Sun Jul 11 21:18:02 2010 +0100 +++ b/Slides/Slides2.thy Mon Jul 12 21:48:39 2010 +0100 @@ -237,6 +237,8 @@ \end{tikzpicture} \end{textblock}} + + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} diff -r b38f8d5e0b09 -r 840a857354f2 Slides/Slides3.thy --- a/Slides/Slides3.thy Sun Jul 11 21:18:02 2010 +0100 +++ b/Slides/Slides3.thy Mon Jul 12 21:48:39 2010 +0100 @@ -11,6 +11,20 @@ text_raw {* \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010} + + \newcommand{\abst}[2]{#1.#2}% atom-abstraction + \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing + \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions + \newcommand{\unit}{\langle\rangle}% unit + \newcommand{\app}[2]{#1\,#2}% application + \newcommand{\eqprob}{\mathrel{{\approx}?}} + + \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}% + {rgb(0mm)=(0,0,0.9); + rgb(0.9mm)=(0,0,0.7); + rgb(1.3mm)=(0,0,0.5); + rgb(1.4mm)=(1,1,1)} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1>[c] @@ -62,40 +76,45 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} - text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}} - \mbox{}\\[-6mm] + \begin{frame}<1-4>[c] + \frametitle{One Motivation} + + \onslide<2->{Typing implemented in Prolog \textcolor{darkgray}{(from a textbook)}}\bigskip\\ - \begin{itemize} - \item old Nominal provided a reasoning infrastructure for single binders\medskip + \onslide<3->{ + \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\\ - \begin{center} - Lam [a].(Var a) - \end{center}\bigskip - - \item<2-> but representing - + type (Gamma, lam(X, M), arrow(T, T')) :-\\ + \hspace{3cm}type ((X, T)::Gamma, M, T').\smallskip\medskip\\ + + member X X::Tail.\\ + member X Y::Tail :- member X Tail.\\ + \end{tabular}} + + \only<4>{ + \begin{textblock}{6}(2.5,2) + \begin{tikzpicture} + \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\color{darkgray} + \begin{minipage}{8cm}\raggedright + The problem is that \smath{\lambda x.\lambda x. (x\;x)} + gets the types \begin{center} - $\forall\{a_1,\ldots,a_n\}.\; T$ - \end{center}\medskip - - with single binders and reasoning about it is a \alert{\bf major} pain; - take my word for it! - \end{itemize} - - \only<1>{ - \begin{textblock}{6}(1.5,11) - \small - for example\\ - \begin{tabular}{l@ {\hspace{2mm}}l} - & a $\fresh$ Lam [a]. t\\ - & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\ - & Barendregt style reasoning about bound variables\\ + \begin{tabular}{l} + \smath{T\rightarrow (T\rightarrow S) \rightarrow S} and\\ + \smath{(T\rightarrow S)\rightarrow T \rightarrow S}\\ \end{tabular} + \end{center} + \end{minipage}}; + \end{tikzpicture} \end{textblock}} \end{frame}} @@ -105,45 +124,16 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-4> - \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1>[c] + \frametitle{Higher-Order Unification} \begin{itemize} - \item binding sets of names has some interesting properties:\medskip - - \begin{center} - \begin{tabular}{l} - $\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$ - \bigskip\smallskip\\ - - \onslide<2->{% - $\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$ - }\bigskip\smallskip\\ - - \onslide<3->{% - $\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$ - }\medskip\\ - \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type} - \end{tabular} - \end{center} + \item Lambda Prolog with full Higher-Order Unification\\ + \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip + \item Higher-Order Pattern Unification\\ + \textcolor{darkgray}{(has mgus, decidable, some restrictions, modulo $\alpha\beta_0$)} \end{itemize} - - \begin{textblock}{8}(2,14.5) - \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct - \end{textblock} - - \only<4>{ - \begin{textblock}{6}(2.5,4) - \begin{tikzpicture} - \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\normalsize\color{darkgray} - \begin{minipage}{8cm}\raggedright - For type-schemes the order of bound names does not matter, and - alpha-equivalence is preserved under \alert{vacuous} binders. - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -151,23 +141,124 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-3> - \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-10>[t] + \frametitle{Underlying Ideas} \begin{itemize} - \item alpha-equivalence being preserved under vacuous binders is \underline{not} always - wanted:\bigskip\bigskip\normalsize + \item<1-> Unification (\alert{only}) up to $\alpha$ + + \item<2-> Swappings / Permutations + + \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}}} & + \onslide<2-5>{\smath{\lambda a.b}} & - \begin{tabular}{@ {\hspace{-8mm}}l} - $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\ - \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}} - \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and} - \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$} + \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}% + \only<3>{\smath{[b\!:=\!a]}}% + \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} & + \onslide<2-5>{\smath{\lambda c.b}}\\ + + \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda a.a}}\only<4-5>{\smath{\lambda b.a}} & + \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda c.a}}\only<4-5>{\smath{\lambda c.a}}\\ + \end{tabular} + \end{center}\bigskip + + \onslide<4-5>{ + \begin{center} + \begin{tikzpicture} + \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{b} and \smath{a} in \smath{t} \end{tabular} - + \end{minipage}}; + \end{tikzpicture} + \end{center}}\bigskip + + \onslide<5>{ + Unlike for \smath{[b\!:=\!a]\act(-)}, for \smath{\swap{a}{b}\act (-)} we do + have if \smath{t =_\alpha t'} then \smath{\pi \act t =_\alpha \pi \act t'.}}} + + \item<6-> Variables (or holes)\bigskip + + \begin{center} + \onslide<7->{\mbox{}\hspace{-25mm}\smath{\lambda x\hspace{-0.5mm}s .}} + \onslide<8-9>{\raisebox{-1.7mm}{\huge\smath{(}}}\raisebox{-4mm}{\begin{tikzpicture} + \fill[blue] (0, 0) circle (5mm); + \end{tikzpicture}} + \onslide<8-9>{\smath{y\hspace{-0.5mm}s}{\raisebox{-1.7mm}{\huge\smath{)}}}}\bigskip + \end{center} + + \only<8-9>{\smath{y\hspace{-0.5mm}s} are the parameters the hole can depend on\onslide<9->{, but + then you need $\beta_0$-reduction\medskip + \begin{center} + \smath{(\lambda x. t) y \longrightarrow_{\beta_0} t[x:=y]} + \end{center}}} + + \only<10>{we will record the information about which parameters a hole + \alert{\bf cannot} depend on} \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4>[c] + \frametitle{Terms} + + \begin{tabular}{lll @ {\hspace{10mm}}lll} + + \onslide<1->{\pgfuseshading{smallbluesphere}} & + \onslide<1->{\colorbox{cream}{\smath{\unit}}} & + \onslide<1->{Units} & + + \onslide<2->{\pgfuseshading{smallbluesphere}} & + \onslide<2->{\colorbox{cream}{\smath{a}}} & + \onslide<2->{Atoms} \\[5mm] + + \onslide<1->{\pgfuseshading{smallbluesphere}} & + \onslide<1->{\colorbox{cream}{\smath{\pair{t}{t'}}}} & + \onslide<1->{Pairs} & + + \onslide<3->{\pgfuseshading{smallbluesphere}} & + \onslide<3->{\colorbox{cream}{\smath{\abst{a}{t}}}} & + \onslide<3->{Abstractions}\\[5mm] + + \onslide<1->{\pgfuseshading{smallbluesphere}} & + \onslide<1->{\colorbox{cream}{\smath{\app{F}{t}}}} & + \onslide<1->{Funct.} & + + \onslide<4->{\pgfuseshading{smallbluesphere}} & + \onslide<4->{\colorbox{cream}{\smath{\pi\susp X}}} & + \onslide<4->{Suspensions} + \end{tabular} + + \only<2>{ + \begin{textblock}{13}(1.5,12) + \small Atoms are constants \textcolor{darkgray}{(infinitely many of them)} + \end{textblock}} + + \only<3>{ + \begin{textblock}{13}(1.5,12) + \small \smath{\ulcorner \lambda\abst{a}{a}\urcorner \mapsto \text{fn\ }\abst{a}{a}}\\ + \small constructions like \smath{\text{fn\ }\abst{X}{X}} are not allowed + \end{textblock}} + + \only<4>{ + \begin{textblock}{13}(1.5,12) + \small \smath{X} is a variable standing for a term\\ + \small \smath{\pi} is an explicit permutation \smath{\swap{a_1}{b_1}\ldots\swap{a_n}{b_n}}, + waiting to be applied to the term that is substituted for \smath{X} + \end{textblock}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -176,23 +267,33 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-3>[c] + \frametitle{Permutations} + + a permutation applied to a term + + \begin{center} + \begin{tabular}{lrcl} + \pgfuseshading{smallbluesphere} & + \smath{[]\act c} & \smath{\dn} & \smath{c} \\ - \begin{itemize} - \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip - - \begin{center} - \begin{tabular}{@ {\hspace{-8mm}}l} - $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\ - $\;\;\;\not\approx_\alpha - \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$ + \pgfuseshading{smallbluesphere} & + \smath{\swap{a}{b}\!::\!\pi\act c} & \smath{\dn} & + \smath{\begin{cases} + a & \text{if}\;\pi\act c = b\\ + b & \text{if}\;\pi\act c = a\\ + \pi\act c & \text{otherwise} + \end{cases}}\\ + + \onslide<2->{\pgfuseshading{smallbluesphere}} & + \onslide<2->{\smath{\pi\act\abst{a}{t}}} & \onslide<2->{\smath{\dn}} & + \onslide<2->{\smath{\abst{\pi\act a}{\pi\act t}}}\\ + + \onslide<3->{\pgfuseshading{smallbluesphere}} & + \onslide<3->{\smath{\pi\act\pi'\act X}} & \onslide<3->{\smath{\dn}} & + \onslide<3->{\smath{(\pi @ \pi')\act X}}\\ \end{tabular} \end{center} - - - \end{itemize} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -201,25 +302,56 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-3>[c] + \frametitle{Freshness Constraints} + + Recall \smath{\lambda a. \raisebox{-0.7mm}{\tikz \fill[blue] (0, 0) circle (2.5mm);}} + \bigskip\pause + + We therefore will identify + + \begin{center} + \smath{\mathtt{fn\ } a. X \;\approx\; \mathtt{fn\ } b. \alert<3->{\swap{a}{b}}\act X} + \end{center} + + provided that `\smath{b} is fresh for \smath{X} --- (\smath{b\fresh X})', + i.e., does not occur freely in any ground term that might be substituted for + \smath{X}.\bigskip\pause + + If we know more about \smath{X}, e.g., if we knew that \smath{a\fresh X} and + \smath{b\fresh X}, then we can replace\\ \smath{\swap{a}{b}\act X} by + \smath{X}. - \begin{itemize} - \item the order does not matter and alpha-equivelence is preserved under - vacuous binders \textcolor{gray}{(restriction)}\medskip - - \item the order does not matter, but the cardinality of the binders - must be the same \textcolor{gray}{(abstraction)}\medskip + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4>[c] + \frametitle{Equivalence Judgements} - \item the order does matter - \end{itemize} + \alt<1>{Our equality is {\bf not} just}{but judgements} + + \begin{center} + \begin{tabular}{rl} + \colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} t \approx t'}} & \alert{$\alpha$-equivalence}\\[1mm] + \onslide<4->{\colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} a \fresh t}}} & + \onslide<4->{\alert{freshness}} + \end{tabular} + \end{center} \onslide<2->{ + where \begin{center} - \isacommand{bind\_res}\hspace{6mm} - \isacommand{bind\_set}\hspace{6mm} - \isacommand{bind} + \smath{\nabla = \{a_1\fresh X_1,\ldots, a_n\fresh X_n\}} + \end{center} + is a finite set of \alert{freshness assumptions}.} + + \onslide<3->{ + \begin{center} + \smath{\{a\fresh X,b\fresh X\} \vdash \text{fn\ } a. X \approx \text{fn\ } b. X} \end{center}} \end{frame}} @@ -229,28 +361,39 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-3> - \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}} - \mbox{}\\[-6mm] + \begin{frame}<1>[c] + \frametitle{Rules for Equivalence} + + \begin{center} + \begin{tabular}{c} + Excerpt\\ + (i.e.~only the interesting rules) + \end{tabular} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} - \mbox{}\hspace{10mm} - \begin{tabular}{ll} - \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ - \hspace{5mm}\phantom{$|$} Var name\\ - \hspace{5mm}$|$ App trm trm\\ - \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm - & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\ - \hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm - & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\ - \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ - \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\ - \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\ - \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\ +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1>[c] + \frametitle{Rules for Equivalence} + + \begin{center} + \begin{tabular}{c} + \colorbox{cream}{\smath{\infer{\nabla \vdash a \approx a}{}}}\\[8mm] + + \colorbox{cream}{% + \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{a}{t'}} + {\nabla \vdash t \approx t'}}}\\[8mm] + + \colorbox{cream}{% + \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{b}{t'}} + {a\not=b\;\; & \nabla \vdash t \approx \swap{a}{b}\act t'\;\;& \nabla \vdash a\fresh t'}}} \end{tabular} - - + \end{center} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -259,60 +402,61 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-5> - \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item this way of specifying binding is inspired by - Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip - + \begin{frame}<1-3>[c] + \frametitle{Rules for Equivalence} - \only<2>{ - \begin{itemize} - \item Ott allows specifications like\smallskip \begin{center} - $t ::= t\;t\; |\;\lambda x.t$ + \colorbox{cream}{% + \smath{% + \infer{\nabla \vdash \pi\act X \approx \pi'\act X} + {\begin{array}{c} + (a\fresh X)\in\nabla\\ + \text{for all}\; a \;\text{with}\;\pi\act a \not= \pi'\act a + \end{array} + }}} \end{center} - \end{itemize}} - \only<3-4>{ - \begin{itemize} - \item whether something is bound can depend in Ott on other bound things\smallskip + \onslide<2->{ + for example\\[4mm] + + \alt<2>{% + \begin{center} + \smath{\{a\fresh\!X, b\fresh\!X\} \vdash X \approx \swap{a}{b}\act X} + \end{center}} + {% \begin{center} - \begin{tikzpicture} - \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$}; - \node (B) at ( 1.1,1) {$s$}; - \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};} - \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);} - \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);} - \end{tikzpicture} - \end{center} - \onslide<4>{this might make sense for ``raw'' terms, but not at all - for $\alpha$-equated terms} - \end{itemize}} + \smath{\{a\fresh\!X, c\fresh\!X\} \vdash \swap{a}{c}\swap{a}{b}\act X \approx \swap{b}{c}\act X} + \end{center}} - \only<5>{ - \begin{itemize} - \item we allow multiple binders and bodies\smallskip + \onslide<3->{ + \begin{tabular}{@ {}lllll@ {}} + because & + \smath{\swap{a}{c}\swap{a}{b}}: & + \smath{a\mapsto b} & + \smath{\swap{b}{c}}: & + \smath{a\mapsto a}\\ + & & \smath{b\mapsto c} & & \smath{b\mapsto c}\\ + & & \smath{c\mapsto a} & & \smath{c\mapsto b}\\ + \end{tabular} + disagree at \smath{a} and \smath{c}.} + } + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1>[c] + \frametitle{Rules for Freshness} + \begin{center} - \isacommand{bind} a b c \isacommand{in} x y z - \end{center}\bigskip\medskip - the reason is that in general - \begin{center} - \begin{tabular}{rcl} - \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ & - \begin{tabular}{@ {}l} - \isacommand{bind\_res} as \isacommand{in} x,\\ - \isacommand{bind\_res} as \isacommand{in} y + \begin{tabular}{c} + Excerpt\\ + (i.e.~only the interesting rules) \end{tabular} - \end{tabular} - \end{center}\smallskip - - same with \isacommand{bind\_set} - \end{itemize}} - \end{itemize} - + \end{center} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -321,26 +465,26 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1>[c] + \frametitle{Rules for Freshness} - \begin{itemize} - \item in old Nominal, we represented single binders as partial functions:\bigskip + \begin{center} + \begin{tabular}{c} + \colorbox{cream}{% + \smath{\infer{\nabla \vdash a\fresh b}{a\not= b}}}\\[5mm] - \begin{center} - \begin{tabular}{l} - Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm] - \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\ - \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\; - \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ + \colorbox{cream}{% + \smath{\infer{\nabla \vdash a\fresh\abst{a}{t}}{}}}\hspace{7mm} + \colorbox{cream}{% + \smath{\infer{\nabla \vdash a\fresh\abst{b}{t}} + {a\not= b\;\; & \nabla \vdash a\fresh t}}}\\[5mm] + + \colorbox{cream}{% + \smath{\infer{\nabla \vdash a\fresh \pi\act X} + {(\pi^{-1}\act a\fresh X)\in\nabla}}} \end{tabular} \end{center} - \end{itemize} - \begin{textblock}{10}(2,14) - \footnotesize $^*$ alpha-equality coincides with equality on functions - \end{textblock} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -348,105 +492,43 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-> - \frametitle{\begin{tabular}{c}New Design\end{tabular}} - \mbox{}\\[4mm] + \begin{frame}<1-4>[t] + \frametitle{$\approx$ is an Equivalence} + \mbox{}\\[5mm] \begin{center} - \begin{tikzpicture} - \alt<2> - {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};} - {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};} - - \alt<3> - {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};} - {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};} + \colorbox{cream}{\alert{Theorem:} + $\approx$ is an equivalence relation.} + \end{center}\bigskip - \alt<4> - {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};} - {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};} - - \alt<5> - {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};} - {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};} - - \alt<6> - {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};} - {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};} - - \alt<7> - {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] - (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};} - {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] - (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};} - - \draw[->,white!50,line width=1mm] (A) -- (B); - \draw[->,white!50,line width=1mm] (B) -- (C); - \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] - (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D); - \draw[->,white!50,line width=1mm] (D) -- (E); - \draw[->,white!50,line width=1mm] (E) -- (F); - \end{tikzpicture} - \end{center} + \only<1>{% + \begin{tabular}{ll} + (Reflexivity) & $\smath{\nabla\vdash t\approx t}$\\[2mm] + (Symmetry) & if $\smath{\nabla\vdash t_1\approx t_2}\;$ + then $\;\smath{\nabla\vdash t_2\approx t_1}$\\[2mm] + (Transitivity) & if $\smath{\nabla\vdash t_1\approx t_2}\;$ and + $\;\smath{\nabla\vdash t_2\approx t_3}$\\ + & then $\smath{\nabla\vdash t_1\approx t_3}$\\ + \end{tabular}} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - + \only<2->{% + \begin{itemize} + \item<2-> \smath{\nabla \vdash t\approx t'} then \smath{\nabla \vdash \pi\act t\approx \pi\act t'} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-9> - \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item lets first look at pairs\bigskip\medskip - - \begin{tabular}{@ {\hspace{1cm}}l} - $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}% - \only<8>{${}_{\text{\alert{list}}}$}% - \only<9>{${}_{\text{\alert{res}}}$}}% - \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ - \end{tabular}\bigskip - \end{itemize} + \item<2-> \smath{\nabla \vdash a\fresh t} then + \smath{\nabla \vdash \pi\act a\fresh \pi\act t} - \only<1>{ - \begin{textblock}{8}(3,8.5) - \begin{tabular}{l@ {\hspace{2mm}}p{8cm}} - & $as$ is a set of atoms\ldots the binders\\ - & $x$ is the body\\ - & $\approx_{\text{set}}$ is where the cardinality - of the binders has to be the same\\ - \end{tabular} - \end{textblock}} + \item<3-> \smath{\nabla \vdash t\approx \pi\act t'} then + \smath{\nabla \vdash (\pi^{-1})\act t\approx t'} + + \item<3-> \smath{\nabla \vdash a\fresh \pi\act t} then + \smath{\nabla \vdash (\pi^{-1})\act a\fresh t} - \only<4->{ - \begin{textblock}{12}(5,8) - \begin{tabular}{ll@ {\hspace{1mm}}l} - $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm] - & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm] - & \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm] - & \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\ - \end{tabular} - \end{textblock}} - - \only<8>{ - \begin{textblock}{8}(3,13.8) - \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms - \end{textblock}} + \item<4-> \smath{\nabla \vdash a\fresh t} and \smath{\nabla \vdash t\approx t'} then + \smath{\nabla \vdash a\fresh t'} + \end{itemize} + } + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -454,72 +536,68 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Examples\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-4> + \frametitle{Comparison $=_\alpha$} - \begin{itemize} - \item lets look at ``type-schemes'':\medskip\medskip + Traditionally \smath{=_\alpha} is defined as \begin{center} - $(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$ - \end{center}\medskip + \colorbox{cream}{% + \begin{minipage}{9cm} + \raggedright least congruence which identifies \smath{\abst{a}{t}} + with \smath{\abst{b}{[a:=b]t}} provided \smath{b} is not free + in \smath{t} + \end{minipage}} + \end{center} - \onslide<2->{ - \begin{center} - \begin{tabular}{l} - $\text{fv}(x) = \{x\}$\\[1mm] - $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\ - \end{tabular} - \end{center}} - \end{itemize} + where \smath{[a:=b]t} replaces all free occurrences of\\ + \smath{a} by \smath{b} in \smath{t}. + \bigskip + \only<2>{% + \begin{textblock}{13}(1.2,10) + For \alert{ground} terms: - \only<2->{ - \begin{textblock}{4}(0.3,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - \\ + \begin{center} + \colorbox{cream}{% + \begin{minipage}{9.0cm} + \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} \end{tabular} - \end{minipage}}; - \end{tikzpicture} + \end{minipage}} + \end{center} \end{textblock}} - \only<2->{ - \begin{textblock}{4}(5.2,12) + + \only<3>{% + \begin{textblock}{13}(1.2,10) + In general \smath{=_\alpha} and \smath{\approx} are distinct! + \begin{center} + \colorbox{cream}{% + \begin{minipage}{6.0cm} + \smath{\abst{a}{X}=_\alpha \abst{b}{X}\;} but not\\[2mm] + \smath{\emptyset \vdash \abst{a}{X} \approx \abst{b}{X}\;} (\smath{a\not=b}) + \end{minipage}} + \end{center} + \end{textblock}} + + \only<4>{ + \begin{textblock}{6}(1,2) \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{set:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - \only<2->{ - \begin{textblock}{4}(10.2,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{list:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} + \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\color{darkgray} + \begin{minipage}{10cm}\raggedright + That is a crucial point: if we had\\[-2mm] + \[\smath{\emptyset \vdash \abst{a}{X}\approx \abst{b}{X}}\mbox{,}\] + then applying $\smath{[X:=a]}$, $\smath{[X:=b]}$, $\ldots$\\ + give two terms that are {\bf not} $\alpha$-equivalent.\\[3mm] + The freshness constraints $\smath{a\fresh X}$ and $\smath{b\fresh X}$ + rule out the problematic substitutions. Therefore + + \[\smath{\{a\fresh X,b\fresh X\} \vdash \abst{a}{X}\approx \abst{b}{X}}\] + + does hold. \end{minipage}}; \end{tikzpicture} \end{textblock}} @@ -531,136 +609,73 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Examples\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-9> + \frametitle{Substitution} + + \begin{tabular}{l@ {\hspace{8mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {}} + \pgfuseshading{smallbluesphere} & + \smath{\sigma(\abst{a}{t})} & \smath{\dn} & \smath{\abst{a}{\sigma(t)}}\\[2mm] - \begin{center} - \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} - \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$} - \end{center} - - \begin{itemize} - \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% - \only<2>{, \alert{$\not\approx_{\text{list}}$}} - \end{itemize} + \pgfuseshading{smallbluesphere} & + \smath{\sigma(\pi\act X)} & \smath{\dn} & + \smath{\begin{cases}% + \pi\;\act\;\sigma(X) & \!\!\text{if\ } \sigma(X)\not=X\\ + \pi\act X & \!\!\text{otherwise}% + \end{cases}}\\[6mm] + \end{tabular}\bigskip\bigskip - - \only<1->{ - \begin{textblock}{4}(0.3,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - \\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - \only<1->{ - \begin{textblock}{4}(5.2,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{set:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - \only<1->{ - \begin{textblock}{4}(10.2,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{list:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} + \pause + \only<2-5>{ + \only<2->{for example} + \def\arraystretch{1.3} + \begin{tabular}{@ {\hspace{14mm}}l@ {\hspace{3mm}}l} + \onslide<2->{\textcolor{white}{$\Rightarrow$}} & + \onslide<2->{\alt<3>{\smath{\underline{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}} + {\smath{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}\\ + \onslide<3->{\smath{\Rightarrow}} & + \onslide<3->{\alt<3,4>{\smath{\abst{a}{\underline{\swap{a}{b}\act X[X:=\pair{b}{Y}]}}}} + {\smath{\abst{a}{\swap{a}{b}\act X}[X:=\pair{b}{Y}]}}}\\ + \onslide<4->{\smath{\Rightarrow}} & + \onslide<4->{\alt<4>{\smath{\abst{a}{\swap{a}{b}\act \underline{\pair{b}{Y}}}}} + {\smath{\abst{a}{\underline{\swap{a}{b}}\act \pair{b}{Y}}}}}\\ + \onslide<5->{\smath{\Rightarrow}} & + \onslide<5->{\smath{\abst{a}{\pair{a}{\swap{a}{b}\act Y}}}} + \end{tabular}} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}Examples\end{tabular}} - \mbox{}\\[-3mm] + \only<6-> + {\begin{tabular}{l@ {\hspace{8mm}}l@ {}} + \pgfuseshading{smallbluesphere} & + if \smath{\nabla\vdash t\approx t'} and\hspace{-2mm}\mbox{} + \raisebox{-2.7mm}{ + \alt<7>{\begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=3mm] + {\smath{\;\nabla'\vdash\sigma(\nabla)\;}}; + \end{tikzpicture}} + {\begin{tikzpicture} + \draw (0,0) node[inner sep=1mm,fill=white, very thick, draw=white, rounded corners=3mm] + {\smath{\;\nabla'\vdash\sigma(\nabla)\;}}; + \end{tikzpicture}}}\\ + & then \smath{\nabla'\vdash\sigma(t)\approx\sigma(t')} + \end{tabular}} - \begin{center} - \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$} - \end{center} + \only<9> + {\begin{tabular}{l@ {\hspace{8mm}}l@ {}} + \\[-4mm] + \pgfuseshading{smallbluesphere} & + \smath{\sigma(\pi\act t)=\pi\act\sigma(t)} + \end{tabular}} - \begin{itemize} - \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$, - $\not\approx_{\text{list}}$ - \end{itemize} - - \only<1->{ - \begin{textblock}{4}(0.3,12) + \only<7>{ + \begin{textblock}{6}(10,10.5) \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{res:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - \\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - \only<1->{ - \begin{textblock}{4}(5.2,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{set:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - \only<1->{ - \begin{textblock}{4}(10.2,12) - \begin{tikzpicture} - \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\tiny\color{darkgray} - \begin{minipage}{3.4cm}\raggedright - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {}l}{list:}\\ - $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ - $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \cdot x = y$\\ - $\wedge$ & $\pi \cdot as = bs$\\ - \end{tabular} + \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=2mm] + {\color{darkgray} + \begin{minipage}{3.8cm}\raggedright + this means\\[1mm] + \smath{\nabla'\vdash a\fresh\sigma(X)}\\[1mm] + holds for all\\[1mm] + \smath{(a\fresh X)\in\nabla} \end{minipage}}; \end{tikzpicture} \end{textblock}} @@ -672,190 +687,23 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-3> - \frametitle{\begin{tabular}{c}General Abstractions\end{tabular}} - \mbox{}\\[-7mm] + \begin{frame}<1-> + \frametitle{Equational Problems} - \begin{itemize} - \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip - \item they are equivalence relations\medskip - \item we can therefore use the quotient package to introduce the - types $\beta\;\text{abs}_\star$\bigskip - \begin{center} - \only<1>{$[as].\,x$} - \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$} - \only<3>{% - \begin{tabular}{r@ {\hspace{1mm}}l} - \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=} [bs].y\;\;\;\text{if\!f}$}\\[2mm] - $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\ - $\wedge$ & $\text{supp}(x) - as \fresh^* \pi$\\ - $\wedge$ & $\pi \act x = y $\\ - $(\wedge$ & $\pi \act as = bs)\;^\star$\\ - \end{tabular}} - \end{center} - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}One Problem\end{tabular}} - \mbox{}\\[-3mm] + An equational problem + \[ + \colorbox{cream}{\smath{t \eqprob t'}} + \] + is \alert{solved} by \begin{center} - $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$ + \begin{tabular}{ll} + \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma} (terms for variables)\\[3mm] + \pgfuseshading{smallbluesphere} & {\bf and} a set of freshness assumptions \smath{\nabla} + \end{tabular} \end{center} - \begin{itemize} - \item we cannot represent this as\medskip - \begin{center} - $\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$ - \end{center}\bigskip - - because\medskip - \begin{center} - $\text{let}\;[x].s\;\;[t_1,t_2]$ - \end{center} - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-> - \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}} - \mbox{}\\[-6mm] - - \mbox{}\hspace{10mm} - \begin{tabular}{ll} - \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ - \hspace{5mm}\phantom{$|$} Var name\\ - \hspace{5mm}$|$ App trm trm\\ - \hspace{5mm}$|$ Lam x::name t::trm - & \isacommand{bind} x \isacommand{in} t\\ - \hspace{5mm}$|$ Let as::assn t::trm - & \isacommand{bind} bn(as) \isacommand{in} t\\ - \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ - \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ - \end{tabular} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}``Raw'' Definitions\end{tabular}} - \mbox{}\\[-6mm] - - \mbox{}\hspace{10mm} - \begin{tabular}{ll} - \multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\ - \hspace{5mm}\phantom{$|$} Var name\\ - \hspace{5mm}$|$ App trm trm\\ - \hspace{5mm}$|$ Lam name trm\\ - \hspace{5mm}$|$ Let assn trm\\ - \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm] - \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ - \end{tabular} - - \only<2>{ - \begin{textblock}{5}(10,5) - $+$ \begin{tabular}{l}automatically\\ - generate fv's\end{tabular} - \end{textblock}} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} - \mbox{}\\[6mm] - - \begin{center} - Lam x::name t::trm \hspace{10mm}\isacommand{bind} x \isacommand{in} t\\ - \end{center} - - - \[ - \infer[\text{Lam-}\!\approx_\alpha] - {\text{Lam}\;x\;t \approx_\alpha \text{Lam}\;x'\;t'} - {([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} - ^{\approx_\alpha,\text{fv}} ([x'], t')} - \] - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} - \mbox{}\\[6mm] - - \begin{center} - Lam x::name y::name t::trm s::trm \hspace{5mm}\isacommand{bind} x y \isacommand{in} t s\\ - \end{center} - - - \[ - \infer[\text{Lam-}\!\approx_\alpha] - {\text{Lam}\;x\;y\;t\;s \approx_\alpha \text{Lam}\;x'\;y'\;t'\;s'} - {([x, y], (t, s)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} - ^{R, fv} ([x', y'], (t', s'))} - \] - - \footnotesize - where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$ - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} - \mbox{}\\[6mm] - - \begin{center} - Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\ - \end{center} - - - \[ - \infer[\text{Let-}\!\approx_\alpha] - {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'} - {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} - ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') & - \onslide<2>{as \approx_\alpha^{\text{bn}} as'}} - \] + so that \smath{\nabla\vdash \sigma(t)\approx \sigma(t')}. \end{frame}} @@ -866,143 +714,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1-> - \frametitle{\begin{tabular}{c}\LARGE{}$\alpha$ for Binding Functions\end{tabular}} - \mbox{}\\[-6mm] - - \mbox{}\hspace{10mm} - \begin{tabular}{l} - \ldots\\ - \isacommand{binder} bn \isacommand{where}\\ - \phantom{$|$} bn(ANil) $=$ $[]$\\ - $|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)\\ - \end{tabular}\bigskip - - \begin{center} - \mbox{\infer{\text{ANil} \approx_\alpha^{\text{bn}} \text{ANil}}{}}\bigskip - - \mbox{\infer{\text{ACons}\;a\;t\;as \approx_\alpha^{\text{bn}} \text{ACons}\;a'\;t'\;as'} - {t \approx_\alpha t' & as \approx_\alpha^{bn} as'}} - \end{center} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-> - \frametitle{\begin{tabular}{c}Automatic Proofs\end{tabular}} - \mbox{}\\[-6mm] - - \begin{itemize} - \item we can show that $\alpha$'s are equivalence relations\medskip - \item as a result we can use the quotient package to introduce the type(s) - of $\alpha$-equated terms - - \[ - \infer - {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'} - {\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} - ^{=,\text{supp}} ([x'], t')}% - \only<2>{[x].t = [x'].t'}} - \] - - - \item the properties for support are implied by the properties of $[\_].\_$ - \item we can derive strong induction principles (almost automatic---just a matter of - another week or two) - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1>[t] - \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}} - \mbox{}\\[-7mm]\mbox{} - - \footnotesize - \begin{center} - \begin{tikzpicture} - \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}}; - - \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}}; - - \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}}; - - \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}}; - - \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}}; - - \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] - (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}}; - - \draw[->,white!50,line width=1mm] (A) -- (B); - \draw[->,white!50,line width=1mm] (B) -- (C); - \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] - (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D); - \draw[->,white!50,line width=1mm] (D) -- (E); - \draw[->,white!50,line width=1mm] (E) -- (F); - \end{tikzpicture} - \end{center} - - \begin{itemize} - \item Core Haskell: 11 types, 49 term-constructors, - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-> - \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}} - \mbox{}\\[-6mm] - - \small - \mbox{}\hspace{10mm} - \begin{tabular}{ll} - \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ - \hspace{5mm}\phantom{$|$} Var name\\ - \hspace{5mm}$|$ App trm trm\\ - \hspace{5mm}$|$ Lam x::name t::trm - & \isacommand{bind} x \isacommand{in} t\\ - \hspace{5mm}$|$ Let as::assn t::trm - & \isacommand{bind} bn(as) \isacommand{in} t\\ - \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ - \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ - \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ - \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ - \end{tabular}\bigskip\medskip - - we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-> - \frametitle{\begin{tabular}{c}Conclusion\end{tabular}} - \mbox{}\\[-6mm] + \frametitle{Conclusion} \begin{itemize} \item the user does not see anything of the raw level\medskip