On the Stability by Union of Reducibility Candidates

Colin Riba

INPL & LORIA^{⋆}, Nancy, France

                              riba@loria.fr

Abstract. We investigate some aspects of proof methods for the termination of (extensions of) the second-order λ-calculus in presence of union and existential types. We prove that Girard’s reducibility candidates are stable by union iff they are exactly the non-empty sets of terminating terms which are downwardclosed w.r.t. a weak observational preorder. We show that this is the case for the Curry-style second-order λ-calculus. As a corollary, we obtain that reducibility candidates are exactly the Tait’s saturated sets that are stable by reduction. We then extend the proof to a system with product, co-product and positive iso-recursive types.

1 Introduction

Since their introduction in [17], union and existential types with type assignment rules are present in many type systems. From a foundational perspective, they are interesting as dual of respectively intersection and second-order types. The paper [3] provides detailed investigations on syntactic as well as semantics issues of union types. As a theoretical tool, they have been used in [8, 9] to prove that a kind of Böhm trees, called Lévy-Longo trees, distinguishes pure λ-terms exactly as does their observation in the lazy concurrent λ-calculus.

Interesting applications of union types are the XML processing languages XDuce [14] and ℂDuce [11]. They describe types of XML documents by means of regular expressions whose internal representation relies on union types.

Existentials and unions are also interesting tools for representing abstractions of programs. In the context of strictness analysis, unions are used in [15] to represent disjunctive properties of programs.

Frédéric Blanqui and the author proposed in [6] a termination criterion for higher-order conditional rewriting that use constrained types. Existential constraints arise naturally, for example when proving that some implementations of QuickSort preserves the size of its argument. This work relies on proof methods for the termination of typed λ-calculus plus rewriting in presence of existential types.

⋆ UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP, Campus Scientifique, BP 239, 54506 Vandoeuvre-lès-Nancy Cedex, France

Usual proofs of strong normalization (i.e. termination) for typed λ-calculi assign to each type T a set of strongly normalizing terms ⟦T ⟧ρ (the interpretation of T, with an assignment ρ of its free variables). Then, they use soundness of this interpretation w.r.t. the type system: typable terms belong to the interpretation of their types. But soundness requires that types are not interpreted by arbitrary sets of terms. They must satisfy some closure conditions. The two most popular ones are Girard’s reducibility candidates and Tait’s saturated sets. See [12] for a detailed discussion and historical references. A comparison of Girard’s and Tait’s closure conditions can also be found in [23].

In order to handle elimination rules of union and existential types, it is convenient to interpret these types by using unions of interpretations: ⟦T_{1} ∪ T_{2}⟧ρ = ⟦T_{1}⟧ρ ∪ ⟦T_{2}⟧ρ and ⟦∃X.T ⟧ρ = ⋃_{C∈Cl}⟦T ⟧ρ[C/X] (Cl is the collection of closed sets under consideration). This making requires stability by union of closed sets: if C is a family of closed sets, then ⋃ C =_{def} ⋃_{C∈C} C is closed. Approaches not relying on stability by union are briefly discussed in Sec. 8.

It is well known (see e.g. [23]) that Tait’s saturated sets for β-reduction are stable by union. However, their extension with additional computational rules can by cumbersome. On the other hand, Girard’s reducibility candidates are more adjustable, in particular for dealing with rewriting [5]. However, their stability by union is known to be problematic [23].

In this paper, we prove the stability by union of reducibility candidates for the polymorphic λ-calculus λ2. To our knowledge, this property was hitherto unknown, and even often believed to be false. We extend the proof to λ2U^{+}, the extension of λ2 with product, co-product and positive iso-recursive types (it is shown in [21] that it is a proper extension of λ2).

The key observation is that reducibility candidates are stable by union iff they are exactly the non-empty sets of strongly-normalizing terms which are downward-closed w.r.t. a weak observational preorder (see [16] for a presentation and references on related topics). This is a very simple structure compared to the one appearing in the definition of reducibility candidates, which is not trivial and somehow mysterious. Hence, studying stability by union of reducibility candidates reveals important facts on their fundamental nature.

We show that the above condition is equivalent to say that some terms, called neutral, have a maximal reduct w.r.t. to that preorder. For the case of λ2 and λ2U^{+}, we prove it by using a simple syntactic property called weakstandardization. It relies on the orthogonality of λ2 and λ2U^{+}: computational rules are non-ambiguous and left-linear (no equality tests between open terms). As a by-product, we obtain that Girard’s sets correspond exactly to the Tait’s sets that are stable by reduction.

We present the syntax of λ2 in Sec. 2, and reducibility in Sec. 3. Our analysis of stability by union of reducibility candidates is presented in Sec. 4. Finally, the system λ2U^{+} is presented in Sec. 6, and stability by union of its reducibility candidates in Sec. 7.

We assume familiarity with λ-calculus and types, and refer to [13, 4] for detailed introductions.

2 The Polymorphic λ-Calculus λ2

The core language of the paper is the Curry-style second-order λ-calculus λ2, as presented in [4]. We recall the main notations below, and then discuss union and existential types.

Let X be a countable set of variables and Λ be the set of untyped λ-terms:

t, u ∈ Λ ::= x ∈ X | λx.t | t u .

They are considered equals modulo α-conversion. Terms come with the usual notion of β-reduction, namely (λx.t)u ↦_{β} t[u/x], where t[u/x] is the captureavoiding substitution of x by u in t. We let → be the smallest rewrite relation on Λ containing ↦_{β}. In the following, we refer to ↦_{β} as the top reduction and denote by TNF the set of terms in ↦_{β}-normal form. We let (t)_{→} =_{def} {u | t → u} and (t)\underrightarrow{∗} =_{def} \{u | t →^{∗} u\}, where →^{∗} is the reflexive-transitive closure of →. We write (t_{1}, …, t_{n}) → (t′_{1}, …, t′_{n}) iff there is i such that t_{i} → t′_{i} and t_{j} = t′_{j} for all j ≠ i. A term t is strongly normalizing iff every reduction sequence issued from t is finite. Let SN be the set of strongly-normalizing terms. Note that t ∈ SN iff either t is not reducible or all its reducts are in SN. It follows that SN is the smallest set such that for all t,

(∀u (t → u ⇒ u ∈ SN)) ⇒ t ∈ SN .

Types are the formulas of second-order minimal logic, with variables in V:

