\[ z : U(\u B_1\with\u B_2) \vdash \force z \equidyn \pair{\pi\force z}{\pi'\force z}\]

which is exactly $\with\eta$

* $\nu\beta$ Immediate by simple $\nu\beta$

* $\nu\eta$ We need to show

\[ z : U(\nu \u Y. \u B) \vdash \force z \equidyn \roll\unroll z \]

which is exactly $\nu\eta$

* $\u F\beta$
We need to show

\[ \bindXtoYinZ {\simp V} x \simp M \equidyn \simp{M[V/x]}\]

which is exactly the compositionality lemma.

* $\u F\eta$ We need to show

\[ z : U(\u F A)\force z \vdash \bindXtoYinZ {\force z} x \bindXtoYinZ {\ret x} x \ret x \]

which follows by $\u F\beta,\u F\eta$

If $M, M'$ are terms in CBPV and $M \ltdyn M'$ is provable in
then $M \ltdyn M'$ is provable in CBPV.

Because de-complexification preserves dynamism, $\simp M \ltdyn
\simp{M'}$ in simple CBPV. Then it follows because
de-complexification is equivalent to identity (in CBPV):

\[ M \equidyn \simp M \ltdyn \simp {M'} \equidyn M' \]

§ OPERATIONAL MODEL OF GTT

In this section, we establish a model of our CBPV inequational theory
using a notion of observational approximation based on the CBPV
operational semantics.

By composition with the axiomatic graduality theorem, this establishes
the operational graduality theorem, i.e., a theorem analogous
to the dynamic gradual guarantee <cit.>.

§.§ Call-by-push-value operational semantics

We use a small-step operational semantics for CBPV
with the following rules (excerpt):

in figure

\[
\begin{array}{rcl}
S[\err] &\stepzero& \err\\
\iflong
S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] &\stepzero & S[M_1[V/x_1]]\\
S[\caseofXthenYelseZ{\inr V}{x_1. M_1}{x_2. M_2}] &\stepzero & S[M_2[V/x_2]]\\
\fi
S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M}] &\stepzero & S[M[V_1/x_1,V_2/x_2]]\\
S[\pmmuXtoYinZ{\rollty A V}{x}{M}] &\stepone & S[M[V/x]]\\
S[\force\thunk M] &\stepzero & S[M]\\
\iflong
S[\letXbeYinZ V x M] &\stepzero & S[M[V/x]]\\
\fi
S[\bindXtoYinZ {\ret V} x M] &\stepzero & S[M[V/x]]\\
S[(\lambda x:A. M)\,V] &\stepzero & S[M[V/x]]\\
\iflong
S[\pi \pair{M}{M'}] &\stepzero & S[M]\\
S[\pi' \pair{M}{M'}] &\stepzero & S[M']\\
\fi
S[\unroll \rollty{\u B} M] &\stepone & S[M]\\
\end{array}
\]

M 0 M

M_1 i M_2 M_2 j M_3
M_1 i+j M_3

CBPV Operational Semantics

This is morally the same as in <cit.>, but we present
stacks in a manner similar to Hieb-Felleisen style evaluation
contexts(rather than as an explicit stack machine with stack frames).

We also make the step relation count unrollings of a recursive or
corecursive type, for the step-indexed logical relation later.

The operational semantics is only defined for terms of type
$\cdot \vdash M : \u F (1+1)$, which we take as the type of whole

We can then observe the following standard operational properties. (We
write $M \step N$ with no index when the index is irrelevant.)

If $M \step M_1$ and $M \step M_2$, then $M_1 = M_2$.

If $\cdot \vdash M : \u F A$ and $M \step M'$ then
$\cdot \vdash M' : \u F A$.

If $\cdot \vdash M : \u F A$ then one of the following holds:

M = M = V with V:A ∃M'.  M M'

It is easy to see that the operational semantics is deterministic
and progress and type preservation theorems hold, which allows us to
define the “final result” of a computation as follows:

The standard progress-and-preservation properties allow us to define
the “final result” of a computation as follows:

For any $\cdot \vdash M : \u F 2$,

one of the following is true:

M ⇑M ⇓M ⇓M ⇓

either $M \Uparrow$ or $M \Downarrow \err$ or $M \Downarrow \ret
\tru$ or  $M \Downarrow \ret \fls$.

We define $M \Uparrow$ to hold when if $M \bigstepsin{i} N$ then
there exists $N'$ with $N \step N'$. For the terminating results, we
define $M \Downarrow R$ to hold if there exists some $i$ with $M
\bigstepsin{i} R$. Then we prove the result by coinduction on
execution traces. If $M \in \{ \err, \ret\tru, \ret\fls \}$ then we
are done, otherwise by progress, $M \step M'$, so we need only
observe that each of the cases above is preserved by $\step$.

The possible results of a computation are $ \diverge, \err,
\ret \tru$ and $\ret \fls$. We denote a result by $R$, and define a
function $\result$ which takes a program $\cdot \vdash M : \u F 2$,
and returns its end-behavior, i.e., $\result(M)= \diverge$ if $M
\Uparrow$ and otherwise $M \Downarrow \result(M)$.

§.§ Observational Equivalence and Approximation

Next, we define observational equivalence and approximation in CBPV.

The (standard) definition of observational equivalence is that we
consider two terms (or values) to be equivalent when replacing one
with the other in any program text produces the same overall resulting

Define a context $C$ to be a 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).  Using contexts, we can lift any relation on
results to relations on open terms, values and stacks.

Given any relation ${\sim} \subseteq \text{Result}^2$, we can define
its 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'])\]

C_V      ::= [·]     μX.AC_V |C_V |C_V |(C_V,V)|(V,C_V)|C_M

C_M     ::=     [·] |C_V x M |V x
C_M |C_V x M |V x C_M

|νY̆.B̆ C_M |C_M |C_V |C_V x_1. M_1x_2.M_2

|V x_1. C_Mx_2.M_2 |V x_1. M_1x_2.C_M |C_V M

|V C_M |C_V x y M|V x y C_M

|C_V |C_MxN
|MxC_M |λx:A.C_M |C_M V |M C_V

|C_MM_2|M_1C_M |πC_M |π' C_M

C_S    =    πC_S |π' C_S |S C_V|C_S V|C_S x M |S x C_M

CBPV Contexts

The contextual lifting $\ctxize\sim$ is a preorder or equivalence
relation whenever the original relation $\sim$ is, and all $\sim$'s we
use will be at least preorders, so we write $\apreorder$ instead of
$\sim$ for a relation on results.

The contextual lifting $\ctxize\sim$ inherits much structure of the
original relation $\sim$ as the following lemma shows.

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).

If $\sim$ is reflexive, symmetric or transitive, then for each
typing, $\ctxize\sim$ is reflexive, symmetric or transitive as well,

In the remainder of the paper we work only with relations that are at
least preorders so we write $\apreorder$ rather than $\sim$.

Three important relations arise as liftings: Equality of results lifts to observational equivalence
($\ctxize=$).  The preorder generated by $\err \ltdyn R$ (i.e. the other
three results are unrelated maximal elements) lifts to the notion of
error approximation used in <cit.> to prove the
graduality property ($\ctxize\ltdyn$).  The preorder generated by
$\diverge \preceq R$ lifts to the standard notion of divergence
approximation ($\ctxize\preceq$).

The most famous use of lifting is for observational equivalence,
which is the lifting of equality of results ($\ctxize=$), and we will show that
$\equidyn$ proofs in GTT imply observational equivalences.

However, as shown in <cit.>, the graduality property is
defined in terms of an observational approximation relation
$\ltdyn$ that places $\err$ as the least element, and every other
element as a maximal element.

Note that this is not the standard notion of observational
approximation, which we write $\preceq$, which makes $\diverge$ a least
element and every other element a maximal element.

To distinguish these, we call $\ltdyn$ error approximation and
$\preceq$ divergence approximation.

We present these graphically (with two more) in Figure

Diverge Approx. $\preceq$

[rd, no head]     [d, no head]     [ld, no head]

Error Approx. $\ltdyn$

[rd, no head]     [d, no head]     [ld, no head]

Error Approx. up to left-divergence

[rd, no head]          [ld, no head]

Error Approx. up to right-divergence

[ld, no head] [rd, no head]

[rd, no head]          [ld, no head]

Error Approx. up to right-divergence Op

[ld, no head] [rd, no head]

[rd, no head]          [ld, no head]

Result Orderings

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'$, proving graduality of the operational model.:

ΓΔ⊢E E' : TΓΔE = E' ∈TΓΔ⊢E E' : TΓΔE E' ∈T

Because we have non-well-founded $\mu/\nu$ types, we use a
step-indexed logical relation to prove properties about the
contextual lifting of certain preorders $\apreorder$ on results.

In step-indexing, the infinitary relation given by
$\ctxize\apreorder$ is related to the set of all of its finitary
approximations $\ix\apreorder i$, which “time out” after observing
$i$ steps of evaluation and declare that the
terms are related.

A preorder $\apreorder$ is only recoverable from its finite
approximations if $\diverge$ is a least element, $\diverge
\apreorder R$, because a diverging term will cause a time out for
any finite index. We call a preorder with $\diverge \apreorder R$ a
divergence preorder.

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 least element.

We call such a preorder a divergence preorder.

A preorder on results $\apreorder$ is a divergence preorder if
$\diverge \apreorder R$ for all results $R$.

But this presents a problem, because neither of our intended
relations ($=$ and $\ltdyn$) is a divergence preorder; rather both have
$\diverge$ as a maximal element.

For observational equivalence, because contextual equivalence is
symmetric divergence approximation ($M \ctxize= N$ iff $M
\ctxize\preceq N$ and $N \ctxize\preceq M$), we can use a step-indexed
logical relation to characterize $\preceq$, and then obtain results
about observational equivalence from that <cit.>.
A similar move works for error
approximation <cit.>, but since $R \ltdyn R'$ is 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
error approximation up to divergence on the right $\errordivergeright$
(the diamond preorder where $\err$ is minimal and $\diverge$ is
maximal, with $\tru$/$\fls$ in between).  Then $\preceq\ltdyn$ and the
opposite of $\ltdyn\succeq$ (written $\errordivergerightop$)
are divergence preorders, so we can use a step-indexed logical
relation to characterize them.  Overall, because $=$ is symmetric
$\ltdyn$, and $\ltdyn$ is the conjunction of $\errordivergeleft$ and
$\errordivergeright$, and contextual lifting commutes with conjunction
and opposites, it will suffice to develop logical relations for
divergence preorders.

However, there is a standard “trick” for subverting this obstacle in
the case of contextual equivalence <cit.>: 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 <cit.>, a similar trick works for error
approximation, but since $\ltdyn$ is not an equivalence
relation, we decompose it rather into two different orderings:
error approximation up to divergence on the left $\errordivergeleft$ and
error approximation up to divergence on the right $\errordivergeright$,
also shown in figure <ref>.

Note that $\errordivergeleft$ is a preorder, but not a poset because
$\err, \diverge$ are order-equivalent but not equal.

Then clearly $\errordivergeleft$ is a divergence preorder and the
opposite of $\errordivergeright$, written $\errordivergerightop$
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 observations.

Let $R, S$ be results.

* $R = S$ if and only if $R \ltdyn S$ and $S \ltdyn R$.

* $R = S$ if and only if $R \preceq S$ and $S \preceq R$.

* $R \errordivergeleft S$ iff $R \ltdyn S$ or $R \preceq S$.

* $R \errordivergeright S$ iff $R \ltdyn S$ or $R \succeq S$.

In the following, we write $\sim^\circ$ for the opposite of a relation
($x \sim^\circ y$ iff $y \sim x$), $\Rightarrow$ for
containment/implication ($\sim \Rightarrow \sim'$ iff $x \sim y$ implies
$x \sim' y$), $\Leftrightarrow$ for bicontainment/equality, $\vee$ for
union ($x (\sim \vee \sim') y$ iff $x \sim y$ or $x \sim' y$), and
$\wedge$ for intersection ($x (\sim \wedge \sim') y$ iff $x \sim y$ and $x \sim' y$).

\[
\ctxize{(\simsub 1 \wedge \simsub 2)} \Leftrightarrow \ctxize{\simsub 1} \wedge \ctxize{\simsub 2}
\]

\[
\ctxize{\sim^\circ} \Leftrightarrow \ctxize{\sim}^\circ
\]

Let $\sim$ be a reflexive relation $(= \Rightarrow \sim)$, and $\leqslant$
be a reflexive, antisymmetric relation (${=} \Rightarrow {\leqslant}$ and
$(\leqslant \wedge {\leqslant^\circ}) \Leftrightarrow {=}$).  Then

\[
\ctxize\sim \Leftrightarrow \ctxize{(\sim \vee \leqslant)} \wedge (\ctxize{(\sim^\circ \vee \leqslant)})^\circ
\]

Note that despite the notation, $\leqslant$ need not be assumed to be
Reflexive relations form a lattice with $\wedge$ and $\vee$ with $=$ as
$\bot$ and the total relation as $\top$ (e.g. $(= \vee \sim)
\Leftrightarrow \sim$ because $\sim$ is reflexive, and $(= \wedge \sim)
\Leftrightarrow =$).  So we have

\[
\sim \Leftrightarrow (\sim \vee \leqslant) \wedge (\sim \vee \leqslant^\circ)
\]

because FOILing the right-hand side gives

\[
(\sim \wedge \sim) \vee (\leqslant \wedge \sim) \vee (\sim \wedge \leqslant^\circ) \vee (\leqslant \wedge \leqslant^\circ)
\]

By antisymmetry, $(\leqslant \wedge \leqslant^\circ)$ is $=$, which is the
unit of $\vee$, so it cancels.  By idempotence, $(\sim \wedge \sim)$ is $\sim$.
Then by absorption, the whole thing is $\sim$.

Opposite is not de Morgan: $(P \vee Q)^\circ = P^\circ \vee
Q^\circ$, and similarly for $\wedge$.  But it is involutive:
$(P^\circ)^\circ \Leftrightarrow P$.

So using Lemmas <ref>, <ref> we can calculate as follows:

\[
\begin{array}{rcl}
\ctxize\sim & \Leftrightarrow &\ctxize{((\sim \vee \leqslant) \wedge (\sim \vee \leqslant^\circ))} \\
& \Leftrightarrow &\ctxize{(\sim \vee \leqslant)} \wedge \ctxize{(\sim \vee \leqslant^\circ)}\\
& \Leftrightarrow &\ctxize{(\sim \vee \leqslant)} \wedge \ctxize{((\sim \vee \leqslant^\circ)^\circ)^\circ}\\
& \Leftrightarrow &\ctxize{(\sim \vee \leqslant)} \wedge \ctxize{((\sim^\circ \vee (\leqslant^\circ)^\circ)^\circ)}\\
& \Leftrightarrow &\ctxize{(\sim \vee \leqslant)} \wedge \ctxize{(\sim^\circ \vee \leqslant)^\circ}\\
& \Leftrightarrow &\ctxize{(\sim \vee \leqslant)} \wedge \ctxize{(\sim^\circ \vee \leqslant)}^\circ
\end{array}
\]

As a corollary, the decomposition of contextual equivalence into diverge
approximation in <cit.> and the decomposition of dynamism in
<cit.> are really the same trick:

* $\ctxize= \mathbin{\Leftrightarrow} \ctxize{\preceq} \wedge

* $\ctxize= \mathbin{\Leftrightarrow} \ctxize{\ltdyn} \wedge (\ctxize{(\ltdyn)})^\circ$

* $\ctxize\ltdyn \mathbin{\Leftrightarrow} \ctxize{\errordivergeleft} \wedge (\ctxize{(\errordivergerightop)})^\circ$

For part 1 (though we will not use this below), applying
Lemma <ref> with $\sim$ taken to be $=$
(which is reflexive) and $\leqslant$ taken to be $\preceq$ (which is
reflexive and antisymmetric) gives that contextual equivalence is
symmetric contextual divergence approximation:

\[
\ctxize= \Leftrightarrow \ctxize{(= \vee \preceq)} \wedge (\ctxize{(=^\circ \vee \preceq)})^\circ
\Leftrightarrow \ctxize{\preceq} \wedge (\ctxize{(\preceq)})^\circ
\]

For part (2), the same argument with $\sim$ taken to be $=$ and
$\leqslant$ taken to be $\ltdyn$ (which is also antisymmetric) gives that
contextual equivalence is symmetric contextual dynamism:

\[
\ctxize= \Leftrightarrow \ctxize{\ltdyn} \wedge (\ctxize{(\ltdyn)})^\circ
\]

For part (3), applying Lemma <ref> with $\sim$
taken to be $\ltdyn$ and $\leqslant$ taken to be $\preceq$ gives that
dynamism decomposes as

\[
\ctxize\ltdyn \Leftrightarrow \ctxize{(\ltdyn \vee \preceq)} \wedge (\ctxize{(\ltdyn^\circ \vee \preceq)})^\circ
\Leftrightarrow \ctxize{\errordivergeleft} \wedge (\ctxize{(\errordivergerightop)})^\circ
\]

Since both ${\errordivergeleft}$ and $\errordivergerightop$ are of the
form $- \vee \preceq$, both are divergence preorders.  Thus, it suffices
to develop logical relations for divergence preorders below.

§.§ CBPV Step Indexed Logical Relation

We use a logical relation to prove results about $E \ctxize\apreorder
E'$ where $\apreorder$ is a divergence preorder.  The
“finitization” of a divergence preorder is a relation between
programs and results: a program approximates a result $R$
at index $i$ if it reduces to $R$ in $< i$ steps or it “times out” by reducing at least $i$ times.

Next, we turn to the problem of proving results about $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.

Fortunately, we can apply standard logical relations techniques to
provide an alternate definition inductively on types.

However, since we have non-well-founded type definitions using
$\mu$ and $\nu$, our logical relation will also be defined inductively on a
step index that times out when we've exhausted our step budget.

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 programs and
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.

Given a divergence preorder $\apreorder$, we define the
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

\[
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)
\]

Note that in this definition, unlike in the definition of divergence,
we only count non-well-founded steps.

This makes it slightly harder to establish the intended equivalence $M
\ix \apreorder \omega R$ if and only if $\result(M) \apreorder R$, but
makes the logical relation theorem stronger: it proves that diverging
terms must use recursive types of some sort and so any term that does
not use them terminates.

This issue would be alleviated if we had proved type safety by a
logical relation rather than by progress and preservation.

However, the following properties of the indexed relation can easily
be established.

First, a kind of “transitivity” of the indexed relation with respect
to the original preorder, which is key to proving transitivity of the
logical relation.

If $M \ix\apreorder i R$ and $R \apreorder R'$ then $M \ix\apreorder i R'$

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'$.

Then we establish a few basic properties of the finitized preorder.

If $M \ix\apreorder i R$ and $j\leq i$ then $M \ix \apreorder j R$.

* If $M \bigstepsin{i} M_i$ then $M \bigstepsin{j} M_j$ and otherwise

* If $M \bigstepsin{j \leq k i} \result(M)$ then $M \bigstepsin{j} M_j$

* if $M \bigstepsin{k < j \leq i} \result(M)$ then $\result(M) \apreorder R$.

For any $\cdot \vdash M : \u F 2$, $M \ix\apreorder 0 R$

Because $M \bigstepsin{0} M$

If $M \bigstepsin{i} N$ then $\result(M) = \result(N)$.

If $M \ix\apreorder i R$ and $N \bigstepsin{j} M$, then $N \ix\apreorder {{i+j}} R$

* If $M \bigstepsin{i} M'$ then $N \bigstepsin{i+j} M'$

* If $M \bigstepsin{k < i} \result(M)$ then $N \bigstepsin{k+j}
\result(M)$ and $\result(M) = \result(N)$ and $k+j < i+j$.

iA ⊆{ ·⊢V : A }^2
iB̆⊆{ ·B̆ ⊢S
: F̆ (1 + 1) }^2

·i · ·   =    ⊤

γ_1,V_1/x i Γ,x:A γ_2,V_2/x    =    γ_1 i Γγ_2 ∧V_1 i A V_2

V_1 i 0 V_2    =

V_1 i A + A' V_2    =     V_1 i A V_2

V_1 i A + A' V_2    =     V_1 i A' V_2

() i 1 ()    =    ⊤

(V_1,V_1') i A ×A' (V_2, V_2')    =    V_1 i A V_2 ∧V_1' i A' V_2'

μX. A V_1 i μX. A μX. A V_2    =    i = 0 ∨V_1 i-1 A[μX.A/X] V_2

V_1 i U B̆ V_2    =    ∀j ≤i, S_1 j B̆ S_2.  S_1[V_1] j (S_2[V_2])

S_1[∙V_1] i A →B̆ S_1[∙V_2]     =     V_1 i A V_2 ∧S_1 iB̆ S_2

S_1[π_1 ∙] i B̆ B̆' S_2[π_1 ∙]    =    S_1 i B̆ S_2

S_1[π_2 ∙] i B̆ B̆' S_2[π_2 ∙]    =    S_1 i B̆' S_2

S_1 i ⊤ S_2    =

S_1[∙] i νY̆. B̆ S_2[∙]    =    i = 0 ∨S_1 i-1 B̆[νY̆. B̆/Y̆] S_2

S_1 i F̆ A S_2     =     ∀j≤i, V_1 j A V_2.  S_1[V_1] j (S_2[V_2])

Logical Relation from a Preorder $\apreorder$ (selected cases)

The (closed) logical preorder (for closed values/stacks) is in Figure
<ref>.  For every $i$ and value type $A$, we define a relation
$\itylrof \apreorder i A$ between two closed values of type $A$, and for
every $i$ and $\u B$, we define a relation for two “closed” stacks $\u
B \vdash \u F 2$ outputting the observation type $\u F 2$—the
definition is by mutual lexicographic induction on $i$ and $A/\u B$.
Two values or stacks are related if they have the same structure, where
for $\mu,\nu$ we decrement $i$ and succeed if $i = 0$.  The shifts $\u
F/U$ take the orthogonal of the relation: the set of all
stacks/values that when composed with those values/stacks are related by
$\apreorder^{j \le i}$; the quantifier over $j \leq i$ is needed to make the
relation downward closed.

Next, we define the (closed) logical preorder (for closed values/stacks) by induction on types and
the index $i$ in figure <ref>.

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

The relation is defined in a type-directed fashion, the intuition being
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

For $\mu$, this definition would not be well-founded, so we decrement
the step index, giving up and relating the terms if $i = 0$.

Finally $U$ is the only negative value type, and so it is treated

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.

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

This is known as the orthogonal of the relation, and one
advantage of the CBPV language is that it makes the use of
orthogonality explicit in the type structure, analogous to the
benefits of using Nakano's later modality <cit.> for step indexing
(which we ironically do not do).

Next, we define when two stacks are related.

First, we define the relation only for two “closed” stacks, which
both have the same type of their hole $\u B$ and both have
“output” 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, \u B)$: either the type reduces and the
index stays the same or the index reduces.

We extend the definition to contexts to closing substitutions
pointwise: two closing substitutions for $\Gamma$ are related at $i$
if they are related at $i$ for each $x:A \in \Gamma$.

The logical preorder for open terms is defined as usual by quantifying
over all related closing substitutions, but also over all stacks to the
observation type $\u F (1+1)$:

For a divergence preorder $\apreorder$, its step-indexed logical
preorder is

for terms (open stack, value cases are defined in the extended version):
$\Gamma \vDash M_1 \ilrof\apreorder{i} M_2 \in \u B$ iff 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]])$.

* $\Gamma \vDash M_1 \ilrof\apreorder{i} M_2 \in \u B$ iff 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]])$.

