Skip to content
Snippets Groups Projects
Select Git revision
  • 69b8a01b717b42b5cdf9894a75ce1e96b332c635
  • master default
  • JS-based-scroll-rendering
  • Paul_Marius_Level
  • Paul_Marius_2
  • Paul_Marius
  • Andi_Mark
  • be-UnityWebView
  • gitignoreFrameitServer
  • ZimmerBSc
  • Bugfix_StageLoading
  • stages
  • MAZIFAU_Experimental
  • tsc/coneworld
  • tsc/fact-interaction
  • marcel
  • MaZiFAU_TopSort
  • mergeHelper
  • zwischenSpeichern
  • tempAndrToMaster
  • SebBranch
  • 3.0
  • v2.1
  • v2.0
  • v1.0
25 results

Fireworks_Animation.prefab.meta

Blame
  • 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}