T, U ∈ T ::= X ∈ V | T ⇒ U | ∀X.T .

We denote by X (t) (resp. V(T)) the set of free variables of t (resp. T). An environment Γ is a finite set of declarations x : A such that x ≠ y whenever (x : A), (y : B) ∈ Γ. Typing judgments are sequents of the form Γ ⊢ t : A, derived with the following rules:

(Ax) \overline{Γ, x : T ⊢ x : T}

(⇒ I) \frac{Γ, x : U ⊢ t : T}{Γ ⊢ λx.t : U ⇒ T}  (⇒ E) \frac{Γ ⊢ t : U ⇒ T  Γ ⊢ u : U}{Γ ⊢ tu : T}
(∀ I) \frac{Γ ⊢ t : T}{Γ ⊢ t : ∀X.T} (X ∉ V(Γ))  (∀ E) \frac{Γ ⊢ t : ∀X.T}{Γ ⊢ t : T [U/X]}

Existential and Union Types. Our main point is to prove the soundness (w.r.t. some closure operator) of elimination rules of union and implicit existential types. Such types are manipulated with type-assignment rules, in the spirit of [17, 3]. Typical rules for these systems are:

\begin{matrix}(∃ I) \frac{Γ ⊢ t : T [U/X]}{Γ ⊢ t : ∃X.T} & (∃ E) \frac{Γ ⊢ t : ∃X.T Γ, x : T ⊢ u : U}{Γ ⊢ u[t/x] : U} (X ∉ V(Γ, U)) \\ (∪I) \frac{Γ ⊢ t : T_{i}}{Γ ⊢ t : T_{1} ∪ T_{2}} (i ∈ \{1, 2\}) & (∪E) \frac{Γ ⊢ t : T_{1} ∪ T_{2} ∀i ∈ \{1, 2\}, Γ, x : T_{i} ⊢ u : U}{Γ ⊢ u[t/x] : U} \end{matrix}

It is worth noting that such types are not subject to the Curry-Howard propositions-as-types isomorphism, in the sense that proofs trees do not corresponds to terms. It would require to reflect all types constructions at the term level, and this leads to use explicit constructs for disjunction and existential quantification, as discussed for e.g. in [13].

This is precisely what we want to avoid in [6], where existential quantifications are used in a constrained type system. We want terms typed in this system to be used in a constrained-free type system. Hence, constraints should not appear at the term level, and we are thus interested in implicit existential types.

On the other-hand, it is clear that the impredicative codings of unions and existential quantification given in [13] do not define union and implicit existential types. This motivates us to handle the soundness of rules (∪E) and (∃ E) by tools lying inside the reducibility framework. A first step is to study the behavior of Girard’s reducibility candidates w.r.t. union. Since type quantifications of [6] are not the usual ones, presented above, that operate on the type structure, we study stability by union in a generic way, without committing to specific typing rules.

3 Reducibility

Strong normalization proofs of λ2 usually interpret types T ∈ T as sets of strongly normalizing terms ⟦T ⟧ρ ⊆ SN. Then strong normalization of typable terms follows from the soundness of the interpretation:

If Γ ⊢ t : T and σ(x) ∈ ⟦A⟧ρ for all (x : A) ∈ Γ, then σ(t) ∈ ⟦T ⟧ρ.  (⋆)

As said in the introduction, (⋆) does not hold when types are interpreted by arbitrary subsets of SN. In this section, we focus on a well-known collection of suitable subsets of SN called Girard’s reducibility candidates.

Definition 3.1 (Neutral Terms). Terms not headed by an abstraction are called neutral. Let N be the set of neutral terms.

Let HN, the set of hereditary neutral terms, be the smallest set such that for all t ∈ N, (∀u (t → u ⇒ u ∈ HN)) ⇒ t ∈ HN.

Note that HN ⊆ SN. Let elimination contexts be E[ ] ::= [ ] | E[ ]t. They correspond to call-by-name evaluation contexts, dual to call-by-value evaluation contexts of [10]. We borrowed from [1] their use in reducibility.

Remark 3.2. The general intuition behind neutral terms is linked to the duality between introductions and eliminations in natural deduction. Since neutral terms are not headed by introductions, they do not interact with elimination contexts: if t ∈ N and E[t] → v then v = E′[t′] with (E[ ], t) → (E′[ ], t′). It follows that for t ∈ N, we have E[t] ∈ N and E[t] ∈ SN as soon as {E[u] | t → u} ⊆ SN.

Definition 3.3 (Reducibility Candidates). The set of reducibility candidates, denoted by CR, is the set of all C ⊆ SN such that (CR0) if t ∈ C and t → u then u ∈ C, (CR1) if t ∈ N and (∀u (t → u ⇒ u ∈ C)) then t ∈ C.

The definition of SN directly implies that SN ∈ CR. Now, let us see why CR is stable by intersection (C ⊆ CR ⇒ ⋂ C ∈ CR). Recall that a closure operator on a partial order (D, ≤) is a function \overline{·} : D → D which is idempotent: \overline{\overline{X}} = \overline{X}; extensive: X ≤ \overline{X}; and monotone: X ≤ Y ⇒ \overline{X} ≤ \overline{Y}. It is well-known that the greatest lower bound of a family of closed elements is closed.

The shape of the clauses of CR is sufficient for the existence of a closure operator \overline{·} : P(SN) → P(SN) such that \overline{X} is the least reducibility candidate containing X. Indeed, clauses (CR0) and (CR1) are closure rules in the sense of [19], p.17, and the existence of \overline{·} is insured by Thm. 2.6, see pages 16–18 of [19]. We thus have X ∈ CR iff X = \overline{X}.

It follows that (CR, ⊆) has all greatest lower bounds, and they are given by ⋂. As a consequence, it has ⋂ CR as least element. It is thus an inf-semi lattice with greatest element SN, hence a complete lattice.

Proposition 3.4. HN is the least element of CR.

Proof. We obviously have HN ⊆ C for all C ∈ CR, hence HN ⊆ ⋂ CR. For the converse, it suffices to remark that HN ∈ CR. ⊓ ⊔

We now define the interpretation of arrow types.

Proposition 3.5 (Arrow Type Constructor). The arrow type constructor ⇒: P(Λ) × P(Λ) → P(Λ), defined as A ⇒ B =_{def} {t | ∀u(u ∈ A ⇒ tu ∈ B)}, maps reducibility candidates A and B to a reducibility candidate.

