diff --git a/paper/gtt.tex b/paper/gtt.tex
index f0c74a953b9a621e291b088056cd8055878c3639..eafd95c8ce8dab5f61c6c637ddab8031e2002f6d 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -176,8 +176,9 @@
\newcommand{\apreorder}{\trianglelefteq}
\newcommand{\ctxpreorder}{\mathrel{\apreorder^{\text{ctx}}}}
-\newcommand{\ctxize}[1]{\mathrel{#1^{\text{ctx}}}}
-\newcommand{\ix}[2]{\mathrel{#1^#2}}
+\newcommand{\ctxize}[1]{\mathrel{{#1}^{\text{ctx}}}}
+\newcommand{\ix}[2]{\mathrel{#1^{#2}}}
+\newcommand{\simsub}[1]{\mathrel{\sim_{#1}}}
\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
\newcommand{\ilrof}[2]{\mathrel{#1^{\text{log}}_{#2}}}
@@ -195,6 +196,7 @@
\newcommand{\stepstar}{\stepsin{*}}
\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
\newcommand{\bigstepzero}{\bigstepsin{0}}
+\newcommand{\bigstepany}{\bigstepsin{}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\pairone}[1]{\{ \pi \mapsto {#1}}
@@ -3236,49 +3238,58 @@ type:
\begin{figure}
\begin{mathpar}
\inferrule
- {\Gamma\pipe \Delta \vdash V : \dynv\\
- \Gamma,x_1 : 1\pipe \Delta \vdash E_1 : T\\
- \Gamma,x_\times : \dynv\times\dynv\pipe \Delta \vdash E_\times : T\\
- \Gamma,x_+ : \dynv+\dynv\pipe \Delta \vdash E_+ : T\\
- \Gamma,x_U : U\dync \pipe \Delta \vdash E_U : T\\
- }
- {\Gamma\pipe \Delta \vdash \dyncaseofXthenOnePairSumU {V} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} : T}
-
- \dyncaseofXthenOnePairSumU {(\upcast{G}{\dynv}V)} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} \equidyn E_{G}[V/x_G]\qquad(\dynv\beta)\\
-
- \inferrule
- {\Gamma , x : \dynv \pipe \Delta \vdash E : \u B}
- {E \equidyn \dyncaseofXthenOnePairSumU x
- {x_1. E[\upcast{1}{\dynv}/x_1]}
- {x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
- {x_+. E[\upcast{+}{\dynv}/x_+]}
- {x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\\
-
- {\dncast{\u F 1}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_1. \ret x_1}{\els \err}}\\
- {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
- {\dncast{\u F(\dynv + \dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_+. \ret x_+}{\els \err}}\\
- {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
-
- \inferrule
- {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
- \Gamma \pipe \Delta \vdash M_{\with} : \dync \with \dync\\
- \Gamma \pipe \Delta \vdash M_{\u F} : \u F}
- {\Gamma \pipe \Delta \vdash \dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} : \u B}
-
- \dncast{\u G}{\dync}\dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)\\
- {\bullet : \dync \vdash \bullet
- \equidyn
- \dyncocaseWithFunF
- {\dncast{\dync\with\dync}{\dync}\bullet}
- {\dncast{\dynv\to\dync}{\dync}\bullet}
- {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)\\
-
- \force\upcast{U(\dync\with\dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\force V}{\err}{\err}\\
- \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\force V}{\err}\\
- \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\err}{\force V}\\
+ {\Gamma\pipe \Delta \vdash V : \dynv\\
+ \Gamma,x_1 : 1\pipe \Delta \vdash E_1 : T\\
+ \Gamma,x_\times : \dynv\times\dynv\pipe \Delta \vdash E_\times : T\\
+ \Gamma,x_+ : \dynv+\dynv\pipe \Delta \vdash E_+ : T\\
+ \Gamma,x_U : U\dync \pipe \Delta \vdash E_U : T\\
+ }
+ {\Gamma\pipe \Delta \vdash \dyncaseofXthenOnePairSumU {V} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} : T}\and
+
+ \dyncaseofXthenOnePairSumU {(\upcast{G}{\dynv}V)} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} \equidyn E_{G}[V/x_G]\qquad(\dynv\beta)\and
+
+ \inferrule
+ {\Gamma , x : \dynv \pipe \Delta \vdash E : \u B}
+ {E \equidyn \dyncaseofXthenOnePairSumU x
+ {x_1. E[\upcast{1}{\dynv}/x_1]}
+ {x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
+ {x_+. E[\upcast{+}{\dynv}/x_+]}
+ {x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\and
+
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
+ \Gamma \pipe \Delta \vdash M_{\with} : \dync \with \dync\\
+ \Gamma \pipe \Delta \vdash M_{\u F} : \u F}
+ {\Gamma \pipe \Delta \vdash \dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} : \u B}\and
+
+ \dncast{\u G}{\dync}\dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)\and
+
+ {\bullet : \dync \vdash \bullet
+ \equidyn
+ \dyncocaseWithFunF
+ {\dncast{\dync\with\dync}{\dync}\bullet}
+ {\dncast{\dynv\to\dync}{\dync}\bullet}
+ {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)
\end{mathpar}
\caption{Natural Dynamic Type Extension of GTT}
\end{figure}
+
+The axioms we choose might seem to underspecify the dynamic type, but
+because of the uniqueness of adjoints, the following are derivable.
+\begin{lemma}[Natural Dynamic Type Extension Theorems]
+ The following are derivable in GTT with the natural dynamic type extension
+ \begin{mathpar}
+ {\dncast{\u F 1}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_1. \ret x_1}{\els \err}}\\
+ {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
+ {\dncast{\u F(\dynv + \dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_+. \ret x_+}{\els \err}}\\
+ {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
+ \force\upcast{U(\dync\with\dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\force V}{\err}{\err}\\
+ \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\force V}{\err}\\
+ \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\err}{\force V}\\
+ \end{mathpar}
+\end{lemma}
+We explore this in more detail with the next dynamic type
+interpretation.
\end{longonly}
One of the reasons this dynamic type is so odd is that it includes
@@ -3367,10 +3378,14 @@ This leads to the following definition.
to $\dynv$ by lemma (TODO: ref). Next, we can define $1$ to be the
ep pair to $1+1$ defined by the left case and lemma (TODO: ref).
Then we get the ep pair for $\dynv + \dynv$ by composing the
- isomorphism $\dynv + \dynv \cong (1+1) \times \dynv$ with the ep
- pair for $1+1$:
- \[ \dynv + \dynv \cong (1+1)\times \dynv \triangleleft \dynv \times \dynv \triangleleft \dynv\]
- And similarly for $\dync \with \dync$:
+ isomorphism $(\dynv + \dynv) \cong ((1+1) \times \dynv)$ with the ep
+
+ pair for $1+1$ using the action of product types on ep pairs (proven
+ as part of lemma \ref{lem:casts-are-ep-pairs}):
+ \[ (\dynv + \dynv) \cong ((1+1)\times \dynv) \triangleleft (\dynv \times \dynv) \triangleleft \dynv \]
+ And similarly for $\dync \with \dync$, using the action of the
+ function type on ep pairs (also proven as part of lemma
+ \ref{lem:casts-are-ep-pairs}):
\[ \dync \with \dync \cong (1+1) \to \dync \triangleleft \dynv \to \dync \triangleleft \dync \]
\end{proof}
@@ -4044,6 +4059,7 @@ established we only have to manipulate values and stacks, which
compose much more nicely than effectful terms.
\begin{lemma}[Casts are EP Pairs]
+ \label{lem:casts-are-ep-pairs}
\begin{enumerate}
\item For any $A \ltdyn A'$, the casts $(x.\sem{\upcast{A}{A'}x},
\sem{\dncast{\u F A}{\u F A'}})$ are a value ep pair from
@@ -6257,14 +6273,16 @@ consider to be the type of whole programs.
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}
+\begin{lemma}[{Reduction is Deterministic}]
If $M \step M_1$ and $M \step M_2$, then $M_1 = M_2$.
\end{lemma}
-\begin{lemma}{Subject Reduction}
- If $\cdot \vdash M : \u F A$ and $M \step M'$ then $\cdot \vdash M'
- : \u F A$.
+
+\begin{lemma}[{Subject Reduction}]
+ If $\cdot \vdash M : \u F A$ and $M \step M'$ then
+ $\cdot \vdash M' : \u F A$.
\end{lemma}
-\begin{lemma}{Progress}
+
+\begin{lemma}[{Progress}]
If $\cdot \vdash M : \u F A$ then one of the following holds:
\begin{enumerate}
\item $M = \err$
@@ -6279,7 +6297,7 @@ of the program.
%
The standard progress-and-preservation properties allow us to define
an associated ``big-step'' semantics as follows.
-\begin{corollary}{Possible Results of Computation}
+\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$
@@ -6340,198 +6358,55 @@ And define a typing $C : (\Gamma \vdash \u B) \Rightarrow (\Gamma'
\end{longfigure}
Then contexts allow us to lift any relation on \emph{results} to
-relations on
-
-\begin{definition}[Observational Lifting]
+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 most famous application of this is to observational equivalence,
-which is the lifting of equality: $\ctxize=$.
+The contextual lifting $\ctxize\sim$ inherits much structure of the
+original relation $\sim$ as the following lemma shows.
%
-However, as shown in \cite{newahmed2018}, the graduality property is
-defined in terms of an observational \emph{approximation} that places
-$\err$ as the least element, and every other element as a maximal
-element.
+This justifies calling $\ctxize\sim$ a contextual preorder when $\sim$
+is a preorder (reflexive and transitive) and similarly a contextual
+equivalence when $\sim$ is an equivalence (preorder and symmetric).
%
-Note that this is \emph{not} the standard notion of observational
-approximation, which normally has .....TODO resume from here
-
-\subsection{Graduality Logical Relation}
-
-\begin{definition}{Observational Error Approximation}
- Define $\Gamma \vDash M_1 \ltctx M_2 \in \u B$ to hold when for any
- closing context $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash
- \u F (1 + 1))$ one of the following is true:
- \begin{enumerate}
- \item $C[M_1] \Downarrow \err$
- \item $C[M_1],C[M_2] \Uparrow$
- \item $C[M_1], C[M_2] \Downarrow \ret V$ where $V = \tru$ or $V =
- \fls$.
- \end{enumerate}
+\begin{definition}[Contextual Preorder, Equivalence]
+ If $\sim$ is reflexive, symmetric or transitive, then for each
+ typing, $\ctxize\sim$ is reflexive, symmetric or transitive as well,
+ respectively.
\end{definition}
+In the remainder of the paper we work only with relations that are at
+least preorders so we write $\apreorder$ rather than $\sim$
-\begin{theorem}{Observational Interpretation of CBPV Inequations}
- If $M_1 \ltdyn M_2$ is provable in CBPV, then $M_1 \ltctx M_2$. As
- an inference rule:
- \[ \inferrule{\Gamma \vdash M_1 \ltdyn M_2 : \u B}{\Gamma \vDash M_1 \ltctx M_2 \in \u B} \]
-\end{theorem}
-
-To prove this we will use a logical relations interpretation of CBPV,
-specifically a step-indexed biorthogonal family of relations.
-%
-We adapt the CBV relation from \cite{graduality-ep} to a biorthogonal
-relation for CBPV, and in the process simplify some of their work.
-%
-The main difficulty with applying standard logical relations
-techniques to our setting is that step-indexed logical relations are a
-natural framework for predicates that are defined \emph{up to
- divergence}, which is made finitary by defining the relation up to
-$n$ non-well-founded reduction steps on one side.
-%
-The most common example of such a relation is the divergence
-approximation relation on closed programs: $M_1 \preceq M_2$, which
-holds when one of the following holds:
-\begin{enumerate}
-\item $M_1 \Uparrow$
-\item $M_1, M_2 \Downarrow \err$
-\item $M_1, M_2 \Downarrow \ret \tru$
-\item $M_1, M_2 \Downarrow \ret \fls$
-\end{enumerate}
-
-We can then finitize this relation by defining for each $i \in
-\mathbb{N}$, $M_1 \mathrel{\preceq^i} M_2$ when one of the following
-holds:
-\begin{enumerate}
-\item $\exists M_1'$ such that $M_1 \stepsin{i} M_1'$
-\item There exists $j < i$ such that
- \begin{enumerate}
- \item $M_1 \stepsin{j} \err$ and $M_2 \Downarrow \err$
- \item $M_1 \stepsin{j} \ret \tru$ and $M_2 \Downarrow \ret \tru$
- \item $M_1 \stepsin{j} \ret \fls$ and $M_2 \Downarrow \ret \fls$
- \end{enumerate}
-\end{enumerate}
-Note the following curious aspects of this relation
-\begin{enumerate}
-\item $M_1 \preceq^0 M_2$ is always true.
-\item While we are ultimately only interested in the extensional
- ``final result'' of a computation, in the step-indexed relation, we
- consider an intensional, small-step, quantitative semantics of the
- language.
-\item The step-indexed relation is \emph{asymmetric} in how much it
- explores the computation of the two sides. A constructive proof of
- $M_1 \mathrel{\preceq^i} M_2$ will only inspect the first $i-1$
- computation steps of $M_1$, but may inspect arbitrarily many steps
- of $M_2$. A concrete consequence of this is that for any fixed
- $M_2$, if we know its termination behavior, then the predicate $M_1
- \mathrel{\preceq^i} M_2$ is decidable because we can just run $M_1$
- for $i-1$ steps. On the other hand, if $M_1 \stepsin{j< i} \ret
- \tru$, then the predicate $M_1 \mathrel{\preceq^i} M_2$ on $M_2$ is
- equivalent to the halting problem.
-\item In the limit, the relation is the same as the original: $M_1
- \preceq M_2$ if and only if for every $i \in \mathbb{N}$, $M_1
- \mathrel{\preceq^i} M_2$.
-\end{enumerate}
-
-The last point is especially crucial because it says we can prove
-theorems about the infinitary relation by working with all finitary
-approximations of it.
-%
-We compositionally construct relations on terms using the finitary
-relation, decrementing the step when working with a non-well-founded
-feature such as non-positive recursive types.
-%
-Since the relation is trivial at $0$, we define a well-founded
-relation.
-
-We would like to apply this process to the notion of observation used
-in the graduality theorem: that $\err$ is the least element and
-divergence is a maximal element.
-% TODO: talk more
-But there is an issue: step-indexed logical relations give us
-relations where \emph{divergence} is a least element, but we have a
-relation where divergence is a \emph{maximal} element.
-%
-However all is not lost because we can modify a standard trick.
-%
-Often step-indexed logical relations are used to prove contextual
-\emph{equivalence} results, but equivalence (which we write $\equiv$)
-is also a relation where $\diverge$ is not a least element.
+The most famous application of this is to observational equivalence,
+which is the lifting of equality: $\ctxize=$, and we will show that
+$\equidyn$ proofs in GTT imply observational equivalences.
%
-The workaround is to express equivalence as a \emph{conjunction} of
-two relations: one of which has divergence as a least element and the
-other of which has divergence as a \emph{greatest} element (which can
-also be defined using step-indexing by defining its opposite
-relation).
+However, as shown in \cite{newahmed2018}, the graduality property is
+defined in terms of an observational \emph{approximation} relation
+$\ltdyn$ that places $\err$ as the least element, and every other
+element as a maximal element.
%
-For equivalence these turn out to just be the domain ordering
-$\preceq$ and its opposite $\succeq$, so we only need to define one
-step-indexed relation.
+Note that this is \emph{not} the standard notion of observational
+approximation, which we write $\preceq$, makes $\diverge$ a least
+element and every other element a maximal element.
%
-However since the relation for graduality is not \emph{symmetric}, we
-will need \emph{two} relations: which we write as $\preceq\ltdyn$ and
-$\ltdyn\succeq$.
+To distinguish these, we call $\ltdyn$ \emph{error} approximation and
+$\preceq$ \emph{divergence} approximation.
%
-We summarize these orderings in figure \ref{fig:orders}.
-
-\begin{lemma}{Graduality Ordering as a Conjunction}
- Let $R_1,R_2$ be results. Then $R_1 \ltdyn R_2$ if and only if $R_1
- \mathrel{\preceq\ltdyn} R_2$ and $R_1 \mathrel{\ltdyn\succeq} R_2$.
-\end{lemma}
-\begin{proof}
- The forward implication is obvious. For the reverse we do a case
- analysis on $R_1$.
- \begin{enumerate}
- \item If $R_1 = \err$, then $\err \ltdyn R_2$
- \item If $R_1 = \ret V$ for boolean $V$, then since $R_1 \precltdyn
- R_2$, $R_2 = \ret V$.
- \item If $R_1 = \diverge$, then since $R_1 \ltdynsucc R_2$, $R_2 = \diverge$
- \end{enumerate}
-\end{proof}
-
-Given any preorder on results, we can define its extension to a
-\emph{contextual preorder} as follows:
-
-\begin{definition}{Contextual Preorder}
- For any preorder on results $\apreorder$, we can extend it to the
- contextual preorder on values, terms and stacks of any type as
- follows:
- \begin{enumerate}
- \item $\Gamma \vDash M_1 \ctxpreorder M_2 \in \u B$ when for every
- context $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash \u F
- 2)$, $\result(C[M_1]) \apreorder \result(C[M_2])$.
- \item $\Gamma \vDash V_1 \ctxpreorder V_2 \in A$ when for every
- context $C : (\Gamma \vdash A) \Rightarrow (\cdot \vdash \u F
- 2)$, $\result(C[V_1]) \apreorder \result(C[V_2])$.
- \item $\Gamma \pipe \u B \vDash S_1 \ctxpreorder S_2 \in \u B'$ when
- for every context $C : (\Gamma\pipe \u B \vdash \u B') \Rightarrow
- (\cdot \vdash \u F 2)$, $\result(C[S_1]) \apreorder
- \result(C[S_2])$.
- \end{enumerate}
-\end{definition}
-
-\begin{lemma}{Contextual Preorder is a Preorder}
- If $\apreorder$ is a preorder then at every type,
- $\ctxize{\apreorder}$ is a preorder.
-\end{lemma}
-
-The contextual preorder for the graduality ordering is our intended
-model of CBPV's ordering.
-%
-We use the following lemma to prove results about it.
-
-\begin{lemma}{Contextual Preorder Commutes with conjunction}
- $M_1 \ctxize{\ltdyn} M_2$ if and only if $M_1 \ctxize{\precltdyn}
- M_2$ and $M_1 \ctxize{\ltdynsucc} M_2$.
-\end{lemma}
+We present these graphically (with two more) in figure
+\ref{fig:result-orders}.
-So now we have reduced the problem of reasoning about our intended
-ordering $\ctxize{\ltdyn}$ to reasoning about two orderings
-$\ctxize{\precltdyn}$ and $\ctxize{\ltdynsucc}$ that are amenable to
-step-indexing techniques.
+The goal of this section is to prove
+\begin{small}
+\begin{mathpar}
+ \inferrule{\Gamma \pipe \Delta \vdash E \equidyn E' : T}{\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}\and
+ \inferrule{\Gamma \pipe \Delta \vdash E \ltdyn E' : T}{\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T}
+\end{mathpar}
+\end{small}
\begin{figure}
\begin{minipage}{0.45\textwidth}
@@ -6576,39 +6451,100 @@ step-indexing techniques.
& \err &
\end{tikzcd}
\end{minipage}
- \caption{Observation Orderings}
+ \caption{Result Orderings}
+ \label{fig:result-orders}
\end{figure}
-Note how we have moved from a setting where we only need to consider
-the big-step ``final result'', with a step-indexed relation, we
-consider a quantitative, small-step semantics.
+For our purposes, step-indexed logical relations are a proof technique
+for establishing theorems about the contextual lifting of certain
+preorders $\apreorder$ on results.
+%
+They work by reducing the \emph{infinitary} relation given by
+$\ctxize\apreorder$ with the set of all of its \emph{finitary
+ approximations} $\ix\apreorder i$ that ``time out'' after observing
+$i$ steps of evaluation.
+%
+When a time out occurs, the relation gives up and declares that the
+terms \emph{are} related.
+%
+This means that the original relation is only recoverable from the
+finite approximations if $\diverge$ is always related to another
+element: if the relation is a preorder, we require that $\diverge$ is
+a \emph{least} element.
+%
+We call such a preorder a \emph{divergence preorder}.
+\begin{definition}[Divergence Preorder]
+ A preorder on results $\apreorder$ is a divergence preorder if
+ $\diverge \apreorder R$ for all results $R$.
+\end{definition}
-\subsubsection{Step Indexing}
+But this presents a problem, because \emph{neither} of our intended
+relations ($=$ and $\ltdyn$) is a divergence preorder, rather in
+$\diverge$ have is a \emph{maximal} element.
+%
+However there is a standard ``trick'' for subverting this obstacle in
+the case of contextual equivalence (\cite{ahmedsomething}): we notice
+that we can define equivalence as the symmetrization of divergence
+approximation, i.e., $M \ctxize= N$ if and only if $M \ctxize\preceq
+N$ and $N \ctxize\preceq M$, and since $\preceq$ has $\diverge$ as
+a least element, we can use a step-indexed relation to prove it.
+%
+As shown in \cite{newahmed2018}, a similar trick works for error
+approximation, but since $\ltdyn$ is \emph{not} an equivalence
+relation, we decompose it rather into two \emph{different} orderings:
+error approximation up to divergence on the left $\preceq\ltdyn$ and
+error approximation up to divergence on the right $\ltdyn\succeq$,
+also shown in figure \ref{fig:result-orders}.
+%
+Note that $\preceq\ltdyn$ is a preorder, but not a poset because
+$\err, \diverge$ are order-equivalent but not equal.
+%
+Then clearly $\preceq\ltdyn$ is a divergence preorder and the
+\emph{opposite} of $\ltdyn\succeq$ is a divergence preorder.
+%
+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.
+\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$.
+ \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'$
+\end{lemma}
+
+\subsection{CBPV Step Indexed Logical Relation}
+Next, we turn to the problem of proving results of the form $E
+\ctxize\apreorder E'$ where $\apreorder$ is a divergence preorder.
+%
Dealing directly with a contextual preorder is practically impossible,
so instead we develop an alternative formulation as a logical relation
-that is much easier to use
-%
-Like the contextual preorder, a logical relation can be defined with
-respect to a quite general class of orderings on results, and we will
-develop a general correspondence theorem between logical and
-contextual preorders generated by a result preorder.
+that is much easier to use.
%
-The first step is to \emph{finitize} our result preorder.
+Fortunately, we can apply standard logical relations techniques to
+provide an alternate definition \emph{inductively} on types.
%
-For this to be sensible, we require that $\diverge$ is \emph{a} least
-element of the preorder, that is $\diverge \apreorder R$ for every
-$R$.
+However, since we have non-well founded type definitions using
+$\mu,\nu$, our logical relation will also be defined inductively on a
+\emph{step-index} that times out when we've exhausted our steps.
%
-Note that since we are working with preorders and not posets, there
-may be more than one least element in this sense (for example in the
-$\precltdyn$ relation both $\diverge$ and $\err$ are least elements).
+To bridge the gap between the indexed logical relation and the
+divergence preorder we care about, we define the ``finitization'' of a
+divergence preorder to be a relation between \emph{programs} and
+\emph{results}: the idea is that a program approximates a result $R$
+at index $i$ if it reduces to $R$ in less than $i$ steps or it reduces
+at least $i$ times.
\begin{definition}{Finitized Preorder}
- Given a preorder on results $\apreorder$ such that $\diverge$ is a
- least element, we define the \emph{finitization} of $\apreorder$ to
- be, for each natural number $i$, a relation between programs and
- results:
+ Given a divergence preorder $\apreorder$, we define the
+ \emph{finitization} of $\apreorder$ to be, for each natural number
+ $i$, a relation between programs and results:
\[ {\ix\apreorder i} \subseteq \{ M \pipe \cdot\vdash M : \u F 2\} \times \text{Results} \]
defined by
\[
@@ -6643,19 +6579,21 @@ logical relation.
preorder: $\result(M) \apreorder R \apreorder R'$.
\end{proof}
-Next, we show the relation is downward-closed
-
+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}
If $M \ix\apreorder i R$ and $j\leq i$ then $M \ix \apreorder j R$.
\end{lemma}
-\begin{proof}
+\begin{longproof}
\begin{enumerate}
\item If $M \bigstepsin{i} M_i$ then $M \bigstepsin{j} M_j$ and otherwise
\item If $M \bigstepsin{j \leq k i} \result(M)$ then $M \bigstepsin{j} M_j$
\item if $M \bigstepsin{k < j \leq i} \result(M)$ then $\result(M) \apreorder R$.
\end{enumerate}
-\end{proof}
+\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}
@@ -6667,33 +6605,89 @@ Next, we show the relation is downward-closed
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$
+ If $M \ix\apreorder i R$ and $N \bigstepsin{j} M$, then $N \ix\apreorder {{i+j}} R$
\end{lemma}
-\begin{proof}
+\begin{longproof}
\begin{enumerate}
\item If $M \bigstepsin{i} M'$ then $N \bigstepsin{i+j} M'$
- \item If $M \bigstepsin{k < i} \result(M)$ then $N \bigstepsin{k+j < i+j}
- \result(M)$ and $\result(M) = \result(N)$.
+ \item If $M \bigstepsin{k < i} \result(M)$ then $N \bigstepsin{k+j}
+ \result(M)$ and $\result(M) = \result(N)$ and $k+j < i+j$.
\end{enumerate}
-\end{proof}
+\end{longproof}
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 $\itylrof
-\apreorder i A$ between closed values of type $A$ and for every
-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$.
+Specifically, for every $i$ and value type $A$ we define a relation
+$\itylrof \apreorder i A$ between closed values of type $A$ because
+these are the only ones that will be pattern matched against at
+runtime.
+%
+The relation is defined in a type-directed fashion, the intuition is
+that we relate two positive values when they are built up in the same
+way: i.e., they have the same introduction form and their subterms are
+related.
+%
+For $\mu$, this definition would not be well-founded, so we decrement
+the step index, giving up and relating the terms if $i = 0$.
%
-The definition is well-founded using the lexicographic ordering on
-$(i, A)$ and $(i, B)$: either the type reduces and the index stays the
-same or the index reduces.
+Finally $U$ is the only negative value type, and so it is treated
+differently.
%
-We extend the definition to contexts point-wise.
+A thunk $V : U\u B$ cannot be inspected by pattern matching, rather
+the only way to interact with it is to force its evaluation.
%
-%TODO: give more explanation about the cases, especially F, U and mu, nu.
+By the definition of the operational semantics, this only ever occurs
+in the step $S[\force V]$, so (ignoring indices for a moment), we
+should define $V_1 \apreorder V_2$ to hold in this case when, given
+$S_1 \apreorder S_2$, the result of $S_2[\force V_2]$ is approximated
+by $S_1[\force V_1]$.
+%
+To incorporate the indices, we have to quantify over $j \leq i$ in
+this definition because we need to know that the values are related in
+all futures, including ones where some other part of the term has been
+reduced (consuming some steps).
+%
+Technically, this is crucial for making sure the relation is
+downward-closed.
+%
+This is known as the \emph{orthogonal} of the relation, and one
+advantage of the CBPV language is that it makes the use of
+orthogonality \emph{explicit} in the type structure, analogous to the
+benefits of using Nakano's \emph{later} modality for step indexing
+(which we ironically do not do) \cite{nakano}.
+Next, we define when two \emph{stacks} are related.
+%
+First, we define the relation only for ``closed'' stacks, which are
+those that have the same type of their hole $\u B$ and whose
+``output'' type is the observation type $\u F 2$.
+%
+The reason is that in evaluating a program $M$, steps always occur as
+$S[N] \bigstepany S[N']$ where $S$ is a stack of this form.
+%
+An intuition is that for negative types, two stacks are related when
+they start with the same elimination form and the remainder of the
+stacks are related.
+%
+For $\nu$, we handle the step indices in the same way as for $\mu$.
+%
+For $\u F A$, a stack $S[\bullet : \u F A]$ is strict in its input and
+waits for its input to evaluate down to a value $\ret V$, so two
+stacks with $\u F A$ holes are related when in any future world, they
+produce related behavior when given related values.
+
+We note that in the CBV restriction of CBPV, the function type is
+given by $U(A \to \u F A')$ and the logical relation we have presented
+reconstructs the usual definition that involves a double orthogonal.
+
+Note that the definition is well-founded using the lexicographic
+ordering on $(i, A)$ and $(i, B)$: either the type reduces and the
+index stays the same or the index reduces.
+%
+We extend the definition to contexts to \emph{closing substitutions}
+pointwise: two closing substitutions for $\Gamma$ are related at $i$
+if they are related at $i$ for each $x:A \in \Gamma$.
\begin{figure}
\begin{mathpar}
@@ -6723,9 +6717,14 @@ We extend the definition to contexts point-wise.
\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.
+%
+The intuition is that while the contextual preorder defines
+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{definition}{Logical Preorder}
Given a preorder on results $\apreorder$ with $\diverge$ a least
element, we define the step-indexed logical preorder as follows:
@@ -6745,7 +6744,9 @@ Next, analogous to the contextual preorder, we define the
We next want to prove that the logical preorder is a congruence
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
@@ -6756,10 +6757,11 @@ relation, i.e., the fundamental lemma of the logical relation.
\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.,
- closed under the congruence rules of figure TODO.
+ preorder $E \ilrof\apreorder i E'$ is a congruence relation, i.e., that
+ it is closed under applying any value/term/stack constructors to
+ both sides.
\end{theorem}
-\begin{proof}
+\begin{longproof}
For each congruence rule
\[
\inferrule
@@ -6969,8 +6971,9 @@ relation, i.e., the fundamental lemma of the logical relation.
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}
+\end{longproof}
+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.\]
@@ -6979,78 +6982,73 @@ relation, i.e., the fundamental lemma of the logical relation.
As another corollary we have the following \emph{strengthening} of the
progress-and-preservation type soundness theorem because it only
counts unrolling steps.
+%
+This shows for instance that terms that never use $\mu$ or $\nu$ types
+are guaranteed to terminate.
\begin{corollary}{Unary LR}
- For every program $\cdot \vdash M : \u F 2$, \[ M \ix\apreorder i \result(M) \]
+ For every program $\cdot \vdash M : \u F 2$ and $i \in \mathbb{N}$,
+ \[ M \ix\apreorder i \result(M) \]
\end{corollary}
-\begin{proof}
+\begin{longproof}
By reflexivity, $\cdot \vDash M \ix\apreorder i M \in \u F 2$ and by
definition $\bullet \itylrof\apreorder i {\u F 2} \bullet$, so
unrolling definitions we get $M \ix\apreorder i \result(M)$.
-\end{proof}
+\end{longproof}
+
+Next, we can show that $\result(M)$ is the
Using the reflexivity proof, we can now prove that the indexed
relation between terms and results recovers the original preorder in
-the limit as $i \to \infty$.
-\begin{corollary}{In the limit, Finitized Preorder Recovers Original}
- For any preorder with divergence-least element $\apreorder$,
+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}]
+ \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$
\end{corollary}
-\begin{proof}
+\begin{longproof}
Two cases
\begin{enumerate}
\item If $\result(M) \apreorder R$ then we need to show for every $i
- \in \mathbb{N}$, $M \ix \apreorder i R$. First, by lemma above, $M
- \ix\apreorder i \result(M)$, so we do a case analysis
- \begin{enumerate}
- \item If $M \bigstepsin{i} M'$, then $M \ix\apreorder R$
- \item If $M \bigstepsin{j<i} R_M$, then $R_M = \result(M)$, so by
- assumption $R_M \apreorder R$.
- \end{enumerate}
+ \in \mathbb{N}$, $M \ix \apreorder i R$. By the unary model lemma,
+ $M \ix\apreorder i \result(M)$, so the result follows by the
+ module lemma \ref{lem:module}.
\item If $M \ix\apreorder i R$ for every $i$, then there are two
- possibilities: $M$ terminates or it doesn't:
+ possibilities: $M$ is always related to $R$ because it takes $i$
+ steps, or at some point $M$ terminates.
\begin{enumerate}
\item If $M \bigstepsin{i} M_i$ for every $i \in \mathbb{N}$, then
- $\result(M) = \diverge$ so by assumption that $\diverge$ is a
- least element, $\result(M) \apreorder R$
+ $\result(M) = \diverge$, so $\result(M) \apreorder R$ because
+ $\apreorder$ is a divergence preorder.
\item Otherwise there exists some $i \in \mathbb{M}$ such that $M
- \bigstepsin{i} \result(M)$ and $\result(M) \apreorder R$, in
- which case there is nothing to show.
+ \bigstepsin{i} \result(M)$, so it follows by the module lemma
+ \ref{lem:module}.
\end{enumerate}
\end{enumerate}
-\end{proof}
+\end{longproof}
-\begin{corollary}{LR is Sound wrt Contextual Preorder}
- If $\Gamma \vDash M \ilrof\apreorder \omega N \in \u B$
+\begin{corollary}[{LR is Sound wrt Contextual Preorder}]
+ If $\Gamma \vDash E \ilrof\apreorder \omega E' \in \u B$
then
- $\Gamma \vDash M \ctxize\apreorder N \in \u B$.
- TODO: value, stack cases
+ $\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 because the identity stack is related to itself
- we have
+ \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.
\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$
- then
- $\Gamma \vDash M \ctxize\ltdyn N \in \u B$.
- TODO: value, stack cases
-\end{corollary}
-\begin{proof}
- By the previous lemma, and the fact that conjunction of the two is
- equivalent to the graduality ordering.
-\end{proof}
-
In fact, we can prove the converse, that at least for the term case,
-our LR is \emph{complete} with respect to contextual graduality
-
-\begin{lemma}{Logical Preorder is Complete wrt Contextual Preorder}
+the logical preorder is \emph{complete} with respect to the contextual
+preorder.
+\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$.
\end{lemma}
@@ -7084,7 +7082,7 @@ our LR is \emph{complete} with respect to contextual graduality
\end{align*}
So $S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[N[\gamma_2]])$ by
- lemma (TODO: module)
+ the module lemma \ref{lem:module}.
\end{proof}
This establishes that our logical relation can prove graduality, so it
@@ -7097,8 +7095,11 @@ reflexivity.
The only remaining rules to validate are the transitivity rules, error
rules, substitution principles, and the $\beta$ and $\eta$
equivalences for each type constructor.
+%
+Other than the $\err \ltdyn M$ rule, all of these hold for any
+divergence preorder.
-With the reflexivity and limiting lemmas in hand, we can prove that
+With the unary model 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
@@ -7122,22 +7123,21 @@ limit is a consequence.
\[ 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
+ which by the limiting lemma \ref{lem:limit} 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
+ so then by the module lemma \ref{lem: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$.
+ First by reflexivity, we know $V_2 \itylr \omega A V_2$, so by assumption,
+ \[ S_2[\ret V_2] \ix\apreorder \omega \result(S_3[\ret V_2]) \]
+ Which by the limit lemma \ref{lem:limit} is equivalent to
+ \[ \result(S_2[\ret V_2]) \ix\apreorder \omega \result(S_3[\ret V_2]) \]
+ So by the module lemma \ref{lem:module}, it is sufficient to show
+ \[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2]) \]
+ which holds by assumption.
\end{enumerate}
\end{proof}
@@ -7162,12 +7162,13 @@ limit is a consequence.
\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
+ by reflxivity and assumption, we know
+ \[ S_2[M_2[\gamma_2]] \ix\apreorder \omega \result(S_2[M_3[\gamma_2]])\]
+ and by limit lemma \ref{lem:limit}, this is equivalent to
+ \[ \result(S_2[M_2[\gamma_2]]) \apreorder \result(S_2[M_3[\gamma_2]])\]
+ so by the module lemma \ref{lem: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]]) \]
+ which follows by assumption.
\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
@@ -7190,11 +7191,13 @@ limit is a consequence.
\end{enumerate}
\end{corollary}
+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$
laws are valid for $\ilrof\apreorder \omega$
\end{lemma}
-\begin{proof}
+\begin{longproof}
The $\beta$ rules for all cases except recursive types are direct
from anti-reduction.
\begin{enumerate}
@@ -7419,7 +7422,7 @@ limit is a consequence.
S_2$, but this is a contradiction.
\end{enumerate}
\end{enumerate}
-\end{proof}
+\end{longproof}
\begin{lemma}{Substitution Principles}
For any diverge-bottom preorder $\apreorder$, the following are
@@ -7431,7 +7434,7 @@ limit is a consequence.
\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}
+\begin{longproof}
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
@@ -7440,58 +7443,73 @@ limit is a consequence.
\[ 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}
+\end{longproof}
+
+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}
+\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 \]
+ \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$
- \[ \err \ilrof\precltdyn i M\]
- and
- \[ M \ilrof\precltdyn i \err\]
- and
- \[ \err \ilrof\ltdynsucc i M\]
- and
- \[ M \ilrof\ltdynsucc i \err\]
+ \begin{mathpar}
+ \err \ilrof\precltdyn i M\and
+ M \ilrof{\preceq\gtdyn} i \err
+ \end{mathpar}
\end{lemma}
-\begin{proof} All are trivial verifications. \end{proof}
-
-\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
+\begin{longproof}
\begin{enumerate}
- \item If $\Gamma \vdash M_1 \ltdyn M_2 : \u B$, then
- \[ \Gamma \vDash M_1 \ix\precltdyn \omega M_2 \in \u B \]
- and
- \[ \Gamma \vDash M_1 \ix\ltdynsucc \omega M_2 \in \u B \]
- \item If $\Gamma \vdash V_1 \ltdyn V_2 : A$, then
- \[ \Gamma \vDash V_1 \ix\precltdyn \omega V_2 \in A
- \]
- \[ \Gamma \vDash V_1 \ix\ltdynsucc \omega V_2 \in A
- \]
- \item If $\Gamma \pipe \bullet : \u B \vdash S_1 \ltdyn S_2 : \u C$ , then
- \[\Gamma \pipe \bullet : \u B \vDash S_1 \ix\precltdyn\omega S_2 \in \u C \]
- and
- \[\Gamma \pipe \bullet : \u B \vDash S_1 \ix\ltdynsucc\omega S_2 \in \u C \]
+ \item It is sufficient by the limit lemma to show $\result(S[\err])
+ \apreorder \err$ which holds by reflexivity because $S[\err]
+ \bigstepzero \err$.
+ \item We need to show $S[\err] \ix\precltdyn i R$ for arbitrary $R$,
+ so by the limit lemma it is sufficient to show $\err \precltdyn
+ R$, which is true by definition.
+ \item By the limit lemma it is sufficient to show $R
+ \mathrel{\preceq\gtdyn} \err$ which is true by definition.
\end{enumerate}
+\end{longproof}
+
+Finally, the lemmas we have shown cover all of the cases of the
+following theorem that says our logical relation is a model of CBPV.
+\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
+ If $\Gamma \pipe \Delta \vdash E \ltdyn E' : \u B$ then both of the
+ following hold:
+ \begin{mathpar}
+ \Gamma \pipe \Delta \vDash E \ix\precltdyn i E' \in \u B\and
+ \Gamma \pipe \Delta \vDash E' \ix\ltdynsucc i E \in \u B
+ \end{mathpar}
\end{lemma}
-\begin{theorem}{$\ctxize \ltdyn$ is a Model of CBPV}
- \begin{enumerate}
- \item If $\Gamma \vdash M_1 \ltdyn M_2 : \u B$, then
- \[ \Gamma \vDash M_1 \ctxize\ltdyn M_2 \in \u B \]
- \item If $\Gamma \vdash V_1 \ltdyn V_2 : A$, then
- \[ \Gamma \vDash V_1 \ctxize\ltdyn V_2 \in A \]
- \item If $\Gamma \pipe \bullet : \u B \vdash S_1 \ltdyn S_2 : \u C$, then
- \[\Gamma \pipe \bullet : \u B \vDash S_1 \ctxize\ltdyn S_2 \in \u C \]
- \end{enumerate}
+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$}
+ \[
+ \inferrule
+ {\Gamma \pipe \Delta \vdash E \ltdyn E' : T}
+ {\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T}
+ \]
\end{theorem}
-\begin{proof}
- TODO: prose
- Logical by prev lemma
- Logical => Contextual by soundness
- Contextual of the 2 => Contextual ltdyn by earlier lemma
-\end{proof}
+\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$}
+ \[
+ \inferrule
+ {\Gamma \pipe \Delta \vdash E \equidyn E' : T}
+ {\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}
+ \]
+\end{corollary}
\section{Discussion}