Type-based termination with sized products

Gilles Barthe^{1}^{⋆}, Benjamin Grégoire^{2}, and Colin Riba^{2}

1 IMDEA Software, Madrid, Spain gilles.barthe@imdea.org 2 INRIA Sophia-Antipolis, France

        {Benjamin.Gregoire,Colin.Riba}@sophia.inria.fr

Abstract. Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive calls operate on smaller arguments. However, many systems using type-based termination rely on a semantical anomaly to guarantee strong normalization; namely, they impose that non-recursive elements of a datatype, e.g. the empty list, have size 1 instead of 0. This semantical anomaly also prevents functions such as quicksort to be given a precise typing. The main contribution of this paper is a type system that remedies this anomaly, and still ensures termination. In addition, our type system features prenex stage polymorphism, a weakening of existential quantification over stages, and is precise enough to type quicksort as a non-size increasing function. Moreover, our system accomodate stage addition with all positive inductive types.

1 Introduction

Type-based termination is a method to guarantee termination of recursive definitions by a non-standard type system in which datatype elements are assigned a size, which is used by the typing rule for letrec to ensure that recursive calls are made on smaller elements, i.e. elements with a smaller size. The semantical intuition behind size-based termination is embedded in the (simplified) typing rule for recursive definitions, which states that the definition of a function on elements of size ı can only make recursive calls on elements of smaller size:

\frac{Γ, f : List^{ı}τ → σ ⊢ e : Listîτ → σ}{Γ ⊢ letrec f = e : List^{∞}τ → σ}  (1)

where ı is a size variable, List^{ı} denotes the type of lists of size less or equal to ı, and is the successor function on stages, Listî denotes the type of lists of size less or equal to î and List^{∞} denotes the usual type of lists.

One distinguishing feature of type-based termination is its expressiveness. Indeed, even the simplest systems of type-based termination are sufficiently expressive to allow to give precise typings for some structurally recursive functions:

map : (X → Y) → List^{ı}X → List^{ı}Y

⋆ Most of this work was performed while working at INRIA Sophia-Antipolis.

and to type functions that are not structurally recursive such as the quicksort function:

letrec qs = λl. case l of | nil ⇒ nil

| cons x xs ⇒ let ⟨z_{1}, z_{2}⟩ = (filter x xs)
in app (qs z_{1}) (cons x (qs z_{2}))

(2)

Many type-based termination systems [7, 1–3] allow the typing:

quicksort : List^{∞}X → List^{∞}X  (3)

but cannot yield the more precise typing:

quicksort : List^{ı}X → List^{ı}X  (4)

Achieving a precise typing for quicksort requires extending the type system so that it yields precise typings for app and filter: first, app must be given a precise typing by means of stage addition:

app : List^{ı}X → List^{ȷ}X → List^{ı+ȷ}X  (5)

Second, we have to express that filter divides a list of size ı into two lists whose respective sizes ȷ_{1} and ȷ_{2} sum up to ı which could be expressed using constrained existential types, as in [4, 10]:

filter : X → List^{ı}X → ∃ȷ_{1}, ȷ_{2} (ȷ_{1} + ȷ_{2} = ı). List^{ȷ_{1}}X × List^{ȷ_{2}}X  (6)

Unfortunately, adding constrained existential quantification over stages may break subject reduction (see Section 2) and leads to complex type systems, where type checking requires solving constraints in Presburger arithmetic.

Furthermore, having nil of size at least ˆ0 (as in [7, 1–3]), we cannot type filter as in (6), and this prevents the typing quicksort as in (4). Thus, we must give the size 0 to nil. Alas, using the typing rule for fixpoints of [7, 1–3], and letting nil : List^{0}X, leads to typable non-terminating terms: using the typing rule for fixpoints of [7, 1–3], (letrec f x = f nil) nil is typable (using the subtyping rule List^{0}X ≤ List^{ı}X) but not terminating.

Thus, defining a simple yet precise type system that enjoys good metatheoretical properties is a challenge. The main contribution of this article is the definition of a type system F_{×} that features a monoidal structure on stages (with zero and addition), that simulates existential quantification over stages, and still enjoys subject reduction and strong normalization for first-order and higherorder inductive types. Technically, we achieve subject reduction for existentials by attaching existential quantification to a container structure: this way, introduction and elimination of existential quantification is linked with introduction and elimination of the corresponding type constructor. This leads to a system which features subject reduction and where eliminations of existential quantification are easier to write for the user. The resulting system provides a wellbehaved intermediate step between basic type-based termination criterion [7, 1–3], and more powerful but less tractable constraint based approaches [10, 4]. For simplicity, in this paper we focus on a binary product, which we call sized product.

To achieve strong normalization, we resort to constraining the form of recursive definitions, requiring that the body of the function immediately performs a case analysis on its recursive argument; this syntactic restriction forces a style of definitions close to rewriting. However, in contrast with rewriting, the body of recursive definitions are still part of the terms. This allows for a more powerful intensional equality between functions than with rewriting. Another feature of F_{×} is the associativity and commutativity of the addition on the stages of higherorder inductive datatypes. This is possible because, in the model construction for strong normalization, stage addition is interpreted by the natural addition on the ordinals which interpret the stages of higher-order inductive datatypes.

The paper is organized as follows. In Sect. 2 we discuss related works and presents informally the main characteristics of F_{×}. Sect. 3 is devoted to the formal definition of the system, while Sect. 4 and Sect. 5 outline respectively the proofs of subject reduction and strong normalization proofs.

2 Overview and related work

The purpose of this section is to present the main characteristics of F_{×} and its relation with other works on type-based termination. We begin with a brief overview of the works that support precise typings for quicksort, and then explain the main specificities of our work.

There has been a lot of interest in using type systems to guarantee termination or to characterize the complexity of recursive functions, see e.g. [1] for an overview. Most systems share the semantical anomaly of F and we are only aware of three systems in which quicksort can be given its exact typing.

The first system is that of Chin and Khoo [5], which annotates every type with size annotations and infers a formula of Presburger arithmetic that guarantees termination. We believe that their system, while expressive, generates constraints which are too complex to be used in practice. The second system is that of Xi [10], which uses restricted dependent types to ensure termination. The third system is that of Blanqui and Riba [4]. Recursive functions are defined by rewrite rules, and as in F_{×}, having non-recursive constructors of size 0 is not problematic.

We now discuss the two main characteristics of F_{×}: the sized product and the typing of fixpoints.

2.1 The sized product

Advanced systems of type-based termination, such as Xi and Blanqui, feature constrained existential and universal stage quantification, respectively written ∃ıP.τ and ∀ıP.τ, where P is a constraint and τ is a type. These systems deal with judgments of the form K; Γ ⊢ e : τ where K is a conjunction of constraints, and their type checking algorithm generate constraints in Presburger arithmetic.

Apart from the inherent complexity of type checking, there are some known difficulties with existential types.

Fully explicit existential types, which are used by Xi [10], enjoy subject reduction but rely on a complex elaboration mechanism for type checking. In contrast, implicit existential types do not satisfy subject reduction. Blanqui and Riba [4] use the elimination rule:

(∃-elim) \frac{K; Γ ⊢ e : ∃ıP.τ K, P ; Γ, x:τ ⊢ e′ : σ}{K; Γ ⊢ let x = e in e′ : σ} ı ∉ K, Γ, σ

together with the let-reduction rule:

let x = e in e′ ↦ e′[x := e]

Subject reduction fails is this system (the example of Tatsuta [9] is easily adapted). Because let-reduction is performed even if the typing of e does not end with an ∃ıP.τ-introduction, the sharing information given by the second premise of (∃- elim), which is lost by let-reduction, is not regained by the witness information given by ∃ıP.τ-introductions. Note that the failure of subject reduction is actually not a so big problem in [4] since the constrained type system is used to analyze rewrite rules, while ensuring their termination in a standard type system which features subject reduction.

The above discussion illustrates the difficulties with existential quantification over stages and justifies our choice to focus on a simpler system that partially simulates, but does not have, existential quantification. Indeed, our type system F_{×} achieves a similar effect using prenex stage quantification and using instead of explicitly existential quantification an embedding of existential quantification inside some specific type constructors. This way, introduction and elimination of existential quantification is linked with introduction and elimination of the corresponding type constructor. This leads to a system which features subject reduction and where eliminations of existential quantification are easier to write for the user. For simplicity, in this paper we focus on a binary product, which we call sized product. We explain it with an example. To express that filter x l computes a pair of lists whose sizes sum up to the size of l, we write

filter : X → List^{ı}X → List X ×^{ı} List X

The existential information on ȷ_{1} and ȷ_{2} in (6) is expressed using the rule (let), which is inspired by the usual elimination of existential quantification

(let) \frac{K; Γ ⊢ filter x l : List X ×^{ı} List X K, ȷ_{1} + ȷ_{2} ≤ ı ; Γ, z_{1} :List^{ȷ_{1}}X, z_{2} :List^{ȷ_{2}}X ⊢ e : List^{ı} X}{K; Γ ⊢ let ⟨z_{1}, z_{2}⟩ = filter x l in e : List^{ı} X} ȷ_{1}, ȷ_{2} ∉ K, Γ

The sized product allows to combine pair opening and let-reduction, which corresponds to the elimination of the existential information in the rule (let). This leads to the following rewrite rule, which is the key-point for subject reduction in F_{×}:

let ⟨x_{1}, x_{2}⟩ = ⟨e_{1}, e_{2}⟩ in e ↦_{θ} e[x_{1} := e_{1}, x_{2} := e_{2}]

2.2 Typing of fixpoints

In order to reject the non-terminating term in the introduction, we constrain the form of recursive definitions, requiring that the body of the function immediately performs a case analysis on its recursive argument, and distinguishing in the typing rule between recursive and non-recursive constructors. This approach is connected to definitions by rewriting [4], where fixpoints and case analysis are performed in a single definition. To avoid the non-normalizing term (letrec f x = f nil) nil while having nil of size 0, we ensure that no evaluation strategy of a typable expression of the form (letrec f = e) nil can make recursive calls to letrec f = e. The simplest syntactic way to achieve this is to stick fixpoints definitions letrec f = e to case analysis, and to make a distinction between the recursive and the non-recursive constructors of a datatype d. Intuitively, d can not occur in the type of the arguments of a non-recursive constructors. Then, our fixpoints have the shape

letrec f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}

where c^{nr} are non-recursive constructors and c^{r} are recursive constructors, and where e^{nr} can not depend on f. Thus, the following term is strongly normalizing:

(letrec f case {0 ⇒ 1 | s ⇒ λx.(f 0) + (f x)}) 0

It would be desirable to separate fixpoints from case analysis, as in F , but we have been unable to find a strongly normalizing system for the usual syntax.

In contrast, Xi [10] can have nil : List^{0}τ without disturbing normalization. Instead of (1), fixpoints can be typed as follows:

\frac{K; Γ, f : ∀ı < ȷ.List^{ı}τ → σ ⊢ e : List^{ȷ}τ → σ}{Γ ⊢ letrec f = e : ∀ı.List^{ı}τ → σ}

It is possible for Xi to rely on a strict ordering on stages, because he relies on existential quantification to encode List^{∞}τ as ∃ı.List^{ı}τ. In our case, we cannot use such a strict ordering, because ı ≤ ∞ but not ı < ∞.

3 System F_{×}

In this section, we present the syntax of system F_{×}. We begin by the stages, then define types, terms, reductions and present the typing rules of the system.

3.1 Stages

Stages expression are built from a set 𝒱_{𝒮} = {ı, ȷ, κ, … } of stage variables. They use a binary stage addition +, a successor operation ˆ · and the constants 0, ∞, denoting respectively the least and the greatest stage.

Definition 3.1 (Stages). The set 𝒮 of stage expressions is given by the abstract syntax:

s, r ::= 𝒱_{𝒮} | 0 | ∞ | ŝ | s + r

The substitution s[ı := r] of the stage variable ı for r in s is defined in the obvious way.

The system uses inequalities s ≤ r on stage expressions. They are derived by judgments of the form K ⊢ s ≤ r, where K is a conjunction of stages inequalities called stage constraint. These judgments are defined by the substage relation.

Definition 3.2. A stage constraint is a finite set K ∈ 𝒦 of stage inequalities s ≤ r with s, r ∈ 𝒮. The substage relation is the smallest relation K ⊢ s ≤ r, where K ∈ 𝒦 and s, r ∈ 𝒮, such that

(ax) \overline{K, s ≤ r ⊢ s ≤ r}  (refl) \overline{K ⊢ s ≤ s}  (inf) \overline{K ⊢ 0 ≤ s}  (sup) \overline{K ⊢ s ≤ ∞}
(trans) \frac{K ⊢ s ≤ r K ⊢ r ≤ p}{K ⊢ s ≤ p}  (mon) \frac{K ⊢ s ≤ r}{K ⊢ s + p ≤ r + p}  (inj) \frac{K ⊢ ŝ ≤ r̂}{K ⊢ s ≤ r}
(com) \overline{K ⊢ s + r ≤ r + s}  (assoc) \overline{K ⊢ s + (r + p) ≤ (s + r) + p}
(succ) \overline{K ⊢ s + r̂ = { \atop s + r}}  (zero) \overline{K ⊢ 0 + s = s}

where \overline{K ⊢ s = r} abbreviates the conjunction of \overline{K ⊢ s ≤ r} and \overline{K ⊢ r ≤ s}.

Note that the rule (sup) implies ˆ∞ ≤ ∞. Moreover, we can derive K ⊢ s ≤ ŝ, K ⊢ (s + r) + p ≤ s + (r + p), K ⊢ s ≤ s + r; and K ⊢ ŝ ≤ r̂ from K ⊢ s ≤ r.

3.2 Types and datatypes declarations

The system F_{×} is an extension of Church’s style System F. In addition to the function space and the second order type quantification ΠX.τ, sized types are built using the sized product ×^{s} and the bounded universal stage quantification ∀ı ≤ s.τ, which binds ı in τ but not in s (so that, by Barendregt convention, we may always assume ı ∉ s). The bound s in universal stage quantification is essential for the typing of fixpoints (typing rule (rec)).

We consider three sets of types: erased types |τ| ∈ |𝒯|, that do not carry size annotations, sized types τ ∈ 𝒯, in which stage variables are free, and constrained types \underline{τ} ∈ \underline{𝒯}, which are built from sized types using prenex universal stage quantification. Erased types are needed because Church’s typing imposes types to appear at the term level, while we do not want size annotations to appear in terms because it makes fail subject reduction (see Sect. 2.4 of [3]).

We assume given a set 𝒱_{𝒯} = {X, Y, … } of type variables and a set 𝒟 of datatype identifiers. Each datatype identifier comes equipped with an arity ar(d).

Definition 3.3 (Types). The sets |𝒯|, 𝒯 and \underline{𝒯} of erased types, sized types and constrained types are given by the following abstract syntaxes:

|𝒯| ::= 𝒱_{𝒯} | |𝒯| → |𝒯| | Π𝒱_{𝒯} .|𝒯| | 𝒟 |𝒯| | |𝒯| × |𝒯|
𝒯 ::= 𝒱_{𝒯} | 𝒯 → 𝒯 | Π𝒱_{𝒯} .𝒯 | 𝒟^{𝒮} 𝒯 | 𝒟 𝒯 ×^{𝒮} 𝒟 𝒯
\underline{𝒯} ::= 𝒯 | ∀ı ≤ s.\underline{𝒯}

where ı ∉ s and in the clause for datatypes, it is assumed that the length of the vectors 𝒯 and |𝒯| is exactly the arity of the datatype.

Let |τ|, |θ|, |σ|, … range over erased types, τ, θ, σ, … range over sized types and \underline{τ}, \underline{θ}, \underline{σ}, … range over constrained types. We write ∀ı.\underline{τ} for ∀ı ≤ ∞.\underline{τ} and ∀ı ≤ s.\underline{τ} for ∀ı_{1} ≤ s_{1}. · · · ∀ı_{n} ≤ s_{n}.\underline{τ}. Note that every \underline{τ} ∈ \underline{𝒯} can be written ∀ı ≤ s.τ with τ ∈ 𝒯. Moreover, we denote by |.| the obvious erasure map from \underline{𝒯} to |𝒯|. A type is closed if it contains no free stage variables and no free type variables.

The subtyping relation is inherited from the substage relation. The rules are syntax-directed.

Definition 3.4 (Subtyping). The subtyping relation is the smallest relation K ⊢ \underline{τ} ⊑ \underline{σ}, where K ∈ 𝒦 and \underline{τ}, \underline{σ} ∈ \underline{𝒯}, such that

(var) \overline{K ⊢ X ⊑ X}  (cst) \frac{K ⊢ r ≤ s K, ı ≤ r ⊢ \underline{τ} ⊑ \underline{σ}}{K ⊢ ∀ı ≤ s.\underline{τ} ⊑ ∀ı ≤ r.\underline{σ}} if ı ∉ K
(func) \frac{K ⊢ τ′ ⊑ τ K ⊢ σ ⊑ σ′}{K ⊢ τ → σ ⊑ τ′ → σ′}  (prod) \frac{K ⊢ σ ⊑ σ′}{K ⊢ ΠX.σ ⊑ ΠX.σ′}
(data) \frac{K ⊢ s ≤ r K ⊢ τ ⊑ τ′}{K ⊢ d^{s}τ ⊑ d^{r}τ′}  (pair) \frac{K ⊢ s ≤ r K ⊢ τ ⊑ σ K ⊢ τ′ ⊑ σ′}{K ⊢ dτ ×^{s} d′τ′ ⊑ dσ ×^{r} d′σ′}

Note that the rule (cst) is contravariant wrt. stages inequalities.

Lemma 3.5. The relation K ⊢ ⊑ is reflexive and transitive.

We now turn to datatype declarations. We assume given a fixed set 𝒞 of constructors, and a function C : 𝒟 ↦ ℘(𝒞) such that C(d) ∩ C(d′) = ∅ for every distinct d, d′ ∈ 𝒟. Each constructor c ∈ C(d) is given an erased type of the form ΠX.|θ| → d X, where |θ| is an erased type in which d and X occur only positively [2]. Note that the arity condition on d imposes that X has the same length for all c ∈ C(d). We let C =_{def} ⋃{C(d) | d ∈ 𝒟}.

Moreover, we distinguish between recursive and non-recursive constructors. This is essential to annotate constructor types and to the reduction and typing rules of fixpoints. Formally, we assume that C(d) = C_{nr}(d) ⊎ C_{r}(d). Then, c ∈ C(d) is recursive if c ∈ C_{r}(d) and non-recursive otherwise. Intuitively, c is nonrecursive iff d does not occur in |θ|. For instance, the constructor nil : ΠX.List X is non-recursive, while cons : ΠX.X → List X → List X is recursive. We write c^{r} (resp. c^{nr}) to denote a recursive (resp. non-recursive) constructor.

Constructor types are annotated as follows: each occurrence of d′ ≠ d in |θ| is annotated with ∞, and each occurrence of d in |θ| is annotated with a stage variable ı. Then, the constrained type of c is of the form ∀ı.ΠX.θ → dîX if c is recursive and of the form ∀ı.ΠX.θ → d^{ı}X otherwise. In particular, we get nil |τ| : List^{0}τ and cons |τ| a l : Listŝτ whenever l : List^{s}τ and a : τ.

Definition 3.6 (Inductive datatypes).

(i) A signature is a map Σ : C ↦ \underline{𝒯} such that for all c ∈ C(d), Σ(c) is a closed type of the form ∀ı.ΠX.θ → d\overline{ı}X where

– θ are sized types on the abstract syntax T^{+} (where d′ ≠ d):

\begin{aligned}T^{+} & ::= & 𝒱_{𝒯} | & T^{−} → T^{+} | & Π𝒱_{𝒯} .T^{+} | & d^{′∞} T^{+} | d^{ı} X \\ T^{−} & ::= & 𝒱_{𝒯} \ X | & T^{+} → T^{−} | & Π𝒱_{𝒯} .T^{−} | & d^{′∞} T^{−} \end{aligned}

– if d occurs in θ then c ∈ C_{r}(d) and \overline{ı} = î; otherwise c ∈ C_{nr}(d) and \overline{ı} = ı. Moreover, let Inst(c, s, τ , σ) =_{def} θ[X := τ , ı := s] → σ.

(ii) Let d ≤_{Σ} d′ iff d occurs in Σ(c) for some c ∈ C(d′). Σ is well-formed if ≤_{Σ} is a partial order whose strict part <_{Σ} is well-founded.

Note that if c ∈ C(d) has type ∀ı.ΠX.θ → d\overline{ı}X, then ı is the sole stage variable occurring in θ. Hence, if c is non-recursive, Inst(c, s, τ , σ) is of the form θ[X := τ] → σ, and we write it Inst(c, , τ , σ).

Note also that well-formed signatures rule out heterogeneous datatypes, and for simplicity, mutually inductive datatypes also. Besides, the positivity requirement for d^{ı}X is standard to guarantee strong normalization. Also, the positivity requirement for X is added to guarantee the soundness of the subtyping rule (data) for datatypes, and to avoid considering polarity, as in e.g. [8].

In the remaining of the paper we assume given a well-formed signature Σ.

3.3 Terms and reductions

Terms are built from variables, abstractions, applications, constructors, caseexpressions, pairs, let-expressions and recursive definitions letrec. Recursive definitions come with case analysis for pattern matching, and let-expressions bind pairs of variables. We assume given a set 𝒱_{ℰ} = {f, x, y, z, … } of term variables.

Definition 3.7. The set ℰ of terms is given by the syntax (where |τ| ∈ |𝒯|):

e, e′ ::= 𝒱_{ℰ} | λx : |τ|.e | e e′ | ΛX.e | e |τ| | c
| case_{|τ|} e of {c ⇒ e}
| ⟨e, e′⟩ | let ⟨x, x′⟩ = e in e′
| letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}

Free and bound variables are defined as usual with the following proviso: in letrec expressions, the (fixpoint) variable f is bound in the branches e^{r} for the recursive constructors, but not in the branches e^{nr} for the non-recursive ones. Hence, by Barendregt convention, we may assume that f ∉ e^{nr}. This is important for the typing and reduction rules of letrec. Note that no stage variable occurs in a term e ∈ ℰ.

Substitutions are maps ρ : (𝒱_{ℰ} ↦ ℰ) ⊎ (𝒱_{𝒯} ↦ |𝒯|) of finite domain. The capture-avoiding application of ρ to e is denoted eρ, but we may also write e[x := ρ(x), X := ρ(X)] when dom(ρ) = x ⊎ X. The reductions are as follows.

Definition 3.8 (Reductions). The relation of βιμθ-reduction → is the smallest rewrite relation containing ↦_{βιμθ}, where

(λx : |τ|.e) e′ ↦_{β} e[x := e′] (ΛX.e) |τ| ↦_{β} e[X := |τ|]
case_{|τ|} (c_{i} |σ| a) of {c ⇒ e} ↦_{ι} e_{i} a
let ⟨x_{1}, x_{2}⟩ = ⟨e_{1}, e_{2}⟩ in e ↦_{θ} e[x_{1} := e_{1}, x_{2} := e_{2}]
letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} (c_{i}^{nr} |σ| a) ↦_{μ} e_{i}^{nr} a
letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} (c_{i}^{r} |σ| a) ↦_{μ} e_{i}^{r}[f := e_{f}] a

with e_{f} = letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}.

The rewrite system ↦_{βιμθ} is orthogonal and thus confluent.

3.4 Typing rules

The typing system is an extension of [3] with sized products and prenex bounded universal stage quantification. Recall that \underline{τ} ∈ \underline{𝒯} denotes a constrained type, ie. a type of the form ∀ı ≤ s.τ where τ ∈ 𝒯 is a sized type. The capture-avoiding substitution of τ for X in σ is written σ[X := τ].

Definition 3.9 (Typing). A context is a map Γ : 𝒱_{ℰ} ↦ \underline{𝒯} of finite domain. The typing relation is the smallest relation K; Γ ⊢ e : \underline{τ} which is closed by the rules of Fig. 1.

The positivity condition ı pos σ in the rule (rec) is defined in the usual way [2]. Note that the expression λx : Nat.x has type ∀ı.Nat^{ı} → Nat^{ı}.

The rule (rec) combines the usual rule of fixpoints (1) with the rule (case). The first premise line is the typing of the branches corresponding to non-recursive constructors. They can not depend on the fixpoint variable f. The others premises are the branches for the recursive constructors, which can depend on the fixpoint variable f. The intuition of the termination argument is the following. Assume that we typecheck the approximation of f at type dĵτ → θ[ı := ĵ] and let c_{k}^{r} : ∀ı.ΠX.θ → dîX. The branch e_{k}^{r} corresponding to c_{k}^{r} must be of type θ[X := τ , ı := ȷ] → θ[ı := ĵ], provided that f is used with type ∀ı ≤ ȷ.d^{ı}τ → θ. That is, only strictly less defined approximations of f can be used to type e_{k}^{r}.

The μ-reduction of fixpoints takes into account the difference between recursive and non-recursive constructors: the fixpoint variable is only substituted in the recursive branches.

Finally, a crucial point with constrained-based approaches is that the satisfiability of the constraints K in judgments K; Γ ⊢ e : τ must be preserved by typing rules read bottom up. With general constraints systems like [10, 4], satisfiability tests of K during type-checking generate existential constraints. This is manageable when stages are interpreted by natural numbers, but this may not be the case when constraints have to be interpreted by countable ordinals. By restricting to bounded universal quantifications ∀ı ≤ s.τ, type checking generates constraints of the form ı ≤ s, which are always satisfiable by [ı := s]. As a consequence, the satisfiability of K in K; Γ ⊢ e : τ is preserved by typing rules, and there is no need of satisfiability tests during type checking. That is why we have a tractable system with stage addition and all positive inductive types.

4 Subject reduction

The proof of the subject reduction property relies on the usual intermediate properties, namely inversion and substitution.

For inversion of typing, it is convenient to work in an equivalent type system, in which stage quantification is independent from the introduction and elimination rules of term constructs.

Definition 4.1. Let F′_{×} be the type system identical to F_{×}, except for the rules (cons) and (rec) which are replaced with

(cons’)  \frac{c ∈ C(d) for some d  Σ(c) = ∀ı.σ}{K; Γ ⊢ c : σ[ı := s]}

(rec’) \frac{C_{nr}(d) = \{c_{1}^{nr}, …, c_{n}^{nr}\}  K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ, θ) (1 ≤ k ≤ n) C_{r}(d) = \{c_{1}^{r}, …, c_{m}^{r}\} K; Γ, f:∀ı ≤ ȷ.d^{ı}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ, θ[ı := ĵ]) (1 ≤ k ≤ m)}{K; Γ ⊢ letrec_{|τ|} f case \{c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}\} : d^{s}τ → θ[ı := s]}
where ı ∉ K, Γ, τ  ı pos θ  ȷ ∉ ı, K, Γ, τ, θ  |τ| = d|τ| → |θ|

Lemma 4.2. K; Γ ⊢ e : \underline{τ} is derivable in F_{×} iff it is derivable in F′_{×}.

Proposition 4.3 (Inversion of stage quantification). Let e ∉ 𝒱_{𝒳} . In F′_{×}, if K; Γ ⊢ e : ∀ı ≤ p.τ then there is a sized type σ such that K, ı ≤ p ⊢ σ ⊑ τ and K, ı ≤ p; Γ ⊢ e : σ is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub).

The main point in using F′_{×} instead of F_{×} in Prop. 4.3 is to ensure that the last rule of the derivation is the rule corresponding to the top symbol of e, when e is not a variable. This leads to the usual inversion properties for typing in F′_{×}, and thus in F_{×} using Lem. 4.2.

Theorem 4.4 (Subject reduction). In F_{×},

(K; Γ ⊢ e_{1} : \underline{τ} ∧ e_{1} → e_{2}) ⟹ K; Γ ⊢ e_{2} : \underline{τ}

5 Strong normalization

We outline a realizability proof that typable terms are strongly normalizing. We begin by the interpretation of stages, and then turn to the strong normalization proof itself, which relies on Tait’s saturated sets.

Stages are interpreted by the ordinals used to build the interpretation of inductive types. While first-order inductive types can be interpreted by induction

(var)  \overline{K; Γ, x:\underline{σ} ⊢ x : \underline{σ}}

(abs)  \frac{K; Γ, x:τ ⊢ e : σ}{K; Γ ⊢ λx : |τ|.e : τ → σ}

(app)  \frac{K; Γ ⊢ e : τ → σ  K; Γ ⊢ e′ : τ}{K; Γ ⊢ e e′ : σ}

(T-abs)  \frac{K; Γ ⊢ e : σ}{K; Γ ⊢ ΛX.e : ΠX.σ} if X ∉ Γ

(T-app)  \frac{K; Γ ⊢ e : ΠX.σ}{K; Γ ⊢ e |τ| : σ[X := τ]}

(S-gen)  \frac{K, ı ≤ s; Γ ⊢ e : \underline{τ}}{K; Γ ⊢ e : ∀ı ≤ s.\underline{τ}} if ı ∉ Γ, K, s

(S-inst)  \frac{K; Γ ⊢ e : ∀ı ≤ s.\underline{τ}  K ⊢ r ≤ s}{K; Γ ⊢ e : \underline{τ}[ı := r]}

(cons)  \frac{c ∈ C(d) for some d}{K; Γ ⊢ c : Σ(c)}

(pair)  \frac{K; Γ ⊢ e_{1} : d_{1}^{s_{1}} τ_{1}  K; Γ ⊢ e_{2} : d_{2}^{s_{2}} τ_{2}}{K; Γ ⊢ ⟨e_{1}, e_{2}⟩ : d_{1} τ_{1} ×^{s_{1}+s_{2}} d_{2} τ_{2}}

(let)  \frac{\begin{matrix}K; Γ ⊢ e : d_{1} τ_{1} ×^{s} d_{2} τ_{2} \\ K, ı_{1} + ı_{2} ≤ s; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2} ⊢ e′ : σ \end{matrix}}{K; Γ ⊢ let ⟨x_{1}, x_{2}⟩ = e in e′ : σ}

where ı_{1}, ı_{2} ∉ Γ, K, σ, s, τ_{1}, τ_{2}

(case)  \frac{\begin{aligned}& K; Γ ⊢ e : dŝτ \\ C(d) = \{c_{1}, …, c_{n}\} & K; Γ ⊢ e_{k} : Inst(c_{k}, s, τ, θ) & (1 ≤ k ≤ n) \end{aligned}}{K; Γ ⊢ case_{|θ|} e of \{c ⇒ e\} : θ}

(rec)  \frac{C_{nr}(d) = \{c_{1}^{nr}, …, c_{n}^{nr}\}  K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ, θ) (1 ≤ k ≤ n) C_{r}(d) = \{c_{1}^{r}, …, c_{m}^{r}\} K; Γ, f:∀ı ≤ ȷ.d^{ı}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ, θ[ı := ĵ]) (1 ≤ k ≤ m)}{K; Γ ⊢ letrec_{|τ|} f case \{c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}\} : ∀ı.d^{ı}τ → θ}
where ı ∉ K, Γ, τ  ı pos θ  ȷ ∉ ı, K, Γ, τ, θ  |τ| = d|τ| → |θ|

(sub)  \frac{K; Γ ⊢ e : \underline{σ}  K ⊢ \underline{σ} ⊑ \underline{τ}}{K; Γ ⊢ e : \underline{τ}}

Fig. 1. Typing rules for F_{×}

on ℕ, higher-order inductive types may require an induction on countable ordinals. Existing systems with stage addition [10, 4] are restricted to first-order inductive types, and stages constraints are formulas of Presburger arithmetic.

We go one step further by allowing at the same time all positive inductive types and stage addition. Stage addition is interpreted by the natural addition on countable ordinals. This operation is associative and commutative, in contrast with the usual ordinal addition which is in general not commutative.

In the whole section, if f is a map from A to B, a ∈ A and b ∈ B, then f(a := b) : A ↦ B maps a to b and is equal to f everywhere else.

5.1 The stage model

Stages are interpreted by ordinals below the first uncountable cardinal.

Definition 5.1 (Countable ordinals). We denote by (Ω, ≤_{Ω}) the well-ordered set of countable ordinals and by +_{Ω} the usual ordinal addition on Ω.

Recall that ℕ can be seen as a proper subset of Ω and that +_{Ω} coincide with the usual addition on ℕ. We want an associative and commutative addition on Ω, but +_{Ω} is in general not commutative on Ω. Instead, we use the natural addition on ordinals. To define it, we use the well-known fact that every α ∈ Ω can be written in Cantor normal form,

α = c_{n}.ω^{α_{n}} +_{Ω} ⋯ +_{Ω} c_{1}.ω^{α_{1}}

where α_{1} <_{Ω} … <_{Ω} α_{n} ∈ Ω and c_{1}, …, c_{n} ∈ ℕ. The natural addition ⊕ on Ω is then defined as

\begin{aligned}& (c_{n}.ω^{α_{n}} +_{Ω} ⋯ +_{Ω} c_{1}.ω^{α_{1}}) ⊕ (d_{n}.ω^{α_{n}} +_{Ω} ⋯ +_{Ω} d_{1}.ω^{α_{1}}) \\ =_{def} & (c_{n} +_{Ω} d_{n}).ω^{α_{n}} +_{Ω} ⋯ +_{Ω} (c_{1} +_{Ω} d_{1}).ω^{α_{1}} \end{aligned}

Proposition 5.2. The natural addition is associative, commutative and with neutral element 0. Moreover, for all α ∈ Ω, the successor ordinal of α is α ⊕ 1.

We are now ready to define our stage model. Each inductive type can be interpreted using an induction up to a countable ordinal (see Prop. 5.9). We can thus interpret ∞ by Ω. This motivates the following definition.

Definition 5.3 (Stage model). Let Ω̂ =_{def} Ω ∪ {Ω}. For all α, β ∈ Ω̂, let

α < β iff (β = Ω ∨ α <_{Ω} β)  and  α + β =_{def} \{ \begin{matrix}α ⊕ β & if α, β ∈ Ω \\ Ω & otherwise \end{matrix}

So we have an addition + on stages which is monotone, associative and commutative. Moreover we have α + β < Ω for all α, β < Ω.

Definition 5.4 (Interpretation of stages). A stage valuation is a map π from 𝒱_{𝒮} to Ω̂, and is extended to a stage interpretation ⦇.⦈_{π} : 𝒮 ↦ Ω̂ as follows:

⦇0⦈_{π} =_{def} 0  ⦇∞⦈_{π} =_{def} Ω  ⦇ŝ⦈_{π} =_{def} ⦇s⦈_{π}+1  ⦇s + r⦈_{π} =_{def} ⦇s⦈_{π}+⦇r⦈_{π}

We let π ⊧ K if ⦇s⦈_{π} ≤ ⦇p⦈_{π} for all s ≤ p ∈ K, and let K ⊧ s ≤ r if π ⊧ s ≤ r for all π such that π ⊧ K. K is satisfiable if there is π such that π ⊧ K.

5.2 Type interpretation

Let SN be the set of strongly normalizing terms. We interpret types by saturated sets. It is convenient to define them by means of elimination contexts:

E[ ] ::= [ ] | E[ ] e | E[ ] |τ| | case_{|τ|} E[ ] of {c ⇒ e}
| let ⟨x, x′⟩ = E[ ] in e′ | letrec_{|τ|} f case {c ⇒ e} E[ ]

Note that the hole [ ] of E[ ] never occurs under a binder. Thus E[ ] can be seen as a term with one occurrence of a special variable [ ].

Let E[e] →_{wh} E[e′] if e ↦_{βιμθ} e′.

Definition 5.5 (Saturated sets). A set S ⊆ SN is saturated (S ∈ SAT) if

(SAT1) E[x] ∈ S for all E[ ] ∈ SN and all x ∈ 𝒱_{𝒳} , (SAT2) if e ∈ SN and e →_{wh} e′ for some e′ ∈ S then e ∈ S.

It is well-known that SN ∈ SAT and that ⋂ 𝒴, ⋃ 𝒴 ∈ SAT for all non-empty 𝒴 ⊆ SAT. Hence, for each X ⊆ SN there is a smallest saturated set containing X, written \overline{X}. As usual, the function space on SAT is given for X, Y ∈ SAT by:

X → Y =_{def} {e | ∀e′. e′ ∈ X ⟹ e e′ ∈ Y }

The interpretation of types is defined in two steps. We first define the interpretation scheme of types, given an interpretation of datatypes. We then define the interpretation of datatypes.

Definition 5.6. An interpretation of datatypes is a family of functions (I_{d})_{d∈𝒟} where I_{d} : SAT^{ar(d)} × Ω̂ ↦ SAT for each d ∈ 𝒟. Given an interpretation of datatypes I, a stage valuation π and a type valuation ξ : 𝒱_{𝒯} ↦ SAT, the type interpretation ⟦.⟧_{π,ξ}^{I} : \underline{𝒯} ↦ SAT is defined by induction on types as follows

⟦∀ı ≤ s.\underline{τ}⟧_{π,ξ}^{I} = ⋂\{⟦\underline{τ}⟧_{π(ı:=α),ξ}^{I} | α ≤ ⦇s⦈_{π}\}
⟦X⟧_{π,ξ}^{I} = ξ(X)
⟦τ → σ⟧_{π,ξ}^{I} = ⟦τ⟧_{π,ξ}^{I} → ⟦σ⟧_{π,ξ}^{I}
⟦ΠX.τ⟧_{π,ξ}^{I} = {e | ∀|σ| ∈ |𝒯|, ∀S ∈ SAT, e |σ| ∈ ⟦τ⟧_{π,ξ(X:=S)}^{I}}
⟦dτ ×^{s} d′τ′⟧_{π,ξ}^{I} = ⋃{⟨I_{d}(⟦τ ⟧_{π,ξ}^{I}, α), I_{d′}(⟦τ′⟧_{π,ξ}^{I}, α′)⟩ | α + α′ ≤ ⦇s⦈_{π}}
⟦d^{s}τ ⟧_{π,ξ}^{I} = I_{d}(⟦τ ⟧_{π,ξ}^{I}, ⦇s⦈_{π})

where ⟨S_{1}, S_{2}⟩ =_{def} \overline{\{⟨e_{1}, e_{2}⟩ | e_{1} ∈ S_{1} ∧ e_{2} ∈ S_{2}\}} for all S_{1}, S_{2} ∈ SAT.

Note that unions and intersections are always taken over non-empty sets of saturated sets.

We now define the interpretation of inductive datatypes. Recall that the relation <_{Σ} is assumed to be a well-founded strict partial order (see Def. 3.6). The interpretation (I_{d})_{d∈𝒟} is defined by induction on <_{Σ}, and for each d ∈ 𝒟, the map I_{d} : SAT^{ar(d)} × Ω̂ ↦ SAT is defined by induction on Ω̂.

Substitution  ⦇p[ı := s]⦈_{π} = ⦇p⦈_{π(ı:=⦇s⦈_{π})}
⟦\underline{τ}[ı := s]⟧_{π,ξ} = ⟦\underline{τ}⟧_{π(ı:=⦇s⦈_{π}),ξ}
⟦\underline{τ}[X := σ]⟧_{π,ξ} = ⟦\underline{τ}⟧_{π,ξ(X:=⟦σ⟧_{π,ξ})}
Stage monotony  α ≤ β ⇒ I_{d}(S, α) ⊆ I_{d}(S, β)
α ≤ β ∧ ı pos θ ⇒ ⟦θ⟧_{π(ı:=α),ξ} ⊆ ⟦θ⟧_{π(ı:=β),ξ}
α ≤ β ∧ ı neg θ ⇒ ⟦θ⟧_{π(ı:=β),ξ} ⊆ ⟦θ⟧_{π(ı:=α),ξ}
Substage soundness  K ⊢ s ≤ p ⇒ K ⊧ s ≤ p
Subtyping soundness  K ⊢ \underline{τ} ⊑ \underline{σ} ∧ π ⊧ K ⇒ ⟦\underline{τ}⟧_{π,ξ} ⊆ ⟦\underline{σ}⟧_{π,ξ}

Fig. 2. Properties of the type interpretation

Definition 5.7. For all d ∈ 𝒟, all S ∈ SAT^{ar(d)} and all α ∈ Ω̂, we define I_{d}(S, α), by induction on pairs (d, α) ordered by (<_{Σ}, <)_{lex}, as follows:

I_{d}(S, 0) = ⋃{c^{nr} ⟦θ⟧_{∅,X:=S}^{I} | c^{nr} ∈ C_{nr}(d) ∧ Σ(c^{nr}) = ∀ı.ΠX.θ → d^{ı}X}
I_{d}(S, α ⊕ 1) = ⋃\{c ⟦θ⟧_{ı:=α,X:=S}^{I} | c ∈ C(d) ∧ Σ(c) = ∀ı.ΠX.θ → d\overline{ı}X\}
I_{d}(S, λ) = ⋃{I_{d}(S, α) | α < λ}  if λ is a limit ordinal

where c S =_{def} \overline{\{c |τ | a | a ∈ S ∧ |τ | ∈ |𝒯|\}} for all S ∈ SAT.

Note that I_{d}(S, α ⊕ 1) only uses c⟦θ⟧_{ı:=α,X:=S}^{I} with c ∈ C(d), which in turn only uses I_{d′}(U, β) with (d′, β) (<_{Σ}, <)_{lex} (d, α ⊕ 1).

Definition 5.8. Let ⟦.⟧_{π,ξ} =_{def} ⟦.⟧_{π,ξ}^{I}.

Fig. 2 collects some essential properties of ⦇.⦈_{π} and ⟦.⟧_{π,ξ}. The following proposition states that each inductive datatype can be interpreted by a countable ordinal. This is crucial in order to deal with the rule (cons) in the proof of Thm. 5.10. The key-point is that for every countable S ⊆ Ω, there is β ∈ Ω such that α < β for all α ∈ S [6].

Proposition 5.9. For all d ∈ 𝒟 and all S ∈ SAT^{ar(d)}, there is an ordinal α < Ω such that I_{d}(S, α) = I_{d}(S, β) for all β such that α ≤ β ≤ Ω.

As usual, soundness is shown by induction on typing derivations. Note that if K is satisfied by π, then every K′ occurring in the derivation of K; Γ ⊢ e : \underline{τ} is satisfied by an extension of π. Thus, in contrast to [4], there is no need of tests of the form K ⊢ ∃ı.P in typing derivations.

Theorem 5.10 (Typing soundness). Given π : 𝒱_{𝒮} ↦ Ω̂, ξ : 𝒱_{𝒯} ↦ SAT and ρ : (𝒱_{ℰ} ↦ ℰ) ⊎ (𝒱_{𝒯} ↦ |𝒯|), we let (π, ξ, ρ) ⊧ K; Γ if and only if π ⊧ K and ρ(x) ∈ ⟦Γ (x)⟧_{π,ξ} for all x ∈ dom(Γ).

If K; Γ ⊢ e : \underline{τ}, then eρ ∈ ⟦\underline{τ}⟧_{π,ξ} for all π, ξ, ρ such that (π, ξ, ρ) ⊧ K; Γ.

We deduce the strong normalization of terms typable with satisfiable K.

Corollary 5.11. If K; Γ ⊢ e : \underline{τ} with K satisfiable, then e ∈ SN.

6 Conclusion

F_{×} is a variant of F that supports simple yet precise typing by using sized products instead of existential quantification, for which subject reduction is problematic. We have proved strong normalization and subject reduction of F_{×}, and conjecture that type-checking is tractable. On the other hand, size inference seems more difficult than in [3], in particular for precise annotations with addition such as for the function append on lists.

Our main next objective is to extend our results to the Calculus of Inductive Constructions, and to implement type-based termination in Coq. It would also be interesting to study the expressivity of more general forms of sized products, both with general container types instead of cartesian products, and arbitrary binary operators instead of +. Moreover, it would be interesting to study the tractability of more liberal subtyping relations for universal stage quantifications. Finally, an outstanding issue is the design of a strongly normalizing type system in which non-recursive constructors can be given the size zero while keeping fixpoint definitions separated from case analysis.

References

1. A. Abel. Type-Base Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, LMU University, Munich, 2006.

2. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-Based Termination of Recursive Definitions. Mathematical Structures in Computer Science, 14(1):97–141, 2004.

3. G. Barthe, B. Grégoire, and F. Pastawski. Practical Inference for Type-Based Termination in a Polymorphic Setting. In Proceedings of TLCA’05, pages 71–85, 2005.

4. F. Blanqui and C. Riba. Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. In Proceedings of LPAR’06, volume 4246 of LNAI, 2006.

5. W.-N. Chin and S.-C. Khoo. Calculating Sized Types. Higher-Order and Symbolic Computation, 14(2–3):261–300, 2001.

6. J.H. Gallier. What’s So Special About Kruskal’s Theorem and the Ordinal Γ_{0}? A Survey of Some Results in Proof Theory. Annals of Pure and Applied Logic, 53(3):199–260, 1991.

7. J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of POPL’96, pages 410–423. ACM, 1996.

8. M. Steffen. Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen, 1997.

9. M. Tatsuta. Simple Saturated Sets for Disjunction and Second-Order Existential Quantification. In Proceedings of TLCA’07, volume 4583 of LNCS, pages 366–380. Springer, 2007.

10. H. Xi. Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation, 15(1):91–131, 2002.

K; Γ ⊢ e_{1} e_{2} : τ ⇒ ∃σ, σ′.

K ⊢ σ ⊑ τ ∧ K; Γ ⊢ e_{1} : σ′ → σ ∧ K; Γ ⊢ e_{2} : σ′

K; Γ ⊢ λx : |σ|.e_{1} : τ ⇒ ∃τ_{1}, τ_{2}.

|τ_{2}| = |σ| ∧ K ⊢ τ_{2} → τ_{1} ⊑ τ ∧ K; Γ, x:τ_{2} ⊢ e : τ_{1}

K; Γ ⊢ e |σ| : τ ⇒ ∃X, σ_{1}, σ_{2}.

|σ_{2}| = |σ| ∧ K ⊢ σ_{1}[X := σ_{2}] ⊑ τ ∧ K; Γ ⊢ e : ΠX.σ_{1}

K; Γ ⊢ ΛX.e : τ ⇒ ∃σ. K ⊢ ΠX.σ ⊑ τ ∧ K; Γ ⊢ e : σ
K; Γ ⊢ c^{nr} : τ ⇒ ∃d, s, θ.

K ⊢ ΠX.θ → d^{s}X ⊑ τ ∧ Σ(c^{nr}) = ∀ı.ΠX.θ → d^{ı}X

K; Γ ⊢ c^{r} : τ ⇒ ∃d, s, θ.

K ⊢ ΠX.θ[ı := s] → dŝX ⊑ τ ∧ Σ(c^{r}) = ∀ı.ΠX.θ → dîX

K; Γ ⊢ ⟨e, e′⟩ : τ ⇒ ∃d, d′, s, s′, τ, τ′.

K ⊢ d τ ×^{s+s′} d′ τ′ ⊑ τ ∧ K; Γ ⊢ e : d^{s}τ ∧ K; Γ ⊢ e′ : d′^{s′}τ′

K; Γ ⊢ letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : τ ⇒ ∃d, s, ı, ȷ, τ, θ.

K ⊢ d^{s}τ → θ[ı := s] ⊑ τ

∧ ∀k ∈ {1, …, n}.  K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ, θ)
∧ ∀k ∈ {1, …, m}.  K; Γ, f:∀ı ≤ ȷ.d^{ı}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ, θ[ı := ĵ])

Fig. 3. Inversion of typing

A Subject reduction

In this section, we prove Thm. 4.4, that is subject reduction for F_{×}. We actually show subject reduction for F′_{×} in Thm. A.12, from which we deduce subject reduction for F_{×} (Cor. A.13). Recall that F′_{×} is defined in Def. 4.1. In this section, unless explicitly stated otherwise we only work in F′_{×}.

The main properties are the usual inversion and substitution lemmas. Substitutions properties are gathered in Fig. 4 and inversion is depicted in Fig. 3.

A.1 Basic lemmas on stages

We begin by some basic lemmas on stages.

Proposition A.1 (Stage weakening). If K ⊢ s ≤ r then K, p ≤ q ⊢ s ≤ r.

Proof. By induction on K ⊢ s ≤ r. ⊓ ⊔

Lemma A.2 (Size cut admissibiliy). Let P and Q be two stages inequalities.

(i) If K, K′, P ⊢ Q and K ⊢ P then K, K′ ⊢ Q. (ii) If K, K′, P ⊢ \underline{τ} ⊑ \underline{σ} and K ⊢ P then K, K′ ⊢ \underline{τ} ⊑ \underline{σ}.

K ⊢ p ≤ q ⇒ K[ı := s] ⊢ p[ı := s] ≤ q[ı := s]
K ⊢ \underline{σ} ⊑ \underline{τ} ⇒ K[ı := s] ⊢ \underline{σ}[ı := s] ⊑ \underline{τ}[ı := s]
K; Γ ⊢ e : \underline{τ} ⇒ K[ı := s] ; Γ [ı := s] ⊢ e : \underline{τ}[ı := s]
(ı pos \underline{τ} ∧ K ⊢ s ≤ r) ⇒ K ⊢ \underline{τ}[ı := s] ⊑ \underline{τ}[ı := r]
(ı neg \underline{τ} ∧ K ⊢ r ≤ s) ⇒ K ⊢ \underline{τ}[ı := s] ⊑ \underline{τ}[ı := r]
(K; Γ, x:\underline{σ} ⊢ e : \underline{τ} ∧ K; Γ ⊢ e′ : \underline{σ}) ⇒ K; Γ ⊢ e[x := e′] : \underline{τ}
K ⊢ \underline{σ} ⊑ \underline{τ} ⇒ K ⊢ \underline{σ}[X := θ] ⊑ \underline{τ}[X := θ]
K; Γ ⊢ e : \underline{τ} ⇒ K; Γ [X := σ] ⊢ e[X := |σ|] : \underline{τ}[X := σ]
(X pos \underline{θ} ∧ K ⊢ σ ⊑ τ) ⇒ K ⊢ \underline{θ}[X := σ] ⊑ \underline{θ}[X := τ]
(X neg \underline{θ} ∧ K ⊢ τ ⊑ σ) ⇒ K ⊢ \underline{θ}[X := σ] ⊑ \underline{θ}[X := τ]

Fig. 4. Substitution properties

(iii) If K, K′, P ; Γ ⊢ e : \underline{τ} and K ⊢ P then K, K′; Γ ⊢ e : \underline{τ} in an isomorphic derivation tree.

Proof. By induction on K, K′, P ⊢ Q for (i); by induction on K, K′, P ⊢ \underline{τ} ≤ \underline{σ}, using (i) for (ii); by induction on K, K′, P ; Γ ⊢ e : \underline{τ}, using (i), (ii) for (iii). ⊓ ⊔

We now turn to properties of stage substitution.

Proposition A.3 (Commutation of substitutions).

(i) If ȷ ≠ ı and (ȷ ∉ s or ı ∉ p), then

p[ȷ := r][ı := s] = p[ı := s][ȷ := r[ı := s]]

(ii) If ȷ ≠ ı and (ȷ ∉ s or ı ∉ \underline{τ}), then

\underline{τ}[ȷ := r][ı := s] = \underline{τ}[ı := s][ȷ := r[ı := s]]

(iii) τ[X := σ][ı := s] = τ[ı := s][X := σ[ı := s]] (iv) For all constructor c,

Inst(c, s, τ , θ)[ȷ := r] = Inst(c, s[ȷ := r], τ [ȷ := r], θ[ȷ := r])

Proof. By induction on p for (i); by induction on \underline{τ}, using (i) for (ii). Property (iii) is shown by induction on τ, and (iv) follows from (ii) and (iii). ⊓ ⊔

The next two lemmas (Lem. A.4 and Lem. A.5) correspond to the first five properties depicted in Fig. 4. Note that the case (iii) of Lem. A.4 is stronger than the corresponding property of Fig. 4. We rely on this to prove Thm. A.12.

Lemma A.4 (Stage substitution).

(i) If K ⊢ p ≤ q then K[ı := s] ⊢ p[ı := s] ≤ q[ı := s]. (ii) If K ⊢ \underline{σ} ⊑ \underline{τ} then K[ı := s] ⊢ \underline{σ}[ı := s] ⊑ \underline{τ}[ı := s] (iii) If K; Γ ⊢ e : \underline{τ} then K[ı := s] ; Γ [ı := s] ⊢ e : \underline{τ}[ı := s] in an isomorphic

derivation tree.

Proof.

(i) By induction on K ⊢ p ≤ q. (ii) By induction on K ⊢ \underline{σ} ⊑ \underline{τ}. (iii) By induction on the height h of the derivation tree of K; Γ ⊢ e : \underline{τ}.

The cases of the rules (var), (abs), (app), (T-abs), (pair), (case) are trivial. We use Prop. A.3.(iii) for the rule (T-app), Prop. A.3.(iv) for the rule (case), and property (ii) for (sub). The rule (S-gen) is dealt with using Barendregt convention: since ȷ appears bound in the sequent K; Γ ⊢ e : ∀ȷ ≤ p.\underline{τ}, we may assume that ȷ ≠ ı and that ȷ ∉ s. Rules (S-inst) and (cons) are dealt with similarly, using the following facts:

– since ȷ ≠ ı and ȷ ∉ s, we have \underline{τ}[ȷ := r][ı := s] = \underline{τ}[ı := s][ȷ := r[ı := s]] by Prop. A.3.(ii).

– since K ⊢ r ≤ p, we have K[ı := s] ⊢ r[ı := s] ≤ p[ı := s] by property (i). It remains the cases of the rules (let) and (rec). (let)

\frac{\begin{matrix}K; Γ ⊢ e : d_{1} τ_{1} ×^{r} d_{2} τ_{2} \\ K, ı_{1} + ı_{2} ≤ r; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2} ⊢ e′ : σ \end{matrix}}{K; Γ ⊢ let ⟨x_{1}, x_{2}⟩ = e in e′ : σ}

where ı_{1}, ı_{2} ∉ Γ, K, σ, r, τ_{1}, τ_{2}

Assume that

K; Γ ⊢ let ⟨x_{1}, x_{2}⟩ = e in e′ : σ  (7)

is derivable in a tree of height less that h + 1, with

K; Γ ⊢ e : d_{1} τ_{1} ×^{r} d_{2} τ_{2}  (8)

and

K, ı_{1} + ı_{2} ≤ r; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2} ⊢ e′ : σ  (9)

derivable in trees of height less than h. Let be two distinct stage variables ȷ_{1}, ȷ_{2} ∉ Γ, K, σ, s, r, τ_{1}, τ_{2}. By applying two times the induction hypothesis with the substitutions [ı_{1} := ȷ_{1}] and [ı_{2} := ȷ_{2}], since ı_{1}, ı_{2} ∉ Γ, K, σ, r, s, τ_{1}, τ_{2} we obtain that

K, ȷ_{1} + ȷ_{2} ≤ r; Γ, x_{1} :d_{1}^{ȷ_{1}} τ_{1}, x_{2} :d_{2}^{ȷ_{2}} τ_{2} ⊢ e′ : σ

is derivable in a tree isomorphic to the derivation tree of (9), hence of height less than h. Applying again the induction hypothesis, we get that

K[ı := s] ; Γ [ı := s] ⊢ e : d_{1} τ_{1}[ı := s] ×^{r[ı:=s]} d_{2} τ_{2}[ı := s]

and

\begin{matrix}K[ı := s], ȷ_{1} + ȷ_{2} ≤ r[ı := s] ; \\ Γ, x_{1} :d_{1}^{ȷ_{1}} τ_{1}[ı := s], x_{2} :d_{2}^{ȷ_{2}} τ_{2}[ı := s] ⊢ e′ : σ[ı := s] \end{matrix}

are derivable in trees isomorphic to the derivation trees of (8) (resp. (9)). Since ȷ_{1}, ȷ_{2} ∉ Γ, K, σ, r, s, τ_{1}, τ_{2}, we have

ȷ_{1}, ȷ_{2} ∉ Γ [ı := s], K[ı := s], σ[ı := s], r[ı := s], τ_{1}[ı := s], τ_{2}[ı := s]

and we can apply the rule (let) to obtain that

K[ı := s] ; Γ [ı := s] ⊢ let ⟨x_{1}, x_{2}⟩ = e in e′ : σ[ı := s]

in a tree isomorphic to the derivation tree of (7). (rec)

\frac{C_{nr}(d) = \{c_{1}^{nr}, …, c_{n}^{nr}\} K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ , θ) (1 ≤ k ≤ n) C_{r}(d) = \{c_{1}^{r}, …, c_{m}^{r}\} K; Γ, f:∀κ ≤ ȷ.d^{κ}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ , θ[κ := ĵ]) (1 ≤ k ≤ m)}{K; Γ ⊢ letrec_{|τ|} f case \{c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}\} : d^{κ}τ → θ[κ := r]}

where κ ∉ K, Γ, τ  κ pos θ  ȷ ∉ κ, K, Γ, τ , θ  |τ| = d|τ | → |θ|

Assume that

K; Γ ⊢ letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : d^{r}τ → θ[κ := r] (10)

is derivable in a tree of height less than h + 1 with for all k ∈ {1, …, n},

K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ , θ)  (11)

and for all k ∈ {1, …, m},

K; Γ, f:∀κ ≤ ȷ.d^{κ}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ , θ[κ := ĵ])  (12)

derivable in trees of height less than h. Recall that thanks to Prop A.3.(iv), for all c ∈ C(d) we have

Inst(c, ȷ, τ, θ[κ := ĵ])[ı := s] = Inst(c, ȷ[ı := s], τ[ı := s], θ[κ := ĵ][ı := s])

We first show the following claim: We can assume that ȷ ≠ ı. Let ȷ′ be a fresh stage variable. Since we

have ȷ ∉ κ, K, Γ, τ , θ, by applying the induction hypothesis to (12) with substitution [ȷ := ȷ′], for all k ∈ {1, …, m}, we can derive

K; Γ, f:∀κ ≤ ȷ′.d^{κ}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ′, τ , θ[κ := ĵ][ȷ := ȷ′])

in trees isomorphic to (12), hence of height less than h. Moreover, since ȷ′ is fresh, By Prop. A.3.(ii), we have

θ[κ := ĵ][ȷ := ȷ′] = θ[ȷ := ȷ′][κ := ĵ[ȷ := ȷ′]]

Hence, since ȷ ∉ θ, we get θ[κ := ĵ][ȷ := ȷ′] = θ[κ := ĵ′]. ⊓ ⊔ By Barendregt convention, since κ appears bound the derivation tree, we may assume that κ ≠ ı and that κ ∉ s. By Prop. A.3.(ii), we have

θ[κ := r][ı := s] = θ[ı := s][κ := r[ı := s]]

Since moreover ȷ ≠ ı, again by Prop. A.3.(ii), we have

θ[κ := ĵ][ı := s] = θ[ı := s][κ := r]

Let K′ =_{def} K[ı := s], Γ′ =_{def} Γ [ı := s], r′ =_{def} r[ı := s], τ′ =_{def} τ [ı := s] and θ′ =_{def} θ[ı := s]. Now, by induction hypothesis, for all k ∈ {1, …, n} we can derive K′; Γ′ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ′, θ′), and for all k ∈ {1, …, m} we can derive K′; Γ′, f:∀κ ≤ ȷ.d^{κ}τ′ → θ′ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ′, θ′[κ := ĵ]) in trees isomorphic to the trees respectively of (11) and of (12), hence of height less than h. We conclude that

K′; Γ′ ⊢ letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : d^{r′}τ′ → θ′[κ := r′]

is derivable in a tree isomorphic to that of (10). ⊓ ⊔

Lemma A.5 (Stage monotony). If ı pos \underline{τ} and K ⊢ s ≤ r then K ⊢ \underline{τ}[ı := s] ⊑ \underline{τ}[ı := r]. If ı neg \underline{τ} and K ⊢ r ≤ s then K ⊢ \underline{τ}[ı := s] ⊑ \underline{τ}[ı := r].

Proof. The two statements are shown simultaneously by induction on \underline{τ}. ⊓ ⊔

A.2 Inversion

We now turn to inversion properties. We begin by the proof of Lem. 3.5.

Lemma A.6 (Lem. 3.5). The following subtyping rules are admissible:

(refl) \overline{K ⊢ \underline{σ} ⊑ \underline{σ}}  (trans) \frac{K ⊢ \underline{σ} ⊑ \underline{σ′} K ⊢ \underline{σ′} ⊑ \underline{σ′′}}{K ⊢ \underline{σ} ⊑ \underline{σ′′}}

Proof. The admissibility of (refl) is shown by induction on \underline{σ}. For the admissibility of (trans), reason by induction on K ⊢ \underline{σ} ⊑ \underline{σ′} and K ⊢ \underline{σ′} ⊑ \underline{σ′′}, using the transitivity of the substage relation. The key-point is that both derivations are isomorphic.

Since the subtyping relation is syntax directed, its inversion property is trivial and we do not state it. To prove inversion of typing, we rely on Prop. 4.3.

Proposition A.7 (Inversion of stage quantification – Prop. 4.3). Let e ∉ 𝒱_{𝒳} . If K; Γ ⊢ e : ∀ı ≤ p.τ then there is a sized type σ such that K, ı ≤ p ⊢ σ ⊑ τ and K, ı ≤ p; Γ ⊢ e : σ is derivable in a derivation tree whose last rule is neither (S-gen), (S-inst) nor (sub).

Proof. By induction on K; Γ ⊢ e : ∀ı ≤ p.τ. Since e is not a variable, the last rule can not be (var). Among the other rules, only (S-gen), (S-inst), (sub) allow a constrained type in their conclusion. Therefore, if the last rule is not one of them, then we have ∀ı ≤ p.τ = τ and we conclude by taking σ =_{def} τ.

(S-gen)

\frac{K, ȷ ≤ q; Γ ⊢ e : ∀ı ≤ p.τ}{K; Γ ⊢ e : ∀ȷ ≤ q.∀ı ≤ p.τ} if ȷ ∉ Γ, K, q

By induction hypothesis there is a sized type σ such that K, ȷ ≤ q, ı ≤ p ⊢ σ ⊑ τ and K, ȷ ≤ q, ı ≤ p; Γ ⊢ e : σ is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub).

(S-inst)

\frac{K; Γ ⊢ e : ∀ȷ ≤ q.∀ı ≤ p.τ K ⊢ s ≤ q}{K; Γ ⊢ e : ∀ı ≤ p.τ[ȷ := s]}

By applying Barendregt convention, since stage variables ȷ, ı appears bound in ∀ȷ ≤ q.∀ı ≤ p.τ, we may assume that ȷ ∉ ı, s and that ı ∉ s, K, Γ. It follows that (∀ı ≤ p.τ)[ȷ := s] = ∀ı ≤ p[ȷ := s].τ[ȷ := s]. By induction hypothesis there is a type σ such that K, ȷ ≤ q, ı ≤ p ⊢ σ ⊑ τ and K, ȷ ≤ q, ı ≤ p; Γ ⊢ e : σ is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub). By Lem. A.4, since ȷ ∉ K, Γ, q we deduce that

K, s ≤ q, ı ≤ p[ȷ := s] ⊢ σ[ȷ := s] ⊑ τ[ȷ := s]

and that K, s ≤ q, ı ≤ p[ȷ := s] ; Γ ⊢ e : σ[ȷ := s] is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub). Since K ⊢ s ≤ q, by Lem. A.2 we obtain K, ı ≤ p[ȷ := s] ⊢ σ[ȷ := s] ⊑ τ[ȷ := s] and that

K, ı ≤ p[ȷ := s] ; Γ ⊢ e : σ[ȷ := s]

is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub).

(sub)

\frac{K; Γ ⊢ e : \underline{σ} K ⊢ \underline{σ} ⊑ ∀ı ≤ p.τ}{K; Γ ⊢ e : ∀ı ≤ p.τ}

By Barendregt convention, we can assume that ı ∉ K, Γ. By repeated application of subtyping inversion, we know that \underline{σ} = ∀ı ≤ q.σ with K, ı ≤ p ⊢ σ ⊑ τ and K ⊢ p ≤ q. By induction hypothesis there is a sized type σ′ such that K, ı ≤ q ⊢ σ′ ⊑ σ and K, ı ≤ q; Γ ⊢ e : σ′ in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub). From K ⊢ p ≤ q, by stage weakening (Prop. A.1) we get K, ı ≤ p ⊢ p ≤ q and using the substage rule (trans) we deduce that K, ı ≤ p ⊢ ı ≤ q. By Lem. A.2 and Prop. A.1 we obtain that K, ı ≤ p ⊢ σ′ ⊑ σ and that K, ı ≤ p; Γ ⊢ e : σ′ is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub) ; and using the subtyping rule (trans) we conclude that K, ı ≤ p ⊢ σ′ ⊑ τ. ⊓ ⊔

We now show the inversion properties of typing stated in Fig. 3. Note that they hold for both F_{×} and F′_{×}.

The main point in using F′_{×} instead of F_{×} in Prop. 4.3 is to ensure that the last rule of the derivation is the rule corresponding to the top symbol of e. Hence the inversion is easily proved in F′_{×}. Inversion for F_{×} then easily follows from Lem. 4.2.

Proposition A.8 (Inversion of typing). The properties of Fig. 3 hold for both F_{×} and F′_{×}.

Proof. We first show them for F′_{×}. The result for F_{×} then follows from Lem. 4.2.

In each case, by Prop. A.7 there is a sized type σ such that K ⊢ σ ⊑ τ and K; Γ ⊢ e : σ is derivable in a derivation whose last rule is neither (S-gen), (S-inst) nor (sub). Therefore, the last applied rule in that derivation can only by the rule corresponding to the top construction of e, and we conclude using subtyping inversion. ⊓ ⊔

A.3 Subject Reduction

We now turn to subject reduction. We begin by some usual substitutions properties. They are the last five properties depicted in Fig. 4.

Lemma A.9 (Term Substitution). If K; Γ, x: \underline{σ} ⊢ e : \underline{τ} and K; Γ ⊢ e′ : \underline{σ} then K; Γ ⊢ e[x := e′] : \underline{τ}.

Proof. By induction on K; Γ, x:\underline{σ} ⊢ e : \underline{τ}. ⊓ ⊔

Lemma A.10 (Type Substitution).

(i) If K ⊢ \underline{σ} ⊑ \underline{τ} then K ⊢ \underline{σ}[X := θ] ⊑ \underline{τ}[X := θ] (ii) If K; Γ ⊢ e : \underline{τ} then K; Γ [X := σ] ⊢ e[X := |σ|] : \underline{τ}[X := σ] (iii) If K ⊢ σ ⊑ τ and X pos \underline{θ} then K ⊢ \underline{θ}[X := σ] ⊑ \underline{θ}[X := τ]

If K ⊢ τ ⊑ σ and X neg \underline{θ} then K ⊢ \underline{θ}[X := σ] ⊑ \underline{θ}[X := τ]

Proof. Property (i) is shown by induction on K ⊢ \underline{σ} ⊑ \underline{τ}. Property (ii) is shown by induction on K; Γ ⊢ e : \underline{τ}, using (i) in the case of (sub). For (iii), the two properties are shown simultaneously by induction on \underline{θ}. ⊓ ⊔

The following property is a simple unrolling of inversion. It is very convenient in the proof of Thm. A.12.

Proposition A.11.

(i) If K; Γ ⊢ c^{r} |σ| a : d^{s}τ, then there are a stage expression r and types σ′ such that

\begin{matrix}K ⊢ & r̂ & ≤ & s & K; Γ ⊢ a : θ[X := σ′, ı := r] \\ K ⊢ & σ′ & ⊑ & τ \end{matrix}

with |σ′| = |σ| and Σ(c^{r}) = ∀ı.ΠX.θ → dîX (ii) If K; Γ ⊢ c^{nr} |σ| a : d^{s}τ, then there are types σ′ such that

K ⊢ σ′ ⊑ τ  K; Γ ⊢ a : θ[X := σ′]

with |σ′| = |σ| and Σ(c^{nr}) = ∀ı.ΠX.θ → d^{ı}X

Proof. We only detail (i): (ii) is similar and simpler.

(i) Assume that K; Γ ⊢ c^{r} |σ| a : d^{s}τ. Then, by Prop. A.8 and subtyping inversion, there are s′, θ′ and τ′ such that

\begin{matrix}K; Γ ⊢ c^{r} |σ| : θ′ → d^{s′}τ′  K; Γ ⊢ a : θ′ \\ K ⊢ s′ ≤ s  K ⊢ τ′ ⊑ τ \end{matrix}

By Prop. A.8, and subtyping inversion there are s′′, θ′′, τ′′ and σ′ such that

\begin{matrix}K; Γ ⊢ c^{r} : ΠX.θ′′ → d^{s′′}τ′′ \\ K ⊢ s′′ ≤ s′  K ⊢ τ′′[X := σ′] ⊑ τ′  K ⊢ θ′ ⊑ θ′′[X := σ′] \end{matrix}

with |σ′| = |σ|. Now, by Prop. A.8, and subtyping inversion, there is r such that we have

K ⊢ r̂ ≤ s′′  K ⊢ θ′′ ⊑ θ[ı := r]  K ⊢ X ⊑ τ′′

where Σ(c^{r}) = ∀ı.ΠX.θ → dîX and ı pos θ and X pos θ. We deduce that K ⊢ r̂ ≤ s. Moreover, by subtyping inversion, we have τ′′ = X, hence K ⊢ σ′ ⊑ τ. Finally, it follows from Lem. A.10.(i) that

K ⊢ θ′′[X := σ′] ⊑ θ[X := σ′, ı := r]

and we deduce that K ⊢ θ′ ⊑ θ[X := σ′, ı := r], hence

K; Γ ⊢ a : θ[X := σ′, ı := r]
⊓ ⊔

We now show subject reduction in F′_{×} and deduce it in F_{×}.

Theorem A.12 (Subject reduction). In F′_{×},

(K; Γ ⊢ e_{1} : \underline{τ} ∧ e_{1} → e_{2}) ⟹ K; Γ ⊢ e_{2} : \underline{τ}

Proof. We reason by induction on K; Γ ⊢ e : \underline{τ}. If the last applied rule is neither (T-app), (app), (case) nor (let), then the result follows from the induction hypothesis. Otherwise, if the reduction occurs in a proper subterm of e_{1}, then the result follows also from the induction hypothesis.

It remains to deal with the rules (T-app), (app), (case) and (let) when furthermore e_{1} → e_{2} contracts a root redex of e_{1}.

(T-app) Assume that e_{1} = (ΛX.e) |τ| and e_{2} = e[X := |τ|] with

\frac{K; Γ ⊢ ΛX.e : ΠX.σ}{K; Γ ⊢ ΛX.e |τ| : σ[X := τ]}

By Prop. A.8, there exists σ′ such that

K ⊢ σ′ ⊑ σ  and  K; Γ ⊢ e : σ′

with X ∉ Γ. By Lem. A.10.(i) and Lem. A.10.(ii), since X ∉ Γ we deduce that

K ⊢ σ′[X := τ] ⊑ σ[X := τ]  and  K; Γ ⊢ e[X := |τ|] : σ′[X := τ]

and we conclude that

K; Γ ⊢ e[X := |τ|] : σ[X := τ]

(app) Assume that e_{1} = a b and the last step is

\frac{K; Γ ⊢ a : τ → σ K; Γ ⊢ b : τ}{K; Γ ⊢ a b : σ}

There are two subcases.

(i) a = λx : |τ′|.e and e_{2} = e_{1}[x := b]. In this case, by Prop. A.8, we know that there are τ′ and σ′ such that

\begin{matrix}K ⊢ & τ ⊑ & τ′ & K; Γ, x:τ′ ⊢ e : σ′ \\ K ⊢ & σ′ ⊑ & σ \end{matrix}

with |τ′| = |τ′|. Since K; Γ ⊢ b : τ we have K; Γ ⊢ b : τ′ and we deduce that K; Γ ⊢ e_{1}[x := b] : σ′ by Lem. A.9. From K ⊢ σ′ ⊑ σ we conclude that K; Γ ⊢ e_{1}[x := b] : σ.

(ii) a = letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} and b = c |σ| a.

By Prop. A.8, and subtyping inversion there exists a datatype identifier d, stages expressions s, r, stage variables ı, ȷ, and types τ, τ′, σ′ such that

K ⊢ s ≤ r  K ⊢ τ ⊑ τ′  K ⊢ σ′[ı := r] ⊑ σ

and for all k ∈ {1, …, n},

K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ′, σ′)  (13)

and for all k ∈ {1, …, m},

K; Γ, f:∀ı ≤ ȷ.d^{ı}τ′ → σ′ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ′, σ′[ı := ĵ])  (14)

with τ = d^{s}τ → σ, ı ∉ K, Γ, τ′, ȷ ∉ ı, K, Γ, τ′, σ′, and i pos σ′. We distinguish two cases, whether c is recursive or not. c is recursive. In this case, c = c_{k}^{r} for some k ∈ {1, …, m} and e_{2} =

e_{k}^{r}[f := e′] a, where

e′ =_{def} letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}

Let Σ(c_{k}^{r}) = ∀ı.ΠX.θ → dîX. By applying the rule (rec) to the derivations (13) and (14), we get

K; Γ ⊢ letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : d^{ı}τ′ → σ′

Since ı ∉ K, Γ, using (S-gen) it follows that

K; Γ ⊢ letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : ∀ı.d^{ı}τ′ → σ′

Since K ⊢ ȷ ≤ ∞, using reflexivity of subtyping and the rule (cst) we derive

K ⊢ ∀ı.d^{ı}τ′ → σ′ ⊑ ∀ı ≤ ȷ.d^{ı}τ′ → σ′

and we deduce that

K; Γ ⊢ letrec_{|σ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} : ∀ı ≤ ȷ.d^{ı}τ′ → σ′

By applying Lem. A.9 to (14) we obtain

K; Γ ⊢ e_{k}^{r}[f := e′] : Inst(c_{k}^{r}, ȷ, τ′, σ′[ı := ĵ])

that is

K; Γ ⊢ e_{k}^{r}[f := e′] : θ[X := τ′, ı := ȷ] → σ′[ı := ĵ]  (15)

By Prop. A.11.(i), from

K; Γ ⊢ c_{k}^{r} |σ| a : d^{s}τ

we deduce that there are a stage expression p and types σ′ such that

\begin{matrix}K ⊢ & p̂ & ≤ & s & K; Γ ⊢ a : θ[X := σ′, ı := p] \\ K ⊢ & σ′ & ⊑ & τ \end{matrix}

with |σ′| = |σ|. Since X pos θ, we obtain from Lem. A.10.(iii) that

K; Γ ⊢ a : θ[X := τ′, ı := p]

On the other hand, by applying Prop. A.4.(ii) to (15) with substitution [ȷ := p], since ȷ ∉ K, Γ, τ′, θ, σ′ we get

K; Γ ⊢ e_{k}^{r}[f := e′] a : σ′[ı := p̂]

Since moreover ı pos σ′, K ⊢ p̂ ≤ s and K ⊢ r ≤ s, by Lem. A.5 we have K ⊢ σ′[ı := p̂] ≤ σ′[ı := r], and since K ⊢ σ′[ı := r] ≤ σ, we deduce that

K; Γ ⊢ e_{k}^{r}[f := e′] a : σ

c is non-recursive. In this case, c = c_{k}^{nr} for some k ∈ {1, …, n} and e_{2} = e_{k}^{nr} a. Let Σ(c_{k}^{nr}) = ∀ı.ΠX.θ → d^{ı}X. We deduce that

K; Γ ⊢ e_{k}^{nr} : θ[X := τ′] → σ′

By Prop. A.11.(ii), from

K; Γ ⊢ c_{k}^{nr} |σ| a : d^{s}τ

we deduce that there are types σ′ such that

K ⊢ σ′ ⊑ τ  K; Γ ⊢ a : θ[X := σ′]

with |σ′| = |σ|. Since X pos θ, we obtain from Lem. A.10.(iii) that

K; Γ ⊢ a : θ[X := τ′]

hence

K; Γ ⊢ e_{k}^{nr} a : σ′

Since ı appears bound in Σ(c_{k}^{nr}), we can assume that ı ∉ K, Γ. Therefore, using Lem. A.4.(ii), since K ⊢ σ′[ı := r] ⊑ σ, we obtain

K; Γ ⊢ e_{k}^{nr} a : σ

(case) Assume that e_{1} = case_{|θ|} e of {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}} with e = c |σ| a and

\frac{K; Γ ⊢ e : dŝτ C_{nr}(d) = \{c_{1}^{nr}, …, c_{n}^{nr}\} K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ , σ) (1 ≤ k ≤ n) C_{r}(d) = \{c_{1}^{r}, …, c_{m}^{r}\} K; Γ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, s, τ , σ) (1 ≤ k ≤ m)}{K; Γ ⊢ case_{|σ|} e of \{c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}\} : σ}

We distinguish two cases, whether c is recursive or not. c is recursive. In this case, c = c_{k}^{r} for some k ∈ {1, …, m} and e_{2} = e_{k}^{r} a.

By Prop. A.11.(i), from

K; Γ ⊢ c_{k}^{r} |σ| a : dŝτ

we deduce that there are a stage expression p and types σ′ such that

\begin{matrix}K ⊢ & p̂ & ≤ & ŝ & K; Γ ⊢ a : θ[X := σ′, ı := p] \\ K ⊢ & σ′ & ⊑ & τ \end{matrix}

with |σ′| = |σ| an Σ(c_{k}^{r}) = ∀ı.ΠX.θ → dîX. Since

K; Γ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, s, τ , σ)

we deduce that

K; Γ ⊢ e_{k}^{r} : θ[X := τ , ı := s] → σ

Since K ⊢ p̂ ≤ ŝ, we deduce from substage rule (inj) that K ⊢ p ≤ s. Since moreover ı pos θ, X pos θ and K ⊢ σ′ ⊑ τ, we deduce from Lem. A.10.(iii) and Lem A.5 that

K; Γ ⊢ a : θ[X := τ , ı := s]

Therefore we have

K; Γ ⊢ e_{k}^{r} a : σ

c is non-recursive. In this case, c = c_{k}^{nr} for some k ∈ {1, …, n} and e_{2} = e_{k}^{nr} a. By Prop. A.11.(ii), from

K; Γ ⊢ c_{k}^{nr} |σ| a : dŝτ

we deduce that there are types σ′ such that

K ⊢ σ′ ⊑ τ  K; Γ ⊢ a : θ[X := σ′]

with |σ′| = |σ| and Σ(c_{k}^{nr}) = ∀ı.ΠX.θ → d^{ı}X. Since

K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ , σ)

we deduce that

K; Γ ⊢ e_{k}^{nr} : θ[X := τ] → σ

Since X pos θ and K ⊢ σ′ ⊑ τ, we deduce from Lem. A.10.(iii) that

K; Γ ⊢ a : θ[X := τ]

Therefore we have

K; Γ ⊢ e_{k}^{nr} a : σ

(let) Assume that e_{1} = let ⟨x_{1}, x_{2}⟩ = ⟨a_{1}, a_{2}⟩ in e and e_{2} = e[x_{1} := a_{1}, x_{2} := a_{2}] with

\frac{\begin{matrix}K; Γ ⊢ ⟨a_{1}, a_{2}⟩ : d_{1} τ_{1} ×^{s} d_{2} τ_{2} \\ K, ı_{1} + ı_{2} ≤ s; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2} ⊢ e : σ \end{matrix}}{K; Γ ⊢ let ⟨x_{1}, x_{2}⟩ = ⟨a_{1}, a_{2}⟩ in e : σ}

where ı_{1}, ı_{2} ∉ Γ, K, σ, s, τ_{1}, τ_{2}

By Prop. A.8, there exists stage expressions s_{1}, s_{2} and types σ_{1}, σ_{2}, such that

K ⊢ s_{1} + s_{2} ≤ s  K; Γ ⊢ a_{1} : d_{1}^{s_{1}} σ_{1}
K ⊢ σ_{1} ⊑ τ_{1} K; Γ ⊢ a_{2} : d_{2}^{s_{2}} σ_{2}
K ⊢  σ_{2} ⊑ τ_{2}

Now, we apply Lem. A.4.(iii) with substitutions [ı_{1} := s_{1}] and [ı_{2} := s_{2}]. Since ı_{1}, ı_{2} ∉ Γ, K, σ, s, τ_{1}, τ_{2}, we obtain that

K, s_{1} + s_{2} ≤ s; Γ, x_{1} :d_{1}^{s_{1}} τ_{1}, x_{2} :d_{2}^{s_{2}} τ_{2} ⊢ e : σ

Since K ⊢ s_{1} + s_{2} ≤ s, by Lem. A.2.(iii) we deduce that

K; Γ, x_{1} :d_{1}^{s_{1}} τ_{1}, x_{2} :d_{2}^{s_{2}} τ_{2} ⊢ e : σ

By Lem. A.9 applied with substitutions [x_{1} := a_{1}] and [x_{2} := a_{2}], we obtain

K; Γ ⊢ e[x_{1} := a_{1}, x_{2} := a_{2}] : σ
⊓ ⊔

Corollary A.13 (Subject reduction – Thm. 4.4). In F_{×},

(K; Γ ⊢ e_{1} : \underline{τ} ∧ e_{1} → e_{2}) ⟹ K; Γ ⊢ e_{2} : \underline{τ}

Proof. By Thm. A.12 and Lem. 4.2. ⊓ ⊔

B Strong normalization

In this section, we show that typable terms are strongly normalizable.

We begin by properties of the stage model (Sect. B.1). We then turn to saturated sets (Sect. B.2) and to the type interpretation (Sect. B.3).

B.1 The stage model

In this section, we show the two properties on stages depicted in Fig. 2. The corresponding definitions are given in Sect. 5.1.

Proposition B.1. ⦇r[ı := s]⦈_{π} = ⦇r⦈_{π(ı:=⦇s⦈_{π})}

Proof. By induction on r. ⊓ ⊔

Lemma B.2. If K ⊢ s ≤ r then K ⊧ s ≤ r.

Proof. By induction on K ⊢ s ≤ r. The interesting cases are the following ones.

(assoc)

\overline{K ⊢ s + (r + p) ≤ (s + r) + p}

We show that for all α, β, γ ∈ Ω̂ we have α + (β + γ) = (α + β) + γ. If either α, β or γ is Ω, then α + (β + γ) = Ω = (α + β) + γ. Otherwise we have α + (β + γ), (α + β) + γ < Ω and we conclude by the associativity of ⊕ in Ω.

(com)

\overline{K ⊢ s + r ≤ r + s}

We have to show that for all α, β ∈ Ω̂ we have α + β ≤ β + α. If either α or β is Ω, then α + β = Ω = β + α. Otherwise we have α + β, β + α < Ω and we conclude by the commutativity of ⊕ in Ω.

(succ)

\overline{K ⊢ s + r̂ = { \atop s + r}}

We have to show that for all α, β ∈ Ω we have α+(β +1) = (α+β)+1. This follows directly from the associativity of +, proved in the case of (assoc).

(zero)

\overline{K ⊢ 0 + s = s}

Because for all α ∈ Ω̂, we have 0 + α = α + 0. (inj)

\frac{K ⊢ ŝ ≤ r̂}{K ⊢ s ≤ r}

We show that α + 1 ≤ β + 1 implies α ≤ β for all α, β ∈ Ω̂. Since Ω is not a successor ordinal, if α + 1 = Ω, then α = β + 1 = Ω and we are done. Otherwise, if β + 1 = Ω, then β = Ω and α + 1 < β, hence α < β. In the remaining case we have α, β < Ω and we conclude by Prop. 5.2. ⊓ ⊔ B.2 Saturated sets

In this section, we prove some properties on saturated sets (defined in Def. 5.5).

Lemma B.3 (Non-interaction). In each of the cases (i), (ii), (iii), (iv) and (v) below, if E[e] → b then b = E′[e′] with (E[ ], e) → (E′[ ], e′).

(i) e =_{def} (λx : |τ|.e_{1}) e_{2} (ii) e =_{def} (ΛX.e_{1})|τ| (iii) e =_{def} let ⟨x_{1}, x_{2}⟩ = ⟨e_{1}, e_{2}⟩ in e_{3} (iv) e =_{def} case_{|τ|} (c_{i} |σ| a) of {c ⇒ e}

(v) e =_{def} letrec_{|τ|} f case {c ⇒ e} (c_{i} |σ| a)

Lemma B.4 (Weak standardization). If a →_{wh} b and a → a′ with a′ ≠ b then a′ →_{wh} b′ and b →^{∗} b′.

Proof. Since a →_{wh} b, be definition of →_{wh} there is E[ ], e and e′ such that e ↦_{βιμθ} e′, E[e] = a and E[e′]. The proof is by induction on E[ ], using Lem. B.3 and that a[x := e] →^{∗} a[x := e′] whenever e → e′.

Lemma B.5.

(i) If e_{2}, E[e_{1}[x := e_{2}]] ∈ SN then E[(λx : |τ|.e_{1}) e_{2}] ∈ SN. (ii) If E[e_{1}[X := |τ|]] ∈ SN then E[(ΛX.e_{1}) |τ|] ∈ SN. (iii) If e_{1}, e_{2}, E[e_{3}[x_{1} := e_{1}, x_{2} := e_{2}]] ∈ SN then

E[let ⟨x_{1}, x_{2}⟩ = ⟨e_{1}, e_{2}⟩ in e_{3}] ∈ SN. (iv) If e, E[e_{i} a] ∈ SN then E[case_{|τ|} (c_{i} |σ| a) of {c ⇒ e}] ∈ SN.

(v) If e, E[e_{i} a] ∈ SN then E[letrec_{|τ|} f case {c ⇒ e} (c_{i}^{nr} |σ| a)] ∈ SN. (vi) If e, E[e′_{i} a] ∈ SN then E[letrec_{|τ|} f case {c ⇒ e} (c_{i}^{r} |σ| a)] ∈ SN, where

e′_{i} = e_{i}[f := letrec_{|τ|} f case {c ⇒ e}].

Proof. By weak standardization B.4. ⊓ ⊔

For each X ⊆ SN the smallest saturated set containing X is

\overline{X} = ⋂\{S ∈ SAT | X ⊆ S\}

It follows that the smallest element of SAT is ⊥ =_{def} \overline{∅} and that X ⊆ Y ⊆ SN implies \overline{X} ⊆ \overline{Y}.

Lemma B.6.

(i) ⊥ = {e ∈ SN | ∃E[ ], x. e →_{wh}^{∗} E[x]}. (ii) If X ⊆ SN then \overline{X} = ⊥ ∪ \{e ∈ SN | e →_{wh}^{∗} X\}.

Lemma B.7. If e ∈ ⊥ and e, e′ ∈ SN then

(i) case_{|τ|} e of {c ⇒ e} ∈ ⊥, (ii) letrec_{|τ|} f case {c ⇒ e} e ∈ ⊥, (iii) let ⟨x_{1}, x_{2}⟩ = e in e′ ∈ ⊥.

Lemma B.8. Let e, e′ ∈ ℰ such that e ∈ SN and e →_{wh} e′.

(i) If letrec_{|τ|} f case {c ⇒ e} e′ ∈ SN then letrec_{|τ|} f case {c ⇒ e} e ∈ SN. (ii) If let ⟨x_{1}, x_{2}⟩ = e′ in e′′ ∈ SN then let ⟨x_{1}, x_{2}⟩ = e in e′′ ∈ SN (iii) If case_{|τ|} e′ of {c ⇒ e} ∈ SN then case_{|τ|} e of {c ⇒ e} ∈ SN.

Proof. By weak standardization B.4. ⊓ ⊔ B.3 Type interpretation

In this section, we prove the soundness of the interpretation defined in Sect. 5.2. We first check that the interpretation scheme of Def. 5.6 is well-defined.

Lemma B.9. If X, Y ∈ SAT then X → Y ∈ SAT.

Proposition B.10 (Interpretation correctness). For all (I_{d})_{d∈𝒟} , all π and all ξ, we have ⟦.⟧_{π,ξ}^{I} : \underline{𝒯} → SAT.

Proof. We reason by induction on the definition of ⟦.⟧_{π,ξ}^{I}. Recall that SAT is closed under non-empty intersections and unions. By Lem. B.9, its moreover closed under the function space →. It remains the case of ⟦ΠX.τ⟧_{π,ξ}^{I}.

Given T ∈ SAT and |σ| ∈ |𝒯|, let T |σ| =_{def} {e | e |σ| ∈ T }. We first show the following claim.

Claim: T |σ| ∈ SAT. First, T |σ| ⊆ SN since T ⊆ SN. Moreover,

(SAT1) if E[ ] ∈ SN, then E[ ] |τ| ∈ SN, hence E[x] |τ| ∈ T by (SAT1) on T,

and it follows that E[x] ∈ T |σ|; (SAT2) if e →_{wh} e′ with e′ ∈ T |σ|, then e|σ| →_{wh} e′|σ| ∈ T, hence e|σ| ∈ T by (SAT2) on T. ⊓ ⊔

Now, by induction hypothesis we have ⟦τ⟧_{π,ξ(X:=S)}^{I} ∈ SAT for all S ∈ SAT. To conclude, it is sufficient to remark that

⟦ΠX.τ⟧_{π,ξ}^{I} = ⋂{⟦τ⟧_{π,ξ(X:=S)}^{I} |σ| | |σ| ∈ |𝒯| ∧ S ∈ SAT} ∈ SAT

⊓ ⊔

We now turn to the second and third substitution properties of Fig. 2.

Proposition B.11. For all (I_{d})_{d∈𝒟} , all π and all ξ,

(i) ⟦\underline{τ}[ı := s]⟧_{π,ξ} = ⟦\underline{τ}⟧_{π(ı:=⦇s⦈_{π}),ξ} (ii) ⟦\underline{τ}[X := σ]⟧_{π,ξ} = ⟦\underline{τ}⟧_{π,ξ(X:=⟦σ⟧_{π,ξ})}

Proof. By induction on \underline{τ}. ⊓ ⊔

The stage monotony properties of Fig. 2 are proved for the datatype interpretation (I_{d})_{d∈𝒟} defined in Def. 5.7. Note that for all S_{1}, S_{2}, T_{1}, T_{2} ∈ SAT such that S_{1} ⊆ T_{1} and T_{1} ⊆ T_{2}, we have ⟨S_{1}, S_{2}⟩ ⊆ ⟨T_{1}, T_{2}⟩ (see Def. 5.6); and that for all S, T ∈ SAT such that S ⊆ T, we have c S ⊆ c T (see Def. 5.7).

Lemma B.12 (Stage monotony). Let (I_{d})_{d∈𝒟} be the datatype interpretation defined in Def. 5.7. Then,

(i) If α ≤ β and S ⊆ T then I_{d}(S, α) ⊆ I_{d}(T , β). (ii) If ı pos θ and α ≤ β then ⟦θ⟧_{π(ı:=α),ξ}^{I} ⊆ ⟦θ⟧_{π(ı:=β),ξ}^{I}.

If ı neg θ and α ≤ β then ⟦θ⟧_{π(ı:=β),ξ}^{I} ⊆ ⟦θ⟧_{π(ı:=α),ξ}^{I}.

Proof. We reason by induction on <_{Σ}. Let d ∈ 𝒟 such that (i) holds for all d′ <_{Σ} d. We show (i) for d and (ii) for all θ in which only occurs d′ ≤_{Σ} d. We reason by induction on β ∈ Ω̂.

(i) We reason by cases on β. The result is trivial if wither β = 0 or β is a limit ordinal. If β is a successor ordinal, then we apply the induction hypothesis on β to the type interpretations of the constructors arguments of d (which only uses I_{d′}(U, γ) with (d′, γ) (<_{Σ}, <)_{lex} (d, β)). We conclude by the monotony of c S w.r.t. S ∈ SAT.

(ii) The two properties are shown simultaneously by induction on θ, using (i) in the cases of datatypes and sized products. ⊓ ⊔

We can now prove Prop. 5.9.

Proposition B.13 (Prop 5.9). For all d ∈ 𝒟 and all S ∈ SAT^{ar(d)}, there is an ordinal α < Ω such that I_{d}(S, α) = I_{d}(S, β) for all β such that α ≤ β ≤ Ω.

Proof. By Lem. B.12.(i), α ≤ β implies I_{d}(S, α) ⊆ I_{d}(S, β) for all α, β.

Assume that for all α < β < Ω we have I_{d}(S, α) ⊊ I_{d}(S, β). Then, since Ω is uncountable, we would have an uncountable set {e_{α} | α ∈ Ω} ⊆ ℰ. But this is not possible as ℰ is countable.

Hence there are α < β < Ω such that I_{d}(S, α) = I_{d}(S, β). Reasoning by well-founded induction on Ω, we have I_{d}(S, α) = I_{d}(S, γ) for all γ such that α < γ < Ω. We obtain that I_{d}(S, Ω) = I_{d}(S, α) by definition of I_{d}(S, Ω). ⊓ ⊔

We now show the soundness of the interpretation. We begin by the soundness of subtyping (see Fig. 2). Recall from Def. 5.8 that ⟦.⟧_{π,ξ} =_{def} ⟦.⟧_{π,ξ}^{I}, where (I_{d})_{d∈𝒟} is the datatype interpretation defined in Def. 5.7.

Lemma B.14 (Subtyping soundness). If K ⊢ \underline{τ} ⊑ \underline{σ} and π ⊧ K then ⟦\underline{τ}⟧_{π,ξ} ⊆ ⟦\underline{σ}⟧_{π,ξ}.

Proof. By induction on K ⊢ \underline{τ} ⊑ \underline{σ}. Rules (var), (func), (prod) and (data) are dealt with as usual (using Lem. B.12.(i) and Lem. B.2 for (data)). We only detail the cases of (cst) and (pair).

(cst)

\frac{K ⊢ r ≤ s K, ı ≤ r ⊢ \underline{τ} ⊑ \underline{σ}}{K ⊢ ∀ı ≤ s.\underline{τ} ⊑ ∀ı ≤ r.\underline{σ}} if ı ∉ K

Let π such that π ⊧ K and e ∈ ⟦∀ı ≤ s.\underline{τ}⟧_{π,ξ}. We have to show that e ∈ ⟦∀ı ≤ r.\underline{σ}⟧_{π,ξ}, i.e., that e ∈ ⟦\underline{σ}⟧_{π(ı:=α),ξ} for all α ∈ Ω̂ such that α ≤ ⦇r⦈_{π} (recall that ı ∉ s). Let α ∈ Ω̂ such that α ≤ ⦇r⦈_{π}. Since K ⊢ r ≤ s and π ⊧ K, by Lem. B.2 we have ⦇r⦈_{π} ≤ ⦇s⦈_{π}, hence α ≤ ⦇s⦈_{π} It follows that e ∈ ⟦\underline{τ}⟧_{π(ı:=α),ξ}. Since ı ∉ K, we have π(ı := α) ⊧ K, ı ≤ r, and by induction hypothesis we get e ∈ ⟦\underline{σ}⟧_{π(ı:=α),ξ}.

(pair)

\frac{K ⊢ s ≤ r  K ⊢ τ ⊑ σ  K ⊢ τ′ ⊑ σ′}{K ⊢ dτ ×^{s} d′τ′ ⊑ dσ ×^{r} d′σ′}

Let π such that π ⊧ K. We have to show that for all α, α′ ∈ Ω̂ such that α + α′ ≤ ⦇s⦈_{π}, there exists β, β′ ∈ Ω̂ such that β + β′ ≤ ⦇r⦈_{π} and

⟨I_{d}(⟦τ ⟧_{π,ξ}, α), I_{d′}(⟦τ′⟧_{π,ξ}, α′)⟩ ⊆ ⟨I_{d}(⟦σ⟧_{π,ξ}, β), I_{d′}(⟦σ′⟧_{π,ξ}, β′)⟩ (16)

Now, since K ⊢ s ≤ r, by Lem. B.2 we have ⦇s⦈_{π} ≤ ⦇r⦈_{π}. It is therefore sufficient to show (16) with β = α and β′ = α′. By induction hypothesis, we get ⟦τ ⟧_{π,ξ} ⊆ ⟦σ⟧_{π,ξ} and ⟦τ′⟧_{π,ξ} ⊆ ⟦σ′⟧_{π,ξ}. By Lem. B.12. (i), for all α, α′ ∈ Ω̂ we have I_{d}(⟦τ ⟧_{π,ξ}, α) ⊆ I_{d}(⟦σ⟧_{π,ξ}, α) and I_{d′}(⟦τ′⟧_{π,ξ}, α′) ⊆ I_{d′}(⟦σ′⟧_{π,ξ}, α′). We conclude thanks to the monotony of ⟨S_{1}, S_{2}⟩ in S_{1}, S_{2} ∈ SAT. ⊓ ⊔

We can now show the main result of this section. The key-point that if K is satisfied with π, then every K′ occurring in the derivation of K; Γ ⊢ e : \underline{τ} is satisfied with an extension of π.

Theorem B.15 (Typing soundness – Thm. 5.10). If K; Γ ⊢ e : \underline{τ}, then eρ ∈ ⟦\underline{τ}⟧_{π,ξ} for all π, ξ, ρ such that (π, ξ, ρ) ⊧ K; Γ.

Proof. We reason by induction on K; Γ ⊢ e : \underline{τ}.

(var)

\overline{K; Γ, x:\underline{σ} ⊢ x : \underline{σ}}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ, x:\underline{τ}. We have xρ = ρ(x) ∈ ⟦\underline{τ}⟧_{π,ξ}. (abs)

\frac{K; Γ, x:τ ⊢ e : σ}{K; Γ ⊢ λx : |τ|.e : τ → σ}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Furthermore let e′ ∈ ⟦τ⟧_{π,ξ} ⊆ SN. We have to show that (λx : |τ|.e)ρ e′ ∈ ⟦σ⟧_{π,ξ}. Since (π, ξ, ρ(x := e′)) ⊧ K; Γ, x: τ, we have eρ(x := e′) ∈ ⟦σ⟧_{π,ξ} ⊆ SN by induction hypothesis. Since x appears bound in λx : |τ|.e, we can assume that x ∉ codom(ρ). Therefore, we have eρ(x := e′) = (eρ)[x := e′]. Now, since (eρ)[x := e′], e′ ∈ SN, by Lem. B.5.(i) we have (λx : |τ|.eρ) e′ ∈ SN, hence (λx : |τ|.eρ) e′ ∈ ⟦σ⟧_{π,ξ}, by (SAT2), that is (λx : |τ|.e)ρ e′ ∈ ⟦σ⟧_{π,ξ}.

(app)

\frac{K; Γ ⊢ e : τ → σ K; Γ ⊢ e′ : τ}{K; Γ ⊢ e e′ : σ}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. By induction hypothesis we have eρ ∈ ⟦τ⟧_{π,ξ} → ⟦σ⟧_{π,ξ} and e′ρ ∈ ⟦τ⟧_{π,ξ}. It follows that e e′ ∈ ⟦σ⟧_{π,ξ}.

(T-abs)

\frac{K; Γ ⊢ e : σ}{K; Γ ⊢ ΛX.e : ΠX.σ} if X ∉ Γ

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Let furthermore τ ∈ 𝒯 and S ∈ SAT. We have to show that (ΛX.e)ρ |τ| ∈ ⟦σ⟧_{π,ξ(X:=S)}. Since X ∉ Γ, we have (π, ξ(X := S), ρ(X := |τ|)) ⊧ K; Γ, and by induction hypothesis we obtain eρ(X := |τ|) ∈ ⟦σ⟧_{π,ξ(X:=S)} ⊆ SN. Since X appears bound in ΛX.e, by Barendregt convention, we can assume that X ∉ codom(ρ). Hence eρ(X := |τ|) = (eρ)[X := |τ|]. Now, since (eρ)[x := |τ|] ∈ SN, by Lem. B.5.(ii) we have (ΛX.eρ) |τ| ∈ SN, hence (ΛX.eρ) |τ| ∈ ⟦σ⟧_{π,ξ(X:=S)}, by (SAT2), that is (ΛX.e)ρ |τ| ∈ ⟦σ⟧_{π,ξ(X:=S)}.

(T-app)

\frac{K; Γ ⊢ e : ΠX.σ}{K; Γ ⊢ e |τ| : σ[X := τ]}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. By induction hypothesis we have e|τ| ∈ ⟦σ⟧_{π,ξ(X:=⟦τ⟧_{π,ξ})} and we conclude that e|τ| ∈ ⟦σ[X := τ]⟧_{π,ξ} by Prop. B.11.(ii).

(S-gen)

\frac{K, ı ≤ s; Γ ⊢ e : \underline{τ}}{K; Γ ⊢ e : ∀ı ≤ s.\underline{τ}} if ı ∉ Γ, K, s

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. First, it follows from ı ∉ s that ⦇ı⦈_{π}(ı := ⦇s⦈_{π}) = ⦇s⦈_{π}. Since ı ∉ Γ, K, we get (π(ı := ⦇s⦈_{π}), ξ, ρ) ⊧ K; Γ. We thus have \{⟦\underline{τ}⟧_{π(ı:=α),ξ} | π(ı := α) ⊧ ı ≤ s\} ≠ ∅. Hence, we have to show that eρ ∈ ⟦\underline{τ}⟧_{π(ı:=α),ξ} for all α ∈ Ω̂ such that π(ı := α) ⊧ ı ≤ s. Now, for all α ∈ Ω̂ such that π(ı := α) ⊧ ı ≤ s, since ı ∉ Γ, K we have (π(ı := α), ξ, ρ) ⊧ K, ı ≤ s; Γ, and by induction hypothesis we conclude that eρ ∈ ⟦\underline{τ}⟧_{π(ı:=α),ξ}.

(S-inst)

\frac{K; Γ ⊢ e : ∀ı ≤ s.\underline{τ} K ⊢ r ≤ s}{K; Γ ⊢ e : \underline{τ}[ı := r]}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Recall that ı ∉ s. By assumption we have π ⊧ r ≤ s, and it follows from Prop. B.1 that π(ı := ⦇r⦈_{π}) ⊧ ı ≤ s. Hence \{⟦\underline{τ}⟧_{π(ı:=α),ξ} | π(ı := α) ⊧ ı ≤ s\} ≠ ∅. By induction hypothesis we have eρ ∈ ⟦\underline{τ}⟧_{π(ı:=⦇r⦈_{π}),ξ}, and we conclude that eρ ∈ ⟦\underline{τ}[ı := r]⟧_{π,ξ} by Prop. B.11.(i).

(cons)

\overline{K; Γ ⊢ c : Σ(c)}if c ∈ C(d) for some d

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Furthermore, Σ(c) is of the form ∀ı.ΠX.θ → d\overline{ı}X where \overline{ı} = î if c is recursive and \overline{ı} = ı otherwise. Recall that ı is the unique free stage variable of θ and that X are the unique free type variables of θ. Hence, using Prop. B.11.(i), we have to show that for all α ∈ Ω̂, all τ and all S ∈ SAT we have

c |τ | ∈ ⟦θ⟧_{ı:=α,X:=S} → I_{d}(S, ⦇\overline{ı}⦈_{ı:=α})

We reason by cases on ⦇\overline{ı}⦈_{ı:=α}. ⦇\overline{ı}⦈_{ı:=α} = 0. In this case, \overline{ı} can not be î and c is a non-recursive constructor.

Note that ı ∉ θ. By definition, we have c |τ | a ∈ c ⟦θ⟧_{∅,X:=S} for all

a ∈ ⟦θ⟧_{∅,X:=S}. Since c ⟦θ⟧_{∅,X:=S} ⊆ I_{d}(S, 0), it follows that
c |τ | ∈ ⟦θ⟧_{ı:=0,X:=S} → I_{d}(S, 0)

⦇\overline{ı}⦈_{ı:=α} = β ⊕ 1. We have c |τ | a ∈ c ⟦θ⟧_{ı:=β,X:=S} for all a ∈ ⟦θ⟧_{ı:=β,X:=S}. Since c ⟦θ⟧_{ı:=β,X:=S} ⊆ I_{d}(S, β ⊕ 1), it follows that

c |τ | ∈ ⟦θ⟧_{ı:=β,X:=S} → I_{d}(S, β ⊕ 1)

⦇\overline{ı}⦈_{ı:=α} is a limit ordinal λ. There are two subcases.

\overline{ı} = ı. Then c is non-recursive and ı ∉ θ. Hence, for all a ∈ ⟦θ⟧_{∅,X:=S}

we have c |τ | a ∈ c ⟦θ⟧_{∅,X:=S} ⊆ I_{d}(S, 0) ⊆ I_{d}(S, λ). It follows that
c |τ | ∈ ⟦θ⟧_{ı:=λ,X:=S} → I_{d}(S, λ).

\overline{ı} = î and α = Ω. According to Prop. B.13, there is γ < Ω such that

I_{d}(S, Ω) = I_{d}(S, γ) for all γ′ ≥ γ. As in the case ⦇\overline{ı}⦈_{ı:=α} = β ⊕ 1, we
get c |τ | ∈ ⟦θ⟧_{ı:=γ,X:=S} → I_{d}(S, γ ⊕ 1). Note that in θ, d occurs only
under the form d^{ı} X. Hence we have ⟦θ⟧_{ı:=γ,X:=S} = ⟦θ⟧_{ı:=Ω,X:=S}
and we deduce c |τ | ∈ ⟦θ⟧_{ı:=Ω,X:=S} → I_{d}(S, Ω). Since ⦇î⦈_{ı:=Ω} = Ω,
we obtain that c |τ | ∈ ⟦θ⟧_{ı:=Ω,X:=S} → I_{d}(S, ⦇î⦈_{ı:=Ω}).

(pair)

\frac{K; Γ ⊢ e_{1} : d_{1}^{s_{1}} τ_{1} K; Γ ⊢ e_{2} : d_{2}^{s_{2}} τ_{2}}{K; Γ ⊢ ⟨e_{1}, e_{2}⟩ : d_{1} τ_{1} ×^{s_{1}+s_{2}} d_{2} τ_{2}}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. By induction hypothesis we have e_{1}ρ ∈ d_{1}(⟦τ_{1}⟧_{π,ξ}, ⦇s_{1}⦈_{π}) and e_{2}ρ ∈ d_{2}(⟦τ_{2}⟧_{π,ξ}, ⦇s_{2}⦈_{π}). Since ⦇s_{1}⦈_{π} + ⦇s_{2}⦈_{π} = ⦇s_{1} + s_{2}⦈_{π}, we have ⦇s_{1}⦈_{π} + ⦇s_{2}⦈_{π} ≤ ⦇s_{1} + s_{2}⦈_{π}, and by definition of ⟦d_{1} τ_{1} ×^{s_{1}+s_{2}} d_{2} τ_{2}⟧_{π,ξ}, it follows that ⟨e_{1}, e_{2}⟩ρ ∈ ⟦d_{1} τ_{1} ×^{s_{1}+s_{2}} d_{2} τ_{2}⟧_{π,ξ}.

(let)

\frac{\begin{matrix}K; Γ ⊢ e : d_{1} τ_{1} ×^{s} d_{2} τ_{2} \\ K, ı_{1} + ı_{2} ≤ s; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2} ⊢ e′ : σ \end{matrix}}{K; Γ ⊢ let ⟨x_{1}, x_{2}⟩ = e in e′ : σ}

where ı_{1}, ı_{2} ∉ Γ, K, σ, s, τ_{1}, τ_{2}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Since x_{1}, x_{2} appears bound in let ⟨x_{1}, x_{2}⟩ = e in e′, by Barendregt convention we may assume that x_{1}, x_{2} ∉ codom(ρ). Hence we have

(let ⟨x_{1}, x_{2}⟩ = e in e′)ρ = let ⟨x_{1}, x_{2}⟩ = eρ in e′ρ

We first show the following claim. Claim: e′ρ ∈ SN. Let π′ =_{def} π(ı_{1} := s, ı_{2} := 0). Hence

(π′, ξ, ρ(x_{1} := x_{1}, x_{2} := x_{2})) ⊧ K, ı_{1} + ı_{2} ≤ s ; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2}

and by induction hypothesis we have

e′ρ = e′ρ(x_{1} := x_{1}, x_{2} := x_{2}) ∈ ⟦σ⟧_{π′,ξ} ⊆ SN
⊓ ⊔

We now show that let ⟨x_{1}, x_{2}⟩ = eρ in e′ρ ∈ ⟦σ⟧_{π,ξ}. By induction hypothesis we have eρ ∈ ⟦d_{1}τ_{1} ×^{s} d_{2}τ_{2}⟧_{π,ξ}, and there are two cases.

(i) If eρ ∈ ⊥, then since e′ρ ∈ SN, by Lem. B.7.(iii) we have

let ⟨x_{1}, x_{2}⟩ = eρ in e′ρ ∈ ⊥ ⊆ ⟦σ⟧_{π,ξ}

(ii) Otherwise, there exist ordinals α_{1}, α_{2} ∈ Ω̂ such that α_{1} + α_{2} ≤ ⦇s⦈_{π} and e →_{wh}^{∗} ⟨e_{1}, e_{2}⟩ with e_{k} ∈ I_{d}(⟦τ_{k}⟧_{π,ξ}, α_{k}) for all k ∈ {1, 2}. Let π′′ =_{def} π(ı_{1} := α_{1}, ı_{2} := α_{2}). Since ı_{1}, ı_{2} ∉ K, Γ, τ_{1}, τ_{2}, we have

(π′′, ξ, ρ(x_{1} := e_{1}, x_{2} := e_{2})) ⊧ K, ı_{1} + ı_{2} ≤ s ; Γ, x_{1} :d_{1}^{ı_{1}} τ_{1}, x_{2} :d_{2}^{ı_{2}} τ_{2}

and by induction hypothesis we obtain that

e′ρ(x_{1} := e_{1}, x_{2} := e_{2}) ∈ ⟦σ⟧_{π′′,ξ}

Since x_{1}, x_{2} ∉ codom(ρ), we have

e′ρ(x_{1} := e_{1}, x_{2} := e_{2}) = (eρ)[x_{1} := e_{1}, x_{2} := e_{2}]

and since ı_{1}, ı_{2} ∉ σ, we deduce that

(e′ρ)[x_{1} := e_{1}, x_{2} := e_{2}] ∈ ⟦σ⟧_{π,ξ}

Therefore, it follows from Lem. B.5.(iii) that

let ⟨x_{1}, x_{2}⟩ = ⟨e_{1}, e_{2}⟩ in e′ρ ∈ ⟦σ⟧_{π,ξ}

Now, since eρ →_{wh}^{∗} ⟨e_{1}, e_{2}⟩, it follows from Lem. B.8.(ii) and (SAT2) that

(let ⟨x_{1}, x_{2}⟩ = e in e′)ρ ∈ ⟦σ⟧_{π,ξ}

(case)

\frac{\begin{matrix}K; Γ ⊢ e : dŝτ \\ K; Γ ⊢ e_{k} : Inst(c_{k}, s, τ , θ) & (1 ≤ k ≤ n) \end{matrix}}{K; Γ ⊢ case_{|θ|} e of \{c ⇒ e\} : θ} if C(d) = \{c_{1}, …, c_{n}\}

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. By induction hypothesis we have eρ ∈ ⟦Inst(c, s, τ , θ)⟧_{π,ξ} ⊆ SN and eρ ∈ I_{d}(⟦τ ⟧_{π,ξ}, ⦇ŝ⦈_{π}). By definition of I_{d}(⟦τ ⟧_{π,ξ}, ⦇ŝ⦈_{π}) and Lem. B.6.(ii), there are two cases. First case: eρ ∈ ⊥. Since eρ ∈ SN, by Lem. B.7.(i) we have

(case_{|τ|} e of {c ⇒ e})ρ ∈ ⊥ ⊆ ⟦θ⟧_{π,ξ}

Second case: e →_{wh}^{∗} c_{k} |τ′| a. Let Σ(c_{k}) = ∀ı.ΠX.θ → d\overline{ı}X. We thus have K; Γ ⊢ e_{k} : θ[X := τ , ı := \overline{ı}] → θ. By Prop. B.11 we obtain that a ∈ ⟦θ[X := τ , ı := \overline{ı}]⟧_{π,ξ}. Moreover, by induction hypothesis, e_{k}ρ belongs to ⟦θ[X := τ , ı := \overline{ı}]⟧_{π,ξ} → ⟦θ⟧_{π,ξ}. We deduce that e_{k}ρ a ∈ ⟦θ⟧_{π,ξ}. Since eρ ∈ SN, by Lem. B.5.(iv) we conclude that

case_{|τ|} c |τ′| a of {c ⇒ eρ} ∈ ⟦θ⟧_{π,ξ}

Now, since eρ →_{wh}^{∗} c |τ′| a, by Lem. B.8.(iii) and (SAT2) we obtain

(case_{|τ|} e of {c ⇒ e})ρ ∈ ⟦θ⟧_{π,ξ}

(rec)

\frac{C_{nr}(d) = \{c_{1}^{nr}, …, c_{n}^{nr}\} K; Γ ⊢ e_{k}^{nr} : Inst(c_{k}^{nr}, , τ , θ) (1 ≤ k ≤ n) C_{r}(d) = \{c_{1}^{r}, …, c_{m}^{r}\} K; Γ, f:∀ı ≤ ȷ.d^{ı}τ → θ ⊢ e_{k}^{r} : Inst(c_{k}^{r}, ȷ, τ , θ[ı := ĵ]) (1 ≤ k ≤ m)}{K; Γ ⊢ letrec_{|τ|} f case \{c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}\} : ∀ı.d^{ı}τ → θ}

where ı ∉ K, Γ, τ  ı pos θ  ȷ ∉ ı, K, Γ, τ , θ  |τ| = d|τ | → |θ|

Let π, ξ and ρ such that (π, ξ, ρ) ⊧ K; Γ. Since ı ∉ τ, we have to show that for all α ∈ Ω̂ we have

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ ∈ I_{d}(⟦τ ⟧_{π,ξ}, α) → ⟦θ⟧_{π(ı:=α),ξ}

We reason by induction on α ∈ Ω̂. Since f appears bound in letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ by Barendregt convention we may assume that f ∉ codom(ρ). Hence we have

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ
= letrec_{|τ|} f case {c^{nr} ⇒ e^{nr}ρ | c^{r} ⇒ e^{r}ρ}

First, we show the following claim. Claim: e^{nr}ρ, e^{r}ρ ∈ SN. By induction hypothesis, since (π, ξ, ρ) ⊧ K; Γ, we

have e^{nr}ρ ∈ ⟦Inst(c^{nr}, , τ , θ)⟧_{π,ξ} ⊆ SN Now, since ȷ ∉ K, Γ and since f ∈ ⊥, for all α ∈ Ω̂ we have

(π(ȷ := α), ξ, ρ(f := f)) ⊧ K; G, f:∀ı ≤ ȷ.d^{ı}τ → θ

Hence by induction hypothesis we obtain

e^{r}ρ(f := f) = e^{r}ρ ∈ ⟦Inst(c^{r}, ȷ, τ , θ[ı := ĵ])⟧_{π(ȷ:=α),ξ} ⊆ SN
⊓ ⊔

Now, let a ∈ I_{d}(⟦τ ⟧_{π,ξ}, α). We show that

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr}ρ | c^{r} ⇒ e^{r}ρ} a ∈ ⟦θ⟧_{π(ı:=α),ξ}

If a ∈ ⊥, since e^{nr}ρ, e^{r}ρ ∈ SN, by Lem. B.7.(ii) we have

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr}ρ | c^{r} ⇒ e^{r}ρ} a ∈ ⊥ ⊆ ⟦θ⟧_{π(ı:=α),ξ}

We now assume that a ∈ I_{d}(⟦τ ⟧_{π,ξ}, α) \ ⊥ and reason by cases on α ∈ Ω̂. α = 0. There are k ∈ {1, …, n} and a ∈ SN such that a →_{wh}^{∗} c_{k}^{nr} |τ′| a with

a ∈ ⟦θ⟧_{∅,X:=⟦τ ⟧_{π,ξ}} and Σ(c_{k}^{nr}) = ∀ı.ΠX.θ → d^{ı}X. Recall that K; Γ ⊢ e_{k}^{nr} : θ[X := τ] → θ. Since ı ∉ K, Γ, we have (π(ı := 0), ξ, ρ) ⊧ K, Γ and by induction hypothesis we get e_{k}^{nr}ρ ∈ ⟦θ[X := τ] → θ⟧_{π(ı:=0),ξ}. Now, recall that ı ∉ θ, τ and moreover that the only free type variables of θ are X. Hence, by Prop. B.11 we get e_{k}^{nr}ρ ∈ ⟦θ⟧_{∅,X:=⟦τ ⟧_{π,ξ}} → ⟦θ⟧_{π(ı:=0),ξ}. We deduce that e_{k}^{nr}ρ a ∈ ⟦θ⟧_{π(ı:=0),ξ}. Since e^{nr}ρ, e^{r}ρ ∈ SN, by Lem. B.5.(v) we have

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr}ρ | c^{r} ⇒ e^{r}ρ} (c_{k}^{nr} |τ′| a) ∈ ⟦θ⟧_{π(ı:=0),ξ}

Now, by (SAT2) and Lem. B.8.(i), since a →_{wh}^{∗} c_{k}^{nr} |τ′| a we deduce that

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ a ∈ ⟦θ⟧_{π(ı:=0),ξ}

α = β ⊕ 1. There are a ∈ SN such that a →_{wh}^{∗} c |τ′| a. If c is non-recursive, then we reason as in the case α = 0. So we assume that c = c_{k}^{r} for some k ∈ {1, …, m}. Thus a ∈ ⟦θ⟧_{ı:=β,X:=⟦τ ⟧_{π,ξ}} and Σ(c_{k}^{r}) is of the form ∀ı.ΠX.θ → dîX. Let e′ =_{def} letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}. By induction hypothesis on α, for all γ ≤ β we have

e′ρ ∈ I_{d}(⟦τ ⟧_{π,ξ}, γ) → ⟦θ⟧_{π(ı:=γ),ξ}

Let π′ =_{def} π(ȷ := β). Since ȷ ∉ ı, τ , θ, it follows that

e′ρ ∈ ⋂{⟦d^{ı}τ → θ⟧_{π′(ı:=γ),ξ} | π′(ı := γ) ⊧ ı ≤ ȷ}

that is e′ρ ∈ ⟦∀ı ≤ ȷ.d^{ı}τ → θ⟧_{π′,ξ}. Since ȷ ∉ K, Γ it follows that we have

(π′, ξ, ρ(f := e′ρ)) ⊧ K; Γ, f:∀ı ≤ ȷ.d^{ı}τ → θ

Recall that K; Γ, f: ∀ı ≤ ȷ.d^{ı}τ → θ ⊢ e_{k}^{r} : θ[X := τ , ı := ȷ] → θ[ı := ĵ]. By induction hypothesis, we obtain

e_{k}^{r}ρ(f := e′ρ) ∈ ⟦θ[X := τ , ı := ȷ] → θ[ı := ĵ]⟧_{π′,ξ}

By Prop. B.11 we deduce that

e_{k}^{r}ρ(f := e′ρ) ∈ ⟦θ⟧_{π′(ı:=⦇ȷ⦈_{π′}),ξ(X:=⟦τ ⟧_{π′,ξ})} → ⟦θ⟧_{π′(ı:=⦇ĵ⦈_{π′}),ξ}

Since ȷ ∉ θ, τ , θ (recall that the only free stage variable of θ is ı and that ı ≠ ȷ), we have e_{k}^{r}ρ(f := e′ρ) ∈ ⟦θ⟧_{π(ı:=β),ξ(X:=⟦τ ⟧_{π,ξ})} → ⟦θ⟧_{π(ı:=β⊕1),ξ}. It follows that e_{k}^{r}ρ(f := e′ρ) a ∈ ⟦θ⟧_{π(ı:=β⊕1),ξ}. Since f ∉ codom(ρ), we have e_{k}^{r}ρ(f := e′ρ) = (e_{k}^{r}ρ)[f := e′ρ]. Since moreover e^{nr}ρ, e^{r}ρ ∈ SN, by Lem. B.5.(vi) we deduce that

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr}ρ | c^{r} ⇒ e^{r}ρ} (c_{k}^{r} |τ′| a) ∈ ⟦θ⟧_{π(ı:=β⊕1),ξ}

Now, by (SAT2) and Lem. B.8.(i), since a →_{wh}^{∗} c_{k}^{r} |τ′| a we deduce that

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ a ∈ ⟦θ⟧_{π(ı:=β⊕1),ξ}

α is a limit ordinal. In this case, there is β < α such that a ∈ I_{d}(⟦τ ⟧_{π,ξ}, β). By induction hypothesis we have

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ a ∈ ⟦θ⟧_{π(ı:=β),ξ}

and since ı pos θ, by Lem. B.12 we deduce

letrec_{|τ|} f case {c^{nr} ⇒ e^{nr} | c^{r} ⇒ e^{r}}ρ a ∈ ⟦θ⟧_{π(ı:=α),ξ}

(sub)

\frac{K; Γ ⊢ e : \underline{σ} K ⊢ \underline{σ} ⊑ \underline{τ}}{K; Γ ⊢ e : \underline{τ}}

By induction hypothesis and Lem. B.14. ⊓ ⊔