Skip to content
Snippets Groups Projects
Select Git revision
  • 904ee35a42a6094e64e05f1e449b765d62d27810
  • master default
2 results

slides-xxx-binary-log-rels.tex

Blame
  • Navid Roux's avatar
    Navid Roux authored and Michael Kohlhase committed
    3af27bc2
    History
    slides-xxx-binary-log-rels.tex 6.37 KiB
    % !TeX root = slides.tex
    \section{Example 2: \texorpdfstring{\Leftrightarrow}{<=>} congruence (binary log. rel.)}
    
    \begin{frame}{Towards Binary Logical Relations}
    	\structure{Key Ideas of Unary Relations:}\rightThing{\alert{already seen}}\begin{enumerate}
    		\item state \alert{type-indexed family of predicates} $\tndClaim{-}{-}$
    		\item for every type $\tau$, \alert{prove predicate is preserved} under constructors $c\colon \tau_1 \to \ldots \to \tau_n \to \tau$:\[
    		\text{if}\ \tndClaim{\tau_1}{t_1} \wedge \ldots \wedge \tndClaim{\tau_n}{t_n},\ \text{then}\ \tndClaim{\tau}{c\ t_1 \ldots\ t_n}
    		\]
    	\end{enumerate}
    	
    	\structure{How about $C_P(p, p') :=\; \lra{p}{p'}$?}
    	\onslide<2->{\begin{enumerate}
    			\item forms a type-indexed family of \alert{binary} predicates\\\rightOptional{together with $C_A(a,b) :=\; \lra{\metaInj(a)}{\metaInj(b)}$}
    			%
    			\item e.g. is preserved under $\wedge$:\begin{itemize}
    				\item given $\lra{p}{p'}$ and $\lra{q}{q'}$
    				\item we can derive $\lra{(p \wedge q)}{(p' \wedge q')}$
    			\end{itemize}
    	\end{enumerate}}
    \end{frame}
    
    \begin{frame}{Example 2: \texorpdfstring{$\Leftrightarrow$}{<=>} congruence in Prop. Logic}
    	\begin{example}[PL Extended]
    		We extend PL's grammar by
    		\plExtGrammar
    		and its proof calculus accordingly.
    	\end{example}
    	\begin{theorem}[Leftrightarrow (LRA) Congruence]
    		$\Leftrightarrow$ is a congruence on $P$. That is, if $\;\lra{p}{p'}$ and $\lra{q}{q'}$, then\begin{columns}
    			\begin{column}{0.5\textwidth}
    				\begin{itemize}
    					\item $\lra{\lnot p}{\lnot p'}$
    					\item $\lra{p \wedge q}{p' \wedge q'}$
    				\end{itemize}
    			\end{column}%
    			\hfill%
    			\begin{column}{0.5\textwidth}
    				\begin{itemize}
    					\item $\lra{p \vee q}{p' \vee q'}$
    					\item $\lra{(p \Leftrightarrow q)}{(p' \Leftrightarrow q')}$,
    				\end{itemize}
    			\end{column}
    		\end{columns}
    		\medskip
    		
    		and, trivially, if $\;\lra{\metaInj(a)}{\metaInj(a')}$, then $\lra{\metaInj(a)}{\metaInj(a')}$.
    	\end{theorem}
    \end{frame}
    
    % typeset the assignment for either \wedge or \vee in the logical relation
    % usage: expects a surrounding align, align*, or aligned environment; pass either \wedge or \vee as argument
    \newcommand{\logicalRelationWedgeVee}[1]{%
    	\mathnormal{#1} &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lam{p^\ast}{\lra{\colM{p}}{\colMM{p'}}}\hspace{2.3em}\text{\optional{{\footnotesize \cn{//} first arg of }}} \scriptstyle{\mathnormal{#1}}\\%
    	&\quad\quad\quad\colM{\lam{q}{\prop}} \colMM{\lam{q'}{\prop}}\lam{q^\ast}{\lra{\colM{q}}{\colMM{q'}}}\quad\text{\optional{{\footnotesize \cn{//} second arg of }}} \scriptstyle{\mathnormal{#1}}\\%
    	&\quad\quad\quad\quad\expTypeComment{\lra{\colM{p} #1 \colMM{q}}{\colM{p'} #1 \colMM{q'}}}%
    }%
    \begin{frame}{LRA as a Logical Relation}
    	\only<-7>{%
    		\onslide<2->{\structure{Recall:} \only<1>{the desired binary relation on atoms}}%
    		\only<2>{$\atom\colon\type$}%
    		\only<3>{$\prop\colon\type$}%
    		\only<4>{$\inj\colon\atom\to\prop$}%
    		\only<5>{$\mathnormal{\lnot}\colon\prop\to\prop$}%
    		\only<6-7>{$\mathnormal{\wedge},\mathnormal{\vee}\colon\prop\to\prop\to\prop$}%
    		\onslide<2->{, map to }%
    		\only<2>{the desired binary relation on atoms}%
    		\only<3>{the desired binary relation on propositions}%
    		\only<4-5>{appropriate proof}%
    		\only<6>{appropriate proofs}%
    	}%
    	\begin{align*}
    		&\logRel{\LRA}{\colM{\id{\PL}} \times \colMM{\id{\PL}}}{\PL}{\PL} = \{\\
    		&\quad\quad\begin{aligned}
    			\onslide<2->{
    				\atom &:= \colM{\lam{a}{\atom}} \colMM{\lam{a'}{\atom}} \lra{\inj(a)}{\inj(a')}\\
    			}
    			\onslide<3->{
    				\prop &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lra{p}{p'}\only<2>{\\}\only<3->{\\[0.6em]}
    			}
    			%
    			\onslide<4->{
    				\inj  &:= \colM{\lam{a}{\atom}} \colMM{\lam{a'}{\atom}} \lam{a^\ast}{\lra{\colM{\inj(a)}}{\colMM{\inj(a')}}}\  a^\ast\\
    			}
    			%
    			\onslide<5->{
    				\mathnormal{\lnot} &:= \colM{\lam{p}{\prop}} \colMM{\lam{p'}{\prop}} \lam{p^\ast}{\lra{\colM{p}}{\colMM{p'}}}\\
    				&\quad\quad\quad\expTypeComment{\lra{\colM{\lnot p}}{\colMM{\lnot p'}}}\\
    			}
    			%
    			\onslide<6->{
    				\logicalRelationWedgeVee{\wedge}\\
    			}
    			\onslide<7->{
    				\logicalRelationWedgeVee{\vee}
    			}
    		\end{aligned}\onslide<8>{\\&\}}
    	\end{align*}
    \end{frame}
    
    \begin{frame}{Logical Relations: A Second Definition}
    	\vspace{-0.5em}
    	\begin{definition}
    		Let $T$ be a theory and $(r_c)_{c \in T}$ a family of $T$-expressions. Define
    		\vspace{-0.75em}
    		\begin{align*}
    			&r(\type) &&= \lam{A}{\type} \colMM{\lam{A'}{\type}} A \to \colMM{A'} \to \type\\
    			&r(\tpi{a}{A} B) &&= \lam{f}{(\tpi{a}{A} B)} \colMM{\lam{f'}{(\tpi{a'}{A'} B')}}\\
    			&&&\quad\quad\quad \tpi{x}{A} \colMM{\tpi{x'}{A'}} \tpi{x^\ast}{r(A)\ x\ \colMM{x'}}\\
    			&&&\quad\quad\quad\quad r(B)\ (f\ x)\ \colMM{(f'\ x')}\\
    			&r(A\ B) &&= r(A)\ B\ B'\ r(B)\\
    			&r(\lam{x}{A} B) &&= \lam{x}{A} \colMM{\lam{x'}{A'}} \lam{x^\ast}{r(A)\ x\ \colMM{x'}} r(B)\\
    			&r(c) &&= r_c\\
    			&r(x) &&= x^\ast\\[-2em]
    		\end{align*}
    		where $A'$ denotes systematic priming.
    		We call $r$ a \defemph{binary logical relation on $\id{T} \times \colMM{\id{T}}$} if $\vdash_T r_c\colon r(\tpName)\ c\ \colMM{c}$ for all constants $c\colon\tpName$ in $T$.
    	\end{definition}
    	\only<-2>{\begin{itemize}
    			\only<1>{\item $\prop\colon\type$, hence $r_{\prop}\colon \prop \to \colMM{\prop} \to \type$\\\rightThing{$\optional{r_{\prop} := \ulam{p}}\colMM{\ulam{p'}} \optional{\lra{p}{p'}}$}}%
    			%
    			\only<2>{\item $\mathnormal{\lnot}\colon\prop\to\prop$, hence
    				$r_{\mathnormal{\lnot}}
    				\colon
    				\tpi{p\,\colMM{p'}}{\prop}
    				\tpi{p^\ast}{\lra{p}{p'}} \lra{\lnot p}{\lnot p'}$}
    	\end{itemize}}%
    	\only<3->{
    		\begin{block}{}
    			\textbf{Theorem (Basic Lemma).} If $\;\vdash_T t \colon \tpName$, then $\vdash_T r(t) \colon r(\tpName)\ t\ t'$.
    		\end{block}
    	}
    \end{frame}
    
    \begin{frame}{Example 2: Summary}
    	\structure{Summary:} we have \alert{$n$-ary logical relations} of the form\[
    		\logRel{r}{\id{T}\times\cdots\times\id{T}}{T}{T} = \{\ldots\}
    	\]
    	\begin{itemize}
    		\item they associate to every type $\tpName$ an \alert{$n$-ary relation} $C_{\tpName}(-,\ldots,-)$
    		\item their well-typedness expresses that these relations are congruences
    		\item ``the basic lemma'' states: if $t\colon \tpName$, then $C_{\tpName}(t, \ldots, t)$\\\rightOptional{reflexivity? TODO}
    	\end{itemize}
    	\medskip
    
    	\structure{Next:} Logical Relations along a \alert{non-trivial} morphism
    \end{frame}