From f40838b6690f2d0fc3968d39de894d0025ef3edc Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 12 Jul 2018 12:40:19 +0100
Subject: [PATCH] edit the rest
---
paper/gtt.tex | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 7593b45..f49034c 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -7948,11 +7948,11 @@ The goal of this section is to prove that a symmetric equality $E \equidyn
E'$ in CBPV (i.e. $E \ltdyn E'$ and $E' \ltdyn E$) implies contextual
equivalence $E \ctxize= E'$ and that inequality in CBPV $E \ltdyn E'$
implies error approximation $E \ctxize\ltdyn E'$, which will give operational
-graduality:
+graduality\ifshort .\else :\fi
\begin{longonly}
\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 \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}
@@ -7998,8 +7998,7 @@ $\diverge$ as a \emph{maximal} element.
logical relation to characterize $\preceq$, and then obtain results
about observational equivalence from that~\cite{ahmed06:lr}.
A similar move works for error
- approximation~\cite{newahmed18}, but since $R \ltdyn R'$ is \emph{not} an equivalence
- relation on results, it is decomposed as the conjunction of two
+ approximation~\cite{newahmed18}, but since $R \ltdyn R'$ is \emph{not} symmetric, it is decomposed as the conjunction of two
orderings: error approximation up to divergence on the left
$\errordivergeleft$ (the preorder where $\err$ and $\diverge$ are both
minimal: $\err \preceq\ltdyn R$ and $\diverge \preceq\ltdyn R$) and
@@ -8167,7 +8166,7 @@ We use a logical relation to prove results about $E \ctxize\apreorder
E'$ where $\apreorder$ is a divergence preorder. The
``finitization'' of divergence preorder is a relation between
\emph{programs} and \emph{results}: a program approximates a result $R$
-at index $i$ if it reduces to $R$ in $\le i$ steps or it reduces at
+at index $i$ if it reduces to $R$ in $< i$ steps or it reduces at
least $i$ times.
\end{shortonly}
@@ -8203,7 +8202,7 @@ at least $i$ times.
\fi
defined by
\[
- M \ix \apreorder i R = (\exists M'.~ M \bigstepsin{i} M') \vee (\exists (j\leq i). \exists R_M.~ M \bigstepsin{j} R_M \wedge R_M \apreorder R)
+ M \ix \apreorder i R = (\exists M'.~ M \bigstepsin{i} M') \vee (\exists (j< i). \exists R_M.~ M \bigstepsin{j} R_M \wedge R_M \apreorder R)
\]
\end{definition}
--
GitLab