diff --git a/paper/gtt.tex b/paper/gtt.tex
index 78b072668b6988a6793bd6e114be14dc1732f148..a1963a567378e155f2b186ae9fcb7f2c163ada46 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -141,8 +141,8 @@
\newcommand{\logpole}{\mathrel{\lesssim^{log}_{\pole}}}
\newcommand{\pole}{\Bot}
\newcommand{\ipole}[1]{\mathrel{\pole^{#1}}}
-\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
\newcommand{\logc}[1]{\mathrel{\pole}^{#1}}
+\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
\newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
\newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
@@ -153,7 +153,10 @@
\newcommand{\ctxize}[1]{\mathrel{#1^{\text{ctx}}}}
\newcommand{\ix}[2]{\mathrel{#1^#2}}
-\newcommand{\ilrof}[3]{\mathrel{#1^{\text{log}}_{#3,#2}}}
+\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
+\newcommand{\ilrof}[2]{\mathrel{#1^{\text{log}}_{#2}}}
+\newcommand{\itylr}[2]{\itylrof{\apreorder}{#1}{#2}}
+\newcommand{\ilr}[1]{\ilrof{\apreorder}{#1}}
%% Operational steps
\newcommand{\step}{\mapsto}
@@ -2601,6 +2604,9 @@ Next, we show the relation is downward-closed
Because $M \bigstepsin{0} M$
\end{proof}
+\begin{lemma}{Result Anti-reduction}
+ If $M \bigstepsin{i} N$ then $\result(M) = \result(N)$.
+\end{lemma}
\begin{lemma}{Anti-reduction}
If $M \ix\apreorder i R$ and $N \bigstepsin{j} M$, then $N \ix\apreorder {i+j} R$
\end{lemma}
@@ -2615,9 +2621,9 @@ Next, we show the relation is downward-closed
Next, we define the \emph{logical} preorder by induction on types and
the index $i$ in figure \ref{lr}.
%
-Specifically, for every value type $A$ we define a relation $\ilrof
+Specifically, for every value type $A$ we define a relation $\itylrof
\apreorder i A$ between closed values of type $A$ and for every
-computation type $\u B$, we define a relation $\ilrof \apreorder i {\u
+computation type $\u B$, we define a relation $\itylrof \apreorder i {\u
B}$ between stacks \emph{from} $\u B$ to our type of results $\u F
2$.
%
@@ -2629,21 +2635,53 @@ We extend the definition to contexts point-wise.
%
%TODO: give more explanation about the cases, especially F, U and mu, nu.
+
+\begin{figure}
+ \begin{mathpar}
+ {\itylrof\apreorder{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2
+ \qquad\qquad\qquad{\itylrof\apreorder{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S
+ : \u F (1 + 1) \}^2\\
+ \begin{array}{rcl}
+ \cdot \itylrof\apreorder i {\cdot} \cdot &=& \top\\
+ \gamma_1,V_1/x \itylrof\apreorder i {\Gamma,x:A} \gamma_2,V_2/x &=& \gamma_1 \itylrof\apreorder i \Gamma \gamma_2 \wedge V_1 \itylrof\apreorder i A V_2\\
+ V_1 \itylr i 0 V_2 &=& \bot\\
+ \inl V_1 \itylr i {A + A'} \inl V_2 &= & V_1 \itylr i A V_2\\
+ \inr V_1 \itylr i {A + A'} \inr V_2 &= & V_1 \itylr i {A'} V_2 \\
+ () \itylr i 1 () &=& \top\\
+ (V_1,V_1') \itylr i {A \times A'} (V_2, V_2') &=& V_1 \itylr i A V_2 \wedge V_1' \itylr i {A'} V_2'\\
+ % Should this be a roll or not?
+ \rollty {\mu X. A} V_1 \itylr 0 {\mu X. A} \rollty {\mu X. A} V_2 &=& \top\\
+ \rollty {\mu X. A} V_1 \itylr {i+1} {\mu X. A} \rollty {\mu X. A} V_2 &=& V_1 \itylr i {A[\mu X.A/X]} V_2\\
+ V_1 \itylr i {U \u B} V_2 &=& \forall j \leq i, S_1 \itylr j {\u B} S_2.~ S_1[\force V_1] \ix\apreorder j \result(S_2[\force V_2]) \\\\
+
+ S_1[\bullet V_1] \itylr i {A \to \u B} S_1[\bullet V_2] & = & V_1 \itylr i A V_2 \wedge S_1 \itylr {i}{\u B} S_2\\
+ S_1[\pi_1 \bullet] \itylr i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \itylr i {\u B} S_2\\
+ S_1[\pi_2 \bullet] \itylr i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \itylr i {\u B'} S_2\\
+ S_1 \itylr i {\top} S_2 &=& \bot\\
+ S_1[\unroll \bullet] \itylr 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
+ S_1[\unroll \bullet] \itylr {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \itylr i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
+ S_1 \itylr i {\u F A} S_2 & = & \forall j\leq i, V_1 \itylr j A V_2.~ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2])
+ \end{array}
+ \end{mathpar}
+ \caption{Logical Relation from a Preorder $\apreorder$}
+\end{figure}
+
+
Next, analogous to the contextual preorder, we define the
\emph{logical} preorder on terms, values and stacks.
\begin{definition}{Logical Preorder}
Given a preorder on results $\apreorder$ with $\diverge$ a least
element, we define the step-indexed logical preorder as follows:
\begin{enumerate}
- \item $\Gamma \vDash M_1 \ilrof\apreorder{i}{} M_2 \in \u B$ holds
- when for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$ and $S_1
- \ilrof\apreorder i {\u B} S_2$, $S_1[M_1[\gamma_1]] \ix\apreorder
+ \item $\Gamma \vDash M_1 \ilrof\apreorder{i} M_2 \in \u B$ holds
+ when for every $\gamma_1 \itylrof\apreorder i {\Gamma} \gamma_2$ and $S_1
+ \itylrof\apreorder i {\u B} S_2$, $S_1[M_1[\gamma_1]] \ix\apreorder
i \result(S_2[M_2[\gamma_2]])$.
- \item $\Gamma \vDash V_1 \ilrof\apreorder{i}{} V_2 \in A$ holds when
- for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$, $V_1[\gamma_1] \ilrof\apreorder i A V_2[\gamma_2]$
- \item $\Gamma \pipe \u B \vDash S_1 \ilrof\apreorder{i}{} S_2 \in \u B'$ holds
- when for every $\gamma_1 \ilrof\apreorder i {\Gamma} \gamma_2$ and
- $S_1' \ilrof\apreorder i {\u B'} S_2'$, $S_1'[S_1[\gamma_1]] \ilrof \apreorder
+ \item $\Gamma \vDash V_1 \ilrof\apreorder{i} V_2 \in A$ holds when
+ for every $\gamma_1 \itylrof\apreorder i {\Gamma} \gamma_2$, $V_1[\gamma_1] \itylrof\apreorder i A V_2[\gamma_2]$
+ \item $\Gamma \pipe \u B \vDash S_1 \ilrof\apreorder{i} S_2 \in \u B'$ holds
+ when for every $\gamma_1 \itylrof\apreorder i {\Gamma} \gamma_2$ and
+ $S_1' \itylrof\apreorder i {\u B'} S_2'$, $S_1'[S_1[\gamma_1]] \itylrof \apreorder
i {\u B} S_2'[S_2[\gamma_2]])$.
\end{enumerate}
\end{definition}
@@ -2653,24 +2691,232 @@ relation, i.e., the fundamental lemma of the logical relation.
\begin{lemma}{Logical Relation Downward Closure}
\begin{enumerate}
- \item If $V_1 \ilrof\apreorder i A V_2$ and $j\leq i$ then $V_1
- \ilrof\apreorder j A V_2$
- \item If $S_1 \ilrof\apreorder i {\u B} S_2$ and $j\leq i$ then $S_1
- \ilrof\apreorder j {\u B} S_2$
+ \item If $V_1 \itylrof\apreorder i A V_2$ and $j\leq i$ then $V_1
+ \itylrof\apreorder j A V_2$
+ \item If $S_1 \itylrof\apreorder i {\u B} S_2$ and $j\leq i$ then $S_1
+ \itylrof\apreorder j {\u B} S_2$
\end{enumerate}
\end{lemma}
\begin{theorem}{Logical Preorder is a Congruence}
For any preorder on results with diverge least element, the logical
- preorder $\ilrof\apreorder i {}$ is a congruence relation, i.e.,
+ preorder $\ilrof\apreorder i$ is a congruence relation, i.e.,
closed under the congruence rules of figure TODO.
\end{theorem}
\begin{proof}
- TODO: adapt from below
+ For each congruence rule
+ \[
+ \inferrule
+ {\Gamma \pipe \Delta \vdash E_1 \ltdyn E_1' : T_1 \cdots}
+ {\Gamma' \pipe \Delta' \vdash E_c \ltdyn E_c' : T_c}
+ \]
+ we prove for every $i \in \mathbb{N}$ the validity of the rule
+ \[
+ \inferrule
+ {\Gamma \pipe \Delta \vDash E_1 \ilr i E_1' \in T_1\cdots }
+ {\Gamma \pipe \Delta \vDash E_c \ilr i E_c' \in T_c}
+ \]
+ \begin{enumerate}
+ \item $\inferrule {} {\Gamma,x : A,\Gamma' \vDash x \ilr i x \in
+ A}$. Given $\gamma_1 \itylr i {\Gamma,x:A,\Gamma'} \gamma_2$,
+ then by definition $\gamma_1(x) \itylr i A \gamma_2(x)$.
+
+ \item $\inferrule{}{\Gamma \vDash \err \itylr \err \in \u B}$ We
+ need to show $S_1[\err] \ix\apreorder i \result(S_2[\err])$. By
+ anti-reduction and strictness of stacks, it is sufficient to show
+ $\err \ilr i \err$. If $i = 0$ there is nothing to show,
+ otherwise, it follows by reflexivity of $\apreorder$.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A \and
+ \Gamma, x : A \vDash M \ilr i M' \in \u B
+ }
+ {\Gamma \vDash \letXbeYinZ V x M \ilr i \letXbeYinZ {V'} {x} {M'} \in \u B}$
+
+ Each side takes a $0$-cost step, so by anti-reduction, this reduces to
+ \[ S_1[M[\gamma_1,V/x]] \ix\apreorder i \result(S_2[M'[\gamma_2,V'/x]]) \] which follows by the assumption $\Gamma, x : A \vDash M \ilr i M' \in \u B$
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in 0}
+ {\Gamma \vDash \abort V \ilr i \abort V' \in \u B}$.
+ By assumption, we get $V[\gamma_1] \logty i {0} V'[\gamma_2]$, but this is a contradiction.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A_1}
+ {\Gamma \vDash \inl V \ilr i \inl V' \in A_1 + A_2}$.
+ Direct from assumption, rule for sums.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A_2}
+ {\Gamma \vDash \inr V \ilr i \inr V' \in A_1 + A_2}$
+ Direct from assumption, rule for sums.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A_1 + A_2\and
+ \Gamma, x_1 : A_1 \vDash M_1 \ilr i M_1' \in \u B\and
+ \Gamma, x_2 : A_2 \vDash M_2 \ilr i M_2' \in \u B
+ }
+ {\Gamma \vDash \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \ilr i \caseofXthenYelseZ {V'} {x_1. M_1'}{x_2.M_2'} \in \u B}$
+ By case analysis of $V[\gamma_1] \ilr i V'[\gamma_2]$.
+ \begin{enumerate}
+ \item If $V[\gamma_1]=\inl V_1, V'[\gamma_2] = \inl V_1'$ with
+ $V_1 \itylr i {A_1} V_1'$, then taking $0$ steps, by anti-reduction
+ the problem reduces to
+ \[ S_1[M_1[\gamma_1,V_1/x_1]] \ix\apreorder i \result(S_1[M_1[\gamma_1,V_1/x_1]]) \]
+ which follows by assumption.
+ \item For $\inr{}$, the same argument.
+ \end{enumerate}
+
+ \item $\inferrule
+ {}
+ {\Gamma \vDash () \ilr i () \in 1}$ Immediate by unit rule.
+
+ \item $\inferrule
+ {\Gamma \vDash V_1 \ilr i V_1' \in A_1\and
+ \Gamma\vDash V_2 \ilr i V_2' \in A_2}
+ {\Gamma \vDash (V_1,V_2) \ilr i (V_1',V_2') \in A_1 \times A_2}$
+ Immediate by pair rule.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A_1 \times A_2\and
+ \Gamma, x : A_1,y : A_2 \vDash M \ilr i M' \in \u B
+ }
+ {\Gamma \vDash \pmpairWtoXYinZ V x y M \ilr i \pmpairWtoXYinZ {V'} {x} {y} {M'} \in \u B}$
+ By $V \itylr i {A_1 \times A_2} V'$, we know $V[\gamma_1] =
+ (V_1,V_2)$ and $V'[\gamma_2] = (V_1', V_2')$ with $V_1 \itylr i
+ {A_1} V_1'$ and $V_2 \itylr i {A_2} V_2'$.
+ Then by anti-reduction, the problem reduces to
+ \[ S_1[M[\gamma_1,V_1/x,V_2/y]] \ix\apreorder i \result(S_1[M'[\gamma_1,V_1'/x,V_2'/y]]) \]
+ which follows by assumption.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A[\mu X.A/X]}
+ {\Gamma \vDash \rollty{\mu X.A} V \ilr i \rollty{\mu X.A} V' \in \mu X.A }$
+ If $i = 0$, we're done. Otherwise $i=j+1$, and our assumption is
+ that $V[\gamma_1] \itylr {j+1} {A[\mu X.A/X]} V'[\gamma_2]$ and we need to show
+ that $\roll V[\gamma_1] \itylr {j+1} {\mu X. A}\roll
+ V'[\gamma_2]$. By definition, we need to show $V[\gamma_1] \itylr
+ j {A[\mu X.A/X]} V'[\gamma_2]$, which follows by downward-closure.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in \mu X. A\and
+ \Gamma, x : A[\mu X. A/X] \vDash M \ilr i M' \in \u B}
+ {\Gamma \vDash \pmmuXtoYinZ V x M \ilr i \pmmuXtoYinZ {V'} {x} {M'} \in \u B}$
+ If $i = 0$, then by triviality at $0$, we're done.
+ Otherwise, $V[\gamma_1] \itylr {j+1} {\mu X. A} V'[\gamma_2]$ so
+ $V[\gamma_1] = \roll V_\mu, V'[\gamma_2] = \roll V_\mu'$ with
+ $V_\mu \itylr j {A[\mu X.A/X]} V_\mu'$. Then each side takes $1$ step, so by anti-reduction it is sufficient to show
+ \[ S_1[M[\gamma_1,V_\mu/x]] \ix\apreorder j \result(S_2[M'[\gamma_2,V_\mu'/x]]) \] which follows by assumption and downward closure of the stack, value relations.
+
+ \item $\inferrule {\Gamma \vDash M \ilr i M' \in \u B} {\Gamma
+ \vDash \thunk M \ilr i \thunk M' \in U \u B}$. We need to show
+ $\thunk M[\gamma_1] \itylr i {U \u B} \thunk M'[\gamma_2]$, so let
+ $S_1 \itylr j {\u B} S_2$ for some $j \leq i$, and we need to show
+ \[ S_1[\force \thunk M_1[\gamma_1]] \ix\apreorder j \result(S_2[\force \thunk M_2[\gamma_2]]) \]
+ Then each side reduces in a $0$-cost step and it is sufficient to show
+ \[ S_1[M_1[\gamma_1]] \ix\apreorder j \result(S_2[M_2[\gamma_2]]) \]
+ Which follows by downward-closure for terms and substitutions.
+
+ \item $\inferrule {\Gamma \vDash V \ilr i V' \in U \u B} {\Gamma
+ \vDash \force V \ilr i \force V' \in \u B}$. We need to show
+ $S_1[\force V[\gamma_1]] \ix\apreorder i \result(S_2[\force
+ V'[\gamma_2]])$, which follows by the definition of $V[\gamma_1]
+ \itylr i {U \u B} V'[\gamma_2]$.
+
+ \item $\inferrule
+ {\Gamma \vDash V \ilr i V' \in A}
+ {\Gamma \vDash \ret V \ilr i \ret V' \in \u F A}$
+ We need to show $S_1[\ret V[\gamma_1]] \ix\apreorder i \result(S_2[\ret
+ V'[\gamma_2]])$, which follows by the orthogonality definition of
+ $S_1 \itylr i {\u F A} S_2$.
+
+ \item $\inferrule
+ {\Gamma \vDash M \ilr i M' \in \u F A\and
+ \Gamma, x: A \vDash N \ilr i N' \in \u B}
+ {\Gamma \vDash \bindXtoYinZ M x N \ilr i \bindXtoYinZ {M'} {x} {N'} \in \u B}$.
+
+ We need to show $\bindXtoYinZ {M[\gamma_1]} x {N[\gamma_2]} \ix\apreorder i \result(\bindXtoYinZ {M'[\gamma_2]} {x} {N'[\gamma_2]})$.
+ By $M \ilr i M' \in \u F A$, it is sufficient to show that
+ \[ \bindXtoYinZ \bullet x {N[\gamma_1]} \itylr i {\u F A} \bindXtoYinZ \bullet {x} {N'[\gamma_2]}\]
+ So let $j \leq i$ and $V \itylr j A V'$, then we need to show
+ \[ \bindXtoYinZ {\ret V} x {N[\gamma_1]} \itylr j {\u F A} \bindXtoYinZ {\ret V'} {x} {N'[\gamma_2]} \]
+ By anti-reduction, it is sufficient to show
+ \[ N[\gamma_1,V/x] \ix\apreorder j \result(N'[\gamma_2,V'/x]) \]
+ which follows by anti-reduction for $\gamma_1 \itylr i {\Gamma} \gamma_2$ and $N \ilr i N'$.
+
+ \item $\inferrule
+ {\Gamma, x: A \vDash M \ilr i M' \in \u B}
+ {\Gamma \vDash \lambda x : A . M \ilr i \lambda x:A. M' \in A \to \u B}$
+ We need to show
+ \[S_1[\lambda x:A. M[\gamma_1]] \ix\apreorder i \result(S_2[\lambda x:A.M'[\gamma_2]]).\]
+ By $S_1 \itylr i {A \to \u B} S_2$, we know $S_1 = S_1'[\bullet V_1]$, $S_2 = S_2'[\bullet V_2]$ with $S_1' \itylr i {\u B} S_2'$ and $V_1 \itylr i {A} V_2$.
+ Then by anti-reduction it is sufficient to show
+ \[
+ S_1'[M[\gamma_1,V_1/x]] \ix\apreorder i \result(S_2'[M'[\gamma_2,V_2/x]])
+ \]
+ which follows by $M \ilr i M'$.
+
+ \item $\inferrule
+ {\Gamma \vDash M \ilr i M' \in A \to \u B\and
+ \Gamma \vDash V \ilr i V' \in A}
+ {\Gamma \vDash M\,V \ilr i M'\,V' \in \u B }$
+ We need to show
+ \[S_1[M[\gamma_1]\,V[\gamma_1]] \ix\apreorder i \result(S_2[M'[\gamma_2]\,V'[\gamma_2]])\] so by $M \ilr i M'$ it is sufficient to show $S_1[\bullet V[\gamma_1]] \itylr i {A \to \u B} S_2[\bullet V'[\gamma_2]]$ which follows by definition and assumption that $V \ilr i V'$.
+
+ \item $\inferrule{}{\Gamma \vdash \{\} : \top}$ We assume we are
+ given $S_1 \itylr i {\top} S_2$, but this is a contradiction.
+
+ \item $\inferrule
+ {\Gamma \vDash M_1 \ilr i M_1' \in \u B_1\and
+ \Gamma \vDash M_2 \ilr i M_2' \in \u B_2}
+ {\Gamma \vDash \pair {M_1} {M_2} \ilr i \pair {M_1'} {M_2'} \in \u B_1 \with \u B_2}$
+ We need to show
+ \[S_1[\pair{M_1[\gamma_1]}{M_2[\gamma_1]}] \ix\apreorder i \result(S_2[\pair{M_1'[\gamma_1]}{M_2'[\gamma_2]}]).\]
+ We proceed by case analsysis of $S_1 \itylr i {\u B_1 \with \u B_2} S_2$
+ \begin{enumerate}
+ \item In the first possibility $S_1 = S_{1}'[\pi \bullet], S_2 =
+ S_2'[\pi \bullet]$ and $S_1' \itylr i {\u B_1} S_2'$.
+ Then by anti-reduction, it is sufficient to show
+ \[ S_1'[M_1[\gamma_1]] \ix\apreorder i \result(S_2'[M_1'[\gamma_2]]) \]
+ which follows by $M_1 \ilr i M_1'$.
+ \item Same as previous case.
+ \end{enumerate}
+
+ \item $\inferrule
+ {\Gamma \vDash M \ilr i M' \in \u B_1 \with \u B_2}
+ {\Gamma \vDash \pi M \ilr i \pi M' \in \u B_1}$
+ We need to show $S_1[\pi M[\gamma_1]] \ix\apreorder i \result(S_2[\pi
+ M'[\gamma_2]])$, which follows by $S_1[\pi \bullet] \itylr i {\u
+ B_1 \with \u B_2} S_2[\pi \bullet]$ and $M \ilr i M'$.
+
+ \item $\inferrule {\Gamma \vDash M \ilr i M' \in \u B_1 \with \u
+ B_2} {\Gamma \vDash \pi' M \ilr i \pi' M' \in \u B_2}$ Similar
+ to previous case.
+
+ \item $\inferrule
+ {\Gamma \vDash M \ilr i M' \in \u B[{\nu \u Y. \u B}/\u Y]}
+ {\Gamma \vDash \rollty{\nu \u Y. \u B} M \ilr i \rollty{\nu \u Y. \u B} M' \in {\nu \u Y. \u B}}$
+ We need to show that
+ \[ S_1[ \rollty{\nu \u Y. \u B} M[\gamma_1]]
+ \ix\apreorder i \result(S_2[ \rollty{\nu \u Y. \u B} M'[\gamma_2]]) \]
+ If $i = 0$, we invoke triviality at $0$.
+ Otherwise, $i = j + 1$ and we know by $S_1 \itylr {j+1} {\nu \u Y. \u B} S_2$ that
+ $S_1 = S_1'[\unroll \bullet]$ and $S_2 = S_2'[\unroll \bullet]$ with $S_1' \itylr j {\u B[{\nu \u Y. \u B}/\u Y]} S_2'$, so by anti-reduction it is sufficient to show
+ \[ S_1'[ M[\gamma_1]] \ix\apreorder i \result(S_2'[ M'[\gamma_2]]) \]
+ which follows by $M \ilr i M'$ and downward-closure.
+
+ \item $\inferrule
+ {\Gamma \vDash M \ilr i M' \in {\nu \u Y. \u B}}
+ {\Gamma \vDash \unroll M \ilr i \unroll M' \in \u B[{\nu \u Y. \u B}/\u Y]}$
+ We need to show
+ \[S_1[\unroll M] \ix\apreorder i \result(S_2[\unroll M']),\] which
+ follows because $S_1[\unroll \bullet] \itylr i {\nu \u Y. \u B}
+ S_2[\unroll \bullet]$ and $M \ilr i M'$.
+ \end{enumerate}
\end{proof}
\begin{corollary}{Reflexivity}
For any $\Gamma \vdash M : \u B$, and $i \in \mathbb{N}$,
- \[\Gamma \vDash M \ilrof\apreorder i {} M \in \u B.\]
+ \[\Gamma \vDash M \ilrof\apreorder i M \in \u B.\]
\end{corollary}
As another corollary we have the following \emph{strengthening} of the
@@ -2681,7 +2927,7 @@ counts unrolling steps.
\end{corollary}
\begin{proof}
By reflexivity, $\cdot \vDash M \ix\apreorder i M \in \u F 2$ and by
- definition $\bullet \ilrof\apreorder i {\u F 2} \bullet$, so
+ definition $\bullet \itylrof\apreorder i {\u F 2} \bullet$, so
unrolling definitions we get $M \ix\apreorder i \result(M)$.
\end{proof}
@@ -2717,14 +2963,14 @@ the limit as $i \to \infty$.
\end{proof}
\begin{corollary}{LR is Sound wrt Contextual Preorder}
- If $\Gamma \vDash M \ilrof\apreorder \omega {} N \in \u B$
+ If $\Gamma \vDash M \ilrof\apreorder \omega N \in \u B$
then
$\Gamma \vDash M \ctxize\apreorder N \in \u B$.
TODO: value, stack cases
\end{corollary}
\begin{proof}
Let $C$ be a closing context. By congruence, $C[M] \ilrof\apreorder
- \omega {} C[N]$, so because the identity stack is related to itself
+ \omega C[N]$, so because the identity stack is related to itself
we have
\[ C[M] \ix\apreorder\omega \result(C[N]) \]
so by the limit lemma, we have
@@ -2733,8 +2979,8 @@ the limit as $i \to \infty$.
\end{proof}
\begin{corollary}{LR is Sound wrt Contextual Graduality Ordering}
- If $\Gamma \vDash M \ilrof\precltdyn \omega {} N \in \u B$
- and $\Gamma \vDash N \ilrof\precgtdyn \omega {} M \in \u B$
+ If $\Gamma \vDash M \ilrof\precltdyn \omega N \in \u B$
+ and $\Gamma \vDash N \ilrof\precgtdyn \omega M \in \u B$
then
$\Gamma \vDash M \ctxize\ltdyn N \in \u B$.
TODO: value, stack cases
@@ -2749,16 +2995,39 @@ our LR is \emph{complete} with respect to contextual graduality
\begin{lemma}{Logical Preorder is Complete wrt Contextual Preorder}
For any $\apreorder$, if $\Gamma \vDash M \ctxize \apreorder N \in
- \u B$, then $\Gamma \vDash M \ilrof\apreorder \omega {} N \in \u B$.
+ \u B$, then $\Gamma \vDash M \ilrof\apreorder \omega N \in \u B$.
\end{lemma}
\begin{proof}
Let $S_1 \ilrof \apreorder i {\u B} S_2$ and $\gamma_1 \ilrof
\apreorder i \Gamma \gamma_2$. We need to show that
\[
- S_1[M[\gamma_1]] \ix\apreorder i S_2[N[\gamma_2]]
+ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[N[\gamma_2]])
\]
- We use \emph{reflexivity} of the relation:
- TODO: adapt the old proof of this below
+
+ So we need to construct a \emph{context} that when $M$ or $N$ is
+ plugged into the hole will reduce to the above.
+
+ To do this, first, we deconstruct the context
+ $x_1:A_1,\ldots,x_n:A_n = \Gamma$. Then we define $\cdot \vdash M'
+ : A_1\to \cdots \to A_n \to \u B$ as
+ \[ \lambda x_1:A_1.\ldots\lambda x_n:A_n. M \]
+ And similarly define $N'$. Then clearly
+ \[ S[M' \,V_1\, \cdots V_n] \bigstepsin{0} S[M[V_1/x_1,\ldots,V_n/x_n]] \]
+ so in particular
+ \[ S[M'\,\gamma(x_1)\cdots\gamma(x_n)] \bigstepsin{0} S[M[\gamma]]\]
+ and similarly for $N'$ if $x_1,\ldots,x_n$ are all of the variables
+ in $\gamma$.
+
+ Then the proof proceeds by the following transitivity chain:
+ \begin{align*}
+ S_1[M[\gamma_1]] &\ix\apreorder i \result(S_2[M[\gamma_2]])\tag{$M \ilr i M$}\\
+ &=\result(S_2[M'\,\gamma_2(x_1)\,\cdots\,\gamma_2(x_n)])\tag{reduction}\\
+ &\apreorder \result(S_2[N'\,\gamma_2(x_1)\,\cdots\,\gamma_2(x_n)])\tag{$M \ctxize\apreorder N$}\\
+ &= \result(S_2[N[\gamma_2]])\tag{reduction}
+ \end{align*}
+
+ So $S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[N[\gamma_2]])$ by
+ lemma (TODO: module)
\end{proof}
This establishes that our logical relation can prove graduality, so it
@@ -2772,37 +3041,82 @@ The only remaining rules to validate are the transitivity rules, error
rules, substitution principles, and the $\beta$ and $\eta$
equivalences for each type constructor.
-
-
With the reflexivity and limiting lemmas in hand, we can prove that
all of our logical relations (open and closed) are transitive in the
limit. To do this, we first prove the following kind of
``quantitative'' transitivity lemma, and then transitivity in the
limit is a consequence.
\begin{lemma}{Logical Relation is Quantitatively Transitive}
- First, for closed terms
\begin{enumerate}
\item If $V_1 \ilrof\apreorder i A V_2$ and $V_2 \ilrof\apreorder
\omega A V_3$, then $V_1 \ilrof\apreorder i A V_3$
\item If $S_1 \ilrof\apreorder i {\u B} S_2$ and $S_2 \ilrof\apreorder
\omega {\u B} S_3$, then $S_1 \ilrof\apreorder i {\u B} S_3$
\end{enumerate}
+\end{lemma}
+\begin{proof}
+ Proof is by mutual lexicographic induction on the pair $(i, A)$ or
+ $(i, \u B)$. All cases are straightforward uses of the inductive
+ hypotheses except the shifts $U, \u F$.
+ \begin{enumerate}
+ \item If $V_1 \itylr i {U \u B} V_2$ and $V_2
+ \ilrof\apreorder \omega {U \u B} V_3$, then we need to show that
+ for any $S_1 \itylr j {\u B} S_2$ with $j \leq i$,
+ \[ S_1[\force V_1] \ix\apreorder j \result(S_2[\force V_3]) \]
+ By reflexivity, we know $S_2 \itylr \omega {\u B} S_2$, so by assumption
+ \[ S_2[\force V_2] \ix\apreorder \omega \result(S_2[\force V_3])\]
+ which by lemma (TODO) is equivalent to
+ \[ \result(S_2[\force V_2]) \apreorder \result(S_2[\force V_3]) \]
+ so then by lemma (TODO: module), it is sufficient to show
+ \[ S_1[\force V_1] \ix\apreorder j \result(S_2[\force V_2]) \]
+ which holds by assumption.
+ \item If $S_1 \itylr i {\u F A} S_2$ and $S_2 \itylr \omega {\u F A}
+ S_3$, then we need to show that for any $V_1 \itylr A j V_2$ with $j \leq i$ that
+ \[ S_1[\ret V_1] \ix\apreorder j \result(S_3[\ret V_2])\]
+ First,
+ \[S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2]) \]
+ by assumption, so by lemma (TODO: module), it is sufficient to show
+ \[ \result(S_2[\ret V_2])\apreorder \result(S_3[\ret V_2])\]
+ which by lemma (TODO: in the limit) is equivalent to
+ \[ S_2[\ret V_2]\ix\apreorder \omega \result(S_3[\ret V_2])\]
+ which follows because $S_2 \itylr \omega {\u F A} S_3$ and by
+ reflexivity (TODO: lemma), $V_2 \itylr \omega A V_2$.
+ \end{enumerate}
+\end{proof}
- Then for open terms
+\begin{lemma}{Logical Relation is Quantitatively Transitive (Open Terms)}
\begin{enumerate}
- \item If $\Gamma \vDash M_1 \ilrof\apreorder i {} M_2 \in \u B$ and
- $\Gamma \vDash M_2 \ilrof\apreorder \omega {} M_3 \in \u B$, then
- $\Gamma \vDash M_1 \ilrof\apreorder i {} M_3 \in \u B$.
- \item If $\Gamma \vDash V_1 \ilrof\apreorder i {} V_2 \in A$ and
- $\Gamma \vDash V_2 \ilrof\apreorder \omega {} V_3 \in A$, then
- $\Gamma \vDash V_1 \ilrof\apreorder i {} V_3 \in A$.
- \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i {} S_2 \in \u B'$ and
- $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega {} S_3 \in \u B'$, then
- $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i {} S_3 \in \u B'$.
+ \item If $\gamma_1 \ilrof\apreorder i \Gamma \gamma_2$ and $\gamma_2 \ilrof\apreorder
+ \omega \Gamma \gamma_3$, then $\gamma_1 \ilrof\apreorder i \Gamma \gamma_3$
+ \item If $\Gamma \vDash M_1 \ilrof\apreorder i M_2 \in \u B$ and
+ $\Gamma \vDash M_2 \ilrof\apreorder \omega M_3 \in \u B$, then
+ $\Gamma \vDash M_1 \ilrof\apreorder i M_3 \in \u B$.
+ \item If $\Gamma \vDash V_1 \ilrof\apreorder i V_2 \in A$ and
+ $\Gamma \vDash V_2 \ilrof\apreorder \omega V_3 \in A$, then
+ $\Gamma \vDash V_1 \ilrof\apreorder i V_3 \in A$.
+ \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i S_2 \in \u B'$ and
+ $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega S_3 \in \u B'$, then
+ $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i S_3 \in \u B'$.
\end{enumerate}
\end{lemma}
\begin{proof}
- TODO: adapt from below
+ \begin{enumerate}
+ \item By induction on the length of the context, follows from closed value case.
+ \item Assume $\gamma_1 \itylr i \Gamma \gamma_2$ and $S_1 \itylr i {\u B} S_2$.
+ We need to show
+ \[ S_1[M_1[\gamma_1]] \ix\apreorder{i} \result(S_2[M_3[\gamma_2]]) \]
+ by lemma (TODO: module), it is sufficient to show
+ \[ S_1[M_1[\gamma_1]] \ix\apreorder{i} \result(S_2[M_2[\gamma_2]]) \]
+ (which follows by assumption) and
+ \[ \result(S_2[M_2[\gamma_2]]) \apreorder \result(S_2[M_3[\gamma_2]]) \]
+ which follows from reflexivity and lemma (TODO: infinity) and
+ \[ S_2[M_2[\gamma_2]] \ix\apreorder\omega \result(S_2[M_3[\gamma_2]]) \]
+ \item Assume $\gamma_1 \itylr i \Gamma \gamma_2$. Then
+ $V_1[\gamma_1] \itylr i A V_2[\gamma_2]$ and by reflexivity
+ $\gamma_2 \itylr \omega \Gamma \gamma_2$ so $V_2[\gamma_2] \itylr
+ \omega A V_3[\gamma_2]$ so the result holds by the closed case.
+ \item Stack case is essentially the same as the value case.
+ \end{enumerate}
\end{proof}
\begin{corollary}{Logical Relation is Transitive in the Limit}
@@ -2816,29 +3130,83 @@ limit is a consequence.
Then for open terms
\begin{enumerate}
- \item If $\Gamma \vDash M_1 \ilrof\apreorder \omega {} M_2 \in \u B$ and
- $\Gamma \vDash M_2 \ilrof\apreorder \omega {} M_3 \in \u B$, then
- $\Gamma \vDash M_1 \ilrof\apreorder \omega {} M_3 \in \u B$.
- \item If $\Gamma \vDash V_1 \ilrof\apreorder \omega {} V_2 \in A$ and
- $\Gamma \vDash V_2 \ilrof\apreorder \omega {} V_3 \in A$, then
- $\Gamma \vDash V_1 \ilrof\apreorder \omega {} V_3 \in A$.
- \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega {} S_2 \in \u B'$ and
- $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega {} S_3 \in \u B'$, then
- $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega {} S_3 \in \u B'$.
+ \item If $\Gamma \vDash M_1 \ilrof\apreorder \omega M_2 \in \u B$ and
+ $\Gamma \vDash M_2 \ilrof\apreorder \omega M_3 \in \u B$, then
+ $\Gamma \vDash M_1 \ilrof\apreorder \omega M_3 \in \u B$.
+ \item If $\Gamma \vDash V_1 \ilrof\apreorder \omega V_2 \in A$ and
+ $\Gamma \vDash V_2 \ilrof\apreorder \omega V_3 \in A$, then
+ $\Gamma \vDash V_1 \ilrof\apreorder \omega V_3 \in A$.
+ \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega S_2 \in \u B'$ and
+ $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega S_3 \in \u B'$, then
+ $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega S_3 \in \u B'$.
\end{enumerate}
\end{corollary}
\begin{lemma}{$\beta, \eta$ Laws are valid}
For any preorder with diverge a least element, the $\beta, \eta$
- laws are valid for $\ilrof\apreorder \omega {}$
+ laws are valid for $\ilrof\apreorder \omega$
\end{lemma}
\begin{proof}
- TODO, easy
+ The $\beta$ rules for all cases except recursive types are direct
+ from anti-reduction.
+ \begin{enumerate}
+ \item $\mu X.A-\beta$:
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_1]} x M[\gamma_1]] \ilr i \result(S_2[M[\gamma_2,V[\gamma_2]/x]]) \]
+ The left side takes $1$ step so if $i \leq 1$ we are done. Otherwise, we need to show
+ \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr {i-1} S_2[M[\gamma_2,V[\gamma_2]/x]] \]
+ which follows by anti-reduction because by assumption, we have
+ \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr {i} S_2[M[\gamma_2,V[\gamma_2]/x]] \]
+ \item The other case is easier, because result is invariant under
+ a step.
+ \end{enumerate}
+ \item $\mu X.A-\eta$:
+ \begin{enumerate}
+ \item We need to show for any $\Gamma, x : \mu X. A \vdash M : \u B$,
+ and appropriate substitutions and stacks,
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A}} {\gamma_1(x)} M] \ilr i \result(S_2[M[\gamma_2]]) \]
+ TODO: finish
+ \end{enumerate}
+ \end{enumerate}
\end{proof}
\begin{lemma}{Substitution Principles}
- TODO
+ For any diverge-bottom preorder $\apreorder$, the following are
+ valid
+ \begin{enumerate}
+ \item $\inferrule{\Gamma \vDash V_1 \ilr i V_2 \in A
+ \and \Gamma, x : A \vDash V_1' \ilr V_2' \in A'}{\Gamma \vDash V_1'[V_1/x] \ilr V_2'[V_2/x] \in A'}$
+ \item $\inferrule{\Gamma \vDash V_1 \ilr i V_2 \in A
+ \and \Gamma, x : A \vDash M_1 \ilr M_2 \in \u B}{\Gamma \vDash M_1[V_1/x] \ilr M_2[V_2/x] \in \u B}$
+ \end{enumerate}
+\end{lemma}
+\begin{proof}
+ We do the term case, the value case is similar. Given $\gamma_1
+ \itylr i \Gamma \gamma_2$, we have $V_1[\gamma_1] \itylr i A
+ V_2[\gamma_2]$ so
+ \[ \gamma_1,V_1[\gamma_1]/x \itylr i {\Gamma, x : A} \gamma_2, V_2[\gamma_2]/x \]
+ and by associativity of substitution
+ \[ M_1[V_1/x][\gamma_1] = M_1[\gamma_1,V_1[\gamma_1]/x] \]
+ and similarly for $M_2$, so if $S_1 \itylr i {\u B} S_2$ then
+ \[ S_1[M_1[\gamma_1,V_1[\gamma_1]/x]] \ix\apreorder i \result(S_2[M_2[\gamma_2,V_2[\gamma_2]/x]])\]
+\end{proof}
+
+\begin{lemma}{Validity of Error Rules}
+ For any divergence-least preorder $\apreorder$,
+ \[ \Gamma \vDash S[\err] \ilr i \err \in \u B \]
+ and
+ \[ \Gamma \vDash \err \ilr i S[\err] \in \u B \]
+ and for any $\Gamma \vdash M : \u B$
+ \[ \err \ilrof\precltdyn i M\]
+ and
+ \[ M \ilrof\precltdyn i \err\]
+ and
+ \[ \err \ilrof\ltdynsucc i M\]
+ and
+ \[ M \ilrof\ltdynsucc i \err\]
\end{lemma}
+\begin{proof} All are trivial verifications. \end{proof}
\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
\begin{enumerate}
@@ -2875,366 +3243,6 @@ limit is a consequence.
Contextual of the 2 => Contextual ltdyn by earlier lemma
\end{proof}
-\begin{figure}
- \begin{mathpar}
- {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2
- \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S
- : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot
- \vdash M : \u F (1 + 1) \}^2\\
- \begin{array}{rcl}
- \Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1 \logty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \logc i S_2[M_2[\gamma_2]]\\
- \Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2.~ V_1[\gamma_1] \logty i A V_2[\gamma_2]\\
- \Gamma\pipe \bullet : \u B \vDash S_1 \ltdyn S_2 \in \u B' &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1' \logty i {\u B'} S_2'.~ S_1'[S_1[\gamma_1]] \logc i S_2'[S_2[\gamma_2]]\\
- \end{array}\\
- \begin{array}{rcl}
- \cdot \logty i {\cdot} \cdot &=& \top\\
- \gamma_1,x \mapsto V_1 \logty i {\Gamma,x:A} \gamma_2,x\mapsto V_2 &=& \gamma_1 \logty i \Gamma \gamma_2 \wedge V_1 \logty i A V_2\\
- V_1 \logty i 0 V_2 &=& \bot\\
- \inl V_1 \logty i {A + A'} \inl V_2 &= & V_1 \logty i A V_2\\
- \inr V_1 \logty i {A + A'} \inr V_2 &= & V_1 \logty i {A'} V_2 \\
- () \logty i 1 () &=& \top\\
- (V_1,V_1') \logty i {A \times A'} (V_2, V_2') &=& V_1 \logty i A V_2 \wedge V_1' \logty i {A'} V_2'\\
- % Should this be a roll or not?
- \rollty {\mu X. A} V_1 \logty 0 {\mu X. A} \rollty {\mu X. A} V_2 &=& \top\\
- \rollty {\mu X. A} V_1 \logty {i+1} {\mu X. A} \rollty {\mu X. A} V_2 &=& V_1 \logty i {A[\mu X.A/X]} V_2\\
- V_1 \logty i {U \u B} V_2 &=& \forall j \leq i, S_1 \logty j {\u B} S_2.~ S_1[\force V_1] \logc j S_2[\force V_2] \\\\
-
- S_1[\bullet V_1] \logty i {A \to \u B} S_1[\bullet V_2] & = & V_1 \logty i A V_2 \wedge S_1 \logty {i}{\u B} S_2\\
- S_1[\pi_1 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \logty i {\u B} S_2\\
- S_1[\pi_2 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \logty i {\u B'} S_2\\
- S_1 \logty i {\top} S_2 &=& \bot\\
- S_1[\unroll \bullet] \logty 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
- S_1[\unroll \bullet] \logty {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \logty i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
- S_1 \logty i {\u F A} S_2 & = & \forall j\leq i, V_1 \logty j A V_2.~ S_1[\ret V_1] \logc j S_2[\ret V_2]
- \end{array}
- \end{mathpar}
- \caption{Logical Relation from a Preorder $\apreorder$}
-\end{figure}
-
-\begin{definition}[Pole]
- A \emph{pole} $\pole$ is a function from natural numbers to sets of
- closed programs of type $\u F (1 + 1)$ satisfying
- \begin{enumerate}
- \item Downward closure: If $M_1 \ipole i M_2$ and $j \leq i$ then $M_1 \ipole j M_2$.
- \item Triviality at $0$: For any appropriately typed terms, $M_1 \ipole 0 M_2$
- \item Step-indexed anti-reduction: If $M_1 \stepsin j M_1'$ and $M_2
- \step M_2'$ and $M_1' \ipole i M_2'$ then $M_1' \ipole {i+j} M_2'$.
- \item Step-indexed transitivity: If $M_1 \ipole i M_2$ and $M_2
- \ipole \omega M_3$ then $M_1 \ipole i M_3$.
-
- % TODO: might as well make error the least element? not sure
-
- \item Error awareness: For all $i \in \nats$, $\err \ipole i \err$.
- \end{enumerate}
-\end{definition}
-
-\begin{definition}[Logical, Contextual Lifting of a Pole]
- Given a pole $\pole$, we define
- \begin{enumerate}
- \item Contextual lifting TODO of a pole to be the congruence
- closure.
- \item Logical lifting of a pole to be given by the rules in figure
- TODO ref.
- \end{enumerate}
-\end{definition}
-
-Next, we show that downward-closure is inherited by the logical
-relation from the pole.
-\begin{lemma}[Logical Relation Downward Closure]
- For any pole $\pole$, and $j \leq i$, we have
- \[ \logty{i}{A} \subseteq \logty{j}{A} \qquad\qquad
- \logty{i}{\u B} \subseteq \logty{j}{\u B} \qquad\qquad \]
-\end{lemma}
-
-\begin{theorem}[Logical Relations Theorem/Fundamental property]
- For any pole $\pole$, the logical lifting generated by it is sound
- with respect to the contextual lifting.
-\end{theorem}
-\begin{proof}
- Since the contextual lifting is the congruence closure of the pole,
- it is sufficient to show that the logical lifting of the pole models
- all of the congruence rules.
- \begin{enumerate}
- \item $\inferrule {} {\Gamma,x : A,\Gamma' \vDash x \logpole x :
- A}$. Given $\gamma_1 \logty i {\Gamma,x:A,\Gamma'} \gamma_2$,
- then by definition $\gamma_1(x) \logty i A \gamma_2(x)$.
-
- \item $\inferrule{}{\Gamma \vdash \err \ltdyn \err : \u B}$ We
- need to show $S_1[\err] \ipole i S_2[\err]$. By anti-reduction
- it is sufficient to show $\err \ipole i \err$, which follows by
- error awareness.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A \and
- \Gamma, x : A \vDash M \logpole M' \in \u B
- }
- {\Gamma \vDash \letXbeYinZ V x M \logpole \letXbeYinZ {V'} {x} {M'} \in \u B}$
- Each side takes $0$ steps so by anti-reduction, this reduces to
- \[ S_1[M[\gamma_1,V/x]] \ipole i S_2[M'[\gamma_2,V'/x]] \] which follows by assumption that $\Gamma, x : A \vDash M \logpole M' \in \u B$ are related.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in 0}
- {\Gamma \vDash \abort V \logpole \abort V' \in \u B}$.
- By assumption, we get $V[\gamma_1] \logty i {0} V'[\gamma_2]$, but this is a contradiction.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A_1}
- {\Gamma \vDash \inl V \logpole \inl V' \in A_1 + A_2}$.
- Direct from assumption, rule for sums.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A_2}
- {\Gamma \vDash \inr V \logpole \inr V' \in A_1 + A_2}$
- Direct from assumption, rule for sums.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A_1 + A_2\and
- \Gamma, x_1 : A_1 \vDash M_1 \logpole M_1' \in \u B\and
- \Gamma, x_2 : A_2 \vDash M_2 \logpole M_2' \in \u B
- }
- {\Gamma \vDash \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \logpole \caseofXthenYelseZ {V'} {x_1. M_1'}{x_2.M_2'} \in \u B}$
- By case analysis of $V[\gamma_1] \logpole V'[\gamma_2]$.
- \begin{enumerate}
- \item If $V[\gamma_1]=\inl V_1, V'[\gamma_2] = \inl V_1'$ with $V_1 \logty i {A_1}$, then taking $0$ steps, by anti-reduction the problem reduces to
- \[ S_1[M_1[\gamma_1,V_1/x_1]] \ipole i S_1[M_1[\gamma_1,V_1/x_1]]\]
- which follows by assumption.
- \item For $\inr{}$, the same argument.
- \end{enumerate}
-
- \item $\inferrule
- {}
- {\Gamma \vDash () \logpole () \in 1}$ Immediate by unit rule.
-
- \item $\inferrule
- {\Gamma \vDash V_1 \logpole V_1' \in A_1\and
- \Gamma\vDash V_2 \logpole V_2' \in A_2}
- {\Gamma \vDash (V_1,V_2) \logpole (V_1',V_2') \in A_1 \times A_2}$
- Immediate by pair rule.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A_1 \times A_2\and
- \Gamma, x : A_1,y : A_2 \vDash M \logpole M' \in \u B
- }
- {\Gamma \vDash \pmpairWtoXYinZ V x y M \logpole \pmpairWtoXYinZ {V'} {x} {y} {M'} \in \u B}$
- By $V \logty i {A_1 \times A_2} V'$, we know $V[\gamma_1] =
- (V_1,V_2)$ and $V'[\gamma_2] = (V_1', V_2')$ with $V_1 \logty i
- {A_1} V_1'$ and $V_2 \logty i {A_2} V_2'$.
- Then by anti-reduction, the problem reduces to
- \[ S_1[M[\gamma_1,V_1/x,V_2/y]] \ipole i S_1[M'[\gamma_1,V_1'/x,V_2'/y]] \]
- which follows by assumption.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A[\mu X.A/X]}
- {\Gamma \vDash \rollty{\mu X.A} V \logpole \rollty{\mu X.A} V' \in \mu X.A }$
- If $i = 0$, we're done. Otherwise $i=j+1$, and our assumption is
- that $V[\gamma_1] \logty {j+1} V'[\gamma_2]$ and we need to show
- that $\roll V[\gamma_1] \logty {j+1} {\mu X. A}\roll
- V'[\gamma_2]$. By definition, we need to show $V[\gamma_1] \logty
- j V'[\gamma_2]$, which follows by downward-closure.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in \mu X. A\and
- \Gamma, x : A[\mu X. A/X] \vDash M \logpole M' \in \u B}
- {\Gamma \vDash \pmmuXtoYinZ V x M \logpole \pmmuXtoYinZ {V'} {x} {M'} \in \u B}$
- If $i = 0$, then by triviality at $0$, we're done.
- Otherwise, $V[\gamma_1] \logty {j+1} {\mu X. A} V'[\gamma_2]$ so
- $V[\gamma_1] = \roll V_\mu, V'[\gamma_2] = \roll V_\mu'$ with
- $V_\mu \logty j {A[\mu X.A/X]} V_\mu'$. Then each side takes $1$ step, so by anti-reduction it is sufficient to show
- \[ S_1[M[\gamma_1,V_\mu/x]] \ipole j S_2[M'[\gamma_2,V_\mu'/x]] \] which follows by assumption and downward closure of the stack, value relations.
-
- \item $\inferrule {\Gamma \vDash M \logpole M' \in \u B} {\Gamma
- \vDash \thunk M \logpole \thunk M' \in U \u B}$. We need to show
- $M[\gamma_1] \logty i {U \u B} M'[\gamma_2]$, so let $S_1 \logty
- j {\u B} S_2$. Then by downward-closure $\gamma_1 \logty j
- {\Gamma} \gamma_2$, so by assumption, $S_1[M_1[\gamma_1]] \ipole
- j S_2[M_2[\gamma_2]] $.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in U \u B}
- {\Gamma \vDash \force V \logpole \force V' \in \u B}$.
- We need to show $S_1[\force V[\gamma_1]] \ipole i S_2[\force
- V'[\gamma_2]]$, which follows by the orthogonality definition of
- $V[\gamma_1] \logty i {U \u B} V'[\gamma_2]$.
-
- \item $\inferrule
- {\Gamma \vDash V \logpole V' \in A}
- {\Gamma \vDash \ret V \logpole \ret V' \in \u F A}$
- We need to show $S_1[\ret V[\gamma_1]] \ipole i S_2[\ret
- V'[\gamma_2]]$, which follows by the orthogonality definition of
- $S_1 \logty i {\u F A} S_2$.
-
- \item $\inferrule
- {\Gamma \vDash M \logpole M' \in \u F A\and
- \Gamma, x: A \vDash N \logpole N' \in \u B}
- {\Gamma \vDash \bindXtoYinZ M x N \logpole \bindXtoYinZ {M'} {x} {N'} \in \u B}$.
-
- We need to show $\bindXtoYinZ {M[\gamma_1]} x {N[\gamma_2]} \ipole i \bindXtoYinZ {M'[\gamma_2]} {x} {N'[\gamma_2]}$.
- By $M \logpole M' \in \u F A$, it is sufficient to show that
- \[ \bindXtoYinZ \bullet x {N[\gamma_1]} \logty i {\u F A} \bindXtoYinZ \bullet {x} {N'[\gamma_2]}\]
- So let $j \leq i$ and $V \logty j A V'$, then we need to show
- \[ \bindXtoYinZ {\ret V} x {N[\gamma_1]} \logty j {\u F A} \bindXtoYinZ {\ret V'} {x} {N'[\gamma_2]} \]
- By anti-reduction, it is sufficient to show
- \[ N[\gamma_1,V/x] \ipole j N'[\gamma_2,V'/x] \]
- which follows by anti-reduction for $\gamma_1 \logty i {\Gamma} \gamma_2$ and $N \logpole N'$.
-
- \item $\inferrule
- {\Gamma, x: A \vDash M \logpole M' \in \u B}
- {\Gamma \vDash \lambda x : A . M \logpole \lambda x:A. M' \in A \to \u B}$
- We need to show $S_1[\lambda x:A. M[\gamma_1]] \ipole i S_2[\lambda x:A.M'[\gamma_2]]$.
- By $S_1 \logty i {A \to \u B} S_2$, we know $S_1 = S_1'[\bullet V_1]$, $S_2 = S_2'[\bullet V_2]$ with $S_1' \logty i {\u B} S_2'$ and $V_1 \logty i {A} V_2$.
- Then by anti-reduction it is sufficient to show
- \[
- S_1'[M[\gamma_1,V_1/x]] \ipole i S_2'[M'[\gamma_2,V_2/x]]
- \]
- which follows by $M \logpole M'$.
-
- \item $\inferrule
- {\Gamma \vDash M \logpole M' \in A \to \u B\and
- \Gamma \vDash V \logpole V' \in A}
- {\Gamma \vDash M\,V \logpole M'\,V' \in \u B }$
- We need to show $S_1[M[\gamma_1]\,V[\gamma_1]] \ipole i S_2[M'[\gamma_2]\,V'[\gamma_2]]$ so by $M \logpole M'$ it is sufficient to show $S_1[\bullet V[\gamma_1]] \logty i {A \to \u B} S_2[\bullet V'[\gamma_2]]$ which follows by definition and assumption that $V \logpole V'$.
-
- \item $\inferrule
- {\Gamma \vDash M_1 \logpole M_1' \in \u B_1\and
- \Gamma \vDash M_2 \logpole M_2' \in \u B_2}
- {\Gamma \vDash \pair {M_1} {M_2} \logpole \pair {M_1'} {M_2'} \in \u B_1 \with \u B_2}$
- We need to show $S_1[\pair{M_1[\gamma_1]}{M_2[\gamma_1]}] \ipole i S_2[\pair{M_1'[\gamma_1]}{M_2'[\gamma_2]}]$.
- We proceed by case analsysis of $S_1 \logty i {\u B_1 \with \u B_2} S_2$
- \begin{enumerate}
- \item In the first possibility $S_1 = S_{1}'[\pi \bullet], S_2 =
- S_2'[\pi \bullet]$ and $S_1' \logty i {\u B_1} S_2'$.
- Then by anti-reduction, it is sufficient to show
- \[ S_1'[M_1[\gamma_1]] \ipole i S_2'[M_1'[\gamma_2]] \]
- which follows by $M_1 \logpole M_1'$.
- \item Same as previous case.
- \end{enumerate}
-
- \item $\inferrule
- {\Gamma \vDash M \logpole M' \in \u B_1 \with \u B_2}
- {\Gamma \vDash \pi M \logpole \pi M' \in \u B_1}$
- We need to show $S_1[\pi M[\gamma_1]] \ipole i S_2[\pi
- M'[\gamma_2]]$, which follows by $S_1[\pi \bullet] \logty i {\u
- B_1 \with \u B_2} S_2[\pi \bullet]$ and $M \logpole M'$.
-
- \item $\inferrule {\Gamma \vDash M \logpole M' \in \u B_1 \with \u
- B_2} {\Gamma \vDash \pi' M \logpole \pi' M' \in \u B_2}$ Similar
- to previous case.
-
- \item $\inferrule
- {\Gamma \vDash M \logpole M' \in \u B[{\nu \u Y. \u B}/\u Y]}
- {\Gamma \vDash \rollty{\nu \u Y. \u B} M \logpole \rollty{\nu \u Y. \u B} M' \in {\nu \u Y. \u B}}$
- We need to show that
- \[ S_1[ \rollty{\nu \u Y. \u B} M[\gamma_1]]
- \ipole i S_2[ \rollty{\nu \u Y. \u B} M'[\gamma_2]] \]
- If $i = 0$, we invoke triviality at $0$.
- Otherwise, $i = j + 1$ and we know by $S_1 \logty {j+1} {\nu \u Y. \u B} S_2$ that
- $S_1 = S_1'[\unroll \bullet]$ and $S_2 = S_2'[\unroll \bullet]$ with $S_1' \logty j {\u B[{\nu \u Y. \u B}/\u Y]} S_2'$, so by anti-reduction it is sufficient to show
- \[ S_1'[ M[\gamma_1]] \ipole i S_2'[ M'[\gamma_2]] \]
- which follows by $M \logpole M'$ and downward-closure.
-
- \item $\inferrule
- {\Gamma \vDash M \logpole M' \in {\nu \u Y. \u B}}
- {\Gamma \vDash \unroll M \logpole \unroll M' \in \u B[{\nu \u Y. \u B}/\u Y]}$
- We need to show $S_1[\unroll M] \ipole i S_2[\unroll M']$, which
- follows because $S_1[\unroll \bullet] \logty i {\nu \u Y. \u B}
- S_2[\unroll \bullet]$ and $M \logpole M'$.
- \end{enumerate}
-\end{proof}
-\begin{corollary}[Reflexivity/Monotonicity]
- For any $\Gamma \vdash M : \u B$, $\Gamma \vdash M \logpole M \in \u B$
-\end{corollary}
-
-\begin{theorem}[Completeness of Logical wrt Contextual]
- For any pole $\pole$, the logical lifting is complete with respect
- to the contextual lifting.
-\end{theorem}
-\begin{proof}
- TODO: modify the proof below
-\end{proof}
-
-\begin{theorem}[LR is Sound for Contextual Error Approximation]
- \begin{enumerate}
- \item If $\Gamma \vDash M_1 \ltdyn M_2 \in \u B$, then $\Gamma \vDash M_1 \ltctx M_2 \in \u B$.
- \item If $\Gamma \vDash V_1 \ltdyn V_2 \in A$, then $\Gamma \vDash V_1 \ltctx V_2 \in A$.
- \item If $\Gamma \pipe \bullet:\u B \vDash S_1 \ltdyn S_2 \in \u B'$,
- then $\Gamma \pipe \bullet:\u B \vDash S_1 \ltctx S_2 \in \u B'$.
- \end{enumerate}
-\end{theorem}
-\begin{proof}
- Proved in 2 pieces: congruence and adequacy.
- \begin{enumerate}
- \item (Congruence) By induction on term constructors, we show the
- relations are closed under all term, value, stack constructors.
- \item (Adequacy) If $\cdot \vDash M_1 \ltdyn M_2 \in \u F (1 + 1)$,
- then TODO (nothing really to say?)
- \end{enumerate}
-\end{proof}
-
-\begin{theorem}[Skewed Transitivity]
- All of the following are true
- \begin{enumerate}
- \item If $V_1 \ltlogty \omega A V_1'$, $V_2' \ltlogty \omega A V_2$,
- and $V_1 \ltlogty i A V_2'$ and $V_1' \ltlogty i A V_2$, then $V_1 \ltlogty i A V_2$.
- \item If $S_1 \ltlogty \omega {\u B} S_1'$, $S_2' \ltlogty \omega {\u B} S_2$,
- and $S_1 \ltlogty i {\u B} S_2'$ and $S_1' \ltlogty i {\u B} S_2$, then $S_1 \ltlogty i {\u B} S_2$.
- \item If $M_1 \ltlogc \omega M_1'$, $M_2' \ltlogc \omega M_2$,
- and $M_1 \ltlogc i M_2'$ and $M_1' \ltlogc i M_2$, then $M_1 \ltlogc i M_2$.
- \end{enumerate}
-\end{theorem}
-\begin{proof}
- TODO: the values and stacks by step-indexed induction on types (uses
- fundamental property so prove that first). The term one by direct
- verification.
-\end{proof}
-\begin{corollary}[Transitivity in the Limit]
- All of the following are true
- \begin{enumerate}
- \item If $V_1 \ltlogty \omega A V_2 \ltlogty \omega A V_3$, then $V_1 \ltlogty \omega A V_3$.
- \item If $S_1 \ltlogty \omega {\u B} S_2 \ltlogty \omega {\u B} S_3$, then $S_1 \ltlogty \omega {\u B} S_3$.
- \item If $M_1 \ltlogc \omega M_2 \ltlogc \omega M_3$, then $M_1 \ltlogc \omega M_3$.
- \end{enumerate}
-\end{corollary}
-\begin{proof}
- Use the previous with $V_2/S_2/M_2$ as the middle term.
-\end{proof}
-
-\begin{theorem}[LR is Complete for Contextual Error Approximation]
- If $\Gamma \vDash M_1 \ltctx M_2 \in \u B$ then $\Gamma \vDash M_1 \ltdyn M_2 \in \u B$.
-\end{theorem}
-\begin{proof}
- Let $S_1 \ltlogty{i}{\u B} S_2$ and $\gamma_1 \ltlogty i \Gamma \gamma_2$.
- %
- Then define $x_1:A_1,\ldots,x_n:A_n = \Gamma$.
- %
-
- Then we define \emph{contexts} $C_1,C_2$ that correspond to the
- ``plugging in'' of the stack-substition pairs.
- %
- Define
- \begin{align*}
- C_1 &= \letXbeYinZ{x_1}{\gamma_1(x_1)}\cdots; S_1[\bullet]\\
- C_2 &= \letXbeYinZ{x_1}{\gamma_2(x_1)}\cdots; S_2[\bullet]
- \end{align*}
- Then clearly for any $M$, $C_1[M] \step^0 S_1[M[\gamma_1]]$ and
- $C_2[M] \step^0 S_2[M[\gamma_2]]$, so by anti-reduction (TODO:
- lemma), they are equivalent to the logical relation.
-
- Then the proof is by the following use of skew transitivity.
- \[\begin{array}{ccccccc}
-{S_1[M_1[\gamma_1]]} & \ltlogc \omega & {C_1[M_1]} & \ltlogc \omega & {C_1[M_2]} & \ltlogc \omega & {S_2[M_2[\gamma_1]]} \\
-\ltlogc i & & & & & & \ltlogc i \\
-{S_2[M_1[\gamma_2]]} & \ltlogc \omega & {C_2[M_1]} & \ltlogc \omega & {C_2[M_2]} & \ltlogc \omega & {S_2[M_2[\gamma_2]]}
- \end{array}\]
- For the top and bottom rows, the middle inequality holds by the assumption that
- $M_1 \ltctx M_2$ and the other two by anti-reduction (TODO: lemma).
- %
- Then these compose by transitivity in the limit (TODO: ref).
- %
- Finally, the left and right sides of the square hold by the
- fundamental property (TODO: ref) applied to $M_1,M_2$ respectively.
-\end{proof}
-
-
\section{Discussion}
\paragraph{Casts as Galois Connections}