diff --git a/paper/gtt.tex b/paper/gtt.tex
index b61ca792277de0c244af55be47839edf81277741..ea6eca1d11e9139aa3c63bf4c389fba11f7001c3 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -188,12 +188,12 @@
\newcommand{\simsub}[1]{\mathrel{\sim_{#1}}}
\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
-\newcommand{\ilrof}[2]{\mathrel{#1^{\text{log}}_{#2}}}
+\newcommand{\ilrof}[2]{\mathrel{{#1}^{\text{log}}_{#2}}}
\newcommand{\itylr}[2]{\itylrof{\apreorder}{#1}{#2}}
\newcommand{\ilr}[1]{\ilrof{\apreorder}{#1}}
-\newcommand{\simp}[1]{#1^{\dag}}
-\newcommand{\simpp}[1]{\simp{(#1)}}
+\newcommand{\simp}[1]{{#1}^{\dag}}
+\newcommand{\simpp}[1]{\simp{({#1})}}
%% Operational steps
\newcommand{\step}{\mapsto}
@@ -7579,8 +7579,6 @@ By composition with the axiomatic graduality theorem, this establishes
the \emph{operational graduality} theorem, i.e., a theorem analogous
to the \emph{dynamic gradual guarantee} as presented in TODO cite.
-TODO: show the ``goal theorem''
-
\subsection{Call-by-push-value operational semantics}
We present a small-step operational semantics for CBPV in figure
@@ -7632,7 +7630,7 @@ consider to be the type of whole programs.
\caption{CBPV Operational Semantics}
\label{fig:cbpv-operational-semantics}
\end{figure}
-
+\iflong
We can then observe the following standard operational properties. (We
write $M \step N$ with no index when the index is irrelevant.)
\begin{lemma}[Reduction is Deterministic]
@@ -7646,27 +7644,24 @@ write $M \step N$ with no index when the index is irrelevant.)
\begin{lemma}[Progress]
If $\cdot \vdash M : \u F A$ then one of the following holds:
- \begin{enumerate}
- \item $M = \err$
- \item $M = \ret V$ for $\cdot \vdash V : A$
- \item there exists $M'$ with $M \step M'$
- \end{enumerate}
+ \begin{mathpar}
+ M = \err \and M = \ret V \text{with} V:A \and \exists M'.~ M \step M
+ \end{mathpar}
\end{lemma}
+\fi
-Though we use a small-step semantics, our definition of
-observational equivalence is defined with respect to the final result
-of the program.
-%
+\begin{ifshort}
+ It is easy to see that the operational semantics is deterministic
+ and progress and type preservation theorems hold.
+\end{ifshort}
The standard progress-and-preservation properties allow us to define
-an associated ``big-step'' semantics as follows.
+the ``final result'' of a computation as follows.
\begin{corollary}[Possible Results of Computation]
- For any $\cdot \vdash M : \u F 2$, one of the following is true
- \begin{enumerate}
- \item $M \Uparrow$
- \item $M \Downarrow \err$
- \item $M \Downarrow \ret \tru$
- \item $M \Downarrow \ret \fls$
- \end{enumerate}
+ For any $\cdot \vdash M : \u F 2$, one of the following is true:
+ \begin{mathpar}
+ M \Uparrow \and M \Downarrow \err\and M \Downarrow \ret \tru \and
+ M \Downarrow \ret \fls
+ \end{mathpar}
\end{corollary}
\begin{longproof}
We define $M \Uparrow$ to hold when if $M \bigstepsin{i} N$ then
@@ -7701,7 +7696,14 @@ term/value/stack with a single $[\cdot]$ as some subterm/value/stack.
And define a typing $C : (\Gamma \vdash \u B) \Rightarrow (\Gamma'
\vdash \u B')$ to hold when for any $\Gamma \vdash M : \u B$, $\Gamma'
\vdash C[M] : \u B'$ (and similarly for values/stacks).
-
+Then contexts allow us to lift any relation on \emph{results} to
+relations on open terms, values and stacks.
+\begin{definition}[Contextual Lifting]
+ Given any relation $\sim \subseteq \text{Result}^2$, we can define
+ its \emph{observational lift} $\ctxize\sim$ to be the typed relation
+ defined by
+ \[ \Gamma \pipe \Delta \vDash E \ctxize\sim E' \in T = \forall C : (\Gamma\pipe\Delta \vdash T) \Rightarrow (\cdot \vdash \u F2).~ \result(C[E]) \sim \result(C[E'])\]
+\end{definition}
\begin{longfigure}
\begin{small}
\begin{mathpar}
@@ -7721,15 +7723,6 @@ And define a typing $C : (\Gamma \vdash \u B) \Rightarrow (\Gamma'
\caption{CBPV Context}
\end{longfigure}
-Then contexts allow us to lift any relation on \emph{results} to
-relations on open terms, values and stacks.
-\begin{definition}[Contextual Lifting]
- Given any relation $\sim \subseteq \text{Result}^2$, we can define
- its \emph{observational lift} $\ctxize\sim$ to be the typed relation
- defined by
- \[ \Gamma \pipe \Delta \vDash E \ctxize\sim E' \in T = \forall C : (\Gamma\pipe\Delta \vdash T) \Rightarrow (\cdot \vdash \u F2).~ \result(C[E]) \sim \result(C[E'])\]
-\end{definition}
-
The contextual lifting $\ctxize\sim$ inherits much structure of the
original relation $\sim$ as the following lemma shows.
%
@@ -7774,30 +7767,31 @@ The goal of this section is to prove
\end{small}
\begin{figure}
- \begin{minipage}{0.45\textwidth}
- \begin{center}
- \textbf{Domain ordering $\preceq$}\\
- \end{center}
- \begin{tikzcd}
-\ret\fls \arrow[rd, no head] & \ret \tru \arrow[d, no head] & \err \arrow[ld, no head] \\
- & \diverge &
-\end{tikzcd}
+ \begin{small}
+ \begin{minipage}{0.45\textwidth}
+ \begin{center}
+ \textbf{Diverge Approx. $\preceq$}\\
+ \end{center}
+ \begin{tikzcd}
+ \ret\fls \arrow[rd, no head] & \ret \tru \arrow[d, no head] & \err \arrow[ld, no head] \\
+ & \diverge &
+ \end{tikzcd}
\end{minipage}
\begin{minipage}{0.45\textwidth}
\begin{center}
\textbf{
- Graduality ordering $\ltdyn$}
+ Error Approx. $\ltdyn$}
\end{center}
\begin{tikzcd}
-\ret\fls \arrow[rd, no head] & \ret \tru \arrow[d, no head] & \diverge \arrow[ld, no head] \\
- & \err &
-\end{tikzcd}
+ \ret\fls \arrow[rd, no head] & \ret \tru \arrow[d, no head] & \diverge \arrow[ld, no head] \\
+ & \err &
+ \end{tikzcd}
\end{minipage}
\\\vspace{1em}
\begin{minipage}{0.45\textwidth}
\begin{center}
- \textbf{Graduality up to left-divergence
- $\preceq\ltdyn$}\\
+ \textbf{Error Approx. up to left-divergence
+ $\preceq\ltdyn$}\\
\end{center}
\begin{tikzcd}
\ret\fls \arrow[rd, no head] & & \ret \tru \arrow[ld, no head] \\
@@ -7807,15 +7801,16 @@ The goal of this section is to prove
\begin{minipage}{0.45\textwidth}
\vspace{1em}
\begin{center}
- \textbf{Graduality up to right-divergence}
+ \textbf{Error Approx. to right-divergence}
$\ltdyn\succeq$\\
\end{center}
- \begin{tikzcd}
- & \diverge \arrow[ld, no head] \arrow[rd, no head] & \\
-\ret\fls \arrow[rd, no head] & & \ret \tru \arrow[ld, no head] \\
- & \err &
- \end{tikzcd}
+ \begin{tikzcd}
+ & \diverge \arrow[ld, no head] \arrow[rd, no head] & \\
+ \ret\fls \arrow[rd, no head] & & \ret \tru \arrow[ld, no head] \\
+ & \err &
+ \end{tikzcd}
\end{minipage}
+ \end{small}
\caption{Result Orderings}
\label{fig:result-orders}
\end{figure}
@@ -7870,17 +7865,18 @@ Then clearly $\preceq\ltdyn$ is a divergence preorder and the
Then we can completely reduce the problem of proving $\ctxize=$ and
$\ctxize\ltdyn$ results to proving results about divergence preorders
by the following two observations.
+\newcommand{\ctxsimi}[1]{\mathrel{\sim_{#1}^{\text{ctx}}}}
\begin{lemma}[Decomposing Result Preorders]
Let $R, S$ be results.
\begin{enumerate}
\item $R = S$ if and only if $R \ltdyn S$ and $S \ltdyn R$
- \item $R \ltdyn S$ if and only if $R \preceq\ltdyn S$ and $S \ltdyn\succeq R$.
+ \item $R \ltdyn S$ if and only if $R \preceq\ltdyn S$ and $R \ltdyn\succeq S$.
\end{enumerate}
\end{lemma}
\begin{lemma}[Contextual Lift commutes with Conjunction]
If $R \sim S$ if and only if $R \simsub 1 S$ and $R \simsub 2 S$,
- then $E \ctxize\sim E'$ if and only if $E \ctxize{\simsub 1} E'$ and
- $E \ctxize{\simsub 2} E'$
+ then $E \ctxize\sim E'$ if and only if $E \ctxsimi 1 E'$ and
+ $E \ctxsimi 2 E'$
\end{lemma}
\subsection{CBPV Step Indexed Logical Relation}
@@ -7940,16 +7936,17 @@ logical relation.
\label{lem:module}
If $M \ix\apreorder i R$ and $R \apreorder R'$ then $M \ix\apreorder i R'$
\end{lemma}
-\begin{proof}
- If $M \bigstepsin{i} M'$ then there's nothing to show, otherwise $M
- \bigstepsin{j< i} \result(M)$ so it follows by transitivity of the
+\begin{longproof}
+ If $M \bigstepsin{i} M'$ then there's nothing to show, otherwise
+ $M \bigstepsin{j< i} \result(M)$ so it follows by transitivity of the
preorder: $\result(M) \apreorder R \apreorder R'$.
-\end{proof}
+\end{longproof}
-Next, we show the relation is downward-closed, meaning it is
-\emph{easier} for the relation to be satisfied if the step-index is
-\emph{smaller} (because time-outs occur earlier).
-\begin{lemma}[Downward Closure of Indexed Relation]
+%% Next, we show the relation is downward-closed, meaning it is
+%% \emph{easier} for the relation to be satisfied if the step-index is
+%% \emph{smaller} (because time-outs occur earlier).
+Then we establish a few basic properties of the finitized preorder.
+\begin{lemma}[Downward Closure of Finitized Preorder]
If $M \ix\apreorder i R$ and $j\leq i$ then $M \ix \apreorder j R$.
\end{lemma}
\begin{longproof}
@@ -7959,16 +7956,13 @@ Next, we show the relation is downward-closed, meaning it is
\item if $M \bigstepsin{k < j \leq i} \result(M)$ then $\result(M) \apreorder R$.
\end{enumerate}
\end{longproof}
-
-We also get the following ``base case'' of our relation.
\begin{lemma}[Triviality at $0$]
For any $\cdot \vdash M : \u F 2$, $M \ix\apreorder 0 R$
\end{lemma}
-\begin{proof}
+\begin{longproof}
Because $M \bigstepsin{0} M$
-\end{proof}
-
-\begin{lemma}[Result Anti-reduction]
+\end{longproof}
+\begin{lemma}[Result (Anti-)reduction]
If $M \bigstepsin{i} N$ then $\result(M) = \result(N)$.
\end{lemma}
\begin{lemma}[Anti-reduction]
@@ -8097,9 +8091,14 @@ observation by application of program contexts, the logical preorder
defines observation in terms of the ``input-output'' behavior: given
related inputs, the terms must give related observations under related
stacks.
+%
+\begin{shortonly}
+ We present this and some related definitions only for open
+ \emph{terms} and not values, stacks,
+\end{shortonly}
\begin{definition}[Logical Preorder]
- Given a preorder on results $\apreorder$ with $\diverge$ a least
- element, we define the step-indexed logical preorder as follows:
+ Given any divergence preorder $\apreorder$ 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 \itylrof\apreorder i {\Gamma} \gamma_2$ and $S_1
@@ -8120,17 +8119,19 @@ relation, i.e., the fundamental lemma of the logical relation.
This requires the easy lemma, that the relation on closed terms and
stacks is downward closed.
\begin{lemma}[Logical Relation Downward Closure]
- \begin{enumerate}
- \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}
+ For any type $T$, if $j \leq i$ then $\itylrof\apreorder i T
+ \subseteq \itylrof\apreorder j T$
+ %% \begin{enumerate}
+ %% \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$ a least element, the logical
- preorder $E \ilrof\apreorder i E'$ is a congruence relation, i.e.,
- it is closed under applying any value/term/stack constructors to
+ preorder $E \ilrof\apreorder i E'$ is \iflong a congruence relation, i.e.,
+ it is \fi closed under applying any value/term/stack constructors to
both sides.
\end{theorem}
\begin{longproof}
@@ -8348,7 +8349,7 @@ stacks is downward closed.
As a direct consequence we get the reflexivity of the relation.
\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
@@ -8377,11 +8378,11 @@ the limit as $i \to \omega$.
We write $\ix\apreorder \omega$ to mean the relation holds for every
$i \in \mathbb N$, i.e., $\ix\apreorder\omega =
\bigcap_{i\in\mathbb{N}} \ix\apreorder i$.
-\begin{corollary}[In the limit, Finitized Preorder Recovers Original]
+\begin{corollary}[Limit Lemma]
\label{lem:limit}
- For any divergence preorder $\apreorder$,
- \[ \result(M) \apreorder R \iff \forall i \in \mathbb{N}.~ M \ix\apreorder i R \]
- we abbreviate the right hand side as $M \ix \apreorder \omega R$
+ For any divergence preorder $\apreorder$, \( \result(M) \apreorder
+ R\) if and only if \(\forall i \in \mathbb{N}.~ M \ix\apreorder i R
+ \).
\end{corollary}
\begin{longproof}
Two cases
@@ -8404,30 +8405,27 @@ $i \in \mathbb N$, i.e., $\ix\apreorder\omega =
\end{enumerate}
\end{longproof}
-\begin{corollary}[LR is Sound wrt Contextual Preorder]
+\begin{corollary}[Logical implies Contextual]
If $\Gamma \vDash E \ilrof\apreorder \omega E' \in \u B$
then
$\Gamma \vDash E \ctxize\apreorder E' \in \u B$.
\end{corollary}
\begin{proof}
Let $C$ be a closing context. By congruence, $C[M] \ilrof\apreorder
- \omega C[N]$, so by the unary model lemma,
- \[ C[M] \ix\apreorder\omega \result(C[N]) \]
- so by the limit lemma, we have
- \[ \result(C[M]) \apreorder \result(C[N]) \]
- which is precisely the contextual preorder.
+ \omega C[N]$, so by the unary model lemma, $C[M] \ix\apreorder\omega
+ \result(C[N])$ so by the limit lemma, we have
+ $\result(C[M]) \apreorder \result(C[N])$.
\end{proof}
In fact, we can prove the converse, that at least for the term case,
the logical preorder is \emph{complete} with respect to the contextual
-preorder.
-\begin{lemma}[Logical Preorder is Complete wrt Contextual Preorder]
+preorder, though we don't use it.
+\begin{lemma}[Contextual implies Logical]
For any $\apreorder$, if $\Gamma \vDash M \ctxize \apreorder N \in
\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
+\begin{longproof}
+ Let $S_1 \itylr i {\u B} S_2$ and $\gamma_1 \itylr i \Gamma \gamma_2$. We need to show that
\[
S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[N[\gamma_2]])
\]
@@ -8456,7 +8454,7 @@ preorder.
So $S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[N[\gamma_2]])$ by
the module lemma \ref{lem:module}.
-\end{proof}
+\end{longproof}
This establishes that our logical relation can prove graduality, so it
only remains to show that our \emph{inequational theory} implies our
@@ -8513,7 +8511,7 @@ limit is a consequence.
which holds by assumption.
\end{enumerate}
\end{longproof}
-
+\iflong
\begin{lemma}[Logical Relation is Quantitatively Transitive (Open Terms)]\hfill
\begin{enumerate}
\item If $\gamma_1 \itylr i \Gamma \gamma_2$ and $\gamma_2 \itylr
@@ -8549,8 +8547,13 @@ limit is a consequence.
\item Stack case is essentially the same as the value case.
\end{enumerate}
\end{longproof}
-
-\begin{corollary}[Logical Relation is Transitive in the Limit]\hfill
+\fi
+\begin{corollary}[Logical Relation is Transitive in the Limit]
+ \begin{shortonly}
+ $\ilrof\apreorder \omega$ is transitive.
+ \end{shortonly}
+ \begin{longonly}
+ \hfill
\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
@@ -8562,12 +8565,14 @@ limit is a consequence.
$\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{longonly}
\end{corollary}
+\iflong
Next, we verify the $\beta, \eta$ equivalences hold as orderings each
way.
-\begin{lemma}[$\beta, \eta$ Laws are valid]
- For any preorder with $\diverge$ a least element, the $\beta, \eta$
+\begin{lemma}[$\beta, \eta$]
+ For any divergence preorder, the $\beta, \eta$
laws are valid for $\ilrof\apreorder \omega$
\end{lemma}
\begin{longproof}
@@ -8817,23 +8822,23 @@ way.
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{longproof}
-
+\fi
Finally, we verify the axioms about errors.
%
The strictness axioms hold for any $\apreorder$, but the axiom that
-$\err$ is a least element hold specifically in $\precltdyn, \ltdyn\succeq$
-
-\begin{lemma}[Validity of Error Rules]
- For any divergence-least preorder $\apreorder$,
+$\err$ is a least element is specific to the definitions of
+$\precltdyn, \ltdyn\succeq$
+\begin{lemma}[Error Rules]
+ For any divergence-least preorder $\apreorder$ and appropriately
+ typed $S, M$,
+ \begin{small}
\begin{mathpar}
\Gamma \vDash S[\err] \ilr i \err \in \u B \and
- \Gamma \vDash \err \ilr i S[\err] \in \u B
- \end{mathpar}
- and for any $\Gamma \vdash M : \u B$
- \begin{mathpar}
+ \Gamma \vDash \err \ilr i S[\err] \in \u B\and
\err \ilrof\precltdyn i M\and
M \ilrof{\preceq\gtdyn} i \err
- \end{mathpar}
+ \end{mathpar}
+ \end{small}
\end{lemma}
\begin{longproof}
\begin{enumerate}
@@ -8864,32 +8869,26 @@ following theorem that says our logical relation is a model of CBPV.
As shown in section (TODO: the observational approximation section),
with the soundness theorem, this gives that $\ctxize\ltdyn$ is a model
as well.
-\begin{theorem}[$\ctxize \ltdyn$ is a Model of CBPV $\ltdyn$]
- \[
-\begin{small}
- \inferrule
- {\Gamma \pipe \Delta \vdash E \ltdyn E' : T}
- {\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T}
-\end{small}
- \]
+And because equivalence is ordering both ways, this shows that
+contextual equivalence is a model of equi-dynamism.
+\begin{theorem}[Contextual Approx./Equiv. Model CBPV]
+ \begin{small}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \pipe \Delta \vdash E \ltdyn E' : T}
+ {\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T}\and
+
+ \inferrule
+ {\Gamma \pipe \Delta \vdash E \equidyn E' : T}
+ {\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}
+ \end{mathpar}
+ \end{small}
\end{theorem}
\begin{longproof}
By the previous lemma, and the soundness of LR wrt contextual
preorder, and commuting of conjection with contextual lifting.
\end{longproof}
-Which shows also that contextual equivalence is a model of
-equi-dynamism.
-\begin{corollary}[$\ctxize =$ is a Model of CBPV $\equidyn$]
- \[
-\begin{small}
- \inferrule
- {\Gamma \pipe \Delta \vdash E \equidyn E' : T}
- {\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}
-\end{small}
- \]
-\end{corollary}
-
\section{Discussion and Related Work}
\label{sec:related}