Select Git revision
slides-xxx-church-to-curry.tex
slides-xxx-church-to-curry.tex 10.52 KiB
% !TeX root = slides.tex
\section{Logical Relations along Morphisms}
\newcommand{\relCol}[1]{\textcolor{PineGreen}{#1}}
\newcommand{\morCol}[1]{\alert{#1}}
\newcommand{\secondMorCol}[1]{\alert{#1}}
\newcommand{\domCol}[1]{\textcolor{blue}{#1}}
\begin{frame}{Logical Relations of a Single Morphism}
%\structure{Recall unary logical relation $\TND$:}
%
\begin{tikzpicture}[
edge from parent/.style={draw=none},% hide arrow
%remember picture,
]
\node (domainDummy) {}; % used to get both leftDomainBody and rightDomainBody on the same height
\node (leftDomainBody) [below=0.125 of domainDummy] {%
$\begin{aligned}
\prop &\colon \type\\
\atom &\colon \type\\[0.3em]
%
\inj &\colon \atom \to \prop\\
\mathnormal{\wedge} &\colon \prop \to \prop \to \prop
\end{aligned}$%
};
\node (rightDomainBody) [below right=0.125 and 3.5 of domainDummy] {%
$\begin{aligned}
&\lam{p}{\prop} \relCol{\vtnd{p}}\\
&\lam{a}{\atom} \relCol{\vtnd{\inj(a)}}\\[0.3em]
&\text{for }\relCol{a}\colon\atom\text{:}\quad \relCol{\inj(a)}\\
&\text{for }\relCol{p}\,\relCol{q}\colon\prop\text{:}\quad \relCol{p \wedge q}
\end{aligned}$%
};
\draw[draw=none] (leftDomainBody.north west) -- (rightDomainBody.north east) node[above,midway] {$\theory{\PL}$};
\draw (leftDomainBody.north west) rectangle (rightDomainBody.south east);
\end{tikzpicture}
\vspace{0.15em}
% full-width horizontal line
\par\hspace*{-\dimexpr0.5\paperwidth-0.5\textwidth}\rule[0.5\baselineskip]{\paperwidth}{1.5pt}
\only<1>{%
\newcommand\curMor{\morCol{\id{\PL}}}%
\newcommand\curCod{\relCol{\PL}}%
}%
\only<2->{%
\newcommand\curMor{\morCol{v}}%
\newcommand\curCod{\relCol{T}}%
}%
\only<3>{%
\newcommand\secondMor{\secondMorCol{w}}%
}%
\begin{tikzpicture}[
edge from parent/.style={draw=none},% hide arrow
%remember picture,
]
\node (domain) {$\theory{\PL}$};
\node (domainBody) [below=0.125 of domain,rectangle,draw] {%
$\begin{aligned}
\prop &\colon \type\\
\atom &\colon \type\\[0.3em]
%
\inj &\colon \atom \to \prop\\
\mathnormal{\wedge} &\colon \prop \to \prop \to \prop
\end{aligned}$%
};
\node (domainDesc) [below=0.14 of domainBody] {``structure space''};
\node (codomain) [right=4.25 of domain] {$\theory{\curCod}$};
\node (codomainBody) [below=0.125 of codomain,rectangle,draw] {%
$\begin{aligned}
&\lam{p}{\curMor(\prop)} \only<3->{\lam{p'}{\secondMor(\prop)}\ldots}\only<-2>{\relCol{\vtnd{p}}}\\
&\lam{a}{\curMor(\atom)}\only<3->{\lam{a'}{\secondMor(\atom)}\ldots}\only<-2>{\relCol{\vtnd{\inj(a)}}}\\[0.3em]
%
&\text{for }\relCol{a}\colon\curMor(\atom)\only<3->{\text{, }\relCol{a'}\colon\secondMor(\atom)}\text{:}\quad \relCol{\curMor(\inj)(a)}\\
&\text{for }\relCol{p}\,\relCol{q}\colon\curMor(\prop)\text{:}\quad \relCol{p \curMor(\wedge) q}
\end{aligned}$%
};
\node (codomainDesc) [below=0.14 of codomainBody] {``assertion/proof space''};
\only<1-2>{
\draw[->] (domain.east) -- (codomain.west) node[above,midway] {$\curMor$};
}
\only<3->{
\draw[transform canvas={yshift=0.3ex},->] (domain.east) -- (codomain.west) node[above,midway] {$\curMor$};
\draw[transform canvas={yshift=-0.3ex},->] (domain.east) -- (codomain.west) node[below,midway] {$\secondMor$};
}
\end{tikzpicture}
\note[item]{Read as logical relation over that morphism}
\end{frame}
\begin{frame}{Logical Relations of a Single Morphism}
\structure{So far:}
$\logRel{\TND}{\id{\PL}}{\PL}{\PL} = \{\ldots\}$:
{\centering\includegraphics[height=3cm]{./img/pl-log-rel-setting.png}}
\structure{What does $\id{\PL}$ stand for?}
{\centering\includegraphics[height=3cm]{./img/pl-log-rel-setting-generalized.png}}
\end{frame}
\begin{frame}{Towards $n$-ary Logical Relations}
\structure{Intuition}:\begin{itemize}
\item have a \alert{single identity morphism} $\id{T}$\\\rightThing{idea: generalize to $\mu: S \to T$}
\item relation asserts a \alert{unary predicate} $C_\tau(t) = C_\tau(\id{T}(t))$ for every $t \colon \tau$ of the domain\\\rightThing{idea: generalize to $n$-ary predicates with $n$ morphisms $S \to T$}
\item domain is ``structure'' space
\item codomain is ``assertion and proof'' space\\\rightThing{idea: need not be the same}
\end{itemize}
\end{frame}
\begin{frame}{$n$-ary Logical Relations}
\begin{itemize}
\item let $\mu_1, \ldots, \mu_n\colon S \to T$ be morphisms\\\rightThing{on common (co)domain theories}
\item introduce construct \[\logRel{r}{\mu_1\times\cdots\times\mu_n}{S}{T} = \{c_1 := e_1, \ldots\}\]
{\centering\includegraphics[height=3cm]{./img/pl-log-rel-setting-generalized.png}}
\end{itemize}
\end{frame}
\begin{frame}{Example 3: Church To Curry}
\begin{example}[Intrinsic vs. Extrinsic Typing]
A type theory is\begin{itemize}
\item \alert{intrinsically typed} if its terms carry their types.\\
\rightThing{pair constructor takes type arguments \emph{and} typed terms}\\
\rightThing{$\tpNot{(a,b)}{A \times B}$ is a term}
%
\item\alert{extrinsically typed} if its terms are untyped, but ``external'' typing judgements exist.\\[-0.25em]
\rightThing{pair constructor takes untyped terms}\\
\rightThing{$(a,b)$ is a term}\\
\rightThing{$\ofType{(a,b)}{A \times B}$ a typing judgement}
\end{itemize}
\end{example}
\rightOptional{also ``Church vs. Curry''}
\end{frame}
\newcommand\churchProdTheory{%
\left\{\begin{aligned}%
&\tp &&\colon \type\\%
&\tm &&\colon \tp \to \type\\[0.4em]%
&\_ \times \_ &&\colon \tp \to \tp \to \tp\\%
&\tpNot{(\_, \_)}{\_\times\_}\hspace{-0.5em}&&\colon \tpi{A\,B}{\tp} \ttm{A} \to \ttm{B} \to \ttm{A \times B}%
\end{aligned}\right\}%
}
\newcommand\curryProdTheory{%
\left\{\begin{aligned}%
\tp,\tm \colon \type\\%
&\ofType{\_}{\_} &&\colon \tm \to \tp \to \type\\[0.4em]%
&\_ \times \_ &&\colon \tp \to \tp \to \tp\\%
&(\_,\_)&&\colon \tm \to \tm \to \tm\\%
&\tpNot{(\_,\_)}{T,\_\times\_}\hspace{-0.75em}&&\colon \tpi{A\,B}{\tp} \tpi{a\,b}{\tm}\\%
&&&\quad\quad\ofTermType{a}{A} \to \ofTermType{b}{B} \to \ofTermType{(a, b)}(A \times B)%
\end{aligned}\right\}%
}
\newcommand\typeErasView{%
\begin{aligned}%
&\tp &&:= \tp\\%
&\tm &&:= \ignorelam \tm\\%
&\_ \times \_ &&:= \_ \times \_%
\hspace{7em}\text{e.g. }\TypeEras(\tpNot{(a, b)}{A \times B}) = (a,b)\\%
&\tpNot{(\_, \_)}{\_\times\_} &&:= \ignorelam\ignorelam (\_, \_)%
\hspace{5em}\text{\alert{type information lost!}}%
\end{aligned}%
}
\begin{frame}{Church and Curry Products}
\vspace{-1.5em}
{\footnotesize\begin{align*}
&\theory{\ChurchProd} &&= \churchProdTheory\\[0.2em]
&\theory{\CurryProd} &&= \curryProdTheory\\
%
%
&\multispan{5}{$\view{\TypeEras}{\ChurchProd}{\CurryProd} = \{$}\\[-0.25em]
&\multispan{4}{$\quad\quad\typeErasView$}\\[-0.25em]
&\multispan{4}{$\}$}
\end{align*}}
\end{frame}
%\newcommand\beamermathcolor[1]{\color{#1}\setbeamercolor{math text}{fg=#1}}
%
%\newcommand{\colWit}[1]{{\beamermathcolor{Emerald}#1}}
%\newcommand{\colRel}[1]{{\beamermathcolor{green}#1}}
%\newcommand{\colArg}[1]{{\beamermathcolor{red}#1}}
%\newcommand{\coloredOfType}[2]{#1 \mathrel{\colRel{::}} #2}
\begin{frame}{Capturing Type Preservation}
\structure{Desired property:}\rightOptional{to be captured \emph{within} the formalization}
\begin{theorem}[Type Preservation]
If $\;\vdash_{\ChurchProd} t \colon \ttm{A}$, %
\only<1-2>{then }%
\only<3->{\alert{there is $\wit$ st.} }%
\[
\vdash_{\CurryProd}%
\only<1>{\ofType{\TypeEras(t)}{A}}%
\only<2>{\ofType{\TypeEras(t)}{\TypeEras(A)}}%
\only<3>{\wit\colon\ofType{\TypeEras(t)}{\TypeEras(A)}}%
\only<4->{\colWit{\wit}\colon\coloredOfType{\colArg{\TypeEras(t)}}{\colArg{\TypeEras(A)}}}.%
\]
\end{theorem}
\onslide<2>{\rightOptional{$\TypeEras$ is identity on types $A\colon\tp$}}%
\onslide<5->{\structure{Resembles Basic Lemma:}
let $\nakedLogRel{r}{\mu}{S}{T}$ be a logical relation over $\mu\colon S \to T$, then
\begin{theorem}[Basic Lemma]
If $\;\vdash_S t \colon \tpName$, then $\,\vdash_T \colWit{r(t)} \colon \colRel{r(\tpName)}\ \colArg{\mu(t)}$.
\end{theorem}
\smallskip
$\Rightarrow$ create relation $\nakedLogRel{\TypePres}{\TypeEras}{\ChurchProd}{\CurryProd}$ mapping $\ttm{-}$ to $\_ \mathnormal{::} \_$
}
\end{frame}
\newcommand{\branch}[4]{\only<-#1>{#3}\only<#2->{#4}}
\makecn{Unit}
\makecn{unit}
\begin{frame}{Type Preservation as a Logical Relation}
\vspace{-2.5em}
{\footnotesize\begin{align*}
&\theory{\ChurchProd} &&= \churchProdTheory\\[0.2em]
&\theory{\CurryProd} &&= \curryProdTheory\\
%
%
&\multispan{4}{$\logrel{\TypePres}{\TypeEras}{\ChurchProd}{\CurryProd} = \{$}\\[-0.25em]
&\multispan{4}{$\quad\quad\begin{aligned}
\onslide<+->{
&\tp &&:= \lam{A}{\alt<+->{\tp}{\TypeEras(tp)}}\Unit\\
}
\onslide<+->{
&\tm &&:=
\lam{A}{\alt<+->{\tp}{\TypeEras(tp)}}
\only<+->{
\lam{t}{\alt<+->{\tm}{\TypeEras(\ttm{A})}}
}
\only<+->{\ \ofType{t}{A}}\\
}
\onslide<+->{
&\_ \times \_ &&:= \ldots \unit\\
}
\onslide<+->{
&\tpNot{(\_,\_)}{\_ \times \_} &&:=
\only<+->{\lam{A}{\alt<+->{\tp}{\TypeEras(\tp)}} \ulam{A^\ast}}
\only<+->{\lam{B}{\alt<+->{\tp}{\TypeEras(\tp)}} \ulam{B^\ast}}\\
}
\onslide<+->{
&&&\quad\quad \lam{a}{\alt<+->{\tm}{\TypeEras(\ttm{A})}}
\only<+->{\lam{a^\ast}{\ofType{a}{A}}}\\
}
\onslide<+->{
&&&\quad\quad\quad
\lam{b}{\alt<+->{\tm}{\TypeEras(\ttm{B})}}
\lam{b^\ast}{\ofType{b}{B}}\ \
}
\onslide<+->{
\tpNot{(a,b)}{T,A \times B}\;a^\ast\;b^\ast
}
\end{aligned}$}\\[-0.25em]
&\multispan{4}{$\}$}
\end{align*}}
\end{frame}
\begin{frame}{Example 3: Summary}
\begin{itemize}
\item formalized two flavors of type theories: $\ChurchProd$, $\CurryProd$\\
\rightThing{extrinsic vs. intrinsic}\\
\rightThing{$\tm\colon\tp\to\type$ vs. $\tm\colon\type$}
%
\item saw \alert{type erasure as a ``lossy'' translation}
\begin{align*}
&\view{\TypeEras}{\ChurchProd}{\CurryProd} = \{\\
&\quad\quad \tm := \ignorelam \tm\\
&\quad\quad\vdots\\
&\}
\end{align*}
%
\item \alert{used a logical relation to complement the morphism} to recover a meta theorem (within the system!)
\begin{align*}
&\logrel{\TypePres}{\TypeEras}{\ChurchProd}{\CurryProd} = \{\\
&\quad\quad \tm := \lam{A}{\tp} \lam{t}{\tm}\ \ofType{t}{A}\\
&\quad\quad\vdots\\
&\}
\end{align*}
\end{itemize}
\end{frame}