Proof. Strong normalization and stability by reduction follows directly from that of B. For (CR1), we have to show that if t ∈ N, then (t)_{→} ⊆ A ⇒ B implies t ∈ A ⇒ B, i.e. u ∈ A ⇒ tu ∈ B. The crucial point is given by Rem. 3.2: since tu ∈ N and t does not interact with the context [ ]u, we are done with (CR1) applied to B, using an induction on (t, u) ∈ SN × SN. ⊓ ⊔

Now, given ρ : V → CR, we can interpret types T ∈ T as reducibility candidates ⟦T ⟧ρ ∈ CR, with ⟦X⟧ρ =_{def} ρ(X), ⟦U ⇒ T ⟧ρ =_{def} ⟦U⟧ρ ⇒ ⟦T ⟧ρ and ⟦∀X.T ⟧ρ =_{def} ⋂{⟦T ⟧ρ[C/X] | C ∈ CR}. We can then prove soundness (⋆), and strong normalization is a consequence of X ⊆ HN and Prop. 3.4. See [13, 12].

4 A General Study of Stability by Union of CR

We have seen that stability by intersection of CR is a consequence of the shape of the clauses (CR0) and (CR1). Such shallow observations do not imply stability by union, which must therefore be proved through a deeper analysis of CR. Indeed, given C ⊆ CR, in order to get ⋃ C ∈ CR we must show that if t is a neutral term with (t)_{→} ⊆ ⋃ C, then every one-step reduct of t must be in the same C ∈ C.

We begin by stability by union of closure operators. In the next Proposition, we assume given a set D and a closure operator \overline{·} : P(D) → P(D). Write \overline{x} for \overline{\{x\}} and \overline{P(D)} for \{\overline{X} | X ⊆ D\}.

Proposition 4.1 (Topological Closure of \overline{·}). Given a closure operator \overline{·} : P(D) → P(D), let \overline{Ω} be the set of non-empty X ⊆ D such that X = ⋃\{\overline{x} | x ∈ X\}. Then \overline{Ω} is the smallest set such that \overline{P(D)} ⊆ \overline{Ω} and C ⊆ \overline{Ω} ⇒ ⋃ C, ⋂ C ∈ \overline{Ω}.

Proof. For all X ∈ \overline{P(D)} we have X = ⋃\{\overline{x} | x ∈ X\} since for all x ∈ X, \overline{x} ⊆ X and x ∈ \overline{x}. It follows that \overline{P(D)} ⊆ \overline{Ω}. If C ⊆ \overline{Ω}, then C = ⋃\{\overline{x} | x ∈ C\} for all C ∈ C. Hence ⋃ C = ⋃\{\overline{x} | x ∈ ⋃ C\}, and ⋃ C ∈ \overline{Ω}. Moreover, if t ∈ ⋂ C, then for all C ∈ C, t ∈ C hence \overline{t} ⊆ C. Therefore \overline{t} ⊆ ⋂ C, and it follows that ⋂ C = ⋃\{\overline{t} | t ∈ ⋂ C\}, i.e. ⋂ C ∈ \overline{Ω}.

Now, let Ω ⊇ \overline{P(D)} be stable by union and intersection. If X ∈ \overline{Ω} then X = ⋃\{\overline{x} | x ∈ X\}. But \{\overline{x} | x ∈ X\} ⊆ Ω, hence ⋃\{\overline{x} | x ∈ X\} ∈ Ω. ⊓ ⊔

In other words, (D, \overline{Ω} ∪ \{∅\}) is a topological space where the set of opens \overline{Ω} ∪\{∅\} contains all \overline{·} -closed sets. Proposition 4.1 implies that it is moreover the coarser topology with this property: if Ω is a collection of opens that contains \overline{·} -closed sets, then \overline{Ω} ⊆ Ω. We now use these facts to study the stability by union of reducibility candidates.

Since we are concerned with properties independent from the calculus, we work with an extension λext of λ2. We assume that every term typable in λ2 is typable in λext and that λext is equipped with a rewrite relation, denoted by →, that is finitely branching and contains ↦_{β}. Notations of Sec. 2 are imported in λext. Finally, we assume given a set of neutral terms of λext, still denoted by N, that contains the neutral terms of λ2.

Definition 4.2 (λext-Reducibility Candidates). The set of λext-reduci-bility candidates, denoted by CR, is the set of all C ⊆ SN such that (CR0) if t ∈ C and t → u then u ∈ C, (CR1) if t ∈ N and (∀u (t → u ⇒ u ∈ C)) then t ∈ C.

As with λ2, CR is the set of closed sets for a closure operator \overline{·} : P(SN) → P(SN). An explicit inductive definition of \overline{·} is useful:

Lemma 4.3 (The Closure Operator \overline{·} of CR). Given X ⊆ SN, let \overline{X}_{0} =_{def} (X)\underrightarrow{∗}, and for all i ≥ 0, \overline{X}_{i+1} =_{def} \overline{X}_{i} ∪ \{t ∈ N | (t)_{→} ⊆ \overline{X}_{i}\}. Then, for all X ⊆ SN, \overline{X} =_{def} ⋃_{i≥0} \overline{X}_{i} is the smallest reducibility candidate containing X.

Proof. First, we show that \overline{X} ∈ CR. (CR0) Let t → v and t ∈ \overline{X}_{i} with i as small as possible. If i = 0, then t ∈ (X)\underrightarrow{∗},

hence v ∈ (X)\underrightarrow{∗} = \overline{X}_{0}. Otherwise, i = j + 1, and v ∈ \overline{X}_{j}. (CR1) Let t ∈ N such that for all v ∈ (t)_{→}, there is i_{v} with v ∈ \overline{X}_{i_{v}}. Since → is

finitely branching, there is a j greater than every i_{v}, thus t ∈ \overline{X}_{j+1}. Second, by induction on i, we prove that if C ∈ CR and X ⊆ C, then \overline{X}_{i} ⊆ C. We have \overline{X}_{0} = (X)\underrightarrow{∗} ⊆ C by (CR0). For i ≥ 0, if t ∈ \overline{X}_{i+1} \ \overline{X}_{i}, then t ∈ N and by induction hypothesis, (t)_{→} ⊆ \overline{X}_{i} ⊆ C. Hence t ∈ C by (CR1). ⊓ ⊔

Thanks to Lem. 4.3, we have an explicit definition of the closure operator of CR, denoted by \overline{·}. Now, Prop. 4.1 gives us \overline{Ω}, which is the topological closure of \overline{·}. We let \overline{CR} =_{def} \overline{Ω}. Proposition. 4.1 implies that CR ⊆ \overline{CR} and that CR is stable by union iff CR = \overline{CR}.

Before studying what insures the equality of CR and \overline{CR}, let us have a look on the structure of the latter. We begin by a characterization of the membership t ∈ \overline{u} that uses the weak observational preorder ⊑.

Definition 4.4. Let t ⊑ u iff for all v ∉ N, t →^{∗} v ⇒ u →^{∗} v. We denote by ⊑_{SN} the restriction of ⊑ to SN.

Observational preorders where introduced to characterize behavioral equivalence: two pieces of programs are observationally equivalent iff when plugged in a program context, the obtained programs both diverges or evaluates to the same value. Contexts are arbitrary terms with a hole, including those of the form t[ ] and λx.[ ]. With closed terms, thanks to Milner’s Context Lemma, this is equivalent to observation in applicative contexts (our elimination contexts). Of course, this fails for open terms. See [18, 16] for a presentation and references on the subject.

In λ2, non-neutral terms are abstractions, hence closed non-neutral terms correspond to the usual notion of value. Moreover, we have t ⊑ u iff for all E[ ], for all v ∉ N, (E[t] →^{∗} v ⇒ E[u] →^{∗} v). Thus, with ⊑ we observe the reduction to values of open terms plugged in elimination contexts. Hence the name weak observational preorder. We generalize these ideas to the system λ2U^{+} in Sec. 7.

In order to characterize t ∈ \overline{u} with ⊑, we need a few properties. First, note that t → u implies u ⊑ t.

Proposition 4.5. Let X ⊆ SN. Then t ∈ \overline{X} iff either t ∈ (X)\underrightarrow{∗} or (t ∈ N and (t)_{→} ⊆ \overline{X}).

Proof. The ”if” direction directly follows from (CR0) and (CR1). Conversely, let i be as small as possible such that t ∈ \overline{X}_{i}. Thus, either i = 0 and t ∈ (X)\underrightarrow{∗} or i = j + 1, t ∈ \overline{X}_{j+1} \ \overline{X}_{j} and by definition t ∈ N and (t)_{→} ⊆ \overline{X}_{j}. ⊓ ⊔

As a consequence, all non-neutral terms of \overline{X} are in (X)\underrightarrow{∗}. In other words, the values of \overline{X} are entirely determined by X.

Proposition 4.6. Let t ∈ N ∩ SN and X ⊆ SN. Then (t)_{→} ⊆ \overline{X} iff for all v ∉ N, t →^{∗} v ⇒ v ∈ (X)\underrightarrow{∗}.

Proof. For the ”only-if” direction, we reason by induction on t ∈ SN. Assume that (t)_{→} ⊆ \overline{X} and let t →^{∗} v′ ∉ N. Since t ∈ N, we have t → v →^{∗} v′ with v ∈ \overline{X}. If v ∉ N, then by Prop. 4.5 we have v ∈ (X)\underrightarrow{∗}, hence v′ ∈ (X)\underrightarrow{∗}. Otherwise, since (v)_{→} ⊆ \overline{X} we can apply the induction hypothesis and get v′ ∈ (X)\underrightarrow{∗}.

For the converse, we also reason by induction on t ∈ SN. If t ∈ (X)\underrightarrow{∗} then we are done since (t)_{→} ⊆ (X)\underrightarrow{∗} ⊆ \overline{X}. Assume that t ∉ (X)\underrightarrow{∗}. Let v ∈ (t)_{→}. If v ∉ N, then by assumption v ∈ (X)\underrightarrow{∗}, hence v ∈ \overline{X}. Otherwise, using (CR1) it suffices to show that (v)_{→} ⊆ \overline{X}. But by assumption, every v′ ∈ (v)\underrightarrow{∗} \N belongs to (X)\underrightarrow{∗}. Hence by induction hypothesis (v)_{→} ⊆ \overline{X}. ⊓ ⊔

Thanks to Proposition 4.6, each \overline{t} is in fact an initial segment w.r.t. ⊑_{SN}.

Lemma 4.7. For all t ∈ SN, \overline{t} = \{u | u ⊑_{SN} t\}.

Proof. By Prop. 4.6, u ∈ \overline{t} iff t, u ∈ SN and either t →^{∗} u or u ∈ N and (u)\underrightarrow{∗} \ N ⊆ (t)\underrightarrow{∗}. But this is exactly u ⊑_{SN} t. ⊓ ⊔

This gives a nice straight structure to the elements of \overline{CR}.

Theorem 4.8. Let O be the set of non empty subsets of SN which are downward closed w.r.t. ⊑_{SN}, i.e. X ∈ O iff ∅ ≠ X ⊆ SN and for all t, u, if t ∈ X and u ⊑_{SN} t then u ∈ X. Then we have \overline{CR} = O.

Proof. Thanks to Lem. 4.7, we have X ∈ \overline{CR} iff it is a non-empty subset of SN such that X = ⋃\{\overline{t} | t ∈ X\} = \{u | ∃t(u ⊑_{SN} t ∧ t ∈ X)\}, i.e. X ∈ O. ⊓ ⊔

It is surprising that we can give such a simple structure to \overline{CR}. The most important, however, is the consequence on the stability by union of CR.

Corollary 4.9. CR is stable by union iff CR = O.

The structure of reducibility candidates is at a first sight not trivial and somehow mysterious. It is therefore extremely interesting to understand what allows CR = O, giving them a so simple structure. Hence the question of their stability by union reveals important facts on their fundamental nature.

The next step is to characterize what implies CR = O. Recall that Thm. 4.8 says that CR ⊆ O.

Proposition 4.10. O ⊆ CR iff for all t ∈ N ∩ SN, there is u ∈ (t)_{→} such that t ⊑_{SN} u.

Proof. Let C ∈ O. Since it is stable by reduction, it suffices to check that if t ∈ N and (t)_{→} ⊆ C, then t ∈ C. But there is u ∈ (t)_{→} such that t ⊑_{SN} u, and u ∈ C implies t ∈ C. Therefore, C ∈ CR. Conversely, assume that O ⊆ CR. Let t ∈ N ∩ SN and X =_{def} ⋃\{\overline{u} | t → u\}. By Lem. 4.7, we have X ∈ O ⊆ CR, hence t ∈ X since t ∈ N and (t)_{→} ⊆ X. It follows that there is some u ∈ (t)_{→} such that t ⊑_{SN} u. ⊓ ⊔

The property of SN neutral terms expressed in Prop. 4.10 is that a reduct u of a neutral term t such that t ⊑_{SN} u is in some sense a principal reduct of t: the values of t are exactly those of u. Moreover, u ∈ max_{⊑_{SN}} (t)_{→}, i.e. a principal reduct is maximal among all possible reducts.

For λ2, this has to be linked with call-by-name languages, in which terms to be evaluated are neutral, and the evaluation preserves possible values.

Definition 4.11. A term u ∈ (t)_{→} is a principal reduct (written p.r.) of t iff t ⊑ u and t is said to have the principal reduct property (written p.r.p.) when either such a u exists or t is a normal form.

We reduce the stability by union of CR to the principal reduct property for neutral terms.

Corollary 4.12. We have C ⊆ CR ⇒ ⋃ C ∈ CR iff every t ∈ N ∩ SN has the principal reduct property.

As pointed out by Prop. 3.5, in order for t ∈ N to belong to C ∈ CR, C uses information on the behavior of t in elimination contexts. This information is given by the values of t, and clause (CR1) relies on the fact since t ∈ N, its values are that of (t)_{→}. But if t ⊑_{SN} u, the values of t are also values of u. That is, if u ∈ C and t ⊑_{SN} u then t ∈ C, and it follows that t ⊑_{SN} u implies t ∈ \overline{u}. Moreover, Lem. 4.7 says that this exactly characterizes \overline{u}: if it contains t, then the values of t are values of u.

Now, recall that given C ⊆ CR, in order to get ⋃ C ∈ CR we must show that if t ∈ N has (t)_{→} ⊆ ⋃ C, then every v ∈ (t)_{→} must be in fact the same C ∈ C. This amounts to say that (t)_{→} contains an u such that t ⊑_{SN} u, hence that t has a principal reduct.

5 Stability by Union of CR in λ2

In this section, we show the p.r.p. for λ2. This leads to observe that reducibility candidates are exactly the Tait’s saturated sets which are stable by reduction. We do not give the proofs that are subsumed by those for λ2U^{+}, presented in Sec. 7.

The p.r.p. is a consequence of the standardization theorem of λ2. However, since we only need this property on SN terms, it can be proved using a weaker property, called weak standardization.

This property was coined in [2] as a consequence of standardization. However, it admits a much direct proof, which rely on the orthogonality of the calculus. By the way, it is less a weak standardization property than a standardization for the weak head reduction, which corresponds to reduction in elimination contexts.

Definition 5.1 (Weak Head Reduction). The relation →_{H} of weak head reduction is defined as t →_{H} u iff t = E[t′], t′ ↦_{β} u′ and E[u′] = u. We denote by HNF the set of terms in →_{H}-normal form.

Lemma 5.2 (Weak Standardization). Let t ↦_{β} u and assume that E[t] → v with v ≠ E[u]. Then v = E′[t′] with (E[ ], t) → (E′[ ], t′) and there exists u′ such that t′ ↦_{β} u′ and E[u] →^{∗} E′[u′].

In order to show that strongly normalizing neutral terms have the p.r.p., we use in addition the fact that HNF ∩ N (i.e. the set of terms of the from E[x]), is stable by reduction. We then obtain stability by union of CR, thanks to Cor. 4.12.

Lemma 5.3 (Principal Reduct Property). Let t ∈ N ∩ SN. If there is u such that t →_{H} u then it is a p.r. of t, otherwise every u ∈ (t)_{→} is a p.r. of t.

Theorem 5.4. If C ⊆ CR then ⋃ C ∈ CR.

The principal reduct property of neutral terms corresponds to the fact that reducibility candidates are stable by strongly normalizing weak head expansions.

Lemma 5.5 (Weak Head Expansion and Reducibility Candidates). Let C ∈ CR. If E[s] ∈ C, t ↦_{β} s and t ∈ SN then E[t] ∈ C.

Weak head reduction is the main notion of the Krivine Abstract Machine, and stability by weak head expansion is the main property required by truth values of Krivine and Danos [7].

Thanks to Cor. 4.9, we have shown that CR = O, thus giving a nice straight structure to CR. Moreover, Lem. 5.3, 4.7 and 5.5 imply that for all C ∈ CR, (SAT 1) if E[x] ∈ SN then E[x] ∈ C; and (SAT 2) if E[s] ∈ C, t ↦_{β} s and t ∈ SN, then E[t] ∈ C.

Subsets of SN satisfying (SAT 1) and (SAT 2) are Tait’s saturated sets.

Definition 5.6. Let SAT be the set of all subsets S ⊆ SN satisfying (SAT 1) and (SAT 2). We denote by SAT_{→} the collection of S ∈ SAT that are stable by reduction: If t ∈ S and t → u then u ∈ S (SAT 0).

The definition makes sense since in (SAT 1) we have E[x] ∈ SN, and, in (SAT 2) we have E[t] ∈ SN by Lem. 5.5.

The stability by union of CR is therefore linked with the fact that every C ∈ CR is saturated. This inclusion has been coined in [12]. The converse is false, as shown by a counter-example given in [23] (Lem. 3.16 pp. 87–88). It relies on the fact that saturated sets are not stable by reduction. However, we can show that saturated sets that are stable by reduction are exactly the reducibility candidates. This seems to have not been remarked before.

Theorem 5.7. SAT_{→} = CR.

Proof. The inclusion CR ⊆ SAT has been coined in [12]. It is a direct consequence of Lem. 5.5 and the stability by reduction of head-normal forms.

The converse, SAT_{→} ⊆ CR, does not seem to have been published before. Let S ∈ SAT_{→}. It satisfies (CR0) thanks to (SAT 0). As for (CR1), let v ∈ N such that (v)_{→} ⊆ S. Thus v ∈ SN. If v ∈ HNF, then v = E[x] ∈ S by (SAT 0). Otherwise, v = E[t] with t ↦_{β} u and E[u] ∈ S by assumption. Hence v ∈ S by (SAT 2). ⊓ ⊔

6 The System λ2U^{+} of Product, Co-Product and Positive Iso-Recursive Types

We now extend results of the previous section by applying Cor. 4.12 to a system with more elaborated types. The system considered, called λ2U^{+}, features product, co-product, positive iso-recursive types and the final type 1. It is a proper extension of λ2 [21]. Our presentation is inspired by that of [1]. Types are extended with:

T, U ∈ T ::= … | T × U | T + U | μX.T | 1

where, in μX.T, X occurs only positively in T: any path from the root of T to an occurrence of X chooses the left argument of ⇒ an even number of times. The syntax of terms is enriched with corresponding introductions and eliminations:

s, t ∈ Λ ::= … | ()
| ⟨t, u⟩ | π_{i}t  i ∈ {1, 2}
| inj_{i} t | case (u, x_{1}.t_{1}, x_{2}.t_{2}) i ∈ {1, 2}
| in t  | out t

We consider the following extension of β-reduction:

π_{i}⟨t_{1}, t_{2}⟩ ↦_{β} t_{i}  case (inj_{i} u, x_{1}.t_{1}, x_{2}.t_{2}) ↦_{β} t_{i}[u/x_{i}]  out (in t) ↦_{β} t .

We let → be the smallest rewrite relation on Λ containing ↦_{β}. The type system is enriched with the following additional rules:

(1 I) \overline{Γ ⊢ () : 1}

(×I) \frac{Γ ⊢ t_{1} : T_{1}  Γ ⊢ t_{2} : T_{2}}{Γ ⊢ ⟨t_{1}, t_{2}⟩ : T_{1} × T_{2}}  (×E) \frac{Γ ⊢ t : T_{1} × T_{2}}{Γ ⊢ π_{i}t : T_{i}} (i ∈ \{1, 2\})

(+I) \frac{Γ ⊢ t : T_{i}}{Γ ⊢ inj_{i} t : T_{1} + T_{2}} (i ∈ \{1, 2\}) (+E) \frac{Γ ⊢ t : T_{1} + T_{2} Γ, x : T_{i} ⊢ t_{i} : U}{Γ ⊢ case (t, x_{1}.t_{1}, x_{2}.t_{2}) : U}

(μI) \frac{Γ ⊢ t : T [μX.T/X]}{Γ ⊢ in t : μX.T} (μE) \frac{Γ ⊢ t : μX.T}{Γ ⊢ out t : T [μX.T/X]}

Example 6.1. Our motivation to consider λ2U^{+} is that it is a very atomic calculus for inductives types. For example, polymorphic lists can be encoded as follows:

List =_{def} ∀Y.μX.1 + Y × X
nil =_{def} in (inj_{1} ())
cons (x, xs) =_{def} in (inj_{2} ⟨x, xs⟩)

In [21], it is shown that higher-order primitive recursion can be defined using iso-recursives types and the rule out (in t) ↦_{β} t, and moreover that this rule can not be simulated in λ2 by means of β-reductions.

7 Reducibility and Stability by Union for λ2U^{+}

We now introduce tools for reducibility in λ2U^{+}. We then prove the p.r.p. and equivalence of CR and a suitable version of SAT_{→}.

We define the top reduction as ↦_{β}, and still denote by TNF the set of terms in top-normal form. It is convenient to factorize the introduction-elimination duality of natural deduction with the following atomic contexts: atomic eliminations contexts (aec) denoted by ϵ[ ] and atomic introduction contexts (aic) denoted by ι[ ] are defined as follows:

ϵ[ ] ::= [ ]t | π_{1}[ ] | π_{2}[ ] | case ([ ], x_{1}.t_{1}, x_{2}.t_{2}) | out [ ] ;
ι[ ] ::= λx.[ ] | ⟨[ ], t⟩ | ⟨t, [ ]⟩ | inj_{1} [ ] | inj_{2} [ ] | in [ ] | () .

Note that the introduction context for the terminal type constructor is not linear. The columns of the above array define a relation written ϵ[ ] ⊥ ι[ ]. We have ϵ[ ] ⊥ ι[ ] when ϵ[ι[ ]] is a β-redex, except for the product, where we let

π_{1}[ ] ⊥ ⟨[ ], t⟩  and  π_{2}[ ] ⊥ ⟨t, [ ]⟩
but  π_{2}[ ] ⊥̸ ⟨[ ], t⟩  and  π_{1}[ ] ⊥̸ ⟨t, [ ]⟩ .

Then, to each aec ϵ[ ] corresponds the set ϵ[ ]^{⊥} of aic ι[ ] such that ϵ[ ] ⊥ ι[ ], and conversely, ι[ ]^{⊥} is the set of aec ϵ[ ] such that ϵ[ ] ⊥ ι[ ]. In the following, we will sometime write unambiguously ι[ ] ⊥ ϵ[ ] instead of ϵ[ ] ⊥ ι[ ]. The extension of elimination contexts E[ ] is obvious: E[ ] ::= [ ] | ϵ[E[ ]].

Proposition 7.1. If E[ϵ[t]] → v, then v = E′[t′] with (E[ ], ϵ[t]) → (E′[ ], t′).

Proof. By structural induction on E[ ]. The case E[ ] = [ ] is obvious. In the other cases, we have E[ ] = ϵ′[F [ ]]. First, the reduction ϵ′[F [ϵ[t]]] → v can not be a top reduction. Hence we have v = ϵ′′[v′] with (ϵ′[ ], v) → (ϵ′′[ ], v′), and by induction hypothesis v′ = F′[t′] with (F [ ], t) → (F′[ ], t′). Take E′[ ] = ϵ′′[F′[ ]].

⊓ ⊔

Definition 7.2. We say that terms not of the form ι[t] are neutral and denote by N the set of neutral terms.

Hence, the terms nil and cons(x, l) of Ex. 6.1 are not neutral. This strengthen our intuition that non-neutral terms corresponds to values. Note that elimination contexts are a generalization of applicative contexts to product, coproduct and iso-recursive types. We can now substantiate our claim that ⊑ is a weak observational preorder.

Proposition 7.3. t ⊑ u iff ∀E[ ] (E[t] →^{∗} ι[h] ⇒ E[u] →^{∗} ι[h]).

Proof. Obviously, ∀E[ ] (E[t] ⊑ E[u]) implies t ⊑ u (take the empty context). Conversely, assume that t ⊑ u. If E[t] →^{∗} ι[h], we are in the case that E[t] →^{∗} E′[ι′[h′]] →^{∗} ι[h] with (E[ ], t) →^{∗} (E′[ ], ι′[t′]). Since t ⊑ u, we have u →^{∗} ι′[h′], hence E[u] →^{∗} E′[ι′[h′]] →^{∗} ι[h]. ⊓ ⊔

We obtain CR by instantiating Def. 4.2 with λ2U^{+} and N. Notions of weak head reduction and weak head normal forms are directly adapted from Sec. 5, with the obvious update of elimination contexts. Recall that u ∈ HNF iff for all E[ ], t such that u = E[t], we have t ∈ TNF. It follows that untyped terms in HNF ∩ N need not to be of the form E[x]. However, stability by reduction of HNF ∩ N still holds.

Proposition 7.4. If t ∈ HNF ∩ N and t → u, then u ∈ HNF ∩ N.

Proof. We reason by structural induction on t. The case t ∈ X is trivial. Assume t = ϵ[t_{1}] and let t → t′. Since t ∈ HNF, we have t′ = ϵ′[t′_{1}] with (t_{1}, ϵ[ ]) → (t′_{1}, ϵ′[ ]), hence t′ ∈ N. If t_{1} ∈ N, then t_{1} ∈ N ∩ HNF and by induction hypothesis t′_{1} ∈ N ∩HNF. It follows that t′ = ϵ′[t′_{1}] ∈ HNF. Otherwise, t_{1} = ι[t_{2}] with ϵ[ ] ⊥̸ ι[ ]. Hence, t′_{1} = ι′[t′_{2}] with (t_{2}, ι[ ]) → (t′_{2}, ι′[ ]), and ϵ′[ ] ⊥̸ ι′[ ]. Hence t′ = ϵ′[ι′[t′_{2}]] ∈ HNF. ⊓ ⊔ We now turn to weak standardization. It is stated and used for λ2U^{+} in [1].

Proposition 7.5. If t ↦_{β} u and t → v, then either v = u or there exists u′ such that v ↦_{β} u′ ←^{∗} u.

Proof. By cases on t ↦_{β} u. t = (λx.t_{1})t_{2}. In this case, u = t_{1}[t_{2}/x] and if v ≠ u, then v = (λx.t′_{1})t′_{2} with

(t_{1}, t_{2}) → (t′_{1}, t′_{2}), and v ↦_{β} t′_{1}[t′_{2}/x] ←^{∗} u. t = π_{i}⟨t_{1}, t_{2}⟩. In this case, u = t_{i}, and if v ≠ u, then v = π_{i}⟨t′_{1}, t′_{2}⟩ with (t_{1}, t_{2}) →

(t′_{1}, t′_{2}), and v ↦_{β} t′_{i} ←^{∗} u. t = case (inj_{i} r, x_{1}.t_{1}, x_{2}.t_{2}). In this case, u = t_{i}[r/x_{i}] and if v ≠ u, then v =

case (inj_{i} r′, x_{1}.t′_{1}, x_{2}.t′_{2}) with (r, t_{1}, t_{2}) → (r′, t′_{1}, t′_{2}) and v ↦_{β} t′_{i}[r′/x_{i}] ←^{∗} u. t = out (in r). In this case, u = r and if v ≠ u, then v = out (in r′) with r → r′

and v ↦_{β} r′ ← u.

⊓ ⊔

Lemma 7.6 (Weak Standardization). If t ↦_{β} u and E[t] → v, then either v = E[u] or v = E′[t′] for some E′[ ], t′ such that (E[ ], t) → (E′[ ], t′) and there exists u′ such that t′ ↦_{β} u′ and E[u] →^{∗} E′[u′].

Proof. Let E[t] → v with v ≠ E[u]. Since t ↦_{β} u, t is an elimination and by Prop. 7.1, v = E′[t′] where (E[ ], t) → (E′[ ], t′). The case E[ ] → E′[ ] with t = t′ is trivial. Otherwise, we have t → t′ with E′[ ] = E[ ] and we conclude by Prop. 7.5. ⊓ ⊔

It follows that strongly normalizing neutral terms have the p.r.p..

Lemma 7.7 (Principal Reduct Property). Let t ∈ N ∩ SN. If there is u such that t →_{H} u, then it is a p.r. of t, otherwise every u ∈ (t)_{→} is a p.r. of t.

Proof. Let t ∈ N ∩ SN. If t ∈ HNF, since HNF ∩ N is stable by reduction by Prop. 7.4, t never reduces to a non-neutral term. It follows that t ⊑_{SN} u for all u ∈ (t)_{→}. Otherwise, t →_{H} u and by induction on t ∈ SN, we show that u is the p.r. of t. If t →^{∗} v ∉ N, since t ∈ N, there is t′ such that t → t′ →^{∗} v. By Lem. 7.6, if t′ ≠ u, there is u′ such that t′ →_{H} u′ ←^{∗} u. Therefore, t′ ∈ N ∩ SN and by induction hypothesis t′ ⊑_{SN} u′, hence u →^{∗} u′ →^{∗} v. ⊓ ⊔

Using Cor. 4.12, we have thus proved:

Theorem 7.8. If C ⊆ CR then ⋃ C ∈ CR.

As in Sec. 5, we get stability of reducibility candidates by weak head expansion.

Lemma 7.9 (Weak Head Expansion and Reducibility Candidates). Let C ∈ CR. If E[s] ∈ C, t ↦_{β} s and t ∈ SN, then E[t] ∈ C.

Proof. We obtain easily that E[t] ∈ SN, using Lem. 7.6 and an induction on (E[ ], t) ∈ SN × SN. It suffices to show that (E[t])_{→} ⊆ SN. Given v ∈ (t)_{→}, if v ≠ E[s], then by Prop. 7.6, v = E′[t′] with (E[ ], t) → (E′[ ], t′) and there is s′ such that t′ ↦_{β} s′ and E[s] →^{∗} E′[s′]. Since E′[s′] ∈ SN, by induction hypothesis E′[t′] ∈ SN.

Now, by Lem. 4.7, E[t] ∈ \overline{E[s]} iff E[t] ⊑_{SN} E[s]. But this follows from Lem. 7.7, and we get E[t] ∈ \overline{E[s]} ⊆ C. ⊓ ⊔

Unlike reducibility candidates, saturated sets are modified. They use elimination contexts in an essential way. The new clauses for SAT are the following: (SAT 1) HNF ∩ SN ∩ N ⊆ S. (SAT 2) If s ∈ S, t →_{H} s and t ∈ SN then t ∈ S. As in Def. 5.6, we denote by SAT_{→} the collection of saturated sets that are stable by reduction (axiom (SAT 0)).

Non-emptiness of SAT follows from Lem. 7.9. The clauses given for SAT are not common. They are usually replaced by: (SAT 1′) If E[x] ∈ SN then E[x] ∈ S. (SAT 2′) If E[s] ∈ S, t ↦_{β} s and t ∈ SN then E[t] ∈ S. First, according to Lem. 7.9, (SAT 2′) is equivalent to (SAT 2). Second, for the strong normalization proof, (SAT 1′) is sufficient. But for the correspondence with Girard sets we use (SAT 1). The following suggests that (SAT 1′) would have been sufficient if CR and SAT_{→} have consists of well typed terms only.

Proposition 7.10. Well typed terms in N are the terms of the form E[t] where either t ∈ X or t ∉ TNF.

Theorem 7.11. SAT_{→} = CR.

Proof. We begin by showing that CR ⊆ SAT_{→}. Let C ∈ CR. (SAT 0) follows from (CR0). For (SAT 1), we can reason by induction on →, since by Prop. 7.4, HNF ∩ N ∩ SN is stable by reduction. Finally, the satisfaction (SAT 2) directly follows from Lem. 7.9.

Conversely, we show that SAT_{→} ⊆ CR. Let S ∈ SAT_{→}. As above, (CR0) follows from (SAT 0). For (CR1), we have to show that for every neutral term v such that (v)_{→} ⊆ S, then v ∈ S. First, v ∈ SN since (v)_{→} ⊆ S ⊆ SN. Thus, we conclude by (SAT 1) if v ∈ HNF. Otherwise, v = E[t] with t ↦_{β} s and E[s] ∈ S. Thus v ∈ S by (SAT 2). ⊓ ⊔

8 Conclusion and Related Works

Related Works. There are interesting alternatives approaches, which may not rely on stability by union. Using bi-orthogonality (see [7]), Melliès and Vouillon present a semantic of types that is not stable by union, and instead relies on a closer adequation between the interpretations and the typing rules [22].

Without unions and existentials, bi-orthogonals work well for strong normalization, especially for classical logic [20]. With non-ambiguous left-linear calculus, it is not unreasonable to expect that they can deal with existentials and union types, but the proof would rely on non-trivial properties of the calculus.

Concluding Remarks. We have shown that, with some well-behaved calculi, Girard’s reducibility candidates are stable by union. This was commonly believed to be false. Moreover, and maybe more important, we have shown that their definition hide a very simple structure, namely that candidates are exactly the non empty subsets of SN that are downward-closed w.r.t. the weak observational preorder ⊑_{SN}.

This shed new light on the semantics of strong normalization. In particular, we hope that this can lead to precise comparisons of bi-orthogonal and candidates. A related question is to know when the soundness of elimination rules of union and existentials types can be proved without stability by union of some type interpretation.

Acknowledgments. The author thanks Frédéric Blanqui and Claude Kirchner for useful advices, support and comments, and Marco Gaboardi for a plenty of interesting discussions. Antoine Reilles suggested interesting improvements in the presentation, and the anonymous referees made interesting insightful comments.

References

[1] A. Abel. Termination Checking with Types. RAIRO – Theoretical Informatics and Applications, 38(4):277–319, 2004. Special Issue (FICS’03). 4, 10, 13

[2] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993. 9

[3] F. Barbanera, M. Dezani-Ciancaglini, and U. de’Liguoro. Intersection and Union Types: Syntax and Semantics. Information and Computation, 119:202–230, 1995. 1, 3

[4] H. Barendregt. Lambda Calculi with Types. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992. 2, 3

[5] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-Data-Types Systems. Theoretical Computer Science, 271, 2002. 2

[6] F. Blanqui and C. Riba. Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. In LPAR’06, LNCS, 2006. 1, 4

[7] V. Danos and J.-L. Krivine. Disjunctive Tautologies as Synchronisation Schemes. In CSL’00, volume 1862 of LNCS, pages 292–301, 2000. 10, 14

[8] M. Dezani-Ciancaglini, U. de’ Liguoro, and P. Piperno. A Filter Model for Concurrent Lambda-Calculus. Siam Journal on Computing, 27(5):1376–1419, 1998. 1

[9] M. Dezani-Ciancaglini, J. Tiuryn, and P. Urzyczyn. Discrimination by Parallel Observers. In LICS’97, 1997. 1

[10] M. Felleisen and R. Hieb. The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science, 103(2):235–271, 1992. 4

[11] A. Frisch, G. Castagna, and V. Benzaken. Semantic Subtyping. In LICS’02, 2002. 1

[12] J.H. Gallier. On Girard’s ”Candidats de Reducibilité”. In P. Odifredi, editor, Logic and Computer Science. Academic Press, 1989. 2, 5, 10

[13] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989. 2, 4, 5

[14] H. Hosoya, J. Vouillon, and B. Pierce. Regular Expression Types for XML. In ICFP’00, 2000. 1 [15] T. Jensen. Disjunctive Strictness Analysis. In LICS’92, 1992. 1

[16] T. Jim and A. R. Meyer. Full Abstraction and the Context Lemma. Siam Journal on Computing, 25(3):663–696, 1996. 2, 7

[17] D. MacQueen, G. Plotkin, and R. Sethi. An Ideal Model for Recursive Polymorphic Types. Information and Control, 71(1-2):95–130, 1986. 1, 3

[18] R. Milner. Fully Abstract Models of Typed λ-Calculi. Theoretical Computer Science, 4:1–22, 1977. 7

[19] J.-B. Nation. Notes on Lattice Theory. Available at http://www.math.hawaii.

    edu/^{∼}jb/books.html. 5

[20] M. Parigot. Proofs of Strong Normalization for Second Order Classical Natural Deduction. Journal of Symbolic Logic, 62(4):1461–1479, 1997. 14

[21] Z. Spławski and P. Urzyczyn. Type Fixpoints: Iteration vs. Recursion. In ICFP’99, pages 102–113. ACM, 1999. 2, 10, 11

[22] J. Vouillon and P.-A. Melliès. Semantic Types: A Fresh Look at the Ideal Model for Types. In POPL’04. ACM, 2004. 14

[23] B. Werner. Une Théorie des Contructions Inductives. PhD thesis, Université Paris 7, 1994. 2, 10