* $\Gamma \vDash V_1 \ilrof\apreorder{i} V_2 \in A$ iff
for every $\gamma_1 \itylrof\apreorder i {\Gamma} \gamma_2$, $V_1[\gamma_1] \itylrof\apreorder i A V_2[\gamma_2]$

* $\Gamma \pipe \u B \vDash S_1 \ilrof\apreorder{i} S_2 \in \u B'$
iff 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]])$.

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.

For any type $T$, if $j \leq i$ then $\itylrof\apreorder i T
\subseteq \itylrof\apreorder j T$

Next, we show the fundamental theorem:

For any divergence preorder, 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 both sides.

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}
\]

* $\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)$.

* $\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$.

* $\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$

* $\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.

* $\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.

* $\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.

* $\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]$.

* 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.

* For $\inr{}$, the same argument.

* $\inferrule
{\Gamma \vDash () \ilr i () \in 1}$ Immediate by unit rule.

* $\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.

* $\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.

* $\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.

* $\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.

* $\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.

* $\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]$.

* $\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$.

* $\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'$.

* $\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'$.

* $\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'$.

* $\inferrule{}{\Gamma \vdash \{\} : \top}$ We assume we are
given $S_1 \itylr i {\top} S_2$, but this is a contradiction.

* $\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 analysis of $S_1 \itylr i {\u B_1 \with \u B_2} S_2$

* 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'$.

* Same as previous case.

* $\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'$.

* $\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.

* $\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.

* $\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']),\]
follows because $S_1[\unroll \bullet] \itylr i {\nu \u Y. \u B}
S_2[\unroll \bullet]$ and $M \ilr i M'$.

As a direct consequence we get the reflexivity of the relation

For any $\Gamma \vdash M : \u B$, and $i \in \mathbb{N}$,
\(\Gamma \vDash M \ilrof\apreorder i  M \in \u B.\)

This in particular implies that the relation is reflexive ($\Gamma
\vDash M \ilrof\apreorder i M \in \u B$ for all well-typed $M$),

so we
have the following strengthening of the progress-and-preservation
type soundness theorem: because $\ix\apreorder i$ only counts unrolling
steps, terms that never use $\mu$ or $\nu$ types (for example) are
guaranteed to terminate.

For every program $\cdot \vdash M : \u F 2$ and $i \in \mathbb{N}$,
$M \ix\apreorder i \result(M)$

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)$.

Using reflexivity, we prove that the indexed relation between terms and
results recovers the original preorder in the limit as $i \to \omega$.

We write $\ix\apreorder \omega$ to mean the relation holds for every
$i$, i.e., $\ix\apreorder\omega =
\bigcap_{i\in\mathbb{N}} \ix\apreorder i$.

For any divergence preorder $\apreorder$, \( \result(M) \apreorder
R\) iff \( M \ix\apreorder \omega R \).

Two cases

* If $\result(M) \apreorder R$ then we need to show for every $i
\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>.

* If $M \ix\apreorder i R$ for every $i$, then there are two
possibilities: $M$ is always related to $R$ because it takes $i$
steps, or at some point $M$ terminates.

* If $M \bigstepsin{i} M_i$ for every $i \in \mathbb{N}$, then
$\result(M) = \diverge$, so $\result(M) \apreorder R$ because
$\apreorder$ is a divergence preorder.

* Otherwise there exists some $i \in \mathbb{M}$ such that $M
\bigstepsin{i} \result(M)$, so it follows by the module lemma

If $\Gamma \vDash E \ilrof\apreorder \omega E' \in \u B$
$\Gamma \vDash E \ctxize\apreorder E' \in \u B$.

Let $C$ be a closing context. By congruence, $C[M] \ilrof\apreorder
\omega C[N]$, so using empty environment and stack, $C[M]
\ix\apreorder\omega \result(C[N])$ and by the limit lemma, we have
$\result(C[M]) \apreorder \result(C[N])$.

In fact, we can prove the converse, that at least for the term case,
the logical preorder is complete with respect to the contextual
preorder, though we don't use it.

For any $\apreorder$, if $\Gamma \vDash M \ctxize \apreorder N \in
\u B$, then $\Gamma \vDash M \ilrof\apreorder \omega N \in \u B$.

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]])
\]

So we need to construct a 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$}\\
&\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
the module lemma <ref>.

This establishes that our logical relation can prove graduality, so it
only remains to show that our inequational theory implies our
logical relation.

Having already validated the congruence rules and reflexivity, we
validate the remaining rules of transitivity, error, substitution, and
$\beta\eta$ for each type constructor.

Other than the $\err \ltdyn M$ rule, all of these hold for any
divergence preorder.

For transitivity, 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
limit is a consequence.

* If $V_1 \itylr i A V_2$ and $V_2 \itylr
\omega A V_3$, then $V_1 \itylr i A V_3$, and analogously
for stacks.
* If $S_1 \itylr i {\u B} S_2$ and $S_2 \itylr
\omega {\u B} S_3$, then $S_1 \itylr i {\u B} S_3$

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$.

* If $V_1 \itylr i {U \u B} V_2$ and $V_2
\itylr \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 the limiting lemma <ref> is equivalent to

\[ \result(S_2[\force V_2]) \apreorder \result(S_2[\force V_3]) \]

so then by the module lemma <ref>, it is sufficient to show

\[ S_1[\force V_1] \ix\apreorder j \result(S_2[\force V_2]) \]

which holds by assumption.

* 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 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> is equivalent to

\[ \result(S_2[\ret V_2]) \ix\apreorder \omega \result(S_3[\ret V_2]) \]

So by the module lemma <ref>, it is sufficient to show

\[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2]) \]

which holds by assumption.

* If $\gamma_1 \itylr i \Gamma \gamma_2$ and $\gamma_2 \itylr
\omega \Gamma \gamma_3$, then $\gamma_1 \itylr i \Gamma \gamma_3$

* If $\Gamma \vDash M_1 \ilr i M_2 \in \u B$ and
$\Gamma \vDash M_2 \ilr \omega M_3 \in \u B$, then
$\Gamma \vDash M_1 \ilr i M_3 \in \u B$.

* If $\Gamma \vDash V_1 \ilr i V_2 \in A$ and
$\Gamma \vDash V_2 \ilr \omega V_3 \in A$, then
$\Gamma \vDash V_1 \ilr i V_3 \in A$.

* If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilr i S_2 \in \u B'$ and
$\Gamma\pipe \bullet : \u B \vDash S_2 \ilr \omega S_3 \in \u B'$, then
$\Gamma\pipe \bullet : \u B \vDash S_1 \ilr i S_3 \in \u B'$.

* By induction on the length of the context, follows from closed value case.

* 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 reflexivity 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>, 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> 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.

* 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.

* Stack case is essentially the same as the value case.

$\ilrof\apreorder \omega$ is transitive.

* 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$.

* 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$.

* 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'$.

Next, we verify the $\beta, \eta$ equivalences hold as orderings each

For any divergence preorder, the $\beta, \eta$
laws are valid for $\ilrof\apreorder \omega$

The $\beta$ rules for all cases except recursive types are direct
from anti-reduction.

* $\mu X.A-\beta$:

* 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 to $S_1[M[\gamma_1,V[\gamma_1]/x]]$ and we know

\[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result (S_2[M[\gamma_2,V[\gamma_2]/x]])  \]

by assumption and reflexivity, so by anti-reduction we have

\[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_1]} x M[\gamma_1]] \ilr {i+1} \result(S_2[M[\gamma_2,V[\gamma_2]/x]]) \]

so the result follows by downward-closure.

* For the other direction we need to show

\[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result(S_2[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_2]} x M[\gamma_2]]) \]

Since results are invariant under steps, this is the same as

\[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result(S_2[M[\gamma_2,V[\gamma_2/x]]]) \]

which follows by reflexivity and assumptions about the stacks
and substitutions.

* $\mu X.A-\eta$:

* 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)}} {y}  M[\rollty{\mu X.A}y/x][\gamma_1]] \ilr i \result(S_2[M[\gamma_2]]) \]

By assumption, $\gamma_1(x) \itylr i {\mu X.A} \gamma_2(x)$, so we know

\[ \gamma_1(x) = \rollty{\mu X.A} V_1 \]

\[ \gamma_2(x) = \rollty{\mu X.A} V_2 \]

so the left side takes a step:

\begin{align*}
S_1[\pmmuXtoYinZ {\roll {\gamma_1(x)}} {y}  M[\roll y/x][\gamma_1]]
&\bigstepsin{1} S_1[M[\roll y/x][\gamma_1][V_1/y]]\\
&= S_1[M[\roll V_1/x][\gamma_1]]\\
& = S_1[M[\gamma_1]]
\end{align*}

and by reflexivity and assumptions we know

\[ S_1[M[\gamma_1]] \ilr {i} \result(S_2[M[\gamma_2]]) \]

so by anti-reduction we know

\[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_1(x)}} {y}  M[\rollty{\mu X.A}y/x][\gamma_1]] \ilr {i+1} \result(S_2[M[\gamma_2]]) \]

so the result follows by downward closure.

* Similarly, to show

\[ S_1[M[\gamma_1]] \ilr i \result(S_2[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_2(x)}} {y}  M[\rollty{\mu X.A}y/x][\gamma_2]]) \]

by the same reasoning as above, $\gamma_2(x) = \rollty{\mu X.A}V_2$, so because result is invariant under reduction we need to show

\[ S_1[M[\gamma_1]] \ilr i \result(S_2[M[\gamma_2]]) \]

which follows by assumption and reflexivity.

* $\nu \u Y. \u B-\beta$

* We need to show

\[ S_1[\unroll \rollty{\nu \u Y. \u B} M[\gamma_1]] \ix\apreorder i
\result(S_2[M[\gamma_2]]) \]

By the operational semantics,

\[ S_1[\unroll \rollty{\nu \u Y. \u B} M[\gamma_1]] \bigstepsin{1} S_1[M[\gamma_1]] \]

and by reflexivity and assumptions

\[ S_1[M[\gamma_1]] \ix\apreorder {i} S_2[M[\gamma_2]] \]

so the result follows by anti-reduction and downward closure.

* We need to show

\[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[\unroll \rollty{\nu \u Y. \u B} M[\gamma_2]]) \]

By the operational semantics and invariance of result under reduction this is equivalent to

\[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]

which follows by assumption.

* $\nu \u Y. \u B-\eta$

* We need to show

\[ S_1[\roll \unroll M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]

by assumption, $S_1 \itylr i {\nu \u Y.\u B} S_2$, so

\[ S_1 = S_1'[\unroll \bullet] \]

and therefore the left side reduces:

\begin{align*}
S_1[\roll \unroll M[\gamma_1]]
&= S_1'[\unroll\roll\unroll M[\gamma_1]]\\
&\bigstepsin{1} S_1'[\unroll M[\gamma_1]]\\
&= S_1[M[\gamma_1]]
\end{align*}

and by assumption and reflexivity,

\[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]

so the result holds by anti-reduction and downward-closure.

* Similarly, we need to show

\[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[\roll\unroll M[\gamma_2]])\]

as above, $S_1 \itylr i {\nu \u Y.\u B} S_2$, so we know

\[ S_2 = S_2'[\unroll\bullet] \]

\[ \result(S_2[\roll\unroll M[\gamma_2]]) = \result(S_2[M[\gamma_2]])\]

and the result follows by reflexivity, anti-reduction and downward closure.

* $0\eta$ Let $\Gamma, x : 0 \vdash M : \u B$.

* We need to show

\[ S_1[\absurd \gamma_1(x)] \ix\apreorder i \result(S_2[M[\gamma_2]])\]

By assumption $\gamma_1(x) \itylr i 0 \gamma_2(x)$ but this is a contradiction

* Other direction is the same contradiction.

* $+\eta$. Let $\Gamma , x:A_1 + A_2 \vdash M : \u B$

* We need to show

\[ S_1[\caseofXthenYelseZ {\gamma_1(x)} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]
\ix\apreorder i \result(S_2[M[\gamma_2]]) \]
by assumption
$\gamma_1(x) \itylr i {A_1 + A_2} \gamma_2(x)$, so either it's
an $\inl$ or $inr$. The cases are symmetric so assume
$\gamma_1(x) = \inl V_1$.

\begin{align*}
S_1[\caseofXthenYelseZ {\gamma_1(x)} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]\\
=S_1[\caseofXthenYelseZ {(\inl V_1)} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]\\
\bigstepsin{0} S_1[M[\inl V_1/x][\gamma_1]]\\
= S_1[M[\gamma_1]]
\end{align*}

and so by anti-reduction it is sufficient to show

\[ S_1[M[\gamma_1]] \ix\apreorder i S_2[M[\gamma_2]]\]

which follows by reflexivity and assumptions.

* Similarly, We need to show

\[
\result(S_1[M[\gamma_1]])
\ix\apreorder i
\result(S_2[\caseofXthenYelseZ {\gamma_2(x)} {x_1. M[\inl x_1/x][\gamma_2]}{x_2. M[\inr x_2/x][\gamma_2]}])
\]

and by assumption $\gamma_1(x) \itylr i {A_1 + A_2}
\gamma_2(x)$, so either it's an $\inl$ or $inr$. The cases are
symmetric so assume $\gamma_2(x) = \inl V_2$.

\[ S_2[\caseofXthenYelseZ {\gamma_2(x)} {x_1. M[\inl x_1/x][\gamma_2]}{x_2. M[\inr x_2/x][\gamma_2]}] \bigstepsin{0}
\]

So the result holds by invariance of result under reduction,
reflexivity and assumptions.

* $1\eta$ Let $\Gamma, x : 1 \vdash M : \u B$

* We need to show

\[ S_1[M[()/x][\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]])\]

By assumption $\gamma_1(x) \itylr i 1 \gamma_2(x)$ so $\gamma_1(x) = ()$, so this is equivalent to

\[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]])\]

which follows by reflexivity, assumption.

* Opposite case is similar.

* $\times\eta$ Let $\Gamma, x : A_1\times A_2 \vdash M : \u B$

* We need to show

\[ S_1[\pmpairWtoXYinZ x {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]

By assumption $\gamma_1(x) \itylr i {A_1\times A_2} \gamma_2(x)$, so $\gamma_1(x) = (V_1,V_2)$, so

\begin{align*}
S_1[\pmpairWtoXYinZ x {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]]
&= S_1[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]]\\
&\bigstepsin{0} S_1[M[(V_1,V_2)/x][\gamma_1]]\\
&= S_1[M[\gamma_1]]
\end{align*}

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 reflexivity, assumption.

* Opposite case is similar.

* $U\eta$ Let $\Gamma \vdash V : U \u B$

* We need to show that

\[ \thunk\force V[\gamma_1] \itylr i {U \u B} V[\gamma_2] \]

So assume $S_1 \itylr j {\u B} S_2$ for some $j\leq i$, then we need to show

\[ S_1[\force \thunk\force V[\gamma_1]] \ix\apreorder j \result(S_2[\force V[\gamma_2]])\]

The left side takes a step:

\[ S_1[\force \thunk\force V[\gamma_1]] \bigstepsin{0} S_1[\force V[\gamma_1]] \]

so by anti-reduction it is sufficient to show

\[ S_1[\force V[\gamma_1]] \ix\apreorder j \result(S_2[\force V[\gamma_2]]) \]

which follows by assumption.

* Opposite case is similar.

* $F\eta$

* We need to show that given $S_1 \itylr i {\u F A} S_2$,

\[ S_1[\bindXtoYinZ \bullet x \ret x] \itylr i {\u F A} S_2 \]

So assume $V_1 \itylr j A V_2$ for some $j\leq i$, then we need to show

\[ S_1[\bindXtoYinZ \bullet {\ret V_1} \ret x] \ix\apreorder j \result(S_2[\ret V_2])
\]

The left side takes a step:

\[ S_1[\bindXtoYinZ \bullet {\ret V_1} \ret x] \bigstepsin{0} S_1[\ret V_1]\]

so by anti-reduction it is sufficient to show

\[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2])\]

which follows by assumption

* Opposite case is similar.

* $\to\eta$ Let $\Gamma \vdash M : A \to \u B$

* We need to show

\[ S_1[(\lambda x:A. M[\gamma_1]\, x)] \ix\apreorder i \result(S_2[M[\gamma_2]])
\]

by assumption that $S_1 \itylr i {A \to \u B} S_2$, we know

\[ S_1 = S_1'[\bullet\, V_1]\]

so the left side takes a step:

\begin{align*}
S_1[(\lambda x:A. M[\gamma_1]\, x)]
&= S_1'[(\lambda x:A. M[\gamma_1]\, x)\, V_1]\\
&\bigstepsin{0} S_1'[M[\gamma_1]\, V_1]\\
&= S_1[M[\gamma_1]]
\end{align*}

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 reflexivity, assumption.

* Opposite case is similar.

* $\with\eta$ Let $\Gamma \vdash M : \u B_1 \with \u B_2$

* We need to show

\[ S_1[\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}] \ix\apreorder i \result(S_1[M[\gamma_2]]) \]

by assumption, $S_1 \itylr i {\u B_1 \with \u B_2} S_2$ so
either it starts with a $\pi$ or $\pi'$ so assume that $S_1 =
S_1'[\pi \bullet]$ ($\pi'$ case is similar).
Then the left side reduces

\begin{align*}
S_1[\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}]
&= S_1'[\pi\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}]\\
&\bigstepsin{0} S_1'[\pi M[\gamma_1]]\\
&= S_1[M[\gamma_1]]
\end{align*}

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 reflexivity, assumption.

* Opposite case is similar.

* $\top\eta$ Let $\Gamma \vdash M : \top$

* In either case, we assume we are given $S_1 \itylr i \top
S_2$, but this is a contradiction.

For any diverge-bottom preorder $\apreorder$, the following are

* $\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'}$

* $\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}$

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]])\]

For errors, the strictness axioms hold for any $\apreorder$, but the axiom that
$\err$ is a least element is specific to the definitions of
$\precltdyn, \ltdyn\succeq$

For any divergence preorder $\apreorder$ and appropriately
typed $S, M$,

S[] ωωS[] ωM M  ω

* It is sufficient by the limit lemma to show $\result(S[\err])
\apreorder \err$ which holds by reflexivity because $S[\err]
\bigstepzero \err$.

* 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.

* By the limit lemma it is sufficient to show $R
\mathrel{\errordivergerightop} \err$ which is true by definition.

The lemmas we have proved cover all of the inequality rules of CBPV, so
applying them with $\apreorder$ chosen to be $\errordivergeleft$ and
$\errordivergerightop$ gives

If $\Gamma \pipe \Delta \vdash E \ltdyn E' : \u B$ then
$\Gamma \pipe \Delta \vDash E \ix\precltdyn \omega E' \in \u B$ and
$\Gamma \pipe \Delta \vDash E' \ix{\mathrel{\preceq\gtdyn}} \omega E \in \u B$.

Because logical implies contextual equivalence, we can
conclude with the main theorem:

If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then
$\Gamma \pipe \Delta \vDash E \ctxize\ltdyn E' \in T$;
${\Gamma \pipe \Delta \vdash E \equidyn E' : T}$ then
${\Gamma \pipe \Delta \vDash E \ctxize= E' \in T}$.

For the first part, from Lemma <ref>,
we have $E \ix\precltdyn \omega E'$ and $E' \ix{\mathrel{\preceq\gtdyn}}
\omega E$.  By Lemma <ref>, we then have
$E \ctxize{\errordivergeleft} E'$ and $E' \ctxize{\errordivergerightop}
E$.  Finally, by Corollary <ref>, $E
\ctxize\ltdyn E' \text{ iff } E \ctxize{\errordivergeleft} E' \text{and
} E (\ctxize{(\errordivergerightop)})^\circ E'$, so we have the result.

For the second part, applying the first part twice gives $E
\ctxize\ltdyn E'$ and $E' \ctxize\ltdyn E$, and we concluded in
Corollary <ref> that this coincides with
contextual equivalence.

§ DISCUSSION AND RELATED WORK

In this paper, we have given a logic for reasoning about gradual
programs in a mixed call-by-value/call-by-name language, shown that
the axioms uniquely determine almost all of the contract translation
implementing runtime casts, and shown that the axiomatics is sound for
contextual equivalence/approximation in an operational model.

In immediate future work, we believe it is straightforward to add
inductive/coinductive types and obtain similar unique cast
implementation theorems
(e.g. $\upcast{\mathtt{list}(A)}{\mathtt{list}(A')} \equidyn
\mathtt{map}\upcast{A}{A'}$).  Additionally, since more efficient cast
implementations such as optimized cast calculi (the lazy variant in
<cit.>) and threesome
casts <cit.>, are equivalent to the lazy contract
semantics, they should also be models of GTT, and if so we could use GTT
to reason about program transformations and optimizations in them.

Applicability of Cast Uniqueness Principles

The cast uniqueness principles given in theorem
<ref> are theorems in the formal logic of Gradual
Type Theory, and so there is a question of to what languages the
theorem applies.

The theorem applies to any model of gradual type theory, such
as the models we have constructed using call-by-push-value given in
Sections <ref>, <ref>, <ref>.

We conjecture that simple call-by-value and call-by-name gradual
languages are also models of GTT, by extending the translation of
call-by-push-value into call-by-value and call-by-name in the appendix
of Levy's monograph <cit.>.

In order for the theorem to apply, the language must validate an
appropriate version of the $\eta$ principles for the types.

So for example, a call-by-value language that has reference equality
of functions does not validate even the value-restricted $\eta$
law for functions, and so the case for functions does not apply.

It is a well-known issue that in the presence of pointer equality of
functions, the lazy semantics of function casts is not compatible with
the graduality property, and our uniqueness theorem provides a
different perspective on this phenomenon

However, we note that the cases of the uniqueness theorem for each
type connective are completely modular: they rely only on the
specification of casts and the $\beta,\eta$ principles for the
particular connective, and not on the presence of any other types,
even the dynamic types.

So even if a call-by-value language may have reference equality
functions, if it has the $\eta$ principle for strict pairs, then the
pair cast must be that of Theorem <ref>.

Next, we consider the applicability to non-eager languages.

Analogous to call-by-value, our uniqueness principle should apply to
simple call-by-name gradual languages, where full $\eta$
equality for functions is satisfied, but $\eta$ equality for booleans
and strict pairs requires a “stack restriction” dual to the value
restriction for call-by-value function $\eta$.

We are not aware of any call-by-name gradual languages, but there is
considerable work on contracts for non-eager languages,
especially Haskell <cit.>.

However, we note that Haskell is not a call-by-name language in
our sense for two reasons.

First, Haskell uses call-by-need evaluation where results of
computations are memoized. However, when only considering Haskell's
effects (error and divergence), this difference is not observable so
this is not the main obstacle.

The bigger difference between Haskell and call-by-name is that Haskell
supports a  operation that enables the programmer to force
evaluation of a term to a value.

This means Haskell violates the function $\eta$ principle because
$\Omega$ will cause divergence under $\seq$, whereas $\lambda
x. \Omega$ will not.

This is a crucial feature of Haskell and is a major source of
differences between implementations of lazy contracts, as noted in

We can understand this difference by using a different translation
into call-by-push-value: what Levy calls the “lazy paradigm”, as
opposed to call-by-name <cit.>.

Simply put, connectives are interpreted as in call-by-value, but with
the addition of extra thunks $UF$, so for instance the lazy function
type $A \to B$ is interpreted as $UFU(UFA \to FB)$ and the extra $UFU$
here is what causes the failure of the call-by-name $\eta$ principle.

With this embedding and the uniqueness theorem, GTT produces a
definition for lazy casts, and the definition matches the work of
<cit.> when restricting to non-dependent contracts.

Comparing Soundness Principles for Cast Semantics<cit.> gives a spectrum of
differing syntactic type soundness theorems for different semantics of
gradual typing.

Our work here is complementary, showing that certain program
equivalences can only be achieved by certain cast semantics.

<cit.> give an analysis of different cast semantics
for contracts in lazy languages, specifically based on Haskell, i.e.,
call-by-need with .

They propose two properties “meaning preservation” and
“completeness” that they show are incompatible and identify which
contract semantics for a lazy language satisfy which of the

The meaning preservation property is closely related to graduality: it
says that evaluating a term with a contract either produces blame or
has the same observable effect as running the term without the

Meaning preservation rules out overly strict contract systems that
force (possibly diverging) thunks that wouldn't be forced in a
non-contracted term.

Completeness, on the other hand, requires that when a contract is
attached to a value that it is deeply checked.

The two properties are incompatible because, for instance, a pair of a
diverging term and a value can't be deeply checked without causing the
entire program to diverge.

Using Levy's embedding of the lazy paradigm into call-by-push-value
their incompatibility theorem should be a consequence of our main
theorem in the following sense.

We showed that any contract semantics departing from the
implementation in Theorem <ref> must violate
$\eta$ or graduality.

Their completeness property is inherently eager, and so must be
different from the semantics GTT would provide, so either the
restricted $\eta$ or graduality fails.

However, since they are defining contracts within the language, they
satisfy the restricted $\eta$ principle provided by the language, and
so it must be graduality, and therefore meaning preservation that

Axiomatic Casts

Henglein's work on dynamic typing also uses an axiomatic semantics of
casts, but axiomatizes behavior of casts at each type directly whereas
we give a uniform definition of all casts and derive implementations
for each type <cit.>.

Because of this, the theorems proven in that paper are more closely
related to our model construction in Section

More specifically, many of the properties of casts needed to prove
Theorem <ref> have direct analogues
in Henglein's work, such as the coherence theorems.

We have not included these lemmas in the paper because they are quite
similar to lemmas proven in <cit.>; see there for a more
detailed comparison, and the extended version of this paper for full proof details <cit.>.

Finally, we note that our assumption of compositionality, i.e., that
all casts can be decomposed into an upcast followed by a downcast, is
based on Henglein's analysis, where it was proven to hold in his
coercion calculus.

Gradual Typing Frameworks

In this work we have applied a method of “gradualizing” axiomatic
type theories by adding in dynamism orderings and adding dynamic
types, casts and errors by axioms related to the dynamism orderings.

This is similar in spirit to two recent frameworks for designing
gradual languages: Abstracting Gradual Typing (AGT) <cit.> and the
Gradualizer <cit.>.

All of these approaches start with a typed language and construct a
related gradual language.

A major difference between our approach and those is that our work is
based on axiomatic semantics and so we take into account the equality
principles of the typed language, whereas Gradualizer is based on the
typing and operational semantics and AGT is based on the type safety
proof of the typed language.

Furthermore, our approach produces not just a single language, but
also an axiomatization of the structure of gradual typing and so we
can prove results about many languages by proving theorems in GTT.

The downside to this is that our approach doesn't directly provide an
operational semantics for the gradual language, whereas for AGT this
is a semi-mechanical process and for Gradualizer, completely

Finally, we note that AGT produces the “eager” semantics for
function types, and it is not clear how to modify the AGT methodology
to reproduce the lazy semantics that GTT provides.

More generally, both AGT and the Gradualizer are known to produce
violations of parametricity when applied to polymorphic languages,
with the explanation being that the parametricity property is in no
way encoded in the input to the systems: the operational semantics and
the type safety proof.

In future work, we plan to apply our axiomatic approach to gradualizing
polymorphism and state by starting with the rich relational logics
and models of program equivalence for these
features <cit.>, which may lend insight into existing
proposals <cit.>— for
example, whether the “monotonic” <cit.> and “proxied”
<cit.> semantics of references support relational reasoning
principles of local state.

We do not give a treatment of runtime blame reporting, but we argue that
the observation that upcasts are thunkable and downcasts are linear is
directly related to blame soundness <cit.> in that if
an upcast were not thunkable, it should raise positive blame and
if a downcast were not linear, it should raise negative blame.

First, consider a potentially effectful stack upcast of the form
$\upcast{\u F A}{\u F A'}$. If it is not thunkable, then in our logical
relation this would mean there is a value $V : A$ such that $\upcast{\u
F A}{\u F A'}(\ret V)$ performs some effect.

Since the only observable effects for casts are dynamic type errors,
$\upcast{\u F A}{\u F A'}(\ret V) \mapsto \err$, and we must decide
whether the positive party or negative party is at fault.

However, since this is call-by-value evaluation, this error happens
unconditionally on the continuation, so the continuation never had a
chance to behave in such a way as to prevent blame, and so we must blame the
positive party.

Dually, consider a value downcast of the form $\dncast{U \u B}{U \u B'}$.
If it is not linear, that would mean it forces its $U \u B'$
input either never or more than once.

Since downcasts should refine their inputs, it is not possible for
the downcast to use the argument twice, since e.g. printing twice does not
refine printing once.

So if the cast is not linear, that means it fails without ever forcing
its input, in which case it knows nothing about the positive party and
so must blame the negative party.

In future work, we plan to investigate extensions of GTT with more than
one $\err$ with different blame labels, and an axiomatic account of
a blame-aware observational equivalence.

Denotational and Category-theoretic Models

We have presented certain concrete models of GTT using ordered CBPV
with errors, in order to efficiently arrive at a concrete operational

It may be of interest to develop a more general notion of model of GTT
for which we can prove soundness and completeness theorems, as in

A model would be a strong adjunction between double categories where
one of the double categories has all “companions” and the other has
all “conjoints”, corresponding to our upcasts and downcasts.

Then the contract translation should be a construction that takes a
strong adjunction between 2-categories and makes a strong adjunction
between double categories where the ep pairs are “Kleisli” ep pairs:
the upcast is has a right adjoint, but only in the Kleisli category and
vice-versa the downcast has a left adjoint in the co-Kleisli category.

Furthermore, the ordered CBPV with errors should also have a sound and
complete notion of model, and so our contract translation should have
a semantic analogue as well.

Gradual Session Types

Gradual session types <cit.> share some
similarities to GTT, in that there are two sorts of types (values and
sessions) with a dynamic value type and a dynamic session type.
However, their language is not polarized in the same way as CBPV,
so there is not likely an analogue between our upcasts always being
between value types and downcasts always being between computation
types.  Instead, we might reconstruct this in a polarized session
type language <cit.>.

The two dynamic types would then be the “universal sender” and
“universal receiver” session types.

Dynamically Typed Call-by-push-value

Our interpretation of the dynamic types in CBPV suggests a design for
a Scheme-like language with a value and computation distinction.

This may be of interest for designing an extension of Typed Racket that
efficiently supports CBN or a Scheme-like language with codata types.

While the definition of the dynamic computation type by a lazy product
may look strange, we argue that it is no stranger than the use of its
dual, the sum type, in the definition of the dynamic value type.

That is, in a truly dynamically typed language, we would not think of
the dynamic type as being built out of some sum type construction, but
rather that it is the union of all of the ground value types, and the
union happens to be a disjoint union and so we can
model it as a sum type.

In the dual, we don't think of the computation dynamic type as a
product, but instead as the intersection of the ground
computation types.

Thinking of the type as unfolding:

\[ \dync = \u F\dync \wedge (\dynv \to \u F \dynv) \wedge (\dynv \to \dynv \to \u F \dynv) \wedge \cdots \]

This says that a dynamically typed computation is one that can be
invoked with any finite number of arguments on the stack, a fairly
accurate model of implementations of Scheme that pass multiple
arguments on the stack.

Dependent Contract Checking

We also plan to explore using GTT's specification of casts in a
dependently typed setting, building on work using
Galois connections for casts between dependent
types <cit.>, and work on effectful dependent
types based a CBPV-like judgement
structure <cit.>.

We thank Ron Garcia, Kenji Maillard and Gabriel Scherer for helpful
discussions about this work. We thank the anonymous reviewers for
helpful feedback on this article. This material is based on research
sponsored by the National Science Foundation under grant CCF-1453796
and the United States Air Force Research Laboratory under agreement
number FA9550-15-1-0053 and FA9550-16-1-0292.

The views and conclusions contained herein are those of the authors and
should not be interpreted as necessarily representing the official
policies or endorsements, either expressed or implied, of the United
States Air Force Research Laboratory, the U.S. Government, or Carnegie
Mellon University.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Ahman, Ghani, and PlotkinAhman
et al2016]
authorpersonDanel Ahman, personNeil Ghani,
and personGordon D. Plotkin. year2016.
Dependent Types and Fibred Computational Effects.
In booktitleFoundations of Software Science and Computation
Structures. pages36–54.

authorpersonAmal Ahmed.
Step-Indexed Syntactic Logical Relations for
Recursive and Quantified Types. In booktitleEuropean
Symposium on Programming (ESOP). pages69–83.

[Ahmed, Dreyer, and RossbergAhmed
et al2009]
authorpersonAmal Ahmed, personDerek Dreyer,
and personAndreas Rossberg. year2009.
State-Dependent Representation Independence. In
booktitleACM Symposium on Principles of Programming
Languages (POPL), Savannah, Georgia.

[Ahmed, Jamner, Siek, and WadlerAhmed
et al2017]
authorpersonAmal Ahmed, personDustin
Jamner, personJeremy G. Siek, and personPhilip
Wadler. year2017.
Theorems for Free for Free: Parametricity, With and
Without Types. In booktitleInternational Conference on
Functional Programming (ICFP), Oxford, United Kingdom.

authorpersonJean-Marc Andreoli.
Logic programming with focusing proofs in linear
journalJournal of Logic and Computation
volume2, number3 (year1992),

[Bauer and PretnarBauer and Pretnar2013]
authorpersonAndrej Bauer and personMatija
Pretnar. year2013.
An Effect System for Algebraic Effects and
Handlers. In booktitleAlgebra and Coalgebra in Computer
Science. publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pages1–16.

[Cimini and SiekCimini and Siek2016]
authorpersonMatteo Cimini and
personJeremy G. Siek. year2016.
The Gradualizer: A Methodology and Algorithm for
Generating Gradual Type Systems. In booktitleProceedings of
the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (seriesPOPL '16).

[Cimini and SiekCimini and Siek2017]
authorpersonMatteo Cimini and
personJeremy G. Siek. year2017.
Automatically Generating the Dynamic Semantics of
Gradually Typed Languages. In booktitleProceedings of the
44th ACM SIGPLAN Symposium on Principles of Programming Languages
(seriesPOPL 2017). pages789–803.

[Dagand, Tabareau, and TanterDagand
et al2018]
authorpersonPierre-Èvariste Dagand,
personNicolas Tabareau, and personÈric Tanter.
Foundations of dependent interoperability.
journalJournal of Functional Programming
volume28 (year2018), pagese9.

[Degen, Thiemann, and WehrDegen
et al2012]
authorpersonMarkus Degen, personPeter
Thiemann, and personStefan Wehr.
The interaction of contracts and laziness.
journalHigher-Order and Symbolic Computation
volume25 (year2012), pages85–125.

authorpersonBrian Patrick Dunphy.
titleParametricity As a Notion of Uniformity in
Reflexive Graphs.
thesistypePh.D. Dissertation.
addressChampaign, IL, USA.
Advisor(s) Reddy, Uday.

[Findler and FelleisenFindler and
authorpersonRobert Bruce Findler and
personMatthias Felleisen. year2002.
Contracts for higher-order functions. In
booktitleInternational Conference on Functional
Programming (ICFP). pages48–59.

[Findler, Flatt, and FelleisenFindler
et al2004]
authorpersonRobert Bruce Findler,
personMatthew Flatt, and personMatthias Felleisen.
Semantic Casts: Contracts and Structural Subtyping
in a Nominal World. In booktitleEuropean Conference on
Object-Oriented Programming (ECOOP).

authorpersonCarsten Führmann.
Direct models of the computational
journalElectronic Notes in Theoretical Computer
Science  volume20 (year1999),

[Garcia, Clark, and TanterGarcia
et al2016]
authorpersonRonald Garcia, personAlison M.
Clark, and personÉric Tanter.
Abstracting Gradual Typing. In
booktitleACM Symposium on Principles of Programming
Languages (POPL).

authorpersonJean-Yves Girard.
Locus Solum: From the rules of logic to the logic
of rules.
journalMathematical Structures in Computer Science
volume11, number3 (year2001),

authorpersonMichael Greenberg.
Space-Efficient Manifest Contracts. In
booktitleACM Symposium on Principles of Programming
Languages (POPL). pages181–194.

[Greenberg, Pierce, and WeirichGreenberg
et al2010]
authorpersonMichael Greenberg,
personBenjamin C. Pierce, and personStephanie
Weirich. year2010.
Contracts Made Manifest
(seriesPOPL '10).

[Greenman and FelleisenGreenman and
authorpersonBen Greenman and
personMatthias Felleisen. year2018.
A Spectrum of Type Soundness and Performance. In
booktitleInternational Conference on Functional
Programming (ICFP), St. Louis, Missouri.

authorpersonFritz Henglein.
Dynamic Typing: Syntax and Proof Theory.
volume22, number3 (year1994),

[Herman, Tomb, and FlanaganHerman
et al2010]
authorpersonDavid Herman, personAaron Tomb,
and personCormac Flanagan. year2010.
Space-efficient gradual typing.
journalHigher-Order and Symbolic Computation

[Hinze, Jeuring, and LöhHinze
et al2006]
authorpersonRalf Hinze, personJohan
Jeuring, and personAndres Löh.
Typed Contracts for Functional Programming. In
booktitleInternational Symposium on Functional and Logic
Programming (FLOPS).

[Igarashi, Thiemann, Vasconcelos, and
WadlerIgarashi et al2017b]
authorpersonAtsushi Igarashi, personPeter
Thiemann, personVasco T. Vasconcelos, and
personPhilip Wadler. year2017b.
Gradual Session Types.
journalProceedings of ACM Programning Languages
volume1, numberICFP, Article articleno38
(dateAug. year2017), numpages28 pages.

[Igarashi, Sekiyama, and IgarashiIgarashi
et al2017a]
authorpersonYuu Igarashi, personTaro
Sekiyama, and personAtsushi Igarashi.
On Polymorphic Gradual Typing. In
booktitleInternational Conference on Functional
Programming (ICFP), Oxford, United Kingdom.

authorpersonPaul Blain Levy.
booktitleCall-By-Push-Value: A Functional/Imperative

authorpersonPaul Blain Levy.
Contextual Isomorphisms. In
booktitleACM Symposium on Principles of Programming
Languages (POPL).

[Lindley, McBride, and McLaughlinLindley
et al2017]
authorpersonSam Lindley, personConor
McBride, and personCraig McLaughlin.
Do Be Do Be Do. In
booktitleProceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages (seriesPOPL 2017).
publisherACM, pages500–514.

[Matthews and AhmedMatthews and
authorpersonJacob Matthews and personAmal
Ahmed. year2008.
Parametric polymorphism through run-time sealing,
or, Theorems for low, low prices!. In booktitleEuropean
Symposium on Programming (ESOP).

authorpersonEugenio Moggi.
Notions of computation and monads.
journalInform. And Computation
volume93, number1 (year1991).

authorpersonGuillaume Munch-Maccagnoni.
Models of a Non-associative Composition. In
booktitleFoundations of Software Science and Computation
Structures. pages396–410.

[NakanoNakano[n. d.]]
authorpersonHiroshi Nakano. year[n.
A modality for recursion. In
booktitleLogic in Computer Science, 2000. Proceedings. 15th
Annual IEEE Symposium on.

[Neis, Dreyer, and RossbergNeis
et al2009]
authorpersonGeorg Neis, personDerek Dreyer,
and personAndreas Rossberg. year2009.
Non-Parametric Parametricity. In
booktitleInternational Conference on Functional
Programming (ICFP). pages135–148.

[New and AhmedNew and Ahmed2018]
authorpersonMax S. New and personAmal
Ahmed. year2018.
Graduality from Embedding-Projection Pairs. In
booktitleInternational Conference on Functional
Programming (ICFP), St. Louis, Missouri.

[New and LicataNew and Licata2018]
authorpersonMax S. New and personDaniel R.
Licata. year2018.
Call-by-name Gradual Type Theory.
journalFSCD (year2018).

[New, Licata, and AhmedNew
et al2018]
authorpersonMax S. New, personDaniel R.
Licata, and personAmal Ahmed.
titleGradual Type Theory (Extend Version).

[Pfenning and GriffithPfenning and
authorpersonFrank Pfenning and
personDennis Griffith. year2015.
Polarized Substructural Session Types (invited
talk). In booktitleInternational Conference on Foundations
of Software Science and Computation Structures (FoSSaCS).

[Plotkin and AbadiPlotkin and Abadi1993]
authorpersonGordon D. Plotkin and
personMartín Abadi. year1993.
A Logic for Parametric Polymorphism. In
booktitleTyped Lambda Calculi and Applications,
International Conference on Typed Lambda Calculi and Applications, TLCA
'93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings.

[Siek, Garcia, and TahaSiek
et al2009]
authorpersonJeremy Siek, personRonald
Garcia, and personWalid Taha.
Exploring the Design Space of Higher-Order Casts.
In booktitleEuropean Symposium on Programming (ESOP).
publisherSpringer-Verlag, addressBerlin, Heidelberg,

[Siek and Tobin-HochstadtSiek and
authorpersonJeremy Siek and personSam
Tobin-Hochstadt. year2016.
The recursive union of some gradual types.
journalA List of Successes That Can Change the
World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday
(Springer LNCS)  volumevolume 9600 (year2016).

[Siek, Vitousek, Cimini, and BoylandSiek
et al2015a]
authorpersonJeremy Siek, personMicahel
Vitousek, personMatteo Cimini, and personJohn Tang
Boyland. year2015a.
Refined Criteria for Gradual Typing. In
booktitle1st Summit on Advances in Programming Languages
(seriesSNAPL 2015).

[Siek and TahaSiek and Taha2006]
authorpersonJeremy G. Siek and personWalid
Taha. year2006.
Gradual Typing for Functional Languages. In
booktitleScheme and Functional Programming Workshop
(Scheme). pages81–92.

[Siek, Vitousek, Cimini, Tobin-Hochstadt, and
GarciaSiek et al2015b]
authorpersonJeremy G. Siek, personMichael M.
Vitousek, personMatteo Cimini, personSam
Tobin-Hochstadt, and personRonald Garcia.
Monotonic References for Efficient Gradual Typing.
In booktitleProceedings of the 24th European Symposium on
Programming on Programming Languages and Systems - Volume 9032.

[Siek and WadlerSiek and Wadler2010]
authorpersonJeremy G. Siek and
personPhilip Wadler. year2010.
Threesomes, with and Without Blame. In
booktitleACM Symposium on Principles of Programming
Languages (POPL). publisherACM, pages365–376.

[Strickland, Tobin-Hochstadt, Findler, and
FlattStrickland et al2012]
authorpersonT. Stephen Strickland, personSam
Tobin-Hochstadt, personRobert Bruce Findler, and
personMatthew Flatt. year2012.
Chaperones and Impersonators: Run-time Support for
Reasonable Interposition (seriesACM Symposium on
Object Oriented Programming: Systems, Languages, and Applications

[Tobin-Hochstadt and FelleisenTobin-Hochstadt
and Felleisen2006]
authorpersonSam Tobin-Hochstadt and
personMatthias Felleisen. year2006.
Interlanguage Migration: From Scripts to Programs.
In booktitleDynamic Languages Symposium (DLS).

[Vitousek, Swords, and SiekVitousek
et al2017]
authorpersonMichael M. Vitousek,
personCameron Swords, and personJeremy G. Siek.
Big Types in Little Runtime: Open-world Soundness
and Collaborative Blame for Gradual Type Systems
(seriesPOPL 2017).

[Wadler and FindlerWadler and
authorpersonPhilip Wadler and
personRobert Bruce Findler. year2009.
Well-typed programs can't be blamed. In
booktitleEuropean Symposium on Programming (ESOP).

[Xu, Peyton Jones, and ClaessenXu
et al2009]
authorpersonDana N. Xu, personSimon
Peyton Jones, and personKoen Claessen.
Static Contract Checking for Haskell
(seriesACM Symposium on Principles of Programming
Languages (POPL), Savannah, Georgia).

authorpersonNoam Zeilberger.
titleThe Logical Basis of Evaluation Order and
thesistypePh.D. Dissertation. schoolCarnegie
Mellon University.