# Pure Subtype Systems Are Type-Safe

Valentin Pasquale<EMAIL_ADDRESS>Université Paris-Saclay, CEA,
List, PalaiseauFrance and  Álvaro García-Pérez<EMAIL_ADDRESS>Université Paris-Saclay, CEA, List, PalaiseauFrance

(2018)

###### Abstract.

We address the open problem of type safety in Hutchins’ pure subtype systems
(PSS). PSS (hereafter in the singular) harmoniously mixes terms and types,
thus enabling a number of advanced language features that combine dependent
types with higher-order subtyping. In PSS terms and types belong to the same
kind (everything is a subtype) and the resulting theory is based on subtyping.
Since PSS lacks strong normalisation, a type soundness result can only be
stated in terms of type safety defined as progress and preservation. Proving
type safety rests on the well-known problem of transitivity elimination in
higher-order subtyping, where a key inversion lemma fails under the presence
of intermediary steps in transitive subtype derivations. Despite his attempts,
Hutchins failed to prove PSS type safety. We propose a reformulation of pure
subtype systems with a more fine-grained notion of subtyping derivation that
enables a direct proof of transitivity elimination, and thus of type safety.
We also reformulate Hutchins’ practical type-checking algorithm to our system
and prove it correct.

Lambda calculus, Pure subtype systems, Dependent types, Higher-order
subtyping, Type safety

††copyright: acmlicensed††journalyear: 2018††doi: XXXXXXX.XXXXXXX††conference:
Make sure to enter the correct conference title from your rights confirmation
emai; June 03–05, 2018; Woodstock, NY††isbn: 978-1-4503-XXXX-X/18/06††ccs:
Theory of computation Lambda calculus††ccs: Theory of computation Type
theory††ccs: Software and its engineering Formal software verification

##  1\. Introduction

This paper addresses the open problem of type safety outlined in prior
research concerning Hutchins’ _pure subtype systems_ (PSS for short)
(Hutchins, 2010, 2009). Contrary to traditional type systems, PSS (hereafter
in the singular) harmoniously mixes terms—such as the natural number $3$—and
types—such as $\mathit{Nat}$ the type of natural numbers. In PSS, one can
therefore have a term that encodes $\mathit{Nat}+3$ with the naive Church
encoding of naturals, which type-checks to $\mathit{Nat}$. Terms can also be
used instead of types: so for instance $\lambda x\,{\leq}\,3.x$, where
$\,{\leq}\,$ is the subtyping operation (the substitute of typing in our
calculus), is a valid expression. The latter example is an instance of
_bounded quantification_ (Pierce and Steffen, 1997) where the term $3$ is the
singleton type $\\{3\\}$ and the subtyping relation is akin to the subset
relation.

PSS is a novel approach to type theory that replaces the typing relation with
a subtyping relation—thus blurring the distinction between terms and types—and
which enable a number of advanced language features for extensibility,
genericity and efficiency, including mixin modules, virtual classes, feature-
oriented programming and partial evaluation (Hutchins, 2010, 2009).

Since terms and types belong to the same kind, PSS naturally subsumes
dependent types. Dependent types have been historically used in theorem
provers, such as Coq and Agda, where strong normalisation ensures that the
logic obtained after them by the Curry-Howard isomorphism is consistent. On
the contrary, PSS lacks strong normalisation: the non-normalising System
$\lambda*$ can be embedded into PSS by the translation on p. 47 of (Hutchins,
2010).111Besides not being strongly normalising, we believe PSS is Turing-
complete too, but the argument is far from direct (see Section 6). But this
lack of strong normalisation is a feature, not a bug, since the interest in
PSS as a programming language is larger than its use as a theorem
prover.222Some existing Turing-complete languages (Casinghino et al., 2014)
have a logical fragment which is used to write proofs where every term is
strongly normalising, and where the Curry-Howard isomorphism holds. A similar
approach could be taken with PSS, although we haven’t explored this direction
yet.

Due to the lack of strong normalisation, the only possible notion of type
soundness in PSS is akin to type safety defined as _progress_ and
_preservation_ (Wright and Felleisen, 1994; Harper, 2016) (cf. type soundness
by building a semantic model of types via a denotational semantics (Milner,
1978)).

Theories that mix terms and types are not new, have been studied for a long
time, and their meta-theory is known to be challenging. The well-known problem
of transitivity elimination in higher-order subtyping (Pierce, 2002; Steffen
and Pierce, 1994) prevents a direct proof of PSS type-safety: the presence of
intermediary steps in a subtyping derivation prevents one from establishing an
inversion principle that is key in the proof of progress. The following
paragraphs elaborate on this problem.

In the original work on PSS, Hutchins introduces a _declarative_ system with
two relations, one for equivalence (akin to $\beta$-equivalence) and the other
for subtyping, both of which are closed by transitivity. Type preservation
hinges on an inversion lemma that states that any two functions in the
subtyping relation must take operands of equivalent subtypes. The inversion
lemma cannot be proven directly when the subtyping derivation relating the two
functions contains transitive steps, because of the intermediary terms that
may not be structurally related to the two functions. This notorious problem
is recurrent in higher-order subtyping systems, where it is known as
_transitivity elimination_ (Pierce, 2002; Steffen and Pierce, 1994).
Transitivity elimination in PSS amounts to showing that transitivity is
admissible in the declarative system. In order to show this, Hutchins proposes
an equivalent syntax-directed, _algorithmic_ system where the subtyping
relation is defined by the combination of two different notions of reduction,
an _equivalence reduction_ that models $\beta$-reduction, and a _subtyping
reduction_ that models small-step subtyping (i.e., _promotion_). In the
algorithmic setting, transitivity can be shown to be admissible if these two
notions of reduction commute.

Despite all the attempts at proving transitivity elimination in (Hutchins,
2009), a proof of type safety of PSS is missing. Hutchins applied the
_decreasing diagrams_ technique of (Van Oostrom, 1994), but he failed at
proving that the two reductions for equivalence and subtyping commute.

In order to establish type safety, we reformulate Hutchins’ system into the
system in Section 2, which resembles Hutchins’ algorithmic system on p. 58 of
(Hutchins, 2009) but where we adopt upfront the simultaneous reduction on p.
74 of the same work. The main difference between our system and Hutchins’ is
that ours instruments a _continuation stack_ that keeps track of operands that
have been passed at a particular scope. The continuation stack is akin to and
directly inspired by the Krivine abstract machine (KAM) (Ager et al., 2003;
Krivine, 2007) which is the canonical abstract machine for call-by-name lambda
calculus evaluation.

The failure of Hutchins’ proof of commutativity of the equivalence and
subtyping reductions is exemplified by the diagram below on the left, where
the premature promotion of the body $x$ of the abstraction to the variable’s
type annotation $t$ in the $\leq_{H}$ edge prevents to complete the right edge
of the diagram in a single subtyping step. With our continuation stack that
keeps track of the operand $v$ that has been passed at this scope, we can
promote the body $x$ directly to the operand $v$ (instead of to the variable’s
annotation $t$), and trivially complete the diagram below on the right with a
single (reflexive) subtyping step. (The failure of Hutchins’ proof is further
explained in Section 3 below.)

${(\lambda x\,{\leq}\,t.t)v}$${t}$${(\lambda
x\,{\leq}\,t.x)v}$${v}$$\scriptstyle{\equiv}$$\scriptstyle{\leq_{H}}$$\scriptstyle{\equiv}$$\scriptstyle{?}$${(\lambda
x\,{\leq}\,t.v)v}$${v}$${(\lambda
x\,{\leq}\,t.x)v}$${v}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

When assuming that the term $(\lambda x\,{\leq}\,t.x)v$ is _well-formed_
(meets the static condition that ensures type safety, to be detailed in
Section 2 below) our system is the same expressive as Hutchins’, since nothing
prevents to further promote the operand $v$ in multiple steps to the
variable’s annotation $t$ (a well-formed redex meets the condition that $v$ is
a subtype of $t$, but perhaps in a transitive way, denoted $v\leq^{*}t$).
However, our subtyping relation is more fine-grained than Hutchins’ in that it
exposes some intermediary terms in the subtyping reduction that are absent in
Hutchins’ formulation. In particular, in the diagram above on the right, our
subtyping relation exposes the term $(\lambda x\,{\leq}\,t.v)v$, which will be
key for applying the induction hypothesis in our direct proof of transitivity
elimination in Section 4, which is the main theoretical result of the paper on
which type safety of PSS rests. To clarify the proof of transitivity
elimination, Section 4.1 provides a detailed example of its application.

After proving that our reformulation of PSS is type-safe, Section 5
reformulates Hutchins’ practical algorithm for subtype checking on page 82 of
(Hutchins, 2009), and proves its correctness. We also provide conditions for
an incremental practical algorithm that avoids re-checking subterms that have
already been checked, in compositional fashion. We conclude the paper by
discussing related and future work (Sections 6 and 7) and provide some
concluding remarks (Section 8).

Our detailed contributions are the following:

  * •

We introduce a reformulation of Hutchins’ algorithmic System
$\lambda_{\vartriangleleft}$ that, among other changes, keeps track of the
operands that have been passed at a particular scope by using a mechanism
reminiscent of the continuation stack of the KAM (Krivine, 2007; Ager et al.,
2003). This feature will be key to prove the transitivity elimination that
enables type safety.

  * •

We define a static condition for terms (well-formedness) that ensures type
safety. Our condition hinges on the use of the continuation stack from our
reformulation of the system, and therefore slightly differs from Hutchins’
condition with the same name in (Hutchins, 2009). We conjecture that both
conditions are equivalent but we leave this as future work.

  * •

We show that the equivalence and subtyping reductions in our system commute,
which enables transitivity elimination and ultimately type safety of PSS.
Thanks to the keeping track of operands by the continuation stack, our proof
of commutativity is direct and proceeds by simple structural induction on
terms. We do away with the _decreasing diagrams technique_ of (Van Oostrom,
1994) that Hutchins considers in his attempts at proving commutativity.

  * •

We reformulate Hutchins’ practical algorithm for checking well-formedness, and
provide conditions for an incremental practical algorithm that avoids re-
checking subterms that have already been checked, in compositional fashion.

These contributions not only propel the theoretical advancements within the
realm of type systems, but also lay the groundwork for practical applications.
To the best of our knowledge, PSS stands as the first type-safe system that
primitively mixes together types and terms by using a single kind where
everything is a subtype.

All the formal proofs of the statements in the paper are collected in the
supplementary material.

##  2\. Our reformulation of PSS

PSS is an extension of the pure lambda calculus with a constant symbol
$\mathsf{Top}$ for the most general supertype, and with subtype annotations in
the formal parameters of abstractions. Assume a countably infinite set of
variables $\mathrm{V}$ ranged over by $x$, $y$, …, the syntax of terms and
contexts of PSS are defined respectively as

$\begin{array}[]{rcl}t,u,v,\ldots\in\Lambda&::=&x\mid\mathsf{Top}\mid(\lambda
x\,{\leq}\,t.u)\mid(u\,v)\\\
\Gamma;s&::=&\varepsilon;\mathrm{nil}\mid\Gamma,x\,{\leq}\,t;s\mid\Gamma;u::s\end{array}$

A _variable_ $x\in\mathrm{V}$ is a term. The term $\mathsf{Top}$ is the _most
general supertype_ , such that any other term (including itself) is a subtype
of $\mathsf{Top}$. We say that $(\lambda x\,{\leq}\,t.u)$ is an _abstraction_
with _parameter_ $x$ annotated with _subtype_ $t$, and with _body_ $u$. We say
that $(u\,v)$ is an _application_ with _operator_ $u$ and _operand_ $v$.

We assume conventional parenthesis-dropping conventions where abstractions
associate to the right and applications to the left, and applications bind
stronger than abstractions.

We assume the usual notions of _free_ and _bound variables_ , and the usual
_capture-avoiding substitution_ function, denoted by $u[x\backslash v]$, that
replaces the free occurrences of variable $x$ in $u$ by $v$, while avoiding
the capture of any bound variable in $u$. We consider terms that result after
the renaming of bound variables to be identical to each other. When needed, we
assume that $\alpha$-equivalence is applied at will as to avoid clashing of
free variables.

An application of the form $(\lambda x\,{\leq}\,t.u)v$ is a _redex_ iff the
operand $v$ is a subtype of the parameter’s annotation $t$, i.e., when
$v\leq^{*}_{\mathrm{wf}}t$ holds (the subtyping relation
$\leq^{*}_{\mathrm{wf}}$ will be defined in a minute). Contraction of a redex
is modelled by $\beta$-reduction, which rewrites $(\lambda x\,{\leq}\,t.u)v$
into $u[x\backslash v]$. Consider the following example of a redex involving
the term $\lambda x\,{\leq}\,\mathsf{Top}.x$ for _universal identity_. Since
universal identity is a subtype of $\mathsf{Top}$, the self-application of
universal identity—i.e., the redex $(\lambda
x\,{\leq}\,\mathsf{Top}.x)(\lambda x\,{\leq}\,\mathsf{Top}.x)$—reduces to
$x[x\backslash\lambda x\,{\leq}\,\mathsf{Top}.x]$, which is equal to universal
identity by the definition of the substitution function.

An _extended context_ $\Gamma;s$ (_context_ for short) is a _subtyping
context_ $\Gamma$ paired wiht a _continuation stack_ $s$. Subtyping context
contains a sequence of _subtype annotations_ $x\,{\leq}\,t$ (_annotations_ for
short) and are used in the definitions in the remainder of the paper to store
the annotations of the abstractions that have been crossed-by at a particular
scope of a term. The continuation stack keeps track of the _arguments_ (i.e.,
operands) that have been passed (_crossed by_ , if we wish, when proceeding
with the operator in an application) at a particular scope of a term. (We use
the Greek letter $\alpha$ to distinguish arguments coming form the stack from
other occurrences of terms.) Our continuation stack is reminiscent and
directly inspired by the Krivine abstract machine (KAM), which is the
canonical abstract machine for call-by-name evaluation (Krivine, 2007; Ager et
al., 2003). We write $\varepsilon;\mathrm{nil}$ for the _empty context_ ,
$\Gamma,x\,{\leq}\,t;s$ for the operation that appends annotation
$x\,{\leq}\,t$ to the subtype annotations of $\Gamma;s$, and $\Gamma;u::s$ for
the operation that appends $u$ to the continuation stack of $\Gamma;s$. (By
abuse of notation, we write $\Gamma_{1},\Gamma_{2}$ for the concatenation of
subtype annotations $\Gamma_{1}$ and $\Gamma_{2}$, and $s_{1}\mathop{++}s_{2}$
for the concatenation of continuation stacks $s_{1}$ and $s_{2}$.) We say that
$x$ _has subtype $t$ in_ $\Gamma$ iff $x\,{\leq}\,t$ is the topmost annotation
for variable $x$ that occurs in $\Gamma$, i.e.,
$\Gamma=\Gamma_{1},x\,{\leq}\,t,\Gamma_{2}$ and there exists not a term $s$
such that $x\,{\leq}\,s\in\Gamma_{2}$. We say that $x$ _is in the support of_
$\Gamma$—written $x\in\mathrm{dom}(\Gamma)$—iff an annotation for variable $x$
occurs in $\Gamma$, i.e., there exists a term $s$ such that
$x\,{\leq}\,s\in\Gamma$.

In the original work on PSS, Hutchins introduces a declarative system and an
algorithmic system. Our approach does away with the declarative system, and we
consider only a system akin to Hutchins’ algorithmic system. Figures 1 and 2
below introduces our reformulation of PSS which combines the original
algorithmic system on p. 58 of (Hutchins, 2009) with the simultaneous
reduction on p. 74, and adds a continuation stack to the subtyping context.
Hutchins introduced simultaneous reduction as a refinement of his algorithmic
equivalence reduction, to ease the application of the decreasing diagrams
technique of (Van Oostrom, 1994). We tackle this refinement at once and
directly present a system that incorporates simultaneous reduction. But yet
our system differs greatly from either p. 58 or p. 74 in (Hutchins, 2009), as
we develop below.

Operational semantics: $t\mapsto t^{\prime}$ C::= [ ] ∣(λx ≤ C.t) ∣(λx ≤ t.C)
∣(C t) ∣(t C)

*[right=E-Cong] t ↦t’ C[t] ↦C[t’]

*[right=E-App] (λx ≤ t.u)v ↦u[x\v]

Normal forms: $t_{n}$ is a normal form

$\begin{array}[]{rcl}t_{n},u_{n}\ldots\in\mathsf{NF}&::=&\mathsf{Top}\mid\lambda
x\,{\leq}\,t_{n}.u_{n}\mid x\\{t_{n}\\}^{*}\\\ \end{array}$

Prevalidity: $\Gamma;s~{}\mathrm{prevalid}$ *[right=P-Ctx1] ε;nil prevalid

*[right=P-Ctx2] Γ;nil prevalidx／∈dom(Γ) fv(t)⊆dom(Γ) Γ,x ≤ t;nil prevalid

*[right=P-Ctx3] Γ;s prevalidfv(α)⊆dom(Γ) Γ;α::s prevalid

Term well-formedness: $\Gamma;s\vdash t~{}\mathrm{wf}$ *[right=W-Var] Γ; s
prevalidx has subtype t in ΓΓ; s ⊢t wf Γ; s ⊢x wf

*[right=W-Top] Γ; s prevalid Γ; s ⊢Top wf

*[right=W-Fun] Γ, x ≤ t; nil⊢u wfΓ; nil⊢t wf Γ; nil⊢λx ≤ t.u wf

*[right=W-FunOp] Γ, x ≤ δ; s ⊢u wfΓ; nil⊢t wf Γ; δ:: s ⊢λx ≤ t.u wf

*[right=W-App] Γ; v::s ⊢u ≤^*_wfλx ≤ t.TopΓ; nil⊢v ≤^*_wft Γ; s ⊢u v wf

Well-subtyping: $\Gamma;s\vdash u\leq_{\mathrm{wf}}t$ *[right=Wf-Rule] Γ; s ⊢u
wfΓ; s ⊢t wfΓ; s ⊢u ≤t Γ; s ⊢u ≤_wft

Transitive well-subtyping:  $\Gamma;s\vdash v\leq_{\mathrm{wf}}^{*}t$
*[right=Wf-Sub] Γ; s ⊢v ≤_wf t Γ; s ⊢v ≤_wf^* t

*[right=Wf-Trans] Γ; s ⊢v ≤_wf^* u Γ; s ⊢u ≤_wf^* t Γ; s ⊢u wf Γ; s ⊢v ≤_wf^* t

Figure 1. Well-formed derivations in System $\lambda_{\vartriangleleft}$

Equivalence reduction: $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$ *[right=Cr-Var]
Γ; s ⊢x ⟶≡ x

*[right=Cr-App] Γ; s ⊢u ⟶≡ u’ Γ; s ⊢v ⟶≡ v’ Γ; s ⊢u v ⟶≡ u’ v’

*[right=Cr-Top] Γ; s ⊢Top⟶≡ Top

*[right=Cr-Fun] Γ; s ⊢t ⟶≡ t’ Γ; s ⊢u ⟶≡ u’ Γ; s ⊢λx ≤ t . u ⟶≡ λx ≤ t’ . u’

*[right=Cr-Beta] Γ; s ⊢u ⟶≡ u’ Γ; s ⊢v ⟶≡ v’ Γ; s ⊢(λx ≤ t . u) v ⟶≡ u’[x\v’]

*[right=Cr-TopApp] Γ; s ⊢Top u ⟶≡ Top

Subtyping reduction:  $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}v$ *[right=Srs-Prom]
Γ;s prevalidx ≤ t ∈Γ Γ;s ⊢x ⟶≤ t

*[right=Srs-Top] Γ;s prevalid Γ;s ⊢u ⟶≤ Top

*[right=Srs-Eq] Γ; s prevalidΓ; s ⊢u ⟶≡ v Γ;s ⊢u ⟶≤ v

*[right=Srs-App] Γ;v :: s ⊢u ⟶≤ u’ Γ;s ⊢u v ⟶≤ u’ v

*[right=Srs-FunOp] Γ,x ≤ α; s ⊢u ⟶≤ u’ Γ;α:: s ⊢λx ≤ t . u ⟶≤ λx ≤ t . u’

*[right=Srs-Fun] Γ,x ≤ t; nil⊢u ⟶≤ u’ Γ;nil⊢λx ≤ t . u ⟶≤ λx ≤ t . u’

Subtyping/equivalence:  $\Gamma;s\vdash v\vartriangleleft t$ *[right=As-Refl]
Γ;s prevalid Γ;s ⊢t ⊲t

*[right=As-Left] Γ; s ⊢v ⟶⊲ v’ Γ; s ⊢v’ ⊲t Γ; s ⊢v ⊲t

*[right=As-Right] Γ; s ⊢v ⊲t’ Γ; s ⊢t ⟶≡ t’ Γ; s ⊢v ⊲t

Transitive subtyping/equivalence:  $\Gamma;s\vdash v\vartriangleleft^{*}t$
*[right=Ast-Sub] Γ; s ⊢v ⊲t Γ; s ⊢v ⊲^* t

*[right=Ast-Trans] Γ; s ⊢v ⊲^* u Γ; s ⊢u ⊲^* t Γ; s ⊢v ⊲^* t

Figure 2. Subtyping and equivalence in System $\lambda_{\vartriangleleft}$

The upper part of Figure 1 describes the operational semantics of our system,
which is identical to the operational semantics on p. 35 of (Hutchins, 2009).
The operational semantics is given by a context-based reduction relation
$\mapsto$ which is the congruence closure (rule E-Cong) of $\beta$-reduction
(rule E-App). The operational semantics reduces terms to normal forms, which
in our system are either $\mathsf{Top}$, function that have a subtype
annotation and a body in normal form, or a variable applied to any number of
normal forms. Our reformulation considers normal forms instead of the values
in the original work.

Figure 1 then defines the _prevalidity_ condition on extended contexts, which
ensures that terms and accompanying extended contexts are well-scoped (i.e.,
variables do not clash and the subtype of every variable is well-defined).
This property, contrary to the well-formedness notion defined after, is always
preserved by reduction. Figure 1 then defines _well-formedness_ , which
constitutes the safety condition for PSS programs that ensures that they will
never get stuck: any application within a well-formed term can be safely
evaluated to a redex that will be contracted, and the subtype of every
variable is well-defined. This notion that is context dependent, a given term
may be well-formed when considered alone, but not when applied. A term $t$ is
well-formed when all its variables are well-scoped (either they are bound, or
otherwise they are in the support of the accompanying extended context), well-
formed in the context it appears, and when all the applications within the
term are well-typed (for any application $u\,v$, the $u$ is a subtype of
function $(\lambda x\,{\leq}\,t.\mathsf{Top})$, and the $v$ is a subtype of
$t$) by rule W-App. The term $\mathsf{Top}$ is always well-formed (rule
W-Top). Finally the rules W-Fun and W-FunOp propagate these conditions to
functions, and distinguish if the function is applied to some arguments (stack
isn’t empty and W-FunOp is used), or not (and then W-Fun is used).

Figure 1 then defines _well-subtyping_ $\leq_{\mathrm{wf}}$ and _transitive
well-subtyping_ $\leq^{*}_{\mathrm{wf}}$. A subtype derivation $v\leq t$ is a
well-subtype derivation $v\leq_{\mathrm{wf}}t$ iff $v$ and $t$ are well-formed
(rule Wf-Rule). The optional rules Wf-Sub and Wf-Trans add transitivity to
well-subtyping. (Thanks to Theorem 4.4 below, we’ll be able to establish that
transitivity in well-subtyping is admissible in our system.)

Now to the top of Figure 2. Reduction
$\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$ models
reflexive, small step, simultaneous, $\beta$-reduction. Rules Cr-App and Cr-
Fun model the congruence closure for functions and applications. Rule Cr-Beta
model $\beta$-reduction. Rules Cr-Var and Cr-Top model the reflexive closure
of $\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$. The extended
context $\Gamma;s$ is immaterial to the equivalence reduction and as such we
may write $u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$
instead of $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$. Besides
$\beta$-reduction, we allow a notion of reduction that collapses applications
of $\mathsf{Top}$ to other terms into $\mathsf{Top}$ with rule Cr-TopApp. This
unusual rule is a device from (Hutchins, 2009), whose objective is to
accommodate ill-formed terms with shape $\mathsf{Top}\,u$, which may pop up in
reductions, since the system does away with the well-formedness condition (see
p. 59 of (Hutchins, 2009) for a further discussion on this issue). Our
equivalence reduction resembles the simultaneous reduction on p. 74 of
(Hutchins, 2009). Our equivalence reduction does away with the subtype
requirement for redexes (premise $s^{\prime}\leq^{*}t$ in rule CR-Beta of
page. 74 of (Hutchins, 2009)). The original work needs the subtype requirement
$s^{\prime}\leq^{*}t$ to ensure that equivalence and subtyping reduction
commutes, but in our system lacking this requirement is innocuous. Proposition
2.1 illustrates the relation between the reduction equivalence and the
reduction semantics.

###### Proposition 2.1 (From reduction semantics to equivalence reduction).

Let $u$ and $v$ be terms. If $u\mapsto v$ then
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$.

We continue with the subtyping reduction
$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$, which resembles
that of p-58 of (Hutchins, 2009) with some important differences. In the
remainder we will sometimes say ‘promotion’ instead of ‘subtyping reduction’.
A variable $x$ promotes to its annotation in the subtyping context, and every
term $u$ promotes to $\mathsf{Top}$ (rules Srs-Prom and Srs-Top). Promotion
subsumes equivalence reduction (rule Srs-Eq) where, differently form the
homonymous rule in (Hutchins, 2009), we include a prevalidity premiss (cf.
equivalence reduction above, which does not impose any prevalidity condition).

For applications $u\,v$, promotion keeps track of the operand $v$ by pushing
the operand on the continuation stack, and proceeds with the promotion of the
operator $u$ in the enlarged extended context in the premiss of rule Srs-App.
For functions $\lambda x\,{\leq}\,t.u$, we distinguish whether there is an
operand $\alpha$ on the top of the stack, or whether the continuation stack is
empty (rules Srs-FunOp and Srs-Fun respectively). In the former case (the
abstraction is applied to operand $\alpha$) the variable $x$ is annotated with
the operand and the annotation $x\,{\leq}\,\alpha$ is appended to the
subtyping context, and promotion proceeds with the body $u$ of the
abstraction. In the latter case (the abstraction is unapplied) promotion
proceeds as in (Hutchins, 2009) by appending the annotation $x\,{\leq}\,t$
from the formal parameter of the abstraction to the subtyping context and
proceeding to the promotion of body $u$. Thanks to rule Srs-FunOp, the formal
parameter of an applied abstraction must be promoted to the operand passed to
the abstraction, instead of to the annotation of the formal parameter in the
abstraction. This feature of our system is cornerstone to prove the
commutativity result, and the transitivity elimination and type-safety that
follow from commutativity. (The importance of commutativity is explained below
in this section.) Promoting to the operand instead of to the annotation in the
abstraction is harmless in derivations that involve well-formed terms, because
in any redex $(\lambda x\,{\leq}\,t.u)v$ the operand $v$ is a subtype of the
annotation $t$, and thus $u$ could always be further promoted to $t$ if
needed.

Both the equivalence reduction and the subtyping reduction are reflexive, as
shown by Lemma 2.2.

###### Lemma 2.2 (Reflexivity).

Let $\Gamma$ be a context, $s$ be a stack, and $u$ be a term, we have
$\Gamma;s\vdash u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u$,
and $u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u$.

The interaction between the subtyping context and the continuation stack
(rules Srs-App and SRS-FunOp) is reminiscent to the interaction of
_environment_ and _stack_ of the KAM (Krivine, 2007; Ager et al., 2003). Our
terms use variables names instead of the deBruijn indices of the KAM, but
capture of variables never occurs thanks to the prevalidity condition that
ensures that the variable names in the support of the subtyping context are
distinct from each other.

Figure 2 then defines the subtyping and equivalence relations, respectively
$\leq$ and $\equiv$, often representated by the meta-variable
$\vartriangleleft$ that stands for either relation (similarly,
$\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow}}}$ stands
for either $\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$ or
$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$). Both relations
are reflexive (rule As-Refl). The rules As-Left-1, As-Left-2, and As-Right
inform on how to extend the relations when viewed as a diagrammatic derivation
as follows:

$u\vartriangleleft t\quad\textup{iff}$
${t}$${v}$${u}$$\scriptstyle{\equiv}$$\scriptstyle{\vartriangleleft}$

A subtype derivation $v^{\prime}\leq t$ can be extended by appending a
vertical subtyping step
$v\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}v^{\prime}$ (rule
As-Left-1). An equivalence derivation $v^{\prime}\equiv t$ can be extended by
appending a vertical equivalence step
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$ (rule
As-Left-2). Any derivation $v\vartriangleleft t^{\prime}$ (equivalence or
subtyping) can be extended by appending a horizontal equivalence step
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$ (rule
As-Right). The well-formed derivation $\leq^{*}_{\mathrm{wf}}$ defined above
is stronger than this relation, as shown by the following Proposition 2.3.

###### Proposition 2.3 (From transitive well-subtyping to transitive
subtyping).

Let $\Gamma;s$ be an extended context and $u$ and $v$ be terms. If
$\Gamma;s\vdash u\leq^{*}_{\mathrm{wf}}v$ then $\Gamma;s\vdash u\leq^{*}v$.

In such diagrammatic derivations we always depict equivalence left-to-right
reduction steps in the horizontal, and either equivalence or subtyping bottom-
to-up reduction steps in the vertical. Since subtyping subsumes equivalence,
without loss of generality we can adopt the intuition that the horizontal
represents equivalence, and vertical represents subtyping. (But mind the
directions left-to-right and bottom-to-up.) Lemma 2.4 ensures the above
informal definition is accurate.

###### Proposition 2.4 (Diagrammatic representation of $\vartriangleleft$).

Let $\Gamma;s$ be an extended context. Let $u$ and $t$ be terms. We have
$\Gamma;s\vdash u\vartriangleleft t$ iff there exists a term $v$ such that
$\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$ and $\Gamma;s\vdash
t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$.

Finally, the optional rules Ast-Sub and Ast-Trans, which are similar to
homonymous rules in (Hutchins, 2009), add transitivity to the system. (Theorem
4.4 below states that transitivity is admissible in our system.) Transitive
relations (i.e., $u\vartriangleleft^{*}v$) shall not be mistaken with
multiple-step reduction (i.e.,
$u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$). As stated in the beginning of the section, our proof of
transitivity elimination proceeds by showing that rules Ast-Sub and Ast-Trans
are admissible in the system (more on this in Section 4).

Transitivity elimination holds if the two reduction relations above commute.
The diagrammatic representation of the relations clarifies this intuition.
Consider the transitive subtype derivation $\Gamma;s\vdash u\leq^{*}w$ that
follows from the elementary derivations $\Gamma;s\vdash u\leq v$ and
$\Gamma;s\vdash v\leq w$, with intermediary term $v$. The diagrammatic
derivation is depicted below:

${w}$..${v}$.${u}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\leq}$

The path containing solid edges corresponds to the transitive derivation,
which has the shape of a stair where each elementary relation stands for each
of the stair’s steps. The individual edges stand for multiple subtyping
reduction (in the vertical) and multiple equivalence reduction (in the
horizontal). If the two reductions commute, the diagram could be completed
with the dashed arrows, such that the path containing the top and right sides
of the diagram would correspond to the derivation $\Gamma;\mathrm{nil}\vdash
u\leq w$ free of transitive steps. Transitivity elimination in well-subtyping
derivations from Figure 1 above (i.e., $\leq^{*}_{\mathrm{wf}}$ and
$\leq_{\mathrm{wf}}$ are equivalent) is a direct consequence from the result
in this paragraph.

##  3\. Failure of Hutchins proof of transitivity elimination

Despite his efforts, Hutchins failed to show that commutativity holds in his
system, prevented him from proving transitivity elimination and type safety.
The culprit of this failure is the premature promotion of a formal parameter
in a abstraction to its annotation in the abstraction, instead of being
promoted to the operand that has been passed to the abstraction. We illustrate
Hutchins’ failure of commutativity by pinpointing the relevant case and
depicting it side by side with the corresponding case in our system.

${(\lambda x\,{\leq}\,t.t)v}$${t}$${(\lambda
x\,{\leq}\,t.x)v}$${v}$$\scriptstyle{\equiv}$$\scriptstyle{\leq_{H}}$$\scriptstyle{\equiv}$$\scriptstyle{?}$${(\lambda
x\,{\leq}\,t.v)v}$${v}$${(\lambda
x\,{\leq}\,t.x)v}$${v}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

We use $\mathop{\stackrel{{\scriptstyle\leq_{H}}}{{\longrightarrow}}}$ to
denote Hutchins subtyping reduction. On the left (Hutchins’) the redex
$(\lambda x\,{\leq}\,t.x)v$ on the bottom-left corner of the diagram is
reduced (in the horizontal) to $v$, and promoted (in the vertical) to
$(\lambda x\,{\leq}\,t.t)v$, where variable $x$ is prematurely promoted to its
annotation $t$. The right edge of the diagram cannot be completed with a
single elementary subtyping reduction. Hutchins’ system require that we have
$v\leq^{*}t$ to do the $\beta$-reduction, so we can complete the diagram in
multiple steps, but unfortunately this is not the required global
commutativity for the type safety. Hutchins resorted to the _decreasing
diagrams_ technique of (Van Oostrom, 1994) to prove global commutativity from
its commutativity, but he failed in assigning depths to each reduction step as
to show that depth decreases in the way prescribed by the decreasing diagrams
technique because $\beta$-reduction may increase this depth (i.e., the depth
of $(\lambda
x\,{\leq}\,t.x)v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}x[x\backslash
v]=v$ is one plus the maximum of the depth of all the reduction of
$v\leq^{*}t$, which can contain $\beta$-reduction as well that result in an
infinite depth). Hutchins himself explains this failure in detail in his PhD
thesis (Section 2.7: Confluence and commutativity)(Hutchins, 2009).

On the right of the diagram (ours) the redex $(\lambda x\,{\leq}\,t.x)v$ on
the bottom-left corner of the diagram is reduced (in the horizontal) to $v$,
but instead the redex is promoted (in the vertical) to $(\lambda
x\,{\leq}\,t.v)v$, thanks to our subtyping reduction with a continuation stack
that keeps track of the operands than have been passed. We complete the right
edge of the diagram trivially with an elementary reflexive promotion form $v$
to $v$, and we directly obtain the diamond property for subtyping and
equivalence reduction, by structural induction on terms, without the
decreasing diagrams technique. This difference is illustrated in the detailed
example of application of our proof of transitivity elimination in the next
section. The example will make clear the importance of exposing the
intermediary step $(\lambda x\,{\leq}\,t.t)v$, absent in Hutchins’ system,
which enables the application of the induction hypothesis in our proof of
transitivity elimination.

##  4\. Proof of type safety

As we’ve commented at length in Section 1 and in the rest of the paper, PSS is
not strongly normalising. Therefore, type soundness in PSS can only be stated
in terms of type safety defined as progress and preservation (Wright and
Felleisen, 1994; Harper, 2016).

###### Theorem 4.1 (Progress).

Let $t$ be a term. For every extended context $\Gamma;s$, if $\Gamma;s\vdash
t~{}\mathrm{wf}$ then either $t$ is in normal form, or there exists a term
$t^{\prime}$ such that $t\mapsto t^{\prime}$.

The progress theorem states that computation in PSS cannot get stuck. Given a
well-formed term (i.e., well-subtyped), the term is either a normal form (a
result) or otherwise we can reduce it further. The missing part in Hutchins’
theory for type safety is the preservation theorem below that states that
reduction in PSS preserves well-subtyping.

###### Theorem 4.2 (Preservation).

Let $\Gamma;s$ be an extended context. Let $t$, $t^{\prime}$, and $u$ be
terms. If $\Gamma;s\vdash t\leq^{*}_{\mathrm{wf}}u$ and $t\mapsto t^{\prime}$,
then $\Gamma;s\vdash t^{\prime}\leq^{*}_{\mathrm{wf}}u$.

The progress theorem rests on the lemma below that states that no function
type is a supertype of $\mathsf{Top}$.

###### Theorem 4.3 (No supertype of Top).

Let $\Gamma;s$ be an extended context. Let $\lambda x\,{\leq}\,t.u$ be a term.
We cannot have $\Gamma;s\vdash\mathsf{Top}\leq^{*}_{\mathrm{wf}}\lambda
x\,{\leq}\,t.u$.

All three theorems above rest on the transitivity elimination, which was the
missing piece in Hutchins’ theory. In the context of higher-order subtyping,
transitivity elimination is known to be crucial to prove type safety (Pierce,
2002; Pierce and Steffen, 1997). In order to remove transitivity from our
system, we remove the commutation by Theorem 4.5 which uses a reduction of
extended context in its induction, which is defined in Figure 3.

###### Theorem 4.4 (Transivity is admissible in the algorithmic system).

Let $\Gamma;s$ be an extended context. Let $u$ and $v$ be terms. If
$\Gamma;s\vdash u\leq^{*}v$ then $\Gamma;s\vdash u\leq v$.

Equivalence reduction for extended context:
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$ *[right=Ctx-Annotation] Γ;
s ↣Γ’; s’ t ⟶≡ t’ Γ, x ≤ t; s ↣Γ’, x ≤ t’; s’

*[right=Ctx-Stack] Γ; s ↣Γ’; s’ α⟶≡ α’ Γ; α:: s ↣Γ’; α’ :: s’

*[right=Ctx-Sym] Γ; s ↣Γ; s

Figure 3. Definition of the equivalence reduction for extended context.

###### Theorem 4.5
($\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$ and
$\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$ strongly
commute).

Let $\Gamma;s$ be an extended context. Let $t_{0}$, $t_{1}$ and $t_{2}$ be
terms. If
$t_{0}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t_{1}$ and
$\Gamma;s\vdash
t_{0}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t_{2}$ then for
all enlarged context $\Gamma^{\prime};s^{\prime}$ with
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$ (defined in Figure 3),
there exists a term $t_{3}$, such that
$t_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t_{3}$ and
$\Gamma^{\prime};s^{\prime}\vdash
t_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t_{3}$.

Diagrammatically,

${t_{2}}$${t_{3}}$${t_{0}}$${t_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\leq}$

where the enlarged contexts $\Gamma;s$ and $\Gamma^{\prime};s^{\prime}$ are
omitted in the two vertical edges, and where the solid arrows are the
conditions for the existence of the dashed arrows.

A slight difference with Hutchins’ theory is that we do not need an inversion
lemma to conclude about type safety. The inversion lemma states that if
$(\lambda x\,{\leq}\,t.u)\leq^{*}(\lambda x\,{\leq}\,t^{\prime}.u^{\prime})$,
then the type annotations of their formal parameters are equivalent, i.e.,
$t\equiv^{*}t^{\prime}$. Hutchins’ theory needs this lemma in one subcase of
the proof of preservation, where one needs to show that $u[x\backslash v]$ is
well-formed from $(\lambda x\leq t.u)v$ being well-formed: in this subcase, we
know that $u$ is well-formed in the context $x\leq t$, and it’s impossible to
conclude that $u[x\backslash v]$ is well-formed because there is no structural
relation between $t$ and $v$, we only know that there exists $t^{\prime}$ such
that $\lambda x\leq t.u\leq^{*}\lambda x\leq t^{\prime}.\mathsf{Top}$ and
$v\leq^{*}t^{\prime}$. The inversion lemma is used to conclude that
$v\leq^{*}t^{\prime}\equiv t$ and finish the proof. In our version, the use of
a stack that track operands removes this complexity, as in the above subcase
we already have that $u$ is well-formed in the context $x\leq v$, which allow
us to conclude immediately.

###  4.1. An example of transitivity elimination

We present an example that illustrates the proof of Lemma 4.4, which is the
main contribution of our paper and was missing in Hutchins works. This lemma
states that we can remove any application of transitivity in an algorithmic
derivation.

Consider two terms $a$ and $A$ such that $a\leq^{*}A$ exists which may
possibly use transitivity and be as lengthy or complicated as it may be.
Consider $(\lambda x\leq A.x)\,a$ and $(\lambda x\leq A.a)\,a$ and $(\lambda
x\leq A.A)\,a$ which will be our three main terms for this example. We denote
$\leq^{*}_{H}$ and
$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}_{H}$ the notions
transitive subtyping and subtype reduction in Hutchins’ theory. The
relationship between the terms of our example is illustrated in Figure 4.

$\begin{array}[]{rcl}A&=&\langle\text{arbitrary type}\rangle\\\
a&=&\langle\text{arbitrary subtype of $A$}\rangle\\\
\varepsilon;\mathrm{nil}\vdash a&\leq^{*}&A\\\ \\\
\varepsilon;\mathrm{nil}\vdash(\lambda x\leq
A.x)\,a&\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}&(\lambda
x\leq A.a)\,a\\\ \varepsilon;\mathrm{nil}\vdash(\lambda x\leq
A.a)\,a&\leq^{*}&(\lambda x\leq A.A)\,a\\\
\varepsilon;\mathrm{nil}\vdash(\lambda x\leq A.x)\,a&\leq^{*}&(\lambda x\leq
A.A)\,a\\\ \\\ \varepsilon\vdash(\lambda x\leq
A.x)\,a&\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}_{H}&(\lambda
x\leq A.A)\,a\\\ \end{array}$ Figure 4. Terms of our example

It is also worth noting that Hutchins’ system do not have a stack, hence the
lack of stack in the last statement of Figure 4. In our system, the subtype
relation $\varepsilon;\mathrm{nil}\vdash(\lambda x\leq A.a)\,a\leq^{*}(\lambda
x\leq A.A)\,a$ comes from $a\leq^{*}A$ which then allow to conclude that
$\varepsilon;\mathrm{nil}\vdash(\lambda x\leq A.x)\,a\leq^{*}(\lambda x\leq
A.A)\,a$. On the contrary, in Hutchins’ system, the subtype reduction
$\varepsilon\vdash(\lambda x\leq
A.x)\,a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}_{H}(\lambda
x\leq A.A)\,a$ is a single step no matter the complexity of $a\leq^{*}A$. How
these subtype relations are built is illustrated Figure 5, where the left part
is our system whereas the right part is Hutchins’ system.

${(\lambda x\,{\leq}\,A.A)\,a}$.${A}$${(\lambda
x\,{\leq}\,A.A)\,a}$${A}$...${(\lambda x\,{\leq}\,A.a)\,a}$${(\lambda
x\,{\leq}\,A.x)\,a}$${a}$${(\lambda
x\,{\leq}\,A.x)\,a}$${a}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{a\leq^{*}A}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\leq_{H}}$$\scriptstyle{\equiv}$$\scriptstyle{a\leq^{*}A}$$\scriptstyle{\leq_{H}}$$\scriptstyle{\equiv}$$\scriptstyle{a\leq_{H}^{*}A?}$
Figure 5. Illustration of transivity elimination

Our proof of transitivity elimination is possible in our system thanks to the
operand stack and rule Srs-FunOp which force to expose the term $(\lambda
x\,{\leq}\,A.a)a$ when we try to derive $(\lambda x\leq
A.x)\,a\leq^{*}(\lambda x\leq A.A)\,a$. It forces the derivation $(\lambda
x\,{\leq}\,A.a)a\leq^{*}(\lambda x\,{\leq}\,A.A)a$ in the middle of the
diagram which preserves the possibly convoluted derivation $a\leq^{*}A$ as a
sub-derivation (marked with a dashed line instead of an arrow in the figure).
Although preserving this convoluted derivation seems at first glance counter-
intuitive, it gives the opportunity to apply the induction hypothesis of the
Lemma 4.4 to the term $(\lambda x\,{\leq}\,A.a)a$, which will flatten the
convoluted derivation. Contrary to ours, Hutchins’ attempts at proving that
transitivity is admissible reduce the complexity of the intermediary step by
avoiding the convoluted derivation upfront (by directly taking the reduction
$(\lambda
x\,{\leq}\,A.x)a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}(\lambda
x\,{\leq}\,A.A)a$ which promotes the variable $x$ to its annotation $A$). But
this premature promotion of a formal parameter to its type annotation is in
fact counter-productive, which manifests in the failure of Hutchins proof of
the commutativity lemma, where the premature promotion prevents one to
complete the diagram for redexes with a transitivity-free right edge, as we
have explained at length in Section 2.

The next section reformulates Hutchins’ practical algorithm for subtyping in
(Section 2.8)(Hutchins, 2009).

##  5\. Practical algorithm

The well-formedness condition of section 2 is akin to the well-typed condition
in traditional type system which ensures that we can always reduce a well-
formed term if it’s not a normal form, and the property is preserved when
executing the term by type safety, which is a static condition. In this
section we build an algorithm that determines if a given term is well-formed.

This algorithm relies on the notion of minimal promotion of terms, which
promotes a term $u$ in normal norm to $v$ such that for any promotion of $u$
to $w$ there exists promotions to do from $v$ to obtain $w$. It then relies on
the notion of _minimal superpath_ of a term $u$, which is a minimal because
any term in normal form $t_{n}$ such that $\Gamma;s\vdash u\leq t_{n}$ will be
a term of this path. Then, we show an algorithm to compute $\Gamma;s\vdash
u\leq t$, which simply reduces $t$ to its normal form and checking if it’s in
the minimal superpath of $u$. And finally, we introduce our typecheck
algorithm that relies on the above notions, and determines if $\Gamma;s\vdash
u~{}\mathrm{wf}$.

It is worth noting that we partially collect and reformulate intuition in the
original work (Hutchins, 2009) to present a slightly different sequence of
lemmas and algorithms, with our different system.

Minimal promotion:  $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\mathrm{mp}}}{{\longrightarrow}}}v$ *[] u ／∈NF
u ⟶→ ≡ u_n Γ; s ⊢u ⟶mpu_n

*[] m ≥0 x ≤t ∈Γ Γ; s ⊢x u_1n ⋯u_mn ⟶mpt u_1n ⋯u_mn

*[] Γ, x ≤t_n; nil⊢u_n ⟶mpu’ Γ; nil⊢λx ≤ t_n. u_n ⟶mpλx ≤ t_n. u’

*[] Γ, x ≤α; nil⊢u_n ⟶mpu’ Γ; α:: s ⊢λx ≤ t_n. u_n ⟶mpλx ≤ t_n. u’

*[] Γ; s ⊢λx ≤ t_n. Top⟶mpTop

Subtyping algorithm:  $\Gamma;s\vdash u{\,\textsc{st}\,}t$ *[] Γ; s ⊢u st t_n
t ⟶→ ≡ t_n Γ; s ⊢u st t

*[] Γ; s ⊢t_n st t_n

*[] Γ; s ⊢u ⟶mpu’ Γ; s ⊢u’ st t_n Γ; s ⊢u st t_n

Well-formedness algorithm: $\Gamma;s\vdash u{~{}\textsc{wf}}$ *[] Γ; s ⊢Top wf

*[] x ≤t ∈ΓΓ; s ⊢t wf Γ; s ⊢x wf

*[] Γ, x ≤t; nil⊢u wfΓ; nil⊢t wf Γ; nil⊢λx ≤ t. u wf

*[] Γ, x ≤α; s ⊢u wfΓ; nil⊢t wf Γ; α:: s ⊢λx ≤ t. u wf

*[] Γ; v :: s ⊢u ⟶→ mpλx ≤t_n. TopΓ; nil⊢v st t_n
Γ; v :: s ⊢u wfΓ; nil⊢v wfΓ; nil⊢t_n wfΓ; v :: s ⊢λx ≤t_n. Top wf Γ; s ⊢u v wf

Figure 6. Definition of our algorithms

To find the minimal superpath of terms we introduce the concept of minimality
for subtyping, that strive to quantify the least amount of promotion to do,
and that for instance delay as most as possible top promotions. We first
introduce with 5.2 our definition of minimality, and prove that what we call
minimal promotion is indeed minimal for that definition. This concept is
essentially the same as in Hutchins’ theory.

###### Lemma 5.1 (Minimal promotion is well defined).

Let $\Gamma;s$ be an extended context. Let $u$ be a term. If $u$ is not
$\mathsf{Top}$, then there exists a unique term $v$ such that $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\mathrm{mp}}}{{\longrightarrow}}}v$.

###### Definition 5.2 (Definition of subtype minimality).

Let $\Gamma;s$ be an extended context. Let $u_{n}$ be a term in normal form.
Let $v$ be such that $\Gamma;s\vdash
u_{n}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}v$. The
promotion $\Gamma;s\vdash
u_{n}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}v$ is said to be
_minimal_ if for all terms $w$ such that $\Gamma;s\vdash
u_{n}\mathop{\stackrel{{\scriptstyle\,{\leq}\,}}{{\longrightarrow}}}w$, then
$\Gamma;s\vdash
v\mathop{\stackrel{{\scriptstyle\,{\leq}\,}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$.

Minimal promotion are minimal in the sense of the following diagram:

${v}$${w}$${u_{n}}$$\scriptstyle{\leq}$$\scriptstyle{\leq}$$\scriptstyle{\mathrm{mp}}$

###### Lemma 5.3 (Minimal promotion is indeed minimal).

Promotions $\mathop{\stackrel{{\scriptstyle\mathrm{mp}}}{{\longrightarrow}}}$
are always minimal.

###### Definition 5.4 (Definition of the minimal superpath).

Let $\Gamma;s$ be an extended context. For any term $u$, we call the minimal
superpath of $u$ in $\Gamma;s$ the iteration of
$\mathop{\stackrel{{\scriptstyle\mathrm{mp}}}{{\longrightarrow}}}$ on $u$ in
context $\Gamma;s$.

The minimal superpath is the iteration of the minimal promotion. In the
minimal superpath below every horizontal step is an application of Srs-Eq, and
every vertical step is an application of a another Srs- rule.

${\mathsf{Top}}$${u^{\prime}}$${u^{\prime}_{n}}$${u}$${u_{n}}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\cdots}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\mathrm{mp}}$

Thanks to this minimal superpath, we can now obtain an algorithm that
determines whether $\Gamma;s\vdash u\leq v$ for any $\Gamma;s$, which we do
now.

As before, we introduce an algorithm that determines if $\Gamma;s\vdash u\leq
v$ for any extended context $\Gamma;s$ and any terms $u$ and $v$, that
applies, when possible, rules given in 6, and otherwise terminates returning
no result. The algorithm is essentially the same as in Hutchins’ theory. Lemma
5.5 ensures correctness.

###### Theorem 5.5 (Correctness of the subtyping algorithm).

Let $\Gamma;s$ be an extended context. Let $u$ and $t$ be terms. If the
algorithm terminates on $\Gamma,s,u,t$ and returns $\Gamma;s\vdash
u{\,\textsc{st}\,}t$ then we have $\Gamma;s\vdash u\leq t$. If $\Gamma;s\vdash
u\leq t$ and the algorithm terminates on $\Gamma,s,u,t$, then it returns
$\Gamma;s\vdash u{\,\textsc{st}\,}t$.

The algorithm checks if the normal form of the left term cross the minimal
superpath of the right term, as depicted below:

${\mathsf{Top}}$${t}$${t_{n}}$${u^{\prime}}$${u^{\prime}_{n}}$${u}$${u_{n}}$$\scriptstyle{\equiv}$$\scriptstyle{\cdots}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\cdots}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\mathrm{mp}}$$\scriptstyle{\mathrm{mp}}$

With these two algorithms, we can finally check if a term is well-formed in a
given context.

As before, we introduce an algorithm that determines if $\Gamma;s\vdash
u~{}\mathrm{wf}$ for any extended context $\Gamma;s$ and any term $u$ that
applies, when possible, rules given in 6, and otherwise terminates returning
no result. Lemma 5.6 ensures correctness.

###### Theorem 5.6 (Correctness of the well-formedness algorithm).

Let $\Gamma;s$ be an extended context, such that $\Gamma;s$ is prevalid. Let
$u$ be a term. If the algorithm terminates on $\Gamma,s,u$ and returns
$\Gamma;s\vdash u{~{}\textsc{wf}}$, then we have $\Gamma;s\vdash
u~{}\mathrm{wf}$. If $\Gamma;s\vdash u~{}\mathrm{wf}$ and the algorithm
terminates on $\Gamma,s,u$, then it returns $\Gamma;s\vdash
u{~{}\textsc{wf}}$.

Now we study incremental typechecking which may be crucial if we are
interested in incremental compilation. If we have a function $f$ that
typechecks, we would like to not typecheck $f$ again everytime we write an
application $f(x)$. In Hutchins’ theory, well-formedness is not dependent on
the context, and therefore it’s incremental without any change. For
incremental typechecking we need the inversion lemma below. Theorem 5.8
ensures we can replace the application case of the algorithm by this new rule
given below, on which the requirement $\Gamma;v::s\vdash u{~{}\textsc{wf}}$
has been replaced by $\Gamma;s\vdash u{~{}\textsc{wf}}$ and some others. *[] u
= λx ≤t’. b’ Γ; nil⊢v st t’ Γ; s ⊢u wfΓ; nil⊢v wfΓ; nil⊢t’ wf
for some (Γ’; s’). Γ’; s’ ⊢v wf∧Γ’; s’ ⊢v st t’ Γ; s ⊢u v wf

###### Lemma 5.7 (Inversion lemma).

Let $\Gamma;s$ be an extended context. Let $\lambda x\,{\leq}\,t.u$ and
$\lambda x\,{\leq}\,t^{\prime}.u^{\prime}$ be terms. If
$\Gamma;s\vdash(\lambda x\,{\leq}\,t.u)\leq^{*}(\lambda
x\,{\leq}\,t^{\prime}.u^{\prime})$ then $\Gamma;s\vdash t\equiv t^{\prime}$.

###### Theorem 5.8 (Composability of the typechecking).

Let $u=\lambda x\leq t^{\prime}.b^{\prime}$ and $v$ be terms. Assume $u$ is in
normal form. Assume $\Gamma;s\vdash u~{}\mathrm{wf}$.

We have that $\Gamma;s\vdash u\,v{~{}\textsc{wf}}$ if
$\Gamma;\mathrm{nil}\vdash v{~{}\textsc{wf}}$ and $\Gamma;\mathrm{nil}\vdash
t^{\prime}{~{}\textsc{wf}}$ and for all $\Gamma^{\prime};s^{\prime}$ extended
context where the variable $x$ appear in $u$,
$\Gamma^{\prime};s^{\prime}\vdash v{~{}\textsc{wf}}$ and
$\Gamma^{\prime};s^{\prime}\vdash v{\,\textsc{st}\,}t^{\prime}$.

Our typechecking algorithm is unfortunatly neither terminating nor complete
and undecidable. Consider $\Omega=(\lambda x\leq\mathsf{Top}.xx)(\lambda
x\leq\mathsf{Top}.xx)$. It is not terminating because of terms that do not
have a normal form such as $\Omega$: the iteration of
$\mathop{\stackrel{{\scriptstyle\mathrm{mp}}}{{\longrightarrow}}}$ will
doesn’t terminates on that term. It is not complete because of terms such as
$\Omega$, which do verify $\Gamma;s\vdash\Omega\leq\Omega$ but the algorithm
will first reduces $\Omega$ to its normal form and never terminates.

Finding a decidable algorithm is an open problem. In general any such
algorithm will be undecidable, due to terms that do have a normal form, as is
undecidable to verify if two terms have the same normal form. In Section 7 we
discuss wheter a notion of solvability exists that would help in making the
algorithm applicable to some pathological terms.

##  6\. Related work

There is mainly two philosophies about dependent types. Either there are an
extension of the regular language, for instance Cayenne (Augustsson, 1998),
Idris (Brady, 2013) or Haskell (Marlow et al., 2010). Otherwise the main use
is theorem proving, for instance Coq (Coquand and Huet, 1986) or Agda (Bove et
al., 2009). We are in neither approach, PSS harmoniously mixes terms and as
such dependent types are de facto in the language and are not an extension,
but our language is not strongly normalising, and therefore the main goal is
not theorem proving as we cannot use the langage as such (below we comment on
approaches that overcome these limitations).

Other attempts to unify typing and subtyping, or to combine non-termination
with dependent types have been made. We present here the most relevant ones
that we are aware.

In 1997, Chen proposed $\lambda_{C_{\leq}}$ (Chen, 1997), an extension of the
calculus of constructions $\lambda_{C}$ with subtyping. Chen’s
$\lambda_{C_{\leq}}$ supports neither top types nor bounded quantification in
order to simplify the meta-theory.

Aspinall studied the combination of subtyping with singleton types (Aspinall,
1994). Singleton types are close to what we study, as in our calculus terms
can be seen as singleton types of this unique value. We have for instance for
every terms $t$, $\epsilon\vdash t\leq t$, that would be translated to $\vdash
t:\\{t\\}$ in a system with singleton types.

A more conservative attempt that tries to unify typing and subtyping is (Yang
and Oliveira, 2017). This work has two major differences with our approach.
First, in (Yang and Oliveira, 2017) the subtyping relation still tracks types
(their unification of subtyping and typing is more conservative than ours).
Second, in PSS functions and functions (sub)types are defined with the same
syntax, and therefore they are both instances of the same construct, which is
not the case in (Yang and Oliveira, 2017).

The origin of mixing terms and types goes back to the introduction of pure
type systems (McKinna and Pollack, 1993) which generalises the seminal works
on lambda calculi with types by (Barendregt et al., 1992). These systems have
the ability to unify types and terms under the same kind, but there is a
typing relation instead of a subtyping one. Moreover, in some of these pure
type systems, the type $\bot$ is inhabited. This gives rise to the well-known
as Girard’s paradox (see (Hurkens, 1995)). In our system, there is not a
primitive $\bot$ subtype, but we could encode such a subtype to be inhabited
by itself, and that would be unproblematic since our aim is not to use PSS as
a theorem prover.

A very interesting approach is the $\lambda^{\theta}$ of (Casinghino, 2014;
Casinghino et al., 2014; Sjoberg, 2015), which combines proofs and program
into a single language that distinguishes two fragments, a logical fragment
where every term is strongly normalising that is suited to write proofs, and a
programmatic fragment that is Turing complete and lacks termination. Such
systems allow so-called _freedom of speech_ , which is the ability to write
(terminating) proofs about non-terminating terms.

Various extensions of System F have been considered in the literature. Within
these we find System F≤ (Cardelli et al., 1994) and System
F${}_{\leq}^{\omega}$ (Pierce and Steffen, 1997), which respectively add
subtyping and higher-order subtyping capabilities. PSS subsumes the version of
System F≤ without contravariant arrow-types (Hutchins, 2009).

Hutchins first introduce his version of PSS in (Hutchins, 2009, 2010), but
couldn’t prove the type safety. His PSS is different from our version mainly
because of the stack mechanism: indeed in our system, variables need to be
promoted to their argument if applicable, and can be promoted to their type
annotation if the function isn’t applied, whereas in Hutchins theory variable
can always be promoted to their type annotation, and therefore Hutchins’
theory do not have a stack as in our system. While both system look similar,
the relationship between them is left for future work. We also tried to add a
stack only into Hutchins’ algorithmic system, and keep Hutchins’ proofs
intact, but it’s then very hard to link the algorithmic system to the
declarative system that doesn’t have a stack.

##  7\. Future work

To the best of our knowledge, whether Hutchins’ PSS (or our PSS for that
matter) is Turing-complete can only be conjectured. The argument for Turing-
completeness rests on the existence of (well-formed) looping combinator in
PSS, which would consist of a family of terms $L_{n}$ such that $L_{n}\,f$
reduces to $f(L_{n+1}\,f)$ for any $f$. Such looping combinator exists for
System $\lambda*$ (Howe, 1987) which can be encoded into our PSS version with
the translation from System $\lambda*$ to Hutchins’ PSS provided on page 47 of
(Hutchins, 2009). In order to establish Turing-completeness of PSS, one should
now adapt the argument made by (Geuvers and Verkoelen, 2009) in Section 2 or
the argument made in (Hindley and Seldin, 2008). There is however no simple
known expression of a looping combinator in System $\lambda*$. The family from
(Howe, 1987) can only be derived mechanically, and working with it directly is
proven to be hard as its length is more than 40 pages (see the discussion on
the logical consistency and impredicativity of System
$\lambda_{\vartriangleleft}$ on pages of 48–51 of (Hutchins, 2009)), it may
therefore be difficult to conclude about Turing-completeness. Establish
whether PSS is Turing-complete or not is left as future work.

The condition upon which our algorithms terminate is also left for future
work. The non-termination comes from terms that do not have a normal form.
Consider for instance $\Omega=(\lambda x\leq\mathsf{Top}.xx)(\lambda
x\leq\mathsf{Top}.xx)$. This term is not strongly normalizing, and our
algorithms doesn’t terminate on that term. But other pathological terms
exists, consider $\Omega^{\prime}=\lambda y\leq(\lambda
x\leq\mathsf{Top}.xx).(y(\lambda x\leq\mathsf{Top}.xx))$, which has a normal
form but doesn’t terminate in our algorithms, as when the variable $y$ is
promoted with
$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}_{Min}$, it
transforms $\Omega^{\prime}$ into $\Omega$. Term $\Omega^{\prime}$ is
pathological since any use of $\Omega^{\prime}$ may be considered absurd:
indeed, pick any term $z$ such that $z\leq\lambda x\leq\mathsf{Top}.xx$. We
have
$\Omega^{\prime}z\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}z(\lambda
x\leq\mathsf{Top}.xx)\leq(\lambda x\leq\mathsf{Top}.xx)(\lambda
x\leq\mathsf{Top}.xx)=\Omega$ which doesn’t have a normal form. Term
$\Omega^{\prime}z$ can never be used ”in a useful way” in a computation, as it
never reduces to a function: suppose it reduces to $\lambda x\leq a.b$, by
commutativity we have $\lambda x\leq
a.b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}\lambda x\leq a^{\prime}.b^{\prime}$ and thus
$\Omega\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}\lambda x\leq a^{\prime}.b^{\prime}$, which is a contradiction.
This reasoning is also possible if all possible use of $\Omega^{\prime}$ are
absurd. We therefore conjecture that a notion of operational relevance
(i.e.solvability) may have an important role in the termination of the
typechecking problem. It is left for future work to provide another algorithm
with stronger termination guarantees.

Another interesting area to explore is the link between our system and
Hutchins’ system. We conjecture that a well-formed term in our system is well-
formed in Hutchins’ system, and that the opposite holds if the inversion lemma
holds in Hutchins’ system (i.e.if Hutchins’ theory is type-safe). We also
conjecture that every well-formed derivation hold in both system, and as such
that both theory are equivalent for a precise meaning to be determined. It is
left as future work.

We also believe the missing point in Hutchins’ proof can be found in our
approach. Hutchins’ proof need an induction principle on reductions for the
decreasing diagram technique. Because our reduction commutes, the constant
depth of $1$ works in our system. And because most Hutchins reduction can be
rewritten in terms of our reductions, picking a depth that is the number of
our relation that needs to be done to replace a given relation in his system
may lead to a working induction principle. Exploring this idea, defining a
depth function with a stack, and proving the type safety of Hutchins’ theory
is also left for future work.

##  8\. Conclusion

This paper presents a reformulation of the PSS originally introduced by
Hutchins in (Hutchins, 2009), and proves that our reformulation is type safe,
a result that has remained elusive for more than a decade. To the best of our
knowledge PSS is the first type-safe theory that unifies harmoniously terms
and types by using a single kind where everything is a subtype.

We present a type-checking algorithm that makes this theory usable in
practise.

Meta-theories of languages with advanced features on types are notoriously
difficult to work with. We believe our work could help in laying the
foundations for a new approach that mixes terms and types in innovative ways.

## References

  * (1)
  * Ager et al. (2003) M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard. 2003\.  A functional correspondence between evaluators and abstract machines. In _Proceedings of International Conference on Principles and Practice of Declarative Programming_. 8–19.
  * Aspinall (1994) David Aspinall. 1994\.  Subtyping with singleton types. In _International Workshop on Computer Science Logic_. Springer, 1–15.
  * Augustsson (1998) Lennart Augustsson. 1998\.  Cayenne—a language with dependent types.  _ACM SIGPLAN Notices_ 34, 1 (1998), 239–250.
  * Barendregt et al. (1992) Henk Barendregt, S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, and H. P. Barendregt. 1992\.  Lambda Calculi with Types.  (1992), 117–309.
  * Bove et al. (2009) Ana Bove, Peter Dybjer, and Ulf Norell. 2009.  A brief overview of Agda–a functional language with dependent types. In _Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22_. Springer, 73–78.
  * Brady (2013) Edwin Brady. 2013\.  Idris, a general-purpose dependently typed programming language: Design and implementation.  _Journal of functional programming_ 23, 5 (2013), 552–593.
  * Cardelli et al. (1994) Luca Cardelli, Simone Martini, John C Mitchell, and Andre Scedrov. 1994.  An extension of system F with subtyping.  _Information and computation_ 109, 1-2 (1994), 4–56.
  * Casinghino (2014) Chris Casinghino. 2014\.  _Combining proofs and programs_.  University of Pennsylvania.
  * Casinghino et al. (2014) Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014\.  Combining proofs and programs in a dependently typed language.  _ACM SIGPLAN Notices_ 49, 1 (2014), 33–45.
  * Chen (1997) Gang Chen. 1997\.  Subtyping calculus of construction. In _International Symposium on Mathematical Foundations of Computer Science_. Springer, 189–198.
  * Coquand and Huet (1986) Thierry Coquand and Gérard Huet. 1986.  _The calculus of constructions_.  Ph. D. Dissertation. INRIA.
  * Geuvers and Verkoelen (2009) Herman Geuvers and Joep Verkoelen. 2009.  On fixed point and looping combinators in type theory.
  * Harper (2016) Robert Harper. 2016\.  _Practical Foundations for Programming Languages (2nd. Ed.)_.  Cambridge University Press.  https://www.cs.cmu.edu/~rwh/pfpl/index.html
  * Hindley and Seldin (2008) J. Roger Hindley and Jonathan P. Seldin. 2008.  _Lambda-Calculus and Combinators, An Introduction, 2nd Edition, 2008. Hardback, ISBN 9780521898850_.  Cambridge University Press.
  * Howe (1987) Douglas J. Howe. 1987\.  The Computational Behaviour of Girard’s Paradox. In _Proceedings of the Symposium on Logic in Computer Science (LICS’87), Ithaca, New York, USA, June 22-25, 1987_. IEEE Computer Society, 205–214.
  * Hurkens (1995) Antonius J. C. Hurkens. 1995\.  A simplification of Girard’s paradox. In _Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi and Applications, TLCA’95 Edinburgh, United Kingdom, April 10–12, 1995 Proceedings 2_. Springer, 266–278.
  * Hutchins (2009) DeLesley Hutchins. 2009\.  _Pure subtype systems: A type theory for extensible software_.  Ph. D. Dissertation. The University of Edinburgh.
  * Hutchins (2010) DeLesley S. Hutchins. 2010\.  Pure Subtype Systems. In _Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’10)_. Association for Computing Machinery, 287–298.
  * Krivine (2007) J.-L. Krivine. 2007\.  A call-by-name lambda-calculus machine.  _Higher-Order and Symbolic Computation_ 20, 3 (2007), 199–207.
  * Marlow et al. (2010) Simon Marlow et al. 2010\.  Haskell 2010 language report.  _Available online http://www. haskell. org/(May 2011)_ (2010).
  * McKinna and Pollack (1993) James McKinna and Robert Pollack. 1993.  Pure type systems formalized. In _Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications TLCA’93 March, 16–18, 1993, Utrech, The Netherlands Proceedings 1_. Springer, 289–305.
  * Milner (1978) Robin Milner. 1978\.  A Theory of Type Polymorphism in Programming.  _J. Comput. Syst. Sci._ 17, 3 (1978), 348–375.
  * Pierce and Steffen (1997) Benjamin Pierce and Martin Steffen. 1997.  Higher-order subtyping.  _Theoretical computer science_ 176, 1-2 (1997), 235–282.
  * Pierce (2002) Benjamin C. Pierce. 2002\.  _Types and programming languages_.  MIT Press.
  * Sjoberg (2015) Vilhelm Sjoberg. 2015\.  _A dependently typed language with nontermination_.  University of Pennsylvania.
  * Steffen and Pierce (1994) Martin Steffen and Benjamin C. Pierce. 1994.  _Higher-Order Subtyping_.  Technical Report. University of Edinburgh.  ECS-LFCS-94-280.
  * Van Oostrom (1994) Vincent Van Oostrom. 1994\.  Confluence by decreasing diagrams.  _Theoretical computer science_ 126, 2 (1994), 259–280.
  * Wright and Felleisen (1994) Andrew K. Wright and Matthias Felleisen. 1994.  A Syntactic Approach to Type Soundness.  _Inf. Comput._ 115, 1 (1994), 38–94.
  * Yang and Oliveira (2017) Yanpeng Yang and Bruno C d S Oliveira. 2017.  Unifying typing and subtyping.  _Proceedings of the ACM on Programming Languages_ 1, OOPSLA (2017), 1–26.

##  Appendix A Lemmas of Section 2

Proposition 2.4 (Diagrammatic representation of $\vartriangleleft$). Let
$\Gamma;s$ be an extended context. Let $u$ and $t$ be terms. We have
$\Gamma;s\vdash u\vartriangleleft t$ iff there exists a term $v$ such that
$\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$ and $\Gamma;s\vdash
t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$.

###### Proof.

We first prove that if $\Gamma;s\vdash u\vartriangleleft t$ then there exists
a term $v$ such that $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$. The converse is proven after.

We prove this case by induction on the derivation tree of $\Gamma;s\vdash
u\vartriangleleft t$. For the base case (the last rule applied is As-Refl),
the results hold because we have as hypothesis $u=t$, so we pick $v=u$ and it
works by reflexivity (Lemma 2.2).

For the general cases, consider the following cases:

As-Left-1 or As-Left-2::

We have as hypothesis a term $u^{\prime}$ such that $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow}}}u^{\prime}$
and $\Gamma;s\vdash u^{\prime}\vartriangleleft t$. By the induction
hypothesis, we obtain a term $t_{f}$ with $\Gamma;s\vdash
u^{\prime}\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$, from $\Gamma;s\vdash u^{\prime}\vartriangleleft t$.

The term $t_{f}$ now works to satisfy the theorem. First, we have
$\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$ by transitivity of
$\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}$ from $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow}}}u^{\prime}$
and $\Gamma;s\vdash
u^{\prime}\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$.

Now, we have $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t_{f}$, with which we can now conclude.

As-Right::

Same reasoning as the case above, with rule Srs-Eq.

Now, to prove the converse we do an induction on the number of steps in
$\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$ and
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$. The base case is $u=v=t$ is by rule As-Refl where we have
$\Gamma;s\vdash u\vartriangleleft u$. There are two induction cases.

Case $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$ is $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow}}}u^{\prime}\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}v$::

In that case, by induction we have $\Gamma;s\vdash u^{\prime}\vartriangleleft
v$. By rule As-Left, we obtain $\Gamma;s\vdash u\vartriangleleft v$ from
$\Gamma;s\vdash u^{\prime}\vartriangleleft v$ and $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\vartriangleleft}}{{\longrightarrow}}}u^{\prime}$.

Case
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$ is
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$::

In that case, by induction we have $\Gamma;s\vdash u\vartriangleleft
v^{\prime}$. By rule As-Right, we obtain $\Gamma;s\vdash u\vartriangleleft v$
from $\Gamma;s\vdash u\vartriangleleft v^{\prime}$ and
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$.

∎

##  Appendix B Lemmas of Section 4

###### Definition B.1.

A term $t$ _preserves well-formedness_ iff for every extended context
$\Gamma;s$ and for every term $t^{\prime}$, the conjunction of $\Gamma;s\vdash
t~{}\mathrm{wf}$ and $t\mapsto t^{\prime}$ implies $\Gamma;s\vdash
t^{\prime}~{}\mathrm{wf}$.

###### Definition B.2 (Substitution in extended context).

Let $\Gamma;s$ be an extended context, $t$ be a term, and $x$ be a variable.
The substitution of $x$ by the $t$ in $\Gamma$ (written $\Gamma[x\backslash
t]$) is as follows:

$\begin{array}[]{rcl}\varepsilon[x\backslash t]&=&\varepsilon\\\ (\Gamma,y\leq
u)[x\backslash t]&=&\left\\{\begin{array}[c]{ll}\Gamma[x\backslash t],y\leq
u[x\backslash t]&(\textup{when}~{}y\not=x)\\\ \Gamma,y\leq
u&(\textup{otherwise})\end{array}\right.\end{array}$

The substitution of $x$ by the $t$ in $s$ (written $s[x\backslash t]$) is as
follows:

$\begin{array}[]{rcl}\mathrm{nil}[x\backslash t]&=&\mathrm{nil}\\\
(\alpha::s)[x\backslash t]&=&\alpha[x\backslash t]::s[x\backslash
t]\end{array}$

###### Proposition B.3 (Transitive well-subtyping preserves well-formedness).

Let $\Gamma;s$ be an extended context and $u$ and $v$ be terms. If
$\Gamma;s\vdash u\leq^{*}_{\mathrm{wf}}v$ then both derivation $\Gamma;s\vdash
u~{}\mathrm{wf}$ and $\Gamma;s\vdash v~{}\mathrm{wf}$ exist in the derivation
tree $\Gamma;s\vdash u\leq^{*}_{\mathrm{wf}}v$.

Note: the requirement that $\Gamma;s\vdash v~{}\mathrm{wf}$ exist in the
original derivation tree is used on other lemmas, because we do induction on
derivation trees. It is not enough to know that $\Gamma;s\vdash
v~{}\mathrm{wf}$. Hence this formulation.

###### Proof.

By induction on the derivation tree of $\Gamma;s\vdash
u\leq^{*}_{\mathrm{wf}}v$. If the last rule applied is Wf-Sub, then the result
holds by rule Wf-Rule. If the last rule applied is Wf-Trans, then there exists
a term $t$ such that $\Gamma;s\vdash u\leq^{*}_{\mathrm{wf}}t$ and
$\Gamma;s\vdash t\leq^{*}_{\mathrm{wf}}v$, and the result holds by the
induction hypothesis. ∎

Proposition (From transitive well-subtyping to transitive subtyping). Let
$\Gamma;s$ be an extended context and $u$ and $v$ be terms. If $\Gamma;s\vdash
u\leq^{*}_{\mathrm{wf}}v$ then $\Gamma;s\vdash u\leq^{*}v$.

###### Proof.

By induction on the derivation tree of $\Gamma;s\vdash
u\leq^{*}_{\mathrm{wf}}v$. If the last rule used is Wf-Sub, then we have that
$\Gamma;s\vdash u\leq_{\mathrm{wf}}v$, and we obtain $\Gamma;s\vdash
u\leq^{*}v$ by application of rules Wf-Rule and Ast-Sub. If the last rules
used is Wf-Trans, then there exist $t$ such that $\Gamma;s\vdash
u\leq^{*}_{\mathrm{wf}}t$ and $\Gamma;s\vdash t\leq^{*}_{\mathrm{wf}}v$, and
we obtain $\Gamma;s\vdash u\leq^{*}t$ and $\Gamma;s\vdash t\leq^{*}v$ by the
induction hypothesis. The result holds by rule Ast-Trans. ∎

Proposition 2.1 (From reduction semantics to equivalence reduction). Let $u$
and $v$ be terms. If $u\mapsto v$ then
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$.

###### Proof.

By induction on the derivation tree of $u\mapsto v$. The base case is when the
last rule used is E-App, and the result holds by rule Cr-Beta and
reflexitivity of $\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$
(Lemma 2.2).

The induction cases is when the last rule used is E-Cong, and the result holds
by induction and rules Cr-Fun and Cr-App. ∎

Lemma 2.2 (Reflexivity). Let $\Gamma$ be a context, $s$ be a stack, and $u$ be
a term, we have $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u$, and
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u$.

###### Proof.

By straightforward induction on the derivation trees of $\Gamma;s\vdash
u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u$ and
$\Gamma;s\vdash u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u$,
noting that the only applicable rules at the leaves are Cr-Top and Cr-Var
(respectively rule Srs-Top), and that at the rest of the nodes only rules Cr-
App and Cr-Fun occur (respectively rules Srs-App, Srs-FunOp, and Srs-Fun).

∎

Theorem 4.1 (Progress). Let $t$ be a term. For every extended context
$\Gamma;s$, if $\Gamma;s\vdash t~{}\mathrm{wf}$ then either $t$ is in normal
form, or there exists a term $t^{\prime}$ such that $t\mapsto t^{\prime}$.

###### Proof.

By structural induction on the term $t$. If $t$ is $\mathsf{Top}$ or a
variable $x$, then the result holds since $t$ is already in normal form.
Therefore it suffices to consider the following cases:

Case $t=\lambda x\,{\leq}\,u.v$ with $u\not\in\mathsf{NF}$::

By assumption we have $\Gamma;s\vdash\lambda x\,{\leq}\,u.v~{}\mathrm{wf}$. By
either rule W-Fun or W-FunOp, we obtain $\Gamma;\mathrm{nil}\vdash
u~{}\mathrm{wf}$. By the induction hypothesis on $u$, there exists
$u^{\prime}$ such that $u\mapsto u^{\prime}$, and as a result $t\mapsto\lambda
x\,{\leq}\,u^{\prime}.v$ by rule E-Cong.

Case $t=\lambda x\,{\leq}\,u.v$ with $v\not\in\mathsf{NF}$::

By assumption we have $\Gamma;s\vdash\lambda x\,{\leq}\,u.v~{}\mathrm{wf}$. By
either rule W-Fun or W-FunOp, we either have that
$\Gamma,x\,{\leq}\,u;\mathrm{nil}\vdash v~{}\mathrm{wf}$ or otherwise we have
that $s=\alpha::s^{\prime}$ and $\Gamma,x\,{\leq}\,\alpha;s^{\prime}\vdash
v~{}\mathrm{wf}$. In both cases, by using the induction hypothesis on $v$,
there exists $v^{\prime}$ such that $u\mapsto v^{\prime}$, and as a result
$t\mapsto\lambda x\,{\leq}\,u.v^{\prime}$ by rule E-Cong.

Case $t=u\,v$ with $u\not\in\mathsf{NF}$::

By assumption we have $\Gamma;s\vdash\lambda x\,{\leq}\,u\,v~{}\mathrm{wf}$.
By rule W-App and Lemma B.3 we have $\Gamma;v::s\vdash u~{}\mathrm{wf}$. Since
$u$ is not a normal form and by the induction hypothesis, there exists a term
$u^{\prime}$ such that $u\mapsto u^{\prime}$, and therefore $t\mapsto
u^{\prime}~{}v$ by rule E-Cong.

Case $t=u_{n}\,v$ with $u_{n}\in\mathsf{NF}$ and $v\not\in\mathsf{NF}$.:

Term $u_{n}$ is either $\mathsf{Top}$, a function, or a neutral. If $u$ is a
function, then $t$ is a redex and $t\mapsto t^{\prime}$ by rule E-App. The
case where $u_{n}$ is $\mathsf{Top}$ is impossible since $\mathsf{Top}$ cannot
have a function supertype by Lemma 4.3, and therefore $t$ could not be well-
formed by rule W-App. If $u_{n}$ is a neutral, then by rule W-App we have that
$\Gamma;v::s\vdash u_{n}\leq^{*}_{\mathrm{wf}}\lambda
x\,{\leq}\,w.\mathsf{Top}$ and $\Gamma;\mathrm{nil}\vdash
v\leq^{*}_{\mathrm{wf}}w$. From the latter judgement we obtain
$\Gamma;\mathrm{nil}\vdash v\leq_{\mathrm{wf}}w$ by Proposition B.3, which
ensures that $\Gamma;\mathrm{nil}\vdash v~{}\mathrm{wf}$ by ruleWf-Rule. Now
by the induction hypothesis on $v$, there exist $v^{\prime}$ such that
$v\mapsto v^{\prime}$, and as a result $t\mapsto u_{n}\,v^{\prime}$ by rule
E-Cong∎

Theorem 4.2 (Preservation). Let $\Gamma;s$ be an extended context. Let $t$,
$t^{\prime}$, and $u$ be terms. If $\Gamma;s\vdash t\leq^{*}_{\mathrm{wf}}u$
and $t\mapsto t^{\prime}$, then $\Gamma;s\vdash
t^{\prime}\leq^{*}_{\mathrm{wf}}u$.

###### Proof.

From the assumption $\Gamma;s\vdash t\leq^{*}_{\mathrm{wf}}u$ and by
Proposition B.3 we know that $\Gamma;s\vdash t~{}\mathrm{wf}$ and
$\Gamma;s\vdash u~{}\mathrm{wf}$. In order to prove $\Gamma;s\vdash
t^{\prime}\leq^{*}_{\mathrm{wf}}u$, it suffices to show that $\Gamma;s\vdash
t^{\prime}~{}\mathrm{wf}$ and $\Gamma;s\vdash t^{\prime}\leq u$ by rules Wf-
Sub and Wf-Rule.

We obtain $\Gamma;s\vdash t^{\prime}~{}\mathrm{wf}$ from the $\Gamma;s\vdash
t~{}\mathrm{wf}$ established earlier and by Lemma B.4 and $t\mapsto
t^{\prime}$.

Now to the $\Gamma;s\vdash t^{\prime}\leq u$. By rule As-Refl we obtain
$\Gamma;s\vdash t^{\prime}\leq t^{\prime}$, which gives us $\Gamma;s\vdash
t^{\prime}\leq t$ from
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$ by
rule As-Right. By rule Wf-Rule we obtain $\Gamma;s\vdash t\leq u$ from the
$\Gamma;s\vdash t\leq_{\mathrm{wf}}u$ established in the first paragraph.
Finally, we obtain $\Gamma;s\vdash t^{\prime}\leq^{*}u$ by rules Ast-Sub and
Ast-Trans, which gives us $\Gamma;s\vdash t^{\prime}\leq u$ by Lemma 4.4 and
we are done. ∎

Theorem 4.3 (No supertype of Top). Let $\Gamma;s$ be an extended context. Let
$\lambda x\,{\leq}\,t.u$ be a term. We cannot have
$\Gamma;s\vdash\mathsf{Top}\leq^{*}_{\mathrm{wf}}\lambda x\,{\leq}\,t.u$.

###### Proof.

Transform $\Gamma;s\vdash\mathsf{Top}\leq^{*}_{\mathrm{wf}}\lambda
x\,{\leq}\,t.u$ into $\Gamma;s\vdash\mathsf{Top}\leq\lambda x\,{\leq}\,t.u$ by
Proposition 2.3 and Lemma 4.4. Assume towards a contradiction that
$\Gamma;s\vdash\mathsf{Top}\leq\lambda x\,{\leq}\,t.u$. By definition of the
subtyping relation (Lemma 2.4), there exists $w$ such that
$\Gamma;s\vdash\mathsf{Top}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$ and $\lambda
x\,{\leq}\,t.u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$. From
$\Gamma;s\vdash\mathsf{Top}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$, we obtain that $w=\mathsf{Top}$ since $\mathsf{Top}$ can only
promote to itself, with rules Srs-Eq and Cr-Top. Now from $\lambda
x\,{\leq}\,t.u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$, we know that $w$ is an abstraction since the only rule for
equivalence reduction that can be applied to $\lambda x\,{\leq}\,t.u$ is Cr-
Fun. But this contradicts the $w=\mathsf{Top}$ established earlier and we are
done. ∎

Theorem 4.4 (Transivity is admissible). Let $\Gamma;s$ be an extended context.
Let $u$ and $v$ be terms. If $\Gamma;s\vdash u\leq^{*}v$ then $\Gamma;s\vdash
u\leq v$.

###### Proof.

By induction on the derivation $\Gamma;s\vdash t\leq^{*}u$. By rules Ast-Sub
and Ast-Trans and by the induction hypothesis, it suffices to prove that for
every terms $t$, $u$, and $v$, if $\Gamma;s\vdash t\leq u$ and $\Gamma;s\vdash
u\leq v$, then $\Gamma;s\vdash t\leq v$. From $\Gamma;s\vdash t\leq u$ and
$\Gamma;s\vdash u\leq v$ we obtain the diagram below

${v}$..${u}$.${t}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\leq}$

where the solid edges correspond to the definition of the subtyping relation
(rules As-Refl, As-Left-1, and As-Right). The result $\Gamma;s\vdash t\leq v$
follows by completing the diagram with the dashed arrows, which can be done by
commutativity of $\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$
and $\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$ established in
Theorem 4.5 below. ∎

Theorem 4.5 [$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$ and
$\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$ strongly
commute] Let $\Gamma;s$ be an extended context. Let $t_{0}$, $t_{1}$ and
$t_{2}$ be terms. If
$t_{0}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t_{1}$ and
$\Gamma;s\vdash
t_{0}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t_{2}$ then for
all enlarged context $\Gamma^{\prime};s^{\prime}$ with
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$ (defined in Figure 3),
there exists a term $t_{3}$, such that
$t_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t_{3}$ and
$\Gamma^{\prime};s^{\prime}\vdash
t_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t_{3}$.

Diagrammatically,

${t_{2}}$${t_{3}}$${t_{0}}$${t_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\leq}$

where the enlarged contexts $\Gamma;s$ and $\Gamma^{\prime};s^{\prime}$ are
omitted in the two vertical edges, and where the solid arrows are the
conditions for the existence of the dashed arrows.

Note: the definition of $\rightarrowtail$ is in Figure 3, but essentially if
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$ then when every element of
either $\Gamma^{\prime}$ or $s^{\prime}$ is an element of either $\Gamma$ or
$s$ respectively, that is reduced only once by
$\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$.

###### Proof of 4.5:
$\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}$ and
$\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}$ commute.

By induction on the term structure of $t_{0}$. We consider cases according to
the last two rules that are applied respectively in the derivation of the
horizontal and vertical edges of the diagram above, starting by the bottom-
left corner. The base case corresponds to when the bottom rule is Cr-Top, or
Cr-TopApp for which the lemma holds trivially. If the vertical edge rule is
Srs-Eq, the result also holds trivial by Lemma B.19. For the general case we
distinguish the sub-cases below:

Case Cr-Var::

We need to prove the diagram below:

${t}$.${x}$${x}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

The left edge is a variable promotion Srs-Prom, that means $x\leq t$ is in the
context $\Gamma;s$. Fix $\Gamma^{\prime};s^{\prime}$ such that
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$. In
$\Gamma^{\prime};s^{\prime}$, we therefore have an annotation
$x\,{\leq}\,t^{\prime}$ with
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$.

$t^{\prime}$ completes the above diagram, the top edge is by
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, and
the right edge is by Srs-Prom with enlarged context
$\Gamma^{\prime};s^{\prime}$.

${t}$${t^{\prime}}$${x}$${x}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Case Cr-App::

We need to prove the diagram below:

${u_{2}\,v_{0}}$${u_{3}\,v_{1}}$${u_{0}\,v_{0}}$${u_{1}\,v_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Fix $\Gamma^{\prime};s^{\prime}$ with
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$.

By rule Ctx-Annotation, we obtain
$\Gamma;v_{0}::s\rightarrowtail\Gamma^{\prime};v_{1}::s^{\prime}$ from
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$ and
$v_{0}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v_{1}$.

By the induction hypothesis with context $\Gamma;v_{0}::s$ there exists
$u_{3}$ such that $\Gamma^{\prime};v_{1}::s^{\prime}\vdash
u_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}$ and
$u_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u_{3}$. This
is legal because
$\Gamma;v_{0}::s\rightarrowtail\Gamma^{\prime};v_{1}::s^{\prime}$.

The top edge of the diagram holds by Cr-App, and the dashed right edge holds
by rule Srs-App with context $\Gamma^{\prime};s^{\prime}$.

Case Cr-Fun with Srs-Fun::

We need to prove the diagram below:

${\lambda x\leq t_{0}.u_{2}}$${\lambda x\leq t_{1}.u_{3}}$${\lambda x\leq
t_{0}.u_{0}}$${\lambda x\leq
t_{1}.u_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Fix $\Gamma^{\prime};s^{\prime}$ with
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$. By the rule Srs-Fun we
obtain $s=\mathrm{nil}$. Therefore we obtain $s^{\prime}=\mathrm{nil}$ from
$\Gamma;s\rightarrowtail\Gamma^{\prime};s^{\prime}$,

By the induction hypothesis with context $\Gamma,x\leq t_{0};\mathrm{nil}$
there exists $u_{3}$ such that $\Gamma^{\prime},x\leq t_{1};\mathrm{nil}\vdash
u_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}$ and
$u_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u_{3}$. The
top edge of the diagram holds by Cr-Fun, and the dashed right edge holds by
rule Srs-App with context $\Gamma^{\prime};\mathrm{nil}$.

Case Cr-Fun with Srs-FunOp::

We need to prove the diagram below:

${\lambda x\leq t_{0}.u_{2}}$${\lambda x\leq t_{1}.u_{3}}$${\lambda x\leq
t_{0}.u_{0}}$${\lambda x\leq
t_{1}.u_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Fix $\Gamma^{\prime};s^{\prime}$.

Similar as above, but the context used in the left edge is $\Gamma;\delta::s$.

By the induction hypothesis with context $\Gamma,x\,{\leq}\,\delta;s$, there
exists $u_{3}$ such that $\Gamma^{\prime},x\,{\leq}\,\delta;s^{\prime}\vdash
u_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}$ and
$u_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u_{3}$. The
top edge of the diagram holds by Cr-Fun, and the right edge holds by Srs-Fun
with context $\Gamma^{\prime};s^{\prime}$.

Case Cr-Beta::

This is the pathological case.

${(\lambda x\leq t.u_{2})s_{0}}$${u_{3}[x\backslash s_{1}]}$${(\lambda x\leq
t.u_{0})s_{0}}$${u_{1}[x\backslash
s_{1}]}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Here is why this case will work, whereas in the original work it doesn’t. Here
is a simple but problematic instantiation of that case with $u_{0}=x$:

${(\lambda x\leq t.s_{0})s_{0}}$${s_{1}[x\backslash s_{1}]=s_{1}}$${(\lambda
x\leq t.x)s_{0}}$${x[x\backslash
s_{1}]=s_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Which obviously works. Whereas in the original work, the diagram is the
following, which doesn’t work, as we only have $s_{1}\leq^{*}t$, so we can’t
complete the diagram in a single reduction.

${(\lambda x\leq t.t)s_{0}}$${t[x\backslash s_{1}]=t}$${(\lambda x\leq
t.x)s_{0}}$${x[x\backslash
s_{1}]=s_{1}}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$

Back to our work. Here is the diagram we want to obtain:

${(\lambda x\leq t.u_{2})v_{0}}$${u_{3}[x\backslash v_{1}]}$${(\lambda x\leq
t.u_{0})v_{0}}$${u_{1}[x\backslash
v_{1}]}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$$\scriptstyle{\equiv}$$\scriptstyle{\leq}$

Fix $\Gamma^{\prime};s^{\prime}$.

By the induction hypothesis with context $\Gamma,x\,{\leq}\,v_{0};s$, there
exists $u_{3}$ such that $\Gamma^{\prime},x\,{\leq}\,v_{1};s^{\prime}\vdash
u_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}$ and
$u_{2}\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u_{3}^{\prime}$.
The top edge of the diagram holds by Cr-Beta.

By Lemma B.9, we obtain $\Gamma^{\prime};s[x\backslash v_{1}]\vdash
u_{1}[x\backslash
v_{1}]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}[x\backslash
v_{1}]$ from $\Gamma^{\prime},x\,{\leq}\,v_{1};s\vdash
u_{1}\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}$.
Fortunatly, there is not $x$ in $s$. Therefore the obtained derivation is
actually
$\Gamma^{\prime};s\vdash u_{1}[x\backslash
v_{1}]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u_{3}[x\backslash
v_{1}]$, hence the right edge of the diagram with context
$\Gamma^{\prime};s^{\prime}$.

∎

###### Lemma B.4 (Reduction preserves well-formedness).

Every term $t$ preserves well-formedness.

###### Proof.

By structural induction on $t$. Let’s fix an extended context $\Gamma;s$. We
assume that $\Gamma;s\vdash t~{}\mathrm{wf}$, otherwise the lemma follows. We
assume that $t$ is not a normal form and that there exists a term $t^{\prime}$
such that $t\mapsto t^{\prime}$, otherwise the lemma follows as well. (The
cases where $t$ is either $\mathsf{Top}$ or a variable $x$ are impossible
since $\mathsf{Top}$ and $x$ are normal forms.)

It suffices to prove that $\Gamma;s\vdash t^{\prime}~{}\mathrm{wf}$. The only
non-basic base case is when $t=(\lambda x\,{\leq}\,u.v)w$ and when rule E-App
is used in the derivation of $t=(\lambda x\,{\leq}\,u.v)w\mapsto v[x\backslash
w]=t^{\prime}$. Without loss of generality, we assume that variable $x$ does
not occur free in any of the arguments in the stack $s$—otherwise we apply
alpha-conversion to substitute $x$ by a fresh variable in $(\lambda
x\,{\leq}\,u.v)w$. By the assumption $\Gamma;s\vdash(\lambda x\leq
u.v)w~{}\mathrm{wf}$ and by rules W-App, Lemma B.3 and W-FunOp, we obtain
$\Gamma,x\,{\leq}\,w;s\vdash v~{}\mathrm{wf}$. Now, by Lemma B.5 we obtain
$\Gamma;s[x\backslash w]\vdash v[x\backslash w]~{}\mathrm{wf}$, which is
equivalent to $\Gamma;s\vdash v[x\backslash w]~{}\mathrm{wf}$ since
$s[x\backslash w]=s$ because there are no free occurrences of $x$ in $s$, and
the lemma holds.

For the general cases we distinguish the context $\mathrm{C}[~{}]$ used for
the last application of rule E-Cong in the derivation $t\mapsto t^{\prime}$.

Case $t=\lambda x\,{\leq}\,[u].v\mapsto\lambda
x\,{\leq}\,[u^{\prime}].v=t^{\prime}$::

By assumption, $\Gamma;s\vdash\lambda x\,{\leq}\,u.v~{}\mathrm{wf}$ holds. We
distinguish whether $s$ is empty or $s=\alpha::s^{\prime}$.

In the former case, $\Gamma;\mathrm{nil}\vdash\lambda
x\,{\leq}\,u.v~{}\mathrm{wf}$. By rule W-Fun we obtain
$\Gamma,x\,{\leq}\,u;\mathrm{nil}\vdash v~{}\mathrm{wf}$ and
$\Gamma;\mathrm{nil}\vdash u~{}\mathrm{wf}$. By the induction hypothesis, we
have that $u$ preserves well-formedness, and together with $u\mapsto
u^{\prime}$ and Lemmas 2.1 and B.11, we obtain
$\Gamma,x\,{\leq}\,u^{\prime};\mathrm{nil}\vdash v~{}\mathrm{wf}$ and
$\Gamma;\mathrm{nil}\vdash u^{\prime}~{}\mathrm{wf}$. Finally, we obtain
$\Gamma;\mathrm{nil}\vdash\lambda x\,{\leq}\,u^{\prime}.v~{}\mathrm{wf}$ by
application of rule W-Fun.

In the latter case, $\Gamma;\alpha::s^{\prime}\vdash\lambda
x\,{\leq}\,u.v~{}\mathrm{wf}$. By rule W-FunOp we obtain
$\Gamma,x\,{\leq}\,\alpha;s^{\prime}\vdash v~{}\mathrm{wf}$. It suffices to
derive $\Gamma;\alpha::s^{\prime}\vdash\lambda
x\,{\leq}\,u^{\prime}.v~{}\mathrm{wf}$ by application of rule W-FunOp with the
type annotation $u^{\prime}$, which as above is well-formed by induction, and
we are done.

Case $t=\lambda x\,{\leq}\,u.[v]\mapsto\lambda
x\,{\leq}\,u.[v^{\prime}]=t^{\prime}$::

By assumption, $\Gamma;s\vdash\lambda x\,{\leq}\,u.v~{}\mathrm{wf}$ holds. We
distinguish whether $s$ is empty or $s=\alpha::s^{\prime}$.

In the former case, $\Gamma;\mathrm{nil}\vdash\lambda
x\,{\leq}\,u.v~{}\mathrm{wf}$. By rule W-Fun we have that
$\Gamma,x\,{\leq}\,u;\mathrm{nil}\vdash v~{}\mathrm{wf}$, and by the induction
hypothesis on $v$ we obtain $\Gamma,x\,{\leq}\,u;\mathrm{nil}\vdash
v^{\prime}~{}\mathrm{wf}$ since $\Gamma,x\,{\leq}\,u;\mathrm{nil}\vdash
v~{}\mathrm{wf}$ and $v\mapsto v^{\prime}$. Finally, we obtain
$\Gamma;\mathrm{nil}\vdash\lambda x\,{\leq}\,u.v^{\prime}~{}\mathrm{wf}$ by
application of rule W-Fun.

In the latter case, $\Gamma;\alpha::s^{\prime}\vdash\lambda
x\,{\leq}\,u.v~{}\mathrm{wf}$. By rule W-FunOp we have that
$\Gamma,x\,{\leq}\,\alpha;s^{\prime}\vdash v~{}\mathrm{wf}$, and by the
induction hypothesis on $v$ we obtain
$\Gamma,x\,{\leq}\,\alpha;s^{\prime}\vdash v^{\prime}~{}\mathrm{wf}$ since
$\Gamma,x\,{\leq}\,\alpha;s^{\prime}\vdash v~{}\mathrm{wf}$ and $v\mapsto
v^{\prime}$. Now we obtain $\Gamma;\alpha::s^{\prime}\vdash\lambda
x\,{\leq}\,u.v^{\prime}~{}\mathrm{wf}$ by application of rule W-FunOp and we
are done.

Case $t=[u]v\mapsto[u^{\prime}]v=t^{\prime}$::

From $u\mapsto u^{\prime}$ we obtain
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$ by
Lemma 2.1. By assumption, $\Gamma;s\vdash u\,v~{}\mathrm{wf}$ holds. By rule
W-App and Lemma B.3, we obtain that $\Gamma;v::s\vdash u~{}\mathrm{wf}$. By
applying the induction hypothesis on $u$, we obtain $\Gamma;v::s\vdash
u^{\prime}~{}\mathrm{wf}$ since $u\mapsto u^{\prime}$. Now, we show that
$u^{\prime}$ has subtype $\lambda x\,{\leq}\,w.\mathsf{Top}$. By rule As-Refl
we have $\Gamma;v::s\vdash u^{\prime}\leq u^{\prime}$, which together with
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$ gives
$\Gamma;v::s\vdash u^{\prime}\leq u$ by rule As-Right. From our assumption,
and Lemma 2.3, we obtain $\Gamma;v::s\vdash u\leq^{*}\lambda
x\,{\leq}\,w.\mathsf{Top}$. Now, by rules Ast-Sub and Ast-Trans, we obtain
$\Gamma;v::s\vdash u^{\prime}\leq^{*}\lambda x\,{\leq}\,w.\mathsf{Top}$.

Finally, we obtain $\Gamma;s\vdash u^{\prime}\,v~{}\mathrm{wf}$ by application
of rules W-App, Wf-Sub and Lemma B.16, from $\Gamma;v::s\vdash
u^{\prime}~{}\mathrm{wf}$ and $\Gamma;v::s\vdash u^{\prime}\leq^{*}\lambda
x\,{\leq}\,w.\mathsf{Top}$, where the missing premisses (i.e.,
$\Gamma;\mathrm{nil}\vdash v~{}\mathrm{wf}$, $\Gamma;\mathrm{nil}\vdash
t~{}\mathrm{wf}$ and $\Gamma;\mathrm{nil}\vdash v\leq^{*}t$) are directly
obtained by the rule W-App itself from the assumption $\Gamma;s\vdash
u\,v~{}\mathrm{wf}$ and Lemma B.3.

Case $t=u[v]\mapsto u[v^{\prime}]=t^{\prime}$::

From $v\mapsto v^{\prime}$ we obtain
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$ by
Lemma 2.1. By assumption, $\Gamma;s\vdash u\,v~{}\mathrm{wf}$ holds. By rule
W-App, Lemmas B.3 and Proposition 2.3, we obtain $\Gamma;v::s\vdash
u~{}\mathrm{wf}$, $\Gamma;v::s\vdash u\leq^{*}\lambda
x\,{\leq}\,w.\mathsf{Top}$, $\Gamma;\mathrm{nil}\vdash v~{}\mathrm{wf}$, and
$\Gamma;\mathrm{nil}\vdash v\leq^{*}w$. By the induction hypothesis on $v$, we
obtain $\Gamma;\mathrm{nil}\vdash v^{\prime}~{}\mathrm{wf}$ since $v\mapsto
v^{\prime}$. Now, we show that $v^{\prime}$ has subtype $w$. By rule As-Refl
we have $\Gamma;\mathrm{nil}\vdash v^{\prime}\leq v^{\prime}$, which together
with $v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$
gives $\Gamma;\mathrm{nil}\vdash v^{\prime}\leq v$ by rule As-Right. Now, by
rules Ast-Sub and Ast-Trans, we obtain $\Gamma;\mathrm{nil}\vdash
v^{\prime}\leq^{*}w$.

Finally, we obtain $\Gamma;v^{\prime}::s\vdash u~{}\mathrm{wf}$ from
$\Gamma;v::s\vdash u~{}\mathrm{wf}$ by Lemma B.17, and we obtain
$\Gamma;\mathrm{nil}\vdash w~{}\mathrm{wf}$ from the assumption and by rule
W-App and Lemma B.3. The result $\Gamma;s\vdash u\,v^{\prime}~{}\mathrm{wf}$
holds by application of rules W-App, Wf-Sub and Lemma B.16 from
$\Gamma;\mathrm{nil}\vdash v^{\prime}~{}\mathrm{wf}$, $\Gamma;v::s\vdash
u\leq^{*}\lambda x\,{\leq}\,w.\mathsf{Top}$, and $\Gamma;\mathrm{nil}\vdash
v^{\prime}\leq^{*}w$.∎

###### Lemma B.5 (Substitution preserves well-formedness).

Let $\Gamma;s$ be an extended context and let $t$ and $u$ be terms. If
$\Gamma,x\leq t,\Gamma^{\prime};s\vdash u~{}\mathrm{wf}$, then
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]\vdash u[x\backslash
t]~{}\mathrm{wf}$.

###### Proof.

First, we establish that $\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash
t]$ is prevalid by Lemma B.6, which we’ll use in most of the cases below. Now
we proceed by induction on the derivation tree of $\Gamma,x\leq
t,\Gamma^{\prime};s\vdash u~{}\mathrm{wf}$. We distinguish cases on the last
rule used:

Rule W-Var, with $u=y$ and $y\leq t^{\prime}\in\Gamma$::

By assumption $\Gamma,x\leq t,\Gamma^{\prime}$ is prevalid and $y$ has subtype
$t^{\prime}$ in $\Gamma,x\leq t,\Gamma^{\prime}$, and we know that
$\Gamma,x\leq t,\Gamma^{\prime};s\vdash t^{\prime}~{}\mathrm{wf}$. By the
induction hypothesis, we obtain $\Gamma,\Gamma^{\prime}[x\backslash
t];s[x\backslash t]\vdash t^{\prime}[x\backslash t]~{}\mathrm{wf}$.

First we show that there are now free occurrences of $x$ in $t^{\prime}$. By
assumption, $\Gamma$ has the shape
$\Gamma_{1},y\,{\leq}\,t^{\prime},\Gamma_{2}$, which ensures that all the free
variables of $t^{\prime}$ are in $\Gamma_{1}$ by rule P-Ctx2 since $\Gamma$ is
prevalid. Now, since
$\Gamma_{1},y\,{\leq}\,t^{\prime},\Gamma_{2},x\,{\leq}\,t$ is prevalid and by
the same rule, we know that $x\not\in\mathrm{dom}(\Gamma_{1})$, and therefore
$t^{\prime}$ contains no free occurrences of $x$.

Therefore, we have $t^{\prime}[x\backslash t]=t^{\prime}$ and thus
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]\vdash
t^{\prime}~{}\mathrm{wf}$ from the $\Gamma,\Gamma^{\prime}[x\backslash
t];s[x\backslash t]\vdash t^{\prime}[x\backslash t]~{}\mathrm{wf}$ established
before. We can now conclude that $\Gamma,\Gamma^{\prime}[x\backslash
t];s[x\backslash t]\vdash y[x\backslash t]~{}\mathrm{wf}$ by rule W-Var since
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]$ is prevalid and from
the facts established before.

Rule W-Var, with $u=y$ and $y\leq t^{\prime}\in\Gamma^{\prime}$::

Essentially the same proof as above. By assumption, $\Gamma,x\leq
t,\Gamma^{\prime}$ is prevalid and $y$ has subtype $t^{\prime}$ in
$\Gamma,x\leq t,\Gamma^{\prime}$, and we know that $\Gamma,x\leq
t,\Gamma^{\prime};s\vdash t^{\prime}~{}\mathrm{wf}$. By the induction
hypothesis, we obtain $\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash
t]\vdash t^{\prime}[x\backslash t]~{}\mathrm{wf}$.

From the fact that $y\leq t^{\prime}$ is a subtype annotation of
$\Gamma^{\prime}$, we have that $y\leq t^{\prime}[x\backslash t]$ is a subtype
annotation of $\Gamma^{\prime}[x\backslash t]$ by Definition B.2. We can now
conclude that $\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]\vdash
y[x\backslash t]~{}\mathrm{wf}$ by rule W-Var since
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]$ is prevalid and from
the facts established before.

Rule W-Var, with $u=x$::

By assumption and by the rule used, we have $\Gamma,x\leq
t,\Gamma^{\prime};s\vdash t~{}\mathrm{wf}$. By the induction hypothesis on
$\Gamma,x\leq t,\Gamma^{\prime};s\vdash t~{}\mathrm{wf}$ we obtain
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]\vdash t[x\backslash
t]~{}\mathrm{wf}$. By Lemma B.7 we know that $x$ does not occur free in $t$
since $\Gamma,x\leq t,\Gamma^{\prime};s\vdash t$ is prevalid. Therefore the
obtained derivation coincides with the desired result
$\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]\vdash
t~{}\mathrm{wf}$.

Rule W-Top, with $u=\mathsf{Top}$::

We have $\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash
t]\vdash\mathsf{Top}~{}\mathrm{wf}$ since $\Gamma,\Gamma^{\prime}[x\backslash
t];s[x\backslash t]$ is prevalid and by rule W-Top.

Rule W-Fun, with $u=\lambda y\,{\leq}\,v.w$ and $s=\mathrm{nil}$::

Without loss of generality we can assume that $y\not=x$. By assumption and by
the rule used, we have
$\Gamma,x\,{\leq}\,t,\Gamma^{\prime},y\,{\leq}\,v;\mathrm{nil}\vdash
w~{}\mathrm{wf}$ and $\Gamma;\mathrm{nil}\vdash v~{}\mathrm{wf}$. By the
induction hypothesis, we obtain $\Gamma,\Gamma^{\prime}[x\backslash
t],y\,{\leq}\,v[x\backslash t];\mathrm{nil}\vdash w[x\backslash
t]~{}\mathrm{wf}$ and $\Gamma,\Gamma^{\prime}[x\backslash
t];\mathrm{nil}\vdash v[x\backslash t]~{}\mathrm{wf}$. Now, we obtain
$\Gamma,\Gamma^{\prime}[x\backslash t];\mathrm{nil}\vdash(\lambda
y\,{\leq}\,v.w)[x\backslash t]$ by rule W-Fun and by definition of the
substitution function since $y\not=x$.

Rule W-FunOp, with $u=\lambda y\,{\leq}\,v.w$ and $s=\alpha::s^{\prime}$::

Without loss of generality we can assume that $y\not=x$. By assumption and by
the rule used, we have
$\Gamma,x\,{\leq}\,t,\Gamma^{\prime},y\,{\leq}\,\alpha;s^{\prime}\vdash
w~{}\mathrm{wf}$ and $\Gamma,x\,{\leq}\,t,\Gamma^{\prime};\mathrm{nil}\vdash
v~{}\mathrm{wf}$. By the induction hypothesis, we obtain

$\qquad\quad\Gamma,\Gamma^{\prime}[x\backslash
t],y\,{\leq}\,\alpha[x\backslash t];s^{\prime}[x\backslash t]\vdash
w[x\backslash
t]~{}\mathrm{wf}\quad\textup{and}\quad\Gamma,\Gamma^{\prime}[x\backslash
t];\mathrm{nil}\vdash v[x\backslash t]~{}\mathrm{wf}$

Now, we obtain $\Gamma,\Gamma^{\prime}[x\backslash
t];(\alpha::s^{\prime})[x\backslash t]\vdash(\lambda
y\,{\leq}\,v.w)[x\backslash t]$ by rule W-FunOp and by definition of the
substitution function since $y\not=x$.

Rule W-App with $u=v\,w$::

By W-App on our assumption, we have $\Gamma,x\leq w,\Gamma^{\prime};b::s\vdash
a\leq^{*}_{\mathrm{wf}}\lambda y\leq t.\mathsf{Top}$ and $\Gamma,x\leq
w,\Gamma^{\prime};\mathrm{nil}\vdash b\leq^{*}_{\mathrm{wf}}t$.

By Lemma B.3 on $\Gamma,x\leq w,\Gamma^{\prime};b::s\vdash
a\leq^{*}_{\mathrm{wf}}\lambda y\leq t.\mathsf{Top}$ and $\Gamma,x\leq
w,\Gamma^{\prime};\mathrm{nil}\vdash b\leq^{*}_{\mathrm{wf}}t$, we know that
the derivation trees of the statements

$\displaystyle\Gamma,x\leq w,\Gamma^{\prime};b::s\vdash a~{}\mathrm{wf},$
$\displaystyle\Gamma,x\leq w,\Gamma^{\prime};b::s\vdash\lambda y\leq
t.\mathsf{Top}~{}\mathrm{wf},$ $\displaystyle\Gamma,x\leq
w,\Gamma^{\prime};\mathrm{nil}\vdash b~{}\mathrm{wf},\quad\textup{and}$
$\displaystyle\Gamma,x\leq w,\Gamma^{\prime};\mathrm{nil}\vdash
t~{}\mathrm{wf}$

are subtrees of the derivation tree $\Gamma;s\vdash u~{}\mathrm{wf}$. We can
now apply the induction hypothesis on the judgements above to obtain

$\displaystyle\Gamma,\Gamma^{\prime}[x\backslash w];(b::s)[x\backslash
w]\vdash a[x\backslash w]~{}\mathrm{wf},$
$\displaystyle\Gamma,\Gamma^{\prime}[x\backslash w];(b::s)[x\backslash
w]\vdash\lambda y\leq t.\mathsf{Top}[x\backslash w]~{}\mathrm{wf},$
$\displaystyle\Gamma,\Gamma^{\prime}[x\backslash w];\mathrm{nil}\vdash
b[x\backslash w]~{}\mathrm{wf},\quad\textup{and}$
$\displaystyle\Gamma,\Gamma^{\prime}[x\backslash w];\mathrm{nil}\vdash
t[x\backslash w]~{}\mathrm{wf}$

Now, by Lemma B.15, we obtain $\Gamma,x\leq w,\Gamma^{\prime};b::s\vdash
a\leq^{*}\lambda y\leq t.\mathsf{Top}$ and $\Gamma,x\leq
w,\Gamma^{\prime};\mathrm{nil}\vdash b\leq^{*}t$ from $\Gamma,x\leq
w,\Gamma^{\prime};b::s\vdash a\leq^{*}_{\mathrm{wf}}\lambda y\leq
t.\mathsf{Top}$ and $\Gamma,x\leq w,\Gamma^{\prime};\mathrm{nil}\vdash
b\leq^{*}_{\mathrm{wf}}t$.

From the judgements obtained before, we have that
$\Gamma,\Gamma^{\prime}[x\backslash w];(b::s)[x\backslash w]\vdash
a[x\backslash w]\leq^{*}(\lambda y\leq t.\mathsf{Top})[x\backslash w]$ and
$\Gamma,\Gamma^{\prime}[x\backslash w];\mathrm{nil}\vdash b[x\backslash
w]\leq^{*}t[x\backslash w]$ by Lemma B.8.

Finally, we obtain $\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash
w]\vdash a[x\backslash w]\,b[x\backslash w]~{}\mathrm{wf}$ rules W-App and Wf-
Sub and by Lemma 2.3.∎

###### Lemma B.6 (Substitution preserves prevalidity).

Let $\Gamma,x\,{\leq}\,t,\Gamma^{\prime};s$ be a prevalid extended context.
The extended context $\Gamma,\Gamma^{\prime}[x\backslash t];s[x\backslash t]$
is prevalid.

###### Proof.

We now do an induction on the derivation tree
$\Gamma,x\,{\leq}\,t,\Gamma^{\prime};s$ prevalid. We distinguish cases on the
last rule used:

Rule P-Ctx1::

This case is impossible since $x\,{\leq}\,t$ cannot occur in an extended
context with an empty logical context.

Rule P-Ctx2 with $\Gamma^{\prime}=\varepsilon$ and $s=\mathrm{nil}$::

This is the base case. By assumption we have that $\Gamma;s$ is prevalid.

Because $s=\mathrm{nil}$ and $\Gamma^{\prime}=\varepsilon$, we have
$s[x\backslash t]=\mathrm{nil}$ and $\Gamma^{\prime}[x\backslash
t]=\varepsilon$. Therefore $\Gamma,\Gamma^{\prime}[x\backslash
t];s[x\backslash t]$ is actually $\Gamma;\mathrm{nil}$. Thus,
$\Gamma;\mathrm{nil}$ is prevalid.

Rule P-Ctx2 with $\Gamma^{\prime}=\Gamma^{\prime\prime},y\leq t^{\prime}$::

This is the general case. By assumption, we have that $\Gamma,x\leq
t,\Gamma^{\prime\prime};\mathrm{nil}$ is prevalid and we know that
$y\not\in\mathrm{dom}(\Gamma,x\leq t,\Gamma^{\prime\prime})$ and
$\mathrm{fv}(t^{\prime})\subseteq\mathrm{dom}(\Gamma,x\leq
t,\Gamma^{\prime\prime})$. By the induction hypothesis on $\Gamma,x\leq
t,\Gamma^{\prime\prime}$ is prevalid, we obtain
$\Gamma,\Gamma^{\prime\prime}[x\backslash t];\mathrm{nil}$ is prevalid.

By definition of the domain function, we have
$\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash
t])=\mathrm{dom}(\Gamma)\cup\mathrm{dom}(\Gamma^{\prime\prime}[x\backslash
t])$. By definition of the substitution function, and because
$x\not\in\Gamma^{\prime\prime}$, we have
$\mathrm{dom}(\Gamma^{\prime\prime}[x\backslash
t])=\mathrm{dom}(\Gamma^{\prime\prime})\cup\mathrm{fv}(t)$. By prevalidity, we
have $\mathrm{fv}(v)\subseteq\mathrm{dom}(\Gamma)$. Thus
$\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash
t])=\mathrm{dom}(\Gamma,x\leq t,\Gamma^{\prime\prime})\cup\\{x\\}$.

Because $y\not=x$, we have
$y\not\in\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash t])$ from
$y\not\in\mathrm{dom}(\Gamma,x\leq t,\Gamma^{\prime\prime})$. We have
$\mathrm{fv}(t^{\prime}[x\backslash
t])=\mathrm{fv}(t^{\prime})\setminus\\{x\\}\cup\mathrm{fv}(t)$ by definition
of the substitution function. From
$\mathrm{fv}(t^{\prime})\subseteq\mathrm{dom}(\Gamma,x\leq
t,\Gamma^{\prime\prime})$,
$\mathrm{fv}(t^{\prime})\setminus\\{x\\}\subseteq\mathrm{dom}(\Gamma,x\leq
t,\Gamma^{\prime\prime})\setminus\\{x\\}=\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash
t])$. From
$\mathrm{fv}(t)\subseteq\mathrm{dom}(\Gamma)\subseteq\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash
t])$, we have $\mathrm{fv}(t^{\prime}[x\backslash
t])\subseteq\mathrm{dom}(\Gamma,\Gamma^{\prime\prime}[x\backslash t])$.

Finally, we have that $\Gamma,\Gamma^{\prime\prime}[x\backslash t],y\leq
t^{\prime}[x\backslash t];\mathrm{nil}$ is prevalid by rule P-Ctx2 from the
facts established before.

∎

###### Lemma B.7 (Prevalidity and freshness of annotations).

Let $\Gamma;s$ be an extended prevalid context, and $t$ be a term. If $x\leq
t\in\Gamma$ then $x$ does not occur free in $t$.

###### Proof.

Assume without loss of generality that $\Gamma=\Gamma_{0},x\leq t,\Gamma_{1}$.
Because $\Gamma;s$ is prevalid, we know that $\Gamma_{0},x\leq t;\mathrm{nil}$
is prevalid by successive applications of rules P-Ctx3 and P-Ctx2. But then by
rule P-Ctx2, we have that $x\not\in\mathrm{dom}(\Gamma_{0})$ and
$\mathrm{fv}(t)\subseteq\mathrm{dom}(\Gamma_{0})$, and the result holds. ∎

###### Lemma B.8 (Substitution preserves subtyping).

Let $\Gamma$ be a context, $s$ be a stack, and $u$, $v$, and $w$ be terms. If
$\Gamma,x\leq w,\Gamma^{\prime};s\vdash u\leq^{*}v$, then
$\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash w]\vdash u[x\backslash
w]\leq^{*}v[x\backslash w]$.

###### Proof.

By Lemma 2.4, from $\Gamma,x\leq w,\Gamma^{\prime};s\vdash u\leq^{*}v$ we
obtain $\Gamma,x\leq w,\Gamma^{\prime};s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$ and
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$.

By Lemma B.9, we obtain $\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash
w]\vdash u[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t[x\backslash w]$ from $\Gamma,x\leq w,\Gamma^{\prime};s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$.

By Lemma B.10, we obtain $v[x\backslash
w]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t[x\backslash w]$ from
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t$.

By the converse of Lemma 2.4, we obtain $\Gamma,\Gamma^{\prime}[x\backslash
w];s[x\backslash w]\vdash u[x\backslash w]\leq^{*}v[x\backslash w]$ from
$\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash w]\vdash u[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t[x\backslash w]$ and $v[x\backslash
w]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}t[x\backslash w]$. ∎

###### Lemma B.9 (Subtyping under substitution).

Let $\Gamma$ be a context, and $s$ be a stack. Let $u$, $u^{\prime}$, and $v$
be terms. If $\Gamma,x\,{\leq}\,v,\Gamma^{\prime};s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$ then
$\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash v]\vdash u[x\backslash
v]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}[x\backslash
v]$

###### Proof.

By induction on the derivation tree of
$\Gamma,x\,{\leq}\,v,\Gamma^{\prime};s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$. The
base cases, if the last rule used is Srs-Top, we complete by Srs-Top. For the
case Srs-Prom, the reduction to prove is $\Gamma,\Gamma^{\prime}[x\backslash
w];s[x\backslash v]\vdash
v\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}v$ which holds by
reflexitivity (Lemma 2.2). For the case Srs-Eq, by Lemma B.10 we obtain
$u[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}[x\backslash
v]$ from
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$ and
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v$, hence the
result by rule Srs-Eq. For the other cases:

Srs-App::

In this case, the start hypothesis is $\Gamma,x\leq w,\Gamma^{\prime};s\vdash
a\,b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}a^{\prime}\,b$ by
rule Srs-App.

By using the induction hypothesis on $\Gamma,x\leq
w,\Gamma^{\prime};b::s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}a^{\prime}$, we
obtain $\Gamma,\Gamma^{\prime}[x\backslash w];b::s[x\backslash v]\vdash
a[x\backslash
v]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}a^{\prime}[x\backslash
v]$.

Hence $\Gamma,\Gamma^{\prime}[x\backslash w];s[x\backslash v]\vdash
a\,b[x\backslash
v]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}a^{\prime}\,b[x\backslash
v]$ by Srs-App.

Srs-Fun::

Same as above.
In this case, the start hypothesis is $\Gamma,x\leq
w,\Gamma^{\prime};\mathrm{nil}\vdash\lambda
y\,{\leq}\,a.b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a.b^{\prime}$ by rule Srs-Fun.

By the induction hypothesis on $\Gamma,x\leq w,\Gamma^{\prime},y\leq
a;\mathrm{nil}\vdash
b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$, we obtain
$\Gamma,\Gamma^{\prime}[x\backslash w],y\leq a[x\backslash
w];\mathrm{nil}\vdash b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b^{\prime}[x\backslash
w]$.

By rule Srs-Fun, we obtain from the previous derivation
$\Gamma,\Gamma^{\prime}[x\backslash w];\mathrm{nil}\vdash\lambda
y\,{\leq}\,a[x\backslash w].b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a[x\backslash w].b^{\prime}[x\backslash w]$.

Hence the result $\Gamma,\Gamma^{\prime}[x\backslash
w];\mathrm{nil}\vdash\lambda y\,{\leq}\,a.b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a.b^{\prime}[x\backslash w]$.

Srs-FunOp::

Exactly the same as above.

In this case, the start hypothesis is $\Gamma,x\leq
w,\Gamma^{\prime};\alpha::s\vdash\lambda
y\,{\leq}\,a.b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a.b^{\prime}$ by rule Srs-Fun.

By the induction hypothesis on $\Gamma,x\leq
w,\Gamma^{\prime},y\leq\alpha;s\vdash
b\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$, we obtain
$\Gamma,\Gamma^{\prime}[x\backslash w],y\leq\alpha[x\backslash
w];s[x\backslash w]\vdash b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b^{\prime}[x\backslash
w]$.

By rule Srs-FunOp, we obtain from the previous derivation
$\Gamma,\Gamma^{\prime}[x\backslash w];\alpha[x\backslash w]::s[x\backslash
w]\vdash$ $\lambda y\,{\leq}\,a[x\backslash w].b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a[x\backslash w].b^{\prime}[x\backslash w]$.

Hence the result $\Gamma,\Gamma^{\prime}[x\backslash w];\alpha::s[x\backslash
w]\vdash\lambda y\,{\leq}\,a.b[x\backslash
w]\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda
y\,{\leq}\,a.b^{\prime}[x\backslash w]$.

∎

###### Lemma B.10 (Reduction under substitution).

Let $u$, $u^{\prime}$, $v$ and $v^{\prime}$ be terms. Let $x$ denote a
variable. If
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$ and
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$, then
$u[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}[x\backslash
v^{\prime}]$.

###### Proof.

By induction on the derivation tree of
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$.

The base cases except Cr-Var (the last rule used in the derivation is Cr-Top
or Cr-TopApp), are immediate as $u[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}[x\backslash
v^{\prime}]$ is
$u\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}$.

For the case Cr-Var, we have $u[x\backslash v]=v$, and therefore we have
$u[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}u^{\prime}[x\backslash
v^{\prime}]$ is
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}v^{\prime}$ which
we have as hypothesis.

The general cases is a straightforward induction. We do the case Cr-App, every
other cases are similar. In this case, $u$ is a application $a\,b$ and
$u^{\prime}=a^{\prime}\,b^{\prime}$ with
$a\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}a^{\prime}$ and
$b\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}b^{\prime}$.

By using the induction hypothesis on
$a\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}a^{\prime}$ and
$b\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}b^{\prime}$, we
obtain $a[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}a^{\prime}[x\backslash
v^{\prime}]$ and $b[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}b^{\prime}[x\backslash
v^{\prime}]$.

By the rule Cr-App, we obtain $a\,b[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}a^{\prime}\,b^{\prime}[x\backslash
v^{\prime}]$ from
$a[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}a^{\prime}[x\backslash
v^{\prime}]$ and $b[x\backslash
v]\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}b^{\prime}[x\backslash
v^{\prime}]$.

This conclude the case Cr-App, every other cases are similar. ∎

###### Lemma B.11 (Narrowing of context in well-formedness derivation).

Let $\Gamma$ be a context, let $s$ be a stack, and let $t$, $t^{\prime}$, and
$u$ be terms. If $\Gamma,x\leq t;s\vdash u~{}\mathrm{wf}$, and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, and
$t$ preserves well-formedness (defined in B.1), then $\Gamma,x\leq
t^{\prime};s\vdash u~{}\mathrm{wf}$.

###### Proof.

Induction on the derivation tree of $\Gamma,x\leq t;s\vdash u~{}\mathrm{wf}$.
We have the following cases:

Rule W-Top::

Ok.

Rule W-Var, with $u\not=x$::

By induction.

Rule W-Var, with $u=x$::

As assumption we have $\Gamma,x\leq t;s\vdash x~{}\mathrm{wf}$. We need to
show $\Gamma,x\leq t^{\prime};s\vdash x~{}\mathrm{wf}$.

By W-Var, we obtain $\Gamma;s\vdash t~{}\mathrm{wf}$ from $\Gamma,x\leq
t;s\vdash x~{}\mathrm{wf}$.

By the fact that $t$ preserves well-formedness (defined in B.1), we obtain
$\Gamma;s\vdash t^{\prime}~{}\mathrm{wf}$ from $\Gamma;s\vdash
t~{}\mathrm{wf}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$.

By rule W-Var, we obtain $\Gamma,x\leq t^{\prime};s\vdash x~{}\mathrm{wf}$
from $\Gamma;s\vdash t^{\prime}~{}\mathrm{wf}$.

Rule W-Fun with $u=\lambda y\leq v.w$ with $s=\mathrm{nil}$::

We have as assumption $\Gamma,x\leq t;\mathrm{nil}\vdash\lambda y\leq
v.w~{}\mathrm{wf}$, and by rule W-Fun, $\Gamma,x\leq t,y\leq
v;\mathrm{nil}\vdash w~{}\mathrm{wf}$.

By using the induction hypothesis on $\Gamma,x\leq t,y\leq v;\ni\vdash
w~{}\mathrm{wf}$, we have $\Gamma,x\leq t^{\prime},y\leq v;\mathrm{nil}\vdash
w~{}\mathrm{wf}$ from $\Gamma,x\leq t,y\leq v;\mathrm{nil}\vdash
w~{}\mathrm{wf}$, and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, and
$t$ preserves well-formedness (defined in B.1).

Hence $\Gamma,x\leq t^{\prime};s\vdash\lambda y\leq v.w~{}\mathrm{wf}$ by
either W-Fun.

W-FunOp, with $u=\lambda y\leq v.w$ with $s=\alpha::s^{\prime}$::

We have as assumption $\Gamma,x\leq t;\alpha::s^{\prime}\vdash\lambda y\leq
v.w~{}\mathrm{wf}$, and by rule W-FunOp, $\Gamma,x\leq
t,y\leq\alpha;s^{\prime}\vdash w~{}\mathrm{wf}$.

By using the induction hypothesis on $\Gamma,x\leq
t,y\leq\alpha;s^{\prime}\vdash w~{}\mathrm{wf}$, we have $\Gamma,x\leq
t^{\prime},y\leq\alpha;s^{\prime}\vdash w~{}\mathrm{wf}$ from $\Gamma,x\leq
t,y\leq\alpha;s^{\prime}\vdash w~{}\mathrm{wf}$, and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, and
$t$ preserves well-formedness (defined in B.1).

Hence $\Gamma,x\leq t^{\prime};s\vdash\lambda y\leq v.w~{}\mathrm{wf}$ by
W-FunOp.

Rule W-App with $u=a\,b$::

By rule W-App on our assumption, we have $\Gamma,x\leq t;s\vdash
u\leq^{*}_{\mathrm{wf}}\lambda y\leq z.\mathsf{Top}$, and $\Gamma,x\leq
t;s\vdash v\leq^{*}_{\mathrm{wf}}z$.

By Lemma B.3 on $\Gamma,x\leq t;s\vdash u\leq^{*}_{\mathrm{wf}}\lambda y\leq
z.\mathsf{Top}$ and $\Gamma,x\leq t;s\vdash v\leq^{*}_{\mathrm{wf}}z$, we
obtain that all the following derivation tree and $\Gamma,x\leq t;v::s\vdash
u~{}\mathrm{wf}$, and $\Gamma,x\leq t;v::s\vdash\lambda y\leq
z.\mathsf{Top}~{}\mathrm{wf}$, and $\Gamma,x\leq t;\mathrm{nil}\vdash
v~{}\mathrm{wf}$ and $\Gamma,x\leq t;\mathrm{nil}\vdash z~{}\mathrm{wf}$.

By Lemma B.12, we obtain $\Gamma,x\leq t^{\prime};s\vdash u\leq^{*}\lambda
y\leq z.\mathsf{Top}$ from $\Gamma,x\leq t;s\vdash u\leq^{*}\lambda y\leq
z.\mathsf{Top}$.

By the same Lemma B.12, we obtain $\Gamma,x\leq t^{\prime};\mathrm{nil}\vdash
v\leq^{*}z$ from $\Gamma,x\leq t;\mathrm{nil}\vdash v\leq^{*}z$.

By using the induction hypothesis, we obtain respectively $\Gamma,x\leq
t^{\prime};v::s\vdash u~{}\mathrm{wf}$, and $\Gamma,x\leq
t^{\prime};v::s\vdash\lambda y\leq z.\mathsf{Top}~{}\mathrm{wf}$, and
$\Gamma,x\leq t^{\prime};\mathrm{nil}\vdash v~{}\mathrm{wf}$ and $\Gamma,x\leq
t^{\prime};\mathrm{nil}\vdash z~{}\mathrm{wf}$. from respectively
$\Gamma,x\leq t;v::s\vdash u~{}\mathrm{wf}$, and $\Gamma,x\leq
t;v::s\vdash\lambda y\leq z.\mathsf{Top}~{}\mathrm{wf}$, and $\Gamma,x\leq
t;\mathrm{nil}\vdash v~{}\mathrm{wf}$ and $\Gamma,x\leq t;\mathrm{nil}\vdash
z~{}\mathrm{wf}$.

By rules W-App, Wf-Sub, and Lemma B.16, we obtain $\Gamma,x\leq
t^{\prime};s\vdash u\,v~{}\mathrm{wf}$ from $\Gamma,x\leq t^{\prime};s\vdash
u\leq^{*}\lambda y\leq z.\mathsf{Top}$, and $\Gamma,x\leq t^{\prime};s\vdash
v\leq^{*}z$, and $\Gamma,x\leq t;v::s\vdash u~{}\mathrm{wf}$, and
$\Gamma,x\leq t;v::s\vdash\lambda y\leq z.\mathsf{Top}~{}\mathrm{wf}$, and
$\Gamma,x\leq t;\mathrm{nil}\vdash v~{}\mathrm{wf}$, and $\Gamma,x\leq
t;\mathrm{nil}\vdash z~{}\mathrm{wf}$.

∎

###### Lemma B.12 (Narrowing of context in subtyping derivation).

Let $\Gamma$ be a context, let $s$ be a stack, and let $t$, $t^{\prime}$, and
$u$ be terms. If we have $\Gamma,x\leq t;s\vdash u\leq^{*}v$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$ then
$\Gamma,x\leq t^{\prime};s\vdash u\leq^{*}v$

###### Proof.

By Lemma 4.4, we obtain $\Gamma,x\leq t;s\vdash u\leq v$ from $\Gamma,x\leq
t;s\vdash u\leq^{*}v$.

By Lemma 2.4, we obtain a term $w$ such that
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$ and $\Gamma,x\leq t;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$ from $\Gamma,x\leq t;s\vdash u\leq v$.

Now, we will prove later in this lemma that for any term $a$ and $b$, if we
have $\Gamma,x\leq t;s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$ then
we have $\Gamma,x\leq t^{\prime};s\vdash a\leq b$. From $\Gamma,x\leq
t^{\prime};s\vdash a\leq b$ we have $\Gamma,x\leq t^{\prime};s\vdash
a\leq^{*}b$ by Ast-Sub.

Now this is sufficient to conclude by transitivity, indeed, $\Gamma,x\leq
t;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$ is sequence of multiple $\Gamma,x\leq t;s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$ that we each
transform into $\Gamma,x\leq t^{\prime};s\vdash a\leq^{*}b$, to then group
them into $\Gamma,x\leq t^{\prime};s\vdash u\leq^{*}w$ by rule Ast-Trans.

By Lemma 2.4, we obtain $\Gamma,x\leq t^{\prime};s\vdash w\leq^{*}v$ from
$v\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow\rightarrow\hskip
1.99997pt}}}w$.

By rule Ast-Trans, we obtain $\Gamma,x\leq t^{\prime};s\vdash u\leq^{*}v$ from
$\Gamma,x\leq t^{\prime};s\vdash u\leq^{*}w$ and $\Gamma,x\leq
t^{\prime};s\vdash w\leq^{*}v$. So it is indeed sufficient to conclude. Now
let’s prove our lemma.

We now want to prove that for any $a$ and $b$ we have $\Gamma,x\leq t;s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$
implies $\Gamma,x\leq t^{\prime};s\vdash a\leq b$.

Start of the proof:

By induction on $\Gamma,x\leq t;s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$. Here are the
cases:

Rule Srs-Prom::

By assumption we have $\Gamma,x\leq t;s\vdash
x\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t$. By Srs-Prom, we
have $\Gamma,x\leq t^{\prime};s\vdash
x\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t^{\prime}$. By
Lemma 2.4, we have $\Gamma,x\leq t^{\prime};s\vdash x\leq t$ from
$\Gamma,x\leq t^{\prime};s\vdash
x\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}t^{\prime}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$.

Rule Srs-Top::

As assumption we have $\Gamma,x\leq t;s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\mathsf{Top}$. By
rule Srs-Top, $\Gamma,x\leq t^{\prime};s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\mathsf{Top}$ is
valid as well.

Rule Srs-Eq::

As assumption we have
$a\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}b$. By rule Srs-
Eq, $\Gamma,x\leq t^{\prime};s\vdash
a\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}b$ is valid as well.

Rule Srs-App::

By assumption we have $\Gamma,x\leq t;s\vdash
u\,v\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}\,v$
and $\Gamma,x\leq t;v::s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$. By
using the induction on $\Gamma,x\leq t;v::s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, we
obtain $\Gamma,x\leq t;v::s\vdash u\leq u^{\prime}$. By Lemma B.13, we obtain
$\Gamma,x\leq t;s\vdash u\,v\leq u^{\prime}\,v$ from $\Gamma,x\leq
t;v::s\vdash u\leq u^{\prime}$. Hence this case.

Rule Srs-FunOp::

By assumption we have $\Gamma,x\leq t;\alpha::s\vdash\lambda y\leq
w.u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda y\leq
w.u^{\prime}$, and $\Gamma,x\leq t,y\leq\alpha;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$. By
using the induction on $\Gamma,x\leq t,y\leq\alpha;s\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, we
obtain $\Gamma,x\leq t^{\prime},y\leq\alpha;s\vdash u\leq u^{\prime}$. By
Lemma B.13, we obtain $\Gamma,x\leq t;\alpha::s\vdash\lambda y\leq
w.u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda y\leq
w.u^{\prime}$ from $\Gamma,x\leq t^{\prime},y\leq\alpha;s\vdash u\leq
u^{\prime}$. Hence this case.

Rule Srs-Fun::

By assumption we have $\Gamma,x\leq t;\mathrm{nil}\vdash\lambda y\leq
w.u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda y\leq
w.u^{\prime}$, and $\Gamma,x\leq t,y\leq w;\mathrm{nil}\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$. By
using the induction on $\Gamma,x\leq t,y\leq w;\mathrm{nil}\vdash
u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}u^{\prime}$ and
$t\mathop{\stackrel{{\scriptstyle\equiv}}{{\longrightarrow}}}t^{\prime}$, we
obtain $\Gamma,x\leq t^{\prime},y\leq w;\mathrm{nil}\vdash u\leq u^{\prime}$.
By Lemma B.13, we obtain $\Gamma,x\leq t;\mathrm{nil}\vdash\lambda y\leq
w.u\mathop{\stackrel{{\scriptstyle\leq}}{{\longrightarrow}}}\lambda y\leq
w.u^{\prime}$ from $\Gamma,x\leq t^{\prime},y\leq w;\mathrm{nil}\vdash u\leq
u^{\prime}$. Hence this case.

∎

###### Lemma B.13 (Congruence of $\leq$).