@@ -2611,6 +2611,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}
...
...
@@ -2647,7 +2650,7 @@ We extend the definition to contexts point-wise.
: \u F (1 + 1) \}^2\\
\begin{array}{rcl}
\cdot\itylrof\apreorder i {\cdot}\cdot&=&\top\\
\gamma_1,x \mapstoV_1 \itylrof\apreorder i {\Gamma,x:A}\gamma_2,x\mapstoV_2 &=&\gamma_1 \itylrof\apreorder i \Gamma\gamma_2 \wedge V_1 \itylrof\apreorder i A V_2\\
\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 \\
...
...
@@ -2707,7 +2710,215 @@ relation, i.e., the fundamental lemma of the logical relation.
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' \in0}
{\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 ()\in1}$ 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
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}
...
...
@@ -2960,191 +3171,7 @@ relation from the pole.
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' \in0}
{\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}$
\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'$.
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$
