% !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}