Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
% !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}