Strong Normalization as Safe Interaction

Colin Riba

INPL & LORIA^{∗}, Nancy, France

E-mail: riba@loria.fr

Abstract

When enriching the λ-calculus with rewriting, union types may be needed to type all strongly normalizing terms. However, with rewriting, the elimination rule (∨ E) of union types may also allow to type non normalizing terms (in which case we say that (∨ E) is unsafe). This occurs in particular with non-determinism, but also with some confluent systems. It appears that studying the safety of (∨ E) amounts to the characterization, in a term, of safe interactions between some of its subterms.

In this paper, we study the safety of (∨ E) for an extension of the λ-calculus with simple rewrite rules. We prove that the union and intersection type discipline without (∨ E) is complete w.r.t. strong normalization. This allows to show that (∨ E) is safe if and only if an interpretation of types based on biorthogonals is sound for it. We also discuss two sufficient conditions for the safety of (∨ E), and study an alternative biorthogonality relation, based on the observation of the least reducibility candidate.

1. Introduction

Strong normalization is an important property of proof systems such as natural deduction. Proofs of strong normalization based on realizability indicate that a crucial point is to understand how λ-terms (i.e. proof-trees) can interact with each other while preserving strong normalization.

From a different perspective, strong normalization is related to must properties of full β-reduction, that hold for a term when they hold for all of its reducts (see [8] for a discussion and references on a notion of must convergence). Strong normalization is the minimal must property of full βreduction in the sense that strongly normalizing terms satisfy all must properties of full β-reduction. This suggests to study the interaction properties for strong normalization of the λ-calculus extended with simple but possibly nondeterministic rewrite rules. A pathological case is the demonic non-deterministic operator +, defined such that the term t_{1} + t_{2} reduces either to t_{1} or to t_{2}.

Our starting point is the following observation. When enriching the λ-calculus with such rewrite rules, intersection types are not always sufficient to characterize strong normalization. Union types may be needed in order to type function symbols defined by rewrite rules having different interaction properties w.r.t. strong normalization. But it is possible that the rule (∨ E) of elimination of union allows to type non normalizing terms (in which case we say that (∨ E) is unsafe). This happens with demonic non-determinism, but also with some confluent systems, whereas (∨ E) is harmless with some non-confluent ones.

It has to be noted that (∨ E) breaks the subject reduction property, even for the pure λ-calculus [2]. In our case, the type system is essentially a syntactic approximation of interaction properties of terms. It is therefore desirable that it gives as much information as possible, even if the approximation is too rough to be preserved by reduction. Hence, it is interesting to understand what kind of properties are given by (∨ E), and what does its safety mean. A similar view is also taken in [4], where subject reduction fails because of existential types.

The properties we are interested in can be characterized by sets of terms satisfying some closure conditions [19, 18]. Biorthogonality can give interesting closure operators, where a closed set is described by a set of contexts with which all terms of the set interact safely [14, 6]. This gives very informative interpretations of (∨ E), as shown in [19, 18]. However, in these works, biorthogonals are built on the observation of reduction without error, possibly involving infinite computations. Moreover, in its full version, (∨ E) behaves well with call-by-value evaluation [19], whereas must properties are more naturally manipulated via (weak) head reductions, that correspond to callby-name evaluation. Regarding strong normalization, it was therefore unclear how to handle the biorthogonal interpretation of the full rule (∨ E).

In this paper, we study a biorthogonal type interpretation which we show to be sound for (∨ E) if and only if (∨ E) is safe, that is, if and only if it can be added to the type system while preserving strong normalization. This means that regarding strong normalization, biorthogonals provide the best possible interpretation of (∨ E). This also gives a computational interpretation to biorthogonality, that were introduced in realizability to deal with classical logic [14].

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

The key point is that the membership of a term to a biorthogonal can be tested by observing the strong normalization of this term plugged in suitable contexts. Since intersection and union types (without (∨ E)) are sound and complete w.r.t. strong normalization, we can extract all the information we need from the observation of strong normalization.

It appears that the safety of (∨ E) is equivalent to a safe interaction principle wich says that if each one-step reduct of an elimination term can be safely duplicated in a captureavoiding context, then this term can be safely duplicated in that context. Hence, its different reducts have to interact safely with each other in that context. Intuitively, such systems have a kind of uniform computational behavior.

Then we consider sufficient conditions for the safety of (∨ E). Besides Girard’s reducibility candidates (whose stability by union is studied in [16]), we consider the interpretation of types arising as the closure by union of a biorthogonality operator. In this case, types are interpreted by nonempty sets upward-closed w.r.t. the observational preorder issued from the orthogonality relation. We show that these sets are reducibility candidates if and only if each elimination term is greater w.r.t. that preorder than one of its immediate reducts.

A natural question is whether (∨ E) is safe with rewrite systems for which intersection types are sufficient for the completeness of type assignment w.r.t. strong normalization (i.e. when unions are not needed). We show that this is not the case. However, it is interesting to note that when reducibility candidates are stable by union, intersection types are sufficient to type strongly normalizing terms.

We conclude by a discussion on an alternative orthogonality relation built on the observation of the least reducibility candidate. It amounts to observing strongly normalizing reduction to an error term. This induces a biorthogonal type interpretation having a better adequacy with the type system and would allow for a more natural subtyping relation. However, for the soundness of (∨ E), it is not clear whether these biorthogonals are equivalent to those issued from strong normalization.

Related Work. Intersection and union types are extensively studied in [7, 8, 9] as the logical intermediate to build fully abstract filter models of non-deterministic λ-calculi. These works consider must normalization of (weak) head reduction. Here, must normalization of a reduction relation means convergence of any reduction with this relation.

This makes sense in non-deterministic calculi even if the considered relation is not the full reduction. In [7, 8] it is remarked that (∨ E) makes the soundness of the type system to fail w.r.t. the considered property. Because they are in a must setting, we think that problems caused in their cases by (∨ E) are in essence similar to ours.

Recent applications of union types are the XML processing languages XDuce [12] and ℂDuce [10].

Concerning strong normalization, existential types are extensively used in the type system of [4]. These types are interpreted using infinite unions, and this motivated our study of stability by union of Girard’s candidates.

Our integration of rewriting with intersection types is inspired from [5]. In comparison to this work, we use simpler rewrite rules and function symbols with a fixed arity. Thus, we get completeness of type assignement w.r.t. strong normalization.

Our presentation of biorthogonals is inspired from [6], see also [14, 19, 15]. For properties on λ-calculus and (union and intersection) types, we refer to [13, 11, 3, 7, 2].

Outline. We present the calculus in Sec. 2, with a discussion on (∨ E) and examples of its unsafety. Section. 3 is devoted to the soundness and completeness of the type systems (without (∨ E)). Our main result on the biorthogonal interpretation of (∨ E) is presented in Sec. 4. We discuss sufficient conditions for safe interaction in Sec. 5. Finally, in Sec. 6, we briefly discuss the orthogonality relation built on the observation of the least reducibility candidate.

2. Preliminaries

2.1. Types and Terms

Let X be a countable set of variables. We write Λ(S) for the set of λ-terms with constants in a set S of symbols of fixed arity:

t, u ∈ Λ(S) ::= x ∈ X | t u | λx.t | f(t_{1}, …, t_{n})

where f ∈ S is a symbol of arity n. We write Λ for Λ(S) when S is clear from the context. As usual, terms are considered modulo α-conversion. Let FV(t) be the set of variables occurring free in t. By t⃗ we mean a sequence of terms of length |t⃗|; we use the same notation for types, etc. We write R for any set of rewrite rules of the form

f(x⃗) ↦ r

where f ∈ S, x⃗ is made of distinct variables, r ∈ Λ and FV(r) ⊆ x⃗. We write f(x⃗) ↦_{R} r for f(x⃗) ↦ r ∈ R. Let R(f) such that r ∈ R(f) iff f(x⃗) ↦_{R} r and S = F ⊎ C where f ∈ C if R(f) = ∅ and f ∈ F otherwise. The capture-avoiding substitution of u for x in t is denoted by

\overline{T ≤ T} \frac{U_{2} ≤ U_{1} T_{1} ≤ T_{2}}{U_{1} ⇒ T_{1} ≤ U_{2} ⇒ T_{2}} \frac{T ≤ U U ≤ V}{T ≤ V}

\overline{(T ⇒ U_{1}) ∧ (T ⇒ U_{2}) ≤ T ⇒ (U_{1} ∧ U_{2})}

\frac{T_{1}, T_{2} ≤ U}{T_{1} ∨ T_{2} ≤ U} \overline{T_{1}, T_{2} ≤ T_{1} ∨ T_{2}}

\overline{T_{1} ∧ T_{2} ≤ T_{1}, T_{2}} \frac{T ≤ U_{1}, U_{2}}{T ≤ U_{1} ∧ U_{2}}

Figure 1. Subtyping

t[u/x]. We generalize substitutions to functions σ : X → Λ with tσ =_{def} t[σ(x)/x | x ∈ dom(σ)]. Define → to be the smallest relation on Λ stable by context and substitution which contains ↦_{R} and (λx.t)u ↦_{β} t[u/x].

We assume that → is finitely branching, hence that R(f) is finite for each f ∈ F. Define (t)_{→} =_{def} {u | t → u} and let →^{∗} be 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 (t ∈ SN) iff every reduction sequence issued from t is finite. Note that t ∈ SN iff either t is not reducible or all its reducts are in SN. Hence SN is the smallest set such that for all t,

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

Types are the following, where o is the base type:

T, U ∈ T ::= o | T ⇒ U | T ∧ U | T ∨ U .

Subtyping rules are in Fig. 1. They axiomatize the fact that (T , ≤, ∧, ∨) is a preorder with all finite non-empty g.l.b.’s and l.u.b.’s. Note that contrary to [7, 8], (T , ≤, ∧, ∨) is not distributive.

Typing contexts are functions Γ : X → T . We write (x : T) ∈ Γ when Γ(x) = T and x ∈ Γ when x ∈ dom(Γ). Given Γ_{0} and Γ_{1}, we let Γ_{0} ∧ Γ_{1} be the context such that

Γ_{0} ∧ Γ_{1}(x) =_{def} \{ \begin{matrix}Γ_{0}(x) ∧ Γ_{1}(x) & if x ∈ Γ_{0} ∩ Γ_{1} , \\ Γ_{i}(x) & if x ∈ Γ_{i} \ Γ_{1−i} . \end{matrix}

Typing rules are given in Fig. 2. We write Γ ⊢_{∧} t : T for typing judgments in the system without ∨ and T_{∧} for the corresponding set of types. Note that for ty ∈ {∧, ∧∨}, if Γ ⊢_{ty} t : T, then for all Γ′ we have Γ ∧ Γ′ ⊢_{ty} t : T and moreover Γ ∧ Γ′ ⊢_{∧∨} t : T ∨ T′ for all T′ ∈ T .

The rule (Fun ), which is not usual, is inspired from [5]. Let us explain it with an example. Consider a symbol f ∈ S defined with rewrite rules f(x⃗_{i}) ↦_{R} r_{i} for all i ∈ {1, …, n} and some n ≥ 0. Assume that Γ ⊢_{∧∨} t⃗: T⃗ and that for all i ∈ {1, …, n}, there is a type U_{i} such that Γ, x⃗_{i} : T⃗ ⊢_{∧∨} r_{i} : U_{i}. Then, using (Sub ) and (Fun ) we can conclude that Γ ⊢_{∧∨} f(t⃗) : ⋁_{1≤i≤n} U_{i}. Note that if f ∈ C, then for all type U we have Γ ⊢_{∧∨} f(t⃗) : U.

2.2. The Elimination Rule of Union Types (∨ E)

In this section, we discuss the rule (∨ E). In the process, we may anticipate on some results presented later in the paper. The elimination rule of union is the following:

(∨ E) \frac{\begin{aligned}& Γ, x : T_{1} ⊢ c : C \\ Γ ⊢ t : T_{1} ∨ T_{2} & Γ, x : T_{2} ⊢ c : C \end{aligned}}{Γ ⊢ c[t/x] : C}

We denote by ⊢_{∧⊻} the type system ⊢_{∧∨} in which we added the rule (∨ E).

The rule can be read as follows: if t : T_{1} ∨ T_{2} and for all i ∈ {1, 2} (v : T_{i} ⇒ c[v/x] : C) then c[t/x] : C. Intuitively, this can be problematic if ∨ is not a union, i.e. if there is t such that t : T_{1} ∨ T_{2} but neither t : T_{1} nor t : T_{2}. Such a situation can occur with non-determinism. Indeed, consider the rewrite system:

t_{1} + t_{2} ↦_{R} t_{1} t_{1} + t_{2} ↦_{R} t_{2} .

Assume that t =_{def} t_{1} + t_{2}, where t_{1} can be given the type T_{1} but not T_{2}, and vice-versa for t_{2}. Then, t is not in the union of T_{1} and T_{2}, since it is neither in T_{1} nor in T_{2}.

Example 2.1. We now give an example of unsoundness of (∨ E). Let t_{1} =_{def} λz.zyδ and t_{2} =_{def} λz.δ where δ =_{def} λx.xx. It is clear that t_{1}t_{1} and t_{2}t_{2} are strongly normalizing. However, t_{1}t_{2} →^{∗} δδ ∉ SN^{1}.

By completeness of type assignment in ⊢_{∧} (see [13, 11]), for i = 1, 2 there are T_{i}, U_{i}, V_{i} such that y : V_{i} ⊢_{∧} t_{i} : T_{i} and y : V_{i}, x : T_{i} ⊢_{∧} xx : U_{i}. Hence we have:

(∨ E) \frac{\begin{matrix}y : V_{1} ∧ V_{2} ⊢_{∧∨} & t_{1} + t_{2} : & T_{1} ∨ T_{2} \\ y : V_{1} ∧ V_{2}, x : T_{1} ⊢_{∧∨} & xx : & U_{1} ∨ U_{2} \\ y : V_{1} ∧ V_{2}, x : T_{2} ⊢_{∧∨} & xx : & U_{1} ∨ U_{2} \end{matrix}}{y : V_{1} ∧ V_{2} ⊢_{∧⊻} (t_{1} + t_{2})(t_{1} + t_{2}) : U_{1} ∨ U_{2}}

but (t_{1} + t_{2})(t_{1} + t_{2}) →^{∗} t_{1}t_{2} →^{∗} δδ ∉ SN.

Example 2.2. This can also occur with confluent systems, such as the following one:

f ↦_{R} λxy.g(xaδ) f ↦_{R} λxy.g(yy) g(x) ↦_{R} a .

Let u_{1} =_{def} λxy.g(xaδ) and u_{2} =_{def} λxy.g(yy). Since we have u_{1}u_{1} ∈ SN and u_{2}u_{2} ∈ SN, by Completeness

1We thank Philippe de Groote for this example.

(Ax) \overline{Γ, x : T ⊢_{∧∨} x : T}  (Fun ) \frac{Γ ⊢_{∧∨} t⃗: T⃗  ∀f(x⃗) ↦_{R} r, Γ, x⃗ : T⃗ ⊢_{∧∨} r : U}{Γ ⊢_{∧∨} f(t⃗) : U}

(⇒ I) \frac{Γ, x : U ⊢_{∧∨} t : T}{Γ ⊢_{∧∨} λx.t : U ⇒ T}  (⇒ E) \frac{Γ ⊢_{∧∨} t : U ⇒ T  Γ ⊢_{∧∨} u : U}{Γ ⊢_{∧∨} tu : T}

(∧ I) \frac{Γ ⊢_{∧∨} t : T_{1}  Γ ⊢_{∧∨} t : T_{2}}{Γ ⊢_{∧∨} t : T_{1} ∧ T_{2}}  (Sub ) \frac{Γ ⊢_{∧∨} t : T  T ≤ U}{Γ ⊢_{∧∨} t : U}

Figure 2. Typing

(Thm. 3.11) and Interpolation (Prop. 3.8), there are T_{1}, T_{2} and U such that:

(∨ E) \frac{\begin{aligned}& x : T_{1} ⊢_{∧∨} & xx : U \\ ⊢_{∧∨} f : T_{1} ∨ T_{2} & x : T_{2} ⊢_{∧∨} & xx : U \end{aligned}}{⊢_{∧⊻} ff : U}

but ff →^{∗} u_{1}u_{2} →^{∗} λy.g(g(δδ)) ∉ SN.

The examples above suggest that (∨ E) asks for call-by-value evaluation. Intuitively, before performing the substitution c[t/x], one should normalize t in order to determine if it belongs to T_{1} or to T_{2}.

3. Soundness and Completeness

In this section, we prove soundness and completeness of typing in ⊢_{∧∨} (i.e. without (∨ E)) w.r.t. strong normalization. This is the occasion to introduce basic notions on reducibility, that are used for biorthogonality-based reducibility in Sec. 4.3. We also prove a few consequences of completeness, which are important for our analysis of (∨ E).

3.1. Reducibility

We introduce well-known basic tools for reducibility. This presentation is consistent with [16], where more details can be found.

As advocated in [19, 18], it is convenient to see type interpretations as closure operators. 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.

Definition 3.1 (Neutral terms). Terms which are not 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, if ∀u(t → u ⇒ u ∈ HN) then t ∈ HN.

Note that HN ⊆ SN.

Definition 3.2 (Reducibility Candidates). The set CR of reducibility candidates 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 property (CR1) is also called the neutral term property. It is easy to define a function \overline{·} : P(SN) → P(SN) such that \overline{A} is the smallest reducibility candidate containing A. This is a closure operator on (P(SN), ⊆).

Proposition 3.3 (Candidates Lattice). The partial order (CR, ⊆) is a complete lattice with least element HN, greatest element SN and whose g.l.b.’s are given by ⋂.

We turn to the interpretation of arrow types.

Proposition 3.4 (Arrow Type Constructor). The arrow type constructor ⇒: P(Λ) × P(Λ) → P(Λ), defined as

A ⇒ B =_{def} {t | ∀u(u ∈ A ⇒ tu ∈ B)}

maps A, B ∈ CR to a reducibility candidate.

We interpret T ∈ T by ⟦T ⟧ ∈ CR as follows:

⟦o⟧ =_{def} SN
⟦T ⇒ U⟧ =_{def} ⟦T ⟧ ⇒ ⟦U⟧
⟦T ∧ U⟧ =_{def} ⟦T ⟧ ∩ ⟦U⟧
⟦T ∨ U⟧ =_{def} \overline{⟦T ⟧ ∪ ⟦U⟧} .

There are many choices possible for ⟦o⟧. In our case, another interesting one is ⟦o⟧ = HN (see Sec. 6 and Theorems 3.12 and 6.1).

3.2. Soundness

We show that Γ ⊢_{∧∨} t : T implies t ∈ SN.

Proposition 3.5 (Soundness of Subtyping). If T ≤ U then ⟦T ⟧ ⊆ ⟦U⟧.

Given a substitution σ : X → Λ and a context Γ, we write σ ⊧_{⟦ · ⟧} Γ when σ(x) ∈ ⟦T ⟧ for all (x : T) ∈ Γ. Recall that the rule (∨ E) is not present in ⊢_{∧∨}.

Theorem 3.6 (Soundness of Typing). If Γ ⊢_{∧∨} t : T and σ ⊧_{⟦ · ⟧} Γ then tσ ∈ ⟦T ⟧.

Proof. By induction on Γ ⊢_{∧∨} t : T, using Prop. 3.5 for (Sub ). We detail the case of (Fun ).

Let σ ⊧_{⟦ · ⟧} Γ and t⃗′ =_{def} t⃗σ. By induction hypothesis, t⃗′ ∈ ⟦T⃗⟧. We have to show that t′ =_{def} f(t⃗′) ∈ ⟦T ⟧. Since this term is neutral, it suffices to show that (t′)_{→} ⊆ ⟦T ⟧. We reason by induction on t⃗′ ∈ SN. Let v ∈ (t′)_{→}. If v = f(u⃗) with t⃗′ → u⃗, then by (CR0), u⃗ ∈ ⟦T⃗⟧ and we conclude by induction hypothesis on u⃗. Otherwise, there is a rule f(x⃗) ↦_{R} r such that v = r[t⃗′/x⃗] and since t⃗′ ∈ ⟦T⃗⟧, by induction hypothesis on Γ, x⃗ : T⃗ ⊢_{∧∨} r : T we have r[t⃗′/x⃗] ∈ ⟦T ⟧.

Corollary 3.7. If Γ ⊢_{∧∨} t : T then t ∈ SN.

3.3. Completeness

The main result of this section is the completeness of intersection and union types with respect to strong normalization: if t ∈ SN, then there are Γ and T such that Γ ⊢_{∧∨} t : T. The result is proved in [13, 11] for the pure λ-calculus with intersection types.

We begin by two important properties, that are characteristic of intersection types. They are the key properties for completeness.

Proposition 3.8 (Interpolation). If Γ ⊢_{∧∨} t[u/x] : T and Γ ⊢_{∧∨} u : U with x ∉ Γ, then there is a type V such that Γ, x : V ⊢_{∧∨} t : T and Γ ⊢_{∧∨} u : V.

Proof. By induction on t.

Lemma 3.9 (Weak Head Expansion).

(i) Assume that Γ ⊢_{∧∨} u : U and Γ ⊢_{∧∨} t[u/x]v⃗ : T. Then Γ ⊢_{∧∨} (λx.t)uv⃗ : T.

(ii) For all f ∈ F, if Γ ⊢_{∧∨} t⃗: T⃗ and Γ ⊢_{∧∨} r[t⃗/x⃗]v⃗ : T for all f(x⃗) ↦_{R} r, then Γ ⊢_{∧∨} f(t⃗)v⃗ : T.

Proof. The two points are similar: the property is proved by induction on |v⃗|, and the base case is obtained using Prop. 3.8.

For the proof of completeness itself, we use an induction on a preorder that combine reduction and subterm and which is well-founded on SN.

Definition 3.10. We let ≺ be the smallest preorder such that t ≺ u if either u → t or t is a strict subterm of u.

Theorem 3.11 (Completeness). If t ∈ SN, then there are Γ and T such that Γ ⊢_{∧∨} t : T.

Proof. The proof is by induction on ≺ and uses Lem. 3.9. We only detail the case of t = f(t⃗)v⃗ with f ∈ F.

First, note that t⃗ ≺ t. For all f(x⃗) ↦_{R} r, we have r[t⃗/x⃗]v⃗ ≺ t and by induction hypothesis there are Γ_{r}, T⃗_{r} and V_{r} such that Γ_{r} ⊢_{∧∨} t⃗ : T⃗_{r} and Γ_{r} ⊢_{∧∨} r[t⃗/x⃗]v⃗ : V_{r}. Now, taking Γ =_{def} ⋀_{r∈R(f)} Γ_{r}, T⃗ =_{def} ⋀_{r∈R(f)} T⃗_{r} and V =_{def} ⋁_{r∈R(f)} V_{r}, we have Γ ⊢_{∧∨} t⃗ : T⃗ and for all f(x⃗) ↦_{R} r, Γ ⊢_{∧∨} r[t⃗/x⃗]v⃗ : V. We conclude that Γ ⊢_{∧∨} f(t⃗)v⃗ : V thanks to Lem. 3.9.(ii).

Note that without further assumptions on R, union types are required for Thm. 3.11. The next result says that it would have been complete to interpret o by HN, the least element of CR.

Theorem 3.12 (HN -Completeness). If t ∈ HN then for all T ∈ T there is Γ such that Γ ⊢_{∧∨} t : T.

Proof. Similar to Thm. 3.11. We reason by induction on ≺, using Thm. 3.11 and Lem. 3.9.

3.4. Two Interesting Consequences

We now prove two consequences of soundness and completeness of ⊢_{∧∨}. They play an important role in our analysis of (∨ E). The first one says that β-reduction leads to uniform computations.

Theorem 3.13. If (λx.t)u ∈ SN and v[t[u/x]/y] ∈ SN then v[(λx.t)u/y] ∈ SN.

Proof. Since (λx.t)u ∈ SN, we have also u ∈ SN and t[u/x] ∈ SN. It follows from Thm. 3.11 that there are Γ′, T and U such that Γ′ ⊢_{∧∨} u : U and Γ′ ⊢_{∧∨} t[u/x] : T.

On the other hand, still thanks to Thm. 3.11, there are Γ′′, V such that Γ′′ ⊢_{∧∨} v[t[u/x]/y] : V. Let Γ =_{def} Γ′ ∧ Γ′′. Since Γ ⊢_{∧∨} t[u/x] : T, we can use Lem. 3.9.(i) to obtain Γ ⊢_{∧∨} (λy.v)(t[u/x]) : V. It follows that there is T′ such that Γ ⊢_{∧∨} λy.v : T′ ⇒ V and Γ ⊢_{∧∨} t[u/x] : T′.

Furthermore, since Γ ⊢_{∧∨} u : U, using Lem. 3.9.(i) we have Γ ⊢_{∧∨} (λx.t)u : T′. Then, Γ ⊢_{∧∨} (λy.v)((λx.t)u) : V, and it follows that v[(λx.t)u/y] ∈ SN by Cor. 3.7.

The analogous of this property for ↦_{R} will be shown to be equivalent to the safety of (∨ E) in Sec. 4.

Note that the capture-avoiding substitution is essential here. Indeed, the property fails if we replace v by a context C[ ] able to capture variables. For example (see [17]), with C[ ] =_{def} (λy.[ ])δ, and (λx.t)u =_{def} (λx.z)(yy), we have C[t[u/x]] = (λy.z)δ which is in SN, but C[(λx.t)u] = (λy.(λx.z)(yy))δ → (λx.z)(δδ) ∉ SN.

Now, we show that hereditary neutral terms are really neutral, in the sense that they can be safely substituted in any strongly normalizing term.

Theorem 3.14. If t ∈ HN and v ∈ SN then v[t/x] ∈ SN.

Proof. First, assume that x ∉ FV(t). Since v ∈ SN, by Thm. 3.11, there are Γ′′, T and V such that Γ′′, x : T ⊢_{∧∨} v : V. Moreover, since t ∈ HN, by Thm. 3.12, there is Γ′ such that Γ′ ⊢_{∧∨} t : T. Hence, taking Γ =_{def} Γ′ ∧ Γ′′ we have Γ, x : T ⊢_{∧∨} v : V and Γ ⊢_{∧∨} t : T. It follows that Γ ⊢_{∧∨} (λx.v)t : V, hence v[t/x] ∈ SN by Cor. 3.7.

Now, assume that x ∈ FV(t). Let y ∉ FV(t, v) and t′ =_{def} t[y/x]. Then we have t′ ∈ HN hence v[t′/x] ∈ SN and v[t/x] = (v[t′/x])[x/y] ∈ SN.

4. Safe Interaction

We now address the problem of the safety of the elimination rule of union:

(∨ E) \frac{\begin{aligned}& Γ, x : T_{1} ⊢ c : C \\ Γ ⊢ t : T_{1} ∨ T_{2} & Γ, x : T_{2} ⊢ c : C \end{aligned}}{Γ ⊢ c[t/x] : C}

Recall that ⊢_{∧⊻} is the type system ⊢_{∧∨} in which we added the rule (∨ E). Since we have proved in Sec. 3.2 that typability in ⊢_{∧∨} implies strong normalization, proving the safety of (∨ E) reduces to proving strong normalization of terms typable in ⊢_{∧⊻}.

In this section, we use biorthogonality to define an interpretation ⦇ · ⦈ : T → CR such that the following points are equivalent (see Thm. 4.9):

(∨ E) is safe: If Γ ⊢_{∧⊻} t : T then t ∈ SN.

(Ip) If f ∈ F, f(t⃗) ∈ SN and v[r[t⃗/x⃗]/y] ∈ SN for all f(x⃗) ↦_{R} r, then v[f(t⃗)/y] ∈ SN.

⦇ · ⦈ is sound: If Γ ⊢_{∧⊻} t : T and σ ⊧_{⦇ · ⦈} Γ then tσ ∈ ⦇T ⦈.

This means that biorthogonality gives the best possible interpretation of (∨ E) w.r.t. strong normalization: if typability in ⊢_{∧⊻} implies strong normalization, then the interpretation ⦇ · ⦈ is sound. This also gives a purely computational interpretation of biorthogonality.

4.1. The Interaction Principle

The interaction principle (Ip) says that if each onestep reduct of a neutral term can be safely duplicated in a capture-avoiding context, then this term can be safely duplicated in that context. Hence, its different reducts have to interact safely with each other in that context.

We now show that the safety of (∨ E) implies (Ip).

Proposition 4.1. For all n ≥ 1, the rule

\frac{Γ ⊢_{∧⊻} t : ⋀_{1≤i≤n}(U_{i} ⇒ T)}{Γ ⊢_{∧⊻} λx.tx : (⋁_{1≤i≤n} U_{i}) ⇒ T} (x ∉ FV(t))

is derivable in ⊢_{∧⊻}.

Theorem 4.2. If (∨ E) is safe, then (Ip) holds.

Proof. Let f(t⃗) ∈ SN and v such that for all f(x⃗) ↦_{R} r, v[r[t⃗/x⃗]/y] ∈ SN. We reason as in Thm. 3.13, using Thm. 3.11 and Lem. 3.9: there are Γ, V and (U_{r})_{r∈R(f)} such that Γ ⊢_{∧∨} f(t⃗) : ⋁_{r∈R(f)} U_{r} and for all r ∈ f(R), Γ ⊢_{∧∨} λy.v : U_{r} ⇒ V.

By Prop. 4.1, we have Γ ⊢_{∧⊻} (λy.v)f(t⃗) : V, hence v[f(t⃗)/y] ∈ SN since (∨ E) is safe by assumption.

4.2. Orthogonality

We will show that the maximal method for the soundness of (∨ E) is given by biorthogonals. We introduce the main notions below.

Given two sets A and Π, and a relation ⊥ ⊥ ⊆ A × Π, let

∀A ⊆ A, A^{⊥ ⊥} =_{def} {π ∈ Π | ∀a (a ∈ A ⇒ a ⊥ ⊥ π)} ;
∀P ⊆ Π, P^{⊥ ⊥} =_{def} {a ∈ A | ∀π (π ∈ P ⇒ a ⊥ ⊥ π)} .

Let us discuss a few properties of ( ·)^{⊥ ⊥}. First, it is easy to see that ( ·)^{⊥ ⊥} is anti-monotonic: X ⊆ Y implies Y^{⊥ ⊥} ⊆ X^{⊥ ⊥}. It follows that X = X\begin{matrix}⊥ ⊥ \\ ⊥ ⊥ \end{matrix} iff there is Y such that X = Y^{⊥ ⊥}. Moreover, ( ·)\begin{matrix}⊥ ⊥ \\ ⊥ ⊥ \end{matrix} is a closure operator on P(A) (resp. P(Π)).

For the interpretation of (∨ E), the important point is the De Morgan laws:

\begin{aligned}X^{⊥ ⊥} ∩ Y^{⊥ ⊥} & = & (X ∪ Y)^{⊥ ⊥} , \\ X^{⊥ ⊥} ∪ Y^{⊥ ⊥} & ⊆ & (X ∩ Y)^{⊥ ⊥} . \end{aligned}

Note that in general, (X ∩ Y)^{⊥ ⊥} ⊈ X^{⊥ ⊥} ∪ Y^{⊥ ⊥}. Indeed, if x is orthogonal to every element of X ∩ Y, then there is no reason for x to be orthogonal to every element of X ∪Y.

4.3. Biorthogonal Reducibility

We now introduce a family of biorthogonals that arises from the observation of SN, the top element of CR.

For the interpretation of (∨ E), we use extended evaluation contexts E[ ] ∈ E that allow call-by-value evaluation [19]. It is useful to see them both as terms and contexts. Therefore, we let [ ] ∈ X be a distinguished variable and define E as follows:

E[ ] ∈ E ::= [ ] | E[ ] t | t E[ ] .

We let E[t] =_{def} (E[ ])[t/[ ]].

Definition 4.3. Let t ⊤ E[ ] iff E[t] ∈ SN.

Note that since E ⊈ SN, we have ∅^{⊤⊤} = ∅. It is easy to see that SN = {[ ]}^{⊤}, hence SN^{⊤⊤} = SN. Therefore, by monotonicity of ( ·)^{⊤⊤}, A ⊆ SN implies A^{⊤⊤} ⊆ SN.

Since we allow call-by-value in evaluation contexts, it needs some work to prove that ⊤-biorthogonals are reducibility candidates. The main point is to prove the neutral term property, for which we use completeness of type assignment and the axiom (Ip).

Proposition 4.4 (Neutral Term Property). Let E[ ] ∈ SN and t ∈ N. If (Ip) holds and ∀u(t → u ⇒ E[u] ∈ SN) then E[t] ∈ SN.

Proof. Since E[ ] ∈ SN, if t ∈ HN then by Thm. 3.14 we have E[t] ∈ SN.

Otherwise, t reduces to an abstraction, and since it is a neutral term, it has an head redex. Then, t is either of the form (λx.t_{1})t_{2}v⃗ and we conclude by Thm. 3.13, or of the form f(t⃗)v⃗ with f ∈ F and the result follows from (Ip).

Then, we obtain that biorthogonals of non-empty subsets of SN are reducibility candidates.

Lemma 4.5. If A ⊆ SN is not empty, then (Ip) implies A^{⊤⊤} ∈ CR.

Proof. Since A ⊆ SN, we have A^{⊤⊤} ⊆ SN. Stability by reduction is trivial. Since A ≠ ∅ we have A^{⊤} ⊆ SN, hence the neutral term property is insured by Prop. 4.4. applied using (Ip).

Hence, the set {A^{⊤⊤} | ∅ ≠ A ⊆ SN } is a subset of CR. Moreover, thanks to the idempotence of ( ·)^{⊤⊤}, it is exactly the set {A^{⊤⊤} | A ∈ CR}. Therefore, we can consistently denote it by CR^{⊤⊤}.

On the other hand, it is interesting to note that the reducibility candidates involved in the interpretation of T ∈ T_{∧} are biorthogonals. This observation seems to originate from [14], and to be the starting point of the utilization of biorthogonals in reducibility. If A ⊆ Λ and B ⊆ E let A · B =_{def} {E[[ ]a] | a ∈ A & E[ ] ∈ B}.

Proposition 4.6 (Types as Biorthogonals). For all T ∈ T_{∧}, ⟦T ⟧ = ⟦T ⟧^{⊤⊤}.

Proof. Indeed, we have

\begin{matrix}⟦o⟧ = & SN = \{[ ]\}^{⊤} \\ ⟦U ⇒ V ⟧ = & (⟦U⟧ · ⟦V ⟧^{⊤})^{⊤} \\ ⟦U ∧ V ⟧ = & (⟦U⟧^{⊤} ∪ ⟦V ⟧^{⊤})^{⊤} . \end{matrix}

4.4. Completeness of Biorthogonals

Biorthogonals are not stable by union because the De Morgan law A^{⊥ ⊥} ∪ B^{⊥ ⊥} = (A ∩ B)^{⊥ ⊥} is in general not satisfied. However, since A^{⊥ ⊥} ∩ B^{⊥ ⊥} = (A ∪ B)^{⊥ ⊥} we have

(A ∪ B)\begin{matrix}⊥ ⊥ \\ ⊥ ⊥ \end{matrix} = (A^{⊥ ⊥} ∩ B^{⊥ ⊥})^{⊥ ⊥} .

Therefore, the closure of union is quite informative: if a belongs to (A ∪ B)\begin{matrix}⊥ ⊥ \\ ⊥ ⊥ \end{matrix} then a ⊥ ⊥ π for all π ∈ A^{⊥ ⊥} ∩ B^{⊥ ⊥}. We take advantage of this fact for the interpretation of (∨ E), and from now on, the interpretation of types with biorthogonals will differ from that of Sec. 3.1. Given T ∈ T , we define ⦇T ⦈ as follows:

⦇o⦈ =_{def} {[ ]}^{⊤} (= SN)
⦇U ⇒ V ⦈ =_{def} (⦇U⦈ · ⦇V ⦈^{⊤})^{⊤}
⦇U ∧ V ⦈ =_{def} (⦇U⦈^{⊤} ∪ ⦇V ⦈^{⊤})^{⊤}
⦇U ∨ V ⦈ =_{def} (⦇U⦈^{⊤} ∩ ⦇V ⦈^{⊤})^{⊤} .

Lemma 4.7. If (Ip) then for all T ∈ T , ⦇T ⦈ ∈ CR.

Proof. By induction on T, using Lem. 4.5 for T = T_{1} ∨ T_{2}. Note that we cannot avoid the induction on T and di-

rectly use Lem. 4.5, since it requires ∅ ≠ ⦇T ⦈ ⊆ SN.

It is directly in the soundness proof that we use the possibility of call-by-value evaluation with E.

Theorem 4.8. Let Γ ⊢_{∧⊻} t : T. If (Ip) and σ ⊧_{⦇ · ⦈} Γ then tσ ∈ ⦇T ⦈.

Proof. By induction on Γ ⊢_{∧⊻} t : T. Thanks to Lem. 4.7, using (Ip), we have ⦇U⦈ ∈ CR for all U ∈ T . Then, the proof is identical to that of Thm. 3.6, except for the case of the rule (∨ E). We only detail this case:

(∨ E) \frac{\begin{aligned}& Γ, x : T_{1} ⊢_{∧⊻} c : C \\ Γ ⊢_{∧⊻} t : T_{1} ∨ T_{2} & Γ, x : T_{2} ⊢_{∧⊻} c : C \end{aligned}}{Γ ⊢_{∧⊻} c[t/x] : C}

Let σ ⊧_{⦇ · ⦈} Γ, t′ =_{def} tσ and c′ =_{def} cσ. Recall that we can assume x ∉ FV(σ). Hence, we show that c′[t′/x] ∈ ⦇C⦈. Let E[ ] ∈ ⦇C⦈^{⊤}. By induction hypothesis, for all v ∈ ⦇T_{1}⦈ ∪ ⦇T_{2}⦈ we have c′[v/x] ⊤ E[ ]. Moreover, since v ∈ SN, we have (λx.c′)v ⊤ E[ ] by Thm. 3.13. It follows that E[(λx.c′)[ ]] ∈ ⦇T_{1}⦈^{⊤} ∩ ⦇T_{2}⦈^{⊤}.

On the other hand, by induction hypothesis we have t′ ∈ (⦇T_{1}⦈^{⊤} ∩ ⦇T_{2}⦈^{⊤})^{⊤}. Therefore t′ ⊤ E[(λx.c′)[ ]], hence (λx.c′)t′ ⊤ E[ ]. We deduce that c′[t′/x] ⊤ E[ ].

Theorem 4.9 (Main Theorem). The following are equivalent:

(i) If Γ ⊢_{∧⊻} t : T then t ∈ SN.

(ii) If f ∈ F, f(t⃗) ∈ SN and v[r[t⃗/x⃗]/y] ∈ SN for all

f(x⃗) ↦_{R} r, then v[f(t⃗)/y] ∈ SN.

(iii) The interpretation ⦇ · ⦈ is sound for (∨ E).

Proof. The implication (i) ⇒ (ii) is proved in Thm. 4.2 and it follows from Thm. 4.8 that (ii) ⇒ (iii). We have (iii) ⇒ (i) since X ⊆ HN ⊆ ⦇T ⦈ ⊆ SN for all T.

4.5. Comparison with Reducibility Candidates

We have shown that the biorthogonal interpretation is sound and complete w.r.t. the safety of (∨ E). We now compare it to the impredicative interpretation of (∨ E) defined in CR. Given A, B ∈ CR, let A ∨ B be

{t | ∀C ∈ CR, ∀c ∈ (A ⇒ C) ∩ (B ⇒ C), ct ∈ C} .

In general, it is unclear whether A, B ∈ CR implies A∨B ∈ CR. Indeed, given t ∈ N, C ∈ CR and knowing that for all u ∈ (t)_{→}, cu ∈ C, it is not clear why ct ∈ C. On the other hand, a subtle modification to A ∨ B makes it much easier to handle: let A ∨_{⊤} B be

{t | ∀C ∈ CR^{⊤⊤}, ∀c ∈ (A ⇒ C) ∩ (B ⇒ C), ct ∈ C} .

The point is that in observing ct ∈ C with C ∈ CR^{⊤⊤}, in fact we observe SN since ct ∈ C holds iff for all E[ ] ∈ C^{⊤}, E[ct] ∈ SN. Thanks to soundness of completeness of ⊢_{∧∨}, we are able to extract the information we need from the observation of SN.

Lemma 4.10. For all A, B ⊆ SN,

(A^{⊤} ∩ B^{⊤})^{⊤} = A ∨_{⊤} B .

Proof. If c ∈ (A ⇒ C) ∩ (B ⇒ C) and E[ ] ∈ C^{⊤}, then E[c[ ]] ∈ A^{⊤} ∩ B^{⊤}. This implies (A^{⊤} ∩ B^{⊤})^{⊤} ⊆ A ∨_{⊤} B.

Conversely, if E[ ] ∈ A^{⊤} ∩ B^{⊤} then λx.E[x] ∈ (A ⇒ SN) ∩ (B ⇒ SN).

In conclusion, the interest and strength of biorthogonals is that they bring observation at an arbitrary C ∈ CR^{⊤⊤} back to the observation of SN, that we can manage thanks to the completeness of type assignment.

5. Sufficient Conditions for Safe Interaction

In this section, we address the question of finding sufficient conditions for the safety of (∨ E).

We begin by studying two conditions, arising when closing by union respectively reducibility candidates and biorthogonals (involving applicative contexts only). These conditions follow a common scheme that we present first.

On the other hand, it is natural to ask whether typability in a subsystem of ⊢_{∧∨} can imply safe interaction (i.e. the safety of (∨ E)). In particular, rewrite systems for which intersection types are sufficient for the completeness of type assignment may have a form of uniformity in their computational behavior. We show that this is not sufficient for the safety of (∨ E). It is interesting to note that, however, stability by union of reducibility candidates implies completeness of ⊢_{∧} w.r.t. strong normalization.

5.1. Stability by Union

One possibility is to use a family of reducibility candidates that is stable by union. We address this question in general terms.

Theorem 5.1. Let U ⊆ CR be a collection of sets such that SN ∈ U and A, B ∈ U implies A ⇒ B, A∩B, A∪B ∈ U. Given T ∈ T , define ⟦T ⟧_{U} ∈ U as

⟦o⟧_{U} =_{def} SN
⟦T ⇒ U⟧_{U} =_{def} ⟦T ⟧_{U} ⇒ ⟦U⟧_{U}
⟦T ∧ U⟧_{U} =_{def} ⟦T ⟧_{U} ∩ ⟦U⟧_{U}
⟦T ∨ U⟧_{U} =_{def} ⟦T ⟧_{U} ∪ ⟦U⟧_{U} .

If Γ ⊢_{∧⊻} t : T and σ ⊧_{⟦ · ⟧_{U}} Γ then tσ ∈ ⟦T ⟧_{U}.

The next point is to build such a U ⊆ CR. We can gain some insight by looking at collections of sets arising as the closure by union of some closure operator. This motivates the following proposition, whose proof is not difficult and can be found in [16]. If \overline{·} : P(D) → P(D) is a closure operator, write \overline{x} for \overline{\{x\}} and \overline{P^{∗}(D)} for \{\overline{X} | ∅ ≠ X ⊆ D\}.

Proposition 5.2. 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{Ω} implies ⋃ C, ⋂ C ∈ \overline{Ω}.

5.2. The Principal Reduct Property

We begin by the closure by union of CR (see [16] for details).

Definition 5.3. Let t ⊑_{SN} u iff t, u ∈ SN and for all v ∉ N, if t →^{∗} v then u →^{∗} v.

Note that if t ⊑_{SN} u and tt⃗, ut⃗ ∈ SN, then tt⃗ ⊑_{SN} ut⃗. In [16], it is shown that \overline{t} = \{u | u ⊑_{SN} t\} for all t ∈ SN (where \overline{·} is the closure operator of CR defined in Sec. 3.1). Then, it follows from Prop. 5.2, that the closure by union of CR, denoted by \overline{CR}, is the set of non-empty C ⊆ SN which are downward closed w.r.t. ⊑_{SN}. We now discuss a condition for CR = \overline{CR}.

Definition 5.4 (Principal Reduct Property). We say that t ∈ N ∩ SN has the principal reduct property (p.r.p.) when there is u ∈ (t)_{→} such that u = sup_{⊑_{SN}} (t)_{→} (modulo the equivalence induced by ⊑_{SN}).

We say that R has the principal reduct property when every f(t⃗) ∈ SN with f ∈ F has the p.r.p.

Note that R has the p.r.p. iff for every f(t⃗) ∈ SN with f ∈ F, there is f(x⃗) ↦_{R} d such that d[t⃗/x⃗] = sup_{⊑_{SN}} {r[t⃗/x⃗] | f(x⃗) ↦_{R} r}. We have shown in [16] that CR = \overline{CR} (i.e. CR is stable by union) if and only if every non-normal t ∈ N ∩ SN has the p.r.p. This property is satisfyed for terms with head β-redexes [16].

Proposition 5.5. Every non-normal t ∈ N ∩ SN has the p.r.p. if and only if R has the p.r.p.

Proof. Easy, using Weak Standardization (see [1, 16]):

If t ↦_{β} u and tt⃗ → v with v ≠ ut⃗, then v = t′t⃗′ with (t, t⃗) → (t′, t⃗′) and there is u′ such that t′ ↦_{β} u′ and ut⃗ →^{∗} u′t⃗′.

To the best of our knowledge, the notion of Weak Standardization appeared first in [1]. To summarize, we obtain that the p.r.p. of R implies that for all T, U ∈ T we have \overline{⟦T ⟧ ∪ ⟦U⟧} = ⟦T ⟧ ∪ ⟦U⟧. Then, the safety of (∨ E) follows from Thm. 5.1.

Theorem 5.6. Assume that R has the principal reduct property. If Γ ⊢_{∧⊻} t : T and σ ⊧_{⟦ · ⟧} Γ then tσ ∈ ⟦T ⟧.

Example 5.7. Consider the non-confluent system

f(x) ↦_{R} x  f(x) ↦_{R} a  f(x) ↦_{R} b .

Since the terms a and b are neutral and in normal from, every non-neutral reduct of f(t) is a reduct of t. Therefore, t = sup_{⊑_{SN}} {r[t/x] | f(t⃗) ↦_{R} r} and the system has the p.r.p.

5.3. Closure by Union of Biorthogonals

We now turn to the closure by union of a family of biorthogonals. Let ⊥ ⊥ ⊆ A × Π and a ≤ b iff a^{⊥ ⊥} ⊆ b^{⊥ ⊥}. For all a ∈ A, we have a\begin{matrix}⊥ ⊥ \\ ⊥ ⊥ \end{matrix} = \{b | a ≤ b\}. Hence, by Prop. 5.2, the closure by union of ⊥ ⊥-biorthogonals is the collection of non-empty subsets of A (resp. Π) that are upward closed w.r.t. ≤.

Definition 5.8. Let t⊥ ∼t⃗ iff tt⃗ ∈ SN and t ≲ u iff t^{⊥ ∼} ⊆ u^{⊥ ∼}.

Let O be the set of all non-empty C ⊆ SN such that if t ∈ C and t ≲ u, then u ∈ C.

Hence, O is the closure by union of CR^{⊥ ∼⊥ ∼}. Note that t ⊑_{SN} u implies u ≲ t. Moreover, t ≲ u implies tt⃗ ≲ ut⃗ for all t⃗, and the next proposition easily follows.

Proposition 5.9 (Type Constructions in O). Let A, B ⊆ O. Then, A ⇒ B, A ∩ B, A ∪ B ∈ O.

Definition 5.10 (Weak Principal Reduct Property). We say that R has the weak principal reduct property (w.p.r.p.) when for every f(t⃗) ∈ SN with f ∈ F there is f(x⃗) ↦_{R} d such that d[t⃗/x⃗] = inf_{≲}{r[t⃗/x⃗] | f(t⃗) ↦_{R} r} (modulo the equivalence induced by ≲).

Note that if R has the p.r.p. then it has the w.p.r.p. The w.p.r.p. is a necessary and sufficient condition for O ⊆ CR.

Lemma 5.11. O ⊆ CR if and only if R has the w.p.r.p.

Proof. Using Weak Standardization (see Prop. 5.5).

Theorem 5.12. Assume that R has the weak principal reduct property. If Γ ⊢_{∧⊻} t : T and σ ⊧_{⟦ · ⟧_{O}} Γ, then tσ ∈ ⟦T ⟧_{O}.

Example 5.13. The confluent system

p ↦_{R} λx.c_{1}  p ↦_{R} λx.c_{2}  c_{i} ↦_{R} d

does not have the p.r.p. since λx.c_{1} and λx.c_{2} are two different non-neutral terms. But it has the w.p.r.p. since for all t⃗ we have (λx.c_{1})t⃗ ∈ SN iff (λx.c_{2})t⃗ ∈ SN.

5.4. Saturated Sets

The w.p.r.p. corresponds to the ability to define sound Tait’s saturated sets. The set SAT of saturated sets is the set of all HN ⊆ S ⊆ SN such that (SAT 2) if h ↦_{β} ∪ ↦_{R} h′ with h′ ≲ h and h′t⃗ ∈ S then

ht⃗ ∈ S. It is easy to see that SAT is stable by ⇒, ⋃ and ⋂. Moreover, it is sound w.r.t. ⊢_{∧⊻} when R has the w.p.r.p.:

Theorem 5.14. Assume that R has the weak principal reduct property. If Γ ⊢_{∧⊻} t : T and σ ⊧_{⟦ · ⟧_{SAT}} Γ then tσ ∈ ⟦T ⟧_{SAT}.

Proof. As for Thm. 3.6, the proof is by induction on typing derivations Γ ⊢_{∧⊻} t : T. The critical cases are that of (⇒ I) and (Fun ).

(⇒ I) \frac{Γ, x : U ⊢_{∧⊻} t : T}{Γ ⊢_{∧⊻} λx.t : U ⇒ T}

Let σ ⊧_{SAT} Γ, u ∈ ⟦U⟧_{SAT} and t′ =_{def} tσ. We can assume that t′[u/x] = t(σ[u/x]).

We have to show that (λx.t′)u ∈ ⟦T ⟧_{SAT}. By induction hypothesis we have t′[u/x] ∈ ⟦T ⟧_{SAT} and we are done if t′[u/x] ≲ (λx.t′)u. But since u ∈ SN, this follows from Weak Standardization (see Prop. 5.5 and [1, 16]).

(Fun ) \frac{Γ ⊢_{∧⊻} t⃗: T⃗ ∀f(x⃗) ↦_{R} r, Γ, x⃗ : T⃗ ⊢_{∧⊻} r : T}{Γ ⊢_{∧⊻} f(t⃗) : T}

Let σ ⊧_{⟦ · ⟧_{SAT}} Γ and t⃗′ =_{def} t⃗σ. By induction hypothesis, t⃗′ ∈ ⟦T⃗⟧_{SAT}. We have to show that f(t⃗′) ∈ ⟦T ⟧_{SAT}.

Since by induction hypothesis, r[t⃗/x⃗] ∈ ⟦T ⟧_{SAT} ⊆ SN for all f(x⃗) ↦_{R} r, we have f(t⃗) ∈ SN. Therefore by assumption there is f(x⃗) ↦_{R} d such that d[t⃗/x⃗] ∈ inf_{≲}{r[t⃗/x⃗] | f(x⃗) ↦_{R} r}. Hence f(t⃗) ≳ d[t⃗/x⃗] ∈ ⟦T ⟧_{SAT} and f(t⃗) ∈ ⟦T ⟧_{SAT}.

Hence, the w.p.r.p. allows to define saturated sets that are stable by union and sound w.r.t. ⊢_{∧⊻}. Since the p.r.p. strictly implies the w.p.r.p., this shows that stability by union of sound saturated sets is strictly more general than stability by union of Girard’s reducibility candidates.

5.5. Typability in ⊢_{∧}

A natural question is whether (∨ E) is safe with rewrite systems for which intersection types are sufficient for the completeness of typing w.r.t. strong normalization.

Indeed, one could expect to have that if for all t ∈ SN there are Γ, T such that Γ ⊢_{∧} t : T, then (∨ E) is safe. This is not the case, as shown by the following example.

Example 5.15. Consider the system of Ex. 2.2. Let T_{S} =_{def} o ∧ (o ⇒ o), hence Γ ⊢_{∧} t : T_{S} implies Γ ⊢_{∧} tt : o. Then, using (Fun ) we can derive:

\frac{\begin{matrix}⊢_{∧} λxy.g(xaδ): & (o ⇒ (T_{S} ⇒ o) ⇒ o) ⇒ T_{S} ⇒ o \\ ⊢_{∧} λxy.g(yy) : & (o ⇒ (T_{S} ⇒ o) ⇒ o) ⇒ T_{S} ⇒ o \end{matrix}}{⊢_{∧} f : (o ⇒ (T_{S} ⇒ o) ⇒ o) ⇒ T_{S} ⇒ o}

Moreover, it is easy to see that with this system, if t ∈ SN then there are Γ and T such that Γ ⊢_{∧} t : T. Since by Ex. 2.2 this system breaks the safety of (∨ E), it follows that completeness of typability in ⊢_{∧} does not imply safe interaction.

However, it is interesting to note that the p.r.p. implies completeness of ⊢_{∧}. That is, if R has the p.r.p. and t ∈ SN then there are Γ and T such that Γ ⊢_{∧} t : T.

Theorem 5.16 (Completeness). Assume that R has the p.r.p. If t ∈ SN, then there are Γ and T such that Γ ⊢_{∧} t : T.

6. HN -Biorthogonality

In this section, we briefly discuss an orthogonality relation based on the observation of HN (the bottom element of CR) rather than SN (its top element). This semantics induces a better adequacy with the type system. However, it is not clear whether it is complete w.r.t. the safety of (∨ E).

We interpret T ∈ T by ⟦T ⟧_{HN} ∈ CR as in Sec. 3.1, except that ⟦o⟧_{HN} =_{def} HN. The properties of Sec. 3.2 holds also for ⟦T ⟧_{HN}. This way we get the soundness of o-typability w.r.t. HN.

Theorem 6.1. If Γ ⊢_{∧∨} t : o then t ∈ HN.

Since Thm. 3.12 says that any hereditary neutral term is typable by any T ∈ T , it follows that a term is typable by o if and only if it can be given any type (in different contexts), suggesting that o may be the least element of T .

This agrees with ⟦ · ⟧_{HN}, since ⟦o⟧_{HN} ⊆ ⟦T ⟧_{HN} for all T ∈ T , but contradicts ⟦o⟧ = SN. It is moreover not clear whether the least ⊤-biorthogonal is HN (note that the least ⊥ ∼-biorthogonal is not HN).

A development similar to that of Sec. 4 goes through with ⟦ · ⟧_{HN}. First, we obtain the analogous of Thm. 3.13 and Thm. 3.14 for HN.

Theorem 6.2. If (λx.t)u ∈ SN and v[t[u/x]/y] ∈ HN then v[(λx.t)u/y] ∈ HN.

Proof. As in Thm. 3.13, from (λx.t)u ∈ SN, thanks to Thm. 3.11 we get Γ′, T and U such that Γ′ ⊢_{∧∨} u : U and Γ′ ⊢_{∧∨} t[u/x] : T. On the other hand, thanks to Thm. 3.12 there is Γ′′ such that Γ′′ ⊢_{∧∨} v[t[u/x]/y] : o. Now, reasoning as in Thm. 3.13, we obtain that Γ′ ∧ Γ′′ ⊢_{∧∨} (λy.v)((λx.t)u) : o, hence v[(λx.t)u/y] ∈ HN by Thm. 6.1.

Theorem 6.3. If t ∈ HN and v ∈ HN then v[t/x] ∈ HN.

Proof. As for Thm. 3.14, using Thm. 3.12 instead of Thm. 3.11 and Thm. 6.1 instead of Cor. 3.7.

In the same way that ⊤-biorthogonals were defined in correspondence with ⟦ · ⟧, we can define ⊥-biorthogonals in correspondence with ⟦ · ⟧_{HN}.

Definition 6.4. Let t ⊥ E[ ] iff E[t] ∈ HN.

In fact, reduction to an hereditary neutral term corresponds to reduction to error in [19, 18]. Since in these papers biorthogonals are based on the observation of nonreduction to error, they are in some sense dual to our HN - biorthogonals.

Note that t^{⊥} ⊆ u^{⊥} implies t^{⊤} ⊆ u^{⊤}, but the converse is false: λx.x^{⊤} ⊆ λyx.yx^{⊤}, but (λx.x)z ∈ HN while (λyx.yx)z ∉ HN. As in Prop. 4.6, if U, V ∈ T_{∧} we have

\begin{matrix}⟦o⟧_{HN} = & HN = \{[ ]\}^{⊥} \\ ⟦U ⇒ V ⟧_{HN} = & (⟦U⟧_{HN} · ⟦V ⟧_{HN}^{⊥})^{⊥} \\ ⟦U ∧ V ⟧_{HN} = & (⟦U⟧_{HN}^{⊥} ∪ ⟦V ⟧_{HN}^{⊥})^{⊥} . \end{matrix}

In order to get an interesting interpretation of (∨ E), we define ⦇ · ⦈_{HN} analogously as ⦇ · ⦈. Note that the only change in the definition is the orthogonality relation: we deduce ⦇o⦈_{HN} = HN from ⦇o⦈_{HN} =_{def} {[ ]}^{⊥}. Again, the important case is that of (∨ E):

⦇T_{1} ∨ T_{2}⦈_{HN} =_{def} (⦇T_{1}⦈_{HN}^{⊥} ∩ ⦇T_{2}⦈_{HN}^{⊥})^{⊥} .

With the same method as in Sec. 4.4, we obtain the dual of Thm. 4.9:

Theorem 6.5. The following are equivalent:

(i) If Γ ⊢_{∧⊻} t : o then t ∈ HN.

(ii) (Ip_{HN}): If f ∈ F, f(t⃗) ∈ SN and v[r[t⃗/x⃗]/y] ∈ HN for all f(x⃗) ↦_{R} r, then v[f(t⃗)/y] ∈ HN.

(iii) ⦇ · ⦈_{HN} is sound for (∨ E).

We conclude by showing that we indeed obtained a sufficient condition for the safety of (∨ E).

Lemma 6.6. (Ip_{HN}) ⇒ (Ip).

Proof. Let f(t⃗) ∈ SN, such that v[r[t⃗/x⃗]/y] ∈ SN for each f(x⃗) ↦_{R} r. Since R(f) is finite, there is u⃗ such that for all f(x⃗) ↦_{R} r, v[r[t⃗/x⃗]/y]u⃗ ∈ HN. By (Ip_{HN}) we obtain that v[f(t⃗)/y]u⃗ ∈ HN hence v[f(t⃗)/y] ∈ SN.

The converse is unclear because we do not have subject reduction in ⊢_{∧⊻}. It would require, at least, to add the subtyping rule U ⇒ (T_{1} ∨ T_{2}) ≤ (U ⇒ T_{1}) ∨ (U ⇒ T_{2}), which may be unsound in our setting. Subject reduction in presence of (∨ E) is extensively studied in [2].

7. Conclusion

We have shown that the rule (∨ E) can break strong normalization, even in the presence of confluent rewriting, and have given sufficient conditions for its safety.

Our main result is that for strong normalization, the best possible interpretation of union types is given by biorthogonals. This gives a computational interpretation of biorthogonality. We conjecture that the result depends on the must nature of strong normalization, and that it extends to must (weak) head reductions.

We considered a very simple form of rewriting, with the objective of concentrating ourselves on the very problem of (∨ E). As future work, it is important to study the case of rewrite rules with pattern matching.

Our results can be summarized in the following diagram:

[figure: (∨ E) is safe; (Sec. 4); (Ip); w.p.r.p. (Sec. 5.3); (Ip_{HN}) (Sec. 6); p.r.p. (Sec. 5.2)]

Acknowledgments. The author thanks Frédéric Blanqui and Claude Kirchner for advices, support and comments. Thanks also to Philippe de Groote for his example (see Ex. 2.1) and to Arnaud Spiwack and Dan Dougherty for some interesting discussions. Anonymous referees gave interesting comments on the presentation of the paper.

References

[1] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993. 9 [2] F. Barbanera, M. Dezani-Ciancaglini, and U. de’Liguoro.

Intersection and Union Types: Syntax and Semantics. Information and Computation, 119:202–230, 1995. 1, 2, 11

[3] H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931–940, 1983. 2, 12, 13

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

[5] T. Coquand and A. Spiwack. A Proof of Strong Normalisation using Domain Theory. In LiCS’06, pages 307–316, 2006. 2, 3

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

[7] M. Dezani-Ciancaglini, U. de’ Liguoro, and P. Piperno. Filter Models for Conjunctive-Disjunctive Lambda-Calculi. Theoretical Computer Science, 170(1-2):83–128, 1996. 2, 3, 12, 13

[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, 2, 3, 12, 13

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

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

[11] J. Gallier. Typing Untyped Lambda-Terms, or Reducibility Strikes Again! Annals of Pure and Applied Logic, 91:231– 270, 1998. 2, 3, 5, 12

[12] H. Hosoya, J. Vouillon, and B. Pierce. Regular Expression Types for XML. In ICFP’00, 2000. 2

[13] J.-L. Krivine. Lambda-Calcul, Types et Modèles. Masson, 1990. 2, 3, 5, 12

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

[15] A. M. Pitts. Parametric Polymorphism and Operational Equivalence. Mathematical Structures in Computer Science, 10:321–359, 2000. 2

[16] C. Riba. On the Stability by Union of Reducibility Candidates. In FoSSaCS’07, volume 4423 of LNCS, 2007. 2, 4, 8, 9

[17] F. von Raamsdonk and P. Severi. On Normalisation. Technical Report CS-R9545, CWI, 1995. 5

[18] J. Vouillon. Subtyping Union Types. In CSL’04, volume 3210 of LNCS, pages 415–429. Springer Verlag, 2004. 1, 4, 10

[19] J. Vouillon and P.-A. Melliès. Semantic Types: A Fresh Look at the Ideal Model for Types. In POPL’04. ACM, 2004. 1, 2, 4, 6, 10

A. Derivability in ⊢_{∧∨} and ⊢_{∧}

In this appendix, we present results on derivability in the type systems ⊢_{∧∨} and ⊢_{∧}.

We begin by some fundamental properties of the type system. They are well-known in the case of the pure λcalculus with intersection types [13, 11, 3]. Concerning union types, they have been proved in [7, 8] when (T , ≤ , ∧, ∨) is a distributive lattice. Proving them in our framework does not bring any difficulty.

We then detail the proof of completeness of type assignment in ⊢_{∧∨} w.r.t. strong normalization.

Excepted Thm. A.5, all the properties presented in this section are common to ⊢_{∧} and ⊢_{∧∨}. Let ty ∈ {∧, ∧∨}.

Proposition A.1 (Inversion).

(i) Γ ⊢_{ty} x : T iff (x : U) ∈ Γ with U ≤ T.

(ii) Γ ⊢_{ty} tu : T iff there is U such that Γ ⊢_{ty} t : U ⇒ T and Γ ⊢_{ty} u : U.

(iii) Γ ⊢_{ty} λx.t : T iff there exists n ≥ 1 and U_{1}, …, U_{n}, V_{1}, …, V_{n} such that ⋀_{i}(U_{i} ⇒ V_{i}) ≤ T and for all i ∈ {1, …, n}, Γ, x : U_{i} ⊢_{ty} t : V_{i}.

(iv) Γ ⊢_{ty} f(t⃗) : V iff there are T⃗ such that Γ ⊢_{ty} t⃗: T⃗ and for all f(x⃗) ↦_{R} r, Γ, x⃗ : T⃗ ⊢_{ty} r : V.

Proof. All cases are proved by trivial inductions on the typing derivations. Note that for the case (iii), thanks to αequivalence we can assume that x ∉ dom(Γ).

The next property is fundamental for type systems. It corresponds to cut-elimination.

Lemma A.2 (Substitution). If Γ, x : U ⊢_{ty} t : T and Γ ⊢_{ty} u : U then Γ ⊢_{ty} t[u/x] : T.

Proof. By a trivial induction on Γ, x : U ⊢_{ty} t : T.

In particular, if x ∉ FV(t) then Γ, x : U ⊢_{ty} t : T implies Γ ⊢_{ty} t : T. This property is called Contraction.

We now turn to the key properties for completeness of type assignment. They are characteristic properties of intersection types (recall that in our case, union types are needed to type function symbols, not for the λ-calculus itself).

Proposition A.3 (Interpolation). Let x ∉ Γ. If Γ ⊢_{ty} t[u/x] : T and Γ ⊢_{ty} u : U, then there is V such that Γ, x : V ⊢_{ty} t : T and Γ ⊢_{ty} u : V.

Proof. Given v ∈ Λ, we let v′ =_{def} v[u/x]. We reason by induction on t. We only detail the case of t = f(t⃗).

By inversion (Prop. A.1.(iv)), there are T⃗ such that Γ ⊢_{ty} t⃗′ : T⃗ and for all f(x⃗) ↦_{R} r, Γ, x⃗ : T⃗ ⊢_{ty} r : T. We can assume that x ∉ x⃗. By induction hypothesis, there is V⃗ such that for all i ∈ {1, …, |t⃗|}, Γ, x : V_{i} ⊢_{ty} t_{i} : T_{i} and Γ ⊢_{ty} u : V_{i}. Taking V =_{def} ⋀_{i} V_{i} we get Γ, x : V ⊢_{ty} t⃗: T⃗ and Γ ⊢_{ty} u : V. Moreover, we have for all f(x⃗) ↦_{R} r Γ, x⃗ : T⃗, x : V ⊢_{ty} r : T and it follows that Γ, x : V ⊢_{ty} f(t⃗) : T.

Note that if Γ ⊢_{ty} t : T and y ∉ Γ, then Γ[y/x] ⊢_{ty} t[y/x] : T.

Lemma A.4 (Weak Head Expansion).

(i) If Γ ⊢_{ty} u : U and Γ ⊢_{ty} t[u/x]v⃗ : T then Γ ⊢_{ty} (λx.t)uv⃗ : T.

(ii) For all f ∈ F, if Γ ⊢_{ty} t⃗ : T⃗, and for all f(x⃗) ↦_{R} r, Γ ⊢_{ty} r[t⃗/x⃗]v⃗ : T, then Γ ⊢_{ty} f(t⃗)v⃗ : T.

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

First, assume that x⃗ is disjoint from dom(Γ). We reason by induction on |v⃗|.

In the case |v⃗| = 0, we have Γ ⊢_{ty} t⃗ : T⃗ and for all f(x⃗) ↦_{R} r, Γ ⊢_{ty} r[t⃗/x⃗] : T. By Prop. A.3, for all f(x⃗) ↦_{R} r there are Γ_{r} and T⃗^{r} such that Γ_{r} ⊢_{ty} t⃗ : T⃗^{r} and Γ_{r}, x⃗ : T⃗^{r} ⊢_{ty} r : T. Hence, taking T⃗′ =_{def} ⋀_{r} T⃗^{r} and Γ =_{def} ⋀_{r} Γ_{r} we have Γ ⊢_{ty} t⃗ : T⃗′ and for all f(x⃗) ↦_{R} r, Γ, x⃗ : T⃗′ ⊢_{ty} r : T. Thus Γ ⊢_{ty} f(t⃗) : T.

Now, assume the property for v⃗ and let Γ ⊢_{ty} t⃗ : T⃗ and for all f(x⃗) ↦_{R} r, Γ ⊢_{ty} r[t⃗/x⃗]v⃗v : T. By Prop. A.1.(ii), for all f(x⃗) ↦_{R} r there is V_{r} such that Γ ⊢_{ty} r[t⃗/x⃗]v⃗ : V_{r} ⇒ T and Γ ⊢_{ty} v : V_{r}. Since R(f) is finite, taking V = ⋀_{r} V_{r}, we get Γ ⊢_{ty} v : V and for all f(x⃗) ↦_{R} r, Γ ⊢_{ty} r[t⃗/x⃗]v⃗ : V ⇒ T. By induction hypothesis we have Γ ⊢_{ty} f(t⃗)v⃗ : V ⇒ T and we conclude that Γ ⊢_{ty} f(t⃗)v⃗v : T.

It remains to consider the case where x⃗ and dom(Γ) are not disjoints. Let x′ =_{def} {x_{i} | i ∈ {1, …, |x⃗|} & x_{i} ∈ Γ}. Hence, Γ is of the form Γ′, x′ : U⃗. Consider y⃗ disjoint from dom(Γ) such that |y⃗| = |x′|, and let t⃗′ =_{def} t⃗[y⃗/x′] and v′ =_{def} v⃗[y⃗/x′]. Therefore, we have Γ′, y⃗ : U⃗ ⊢_{ty} t⃗′ : T⃗ and for all f(x⃗) ↦_{R} r, Γ′, y⃗ : U⃗ ⊢_{ty} r[t⃗′/x⃗]v′ : T. Hence Γ′, y⃗ : U⃗ ⊢_{ty} f(t⃗′)v′ : T, since x⃗ is disjoint from dom(Γ′, y⃗ : U⃗) ; and we have Γ′, x′ : U⃗ ⊢_{ty} f(t⃗)v⃗ : T.

We finish by the full proof of Thm. 3.11 (Completeness).

Theorem A.5 (Completeness). If t ∈ SN, then there are Γ and T such that Γ ⊢_{∧∨} t : T.

Proof. The proof is by induction on ≺. Recall that t = λx⃗.hv⃗ where h is either a variable, a β-redex or a symbol f(t⃗).

If |x⃗| ≠ 0, then by induction hypothesis there are Γ and T⃗ such that Γ, x⃗ : T⃗ ⊢_{∧∨} hv⃗ : T, and therefore Γ ⊢_{∧∨} λx⃗.hv⃗ : T⃗ ⇒ T.

Now we assume that |x⃗| = 0 and reason by cases on h. h = x ∈ X. Since v⃗ ≺ t, by induction hypothesis there are

Γ_{i}, U⃗^{i} and T_{i} such that Γ_{i}, x⃗ : U⃗^{i} ⊢_{∧∨} v_{i} : T_{i}. Hence, with Γ′ =_{def} ⋀_{i}(Γ_{i}, x⃗ : U⃗^{i}), we have for all i that Γ′ ⊢_{∧∨} v_{i} : T_{i}. Let T ∈ T and Γ =_{def} Γ′ ∧ (x : T⃗ ⇒ T). We have Γ ⊢_{∧∨} xv⃗ : T.

h = (λx.u)v. We have v ≺ t and u[v/x]v⃗ ≺ t, hence by induction hypothesis there are Γ, T and V such that Γ ⊢_{∧∨} u[v/x]v⃗ : T and Γ ⊢_{∧∨} v : V. By Lem. A.4.(i), we have Γ ⊢_{∧∨} (λx.u)vv⃗ : T.

h = f(t⃗). First, note that t⃗ ≺ t.

If f ∈ C, since v⃗ ≺ t, there are Γ, T⃗ and V⃗ such that Γ ⊢_{∧∨} t⃗ : T⃗ and Γ ⊢_{∧∨} v⃗ : V⃗. Hence Γ ⊢_{∧∨} f(t⃗)v⃗ : T for all T ∈ T . The interesting case is when f ∈ F. For all f(x⃗) ↦_{R} r we have r[t⃗/x⃗]v⃗ ≺ t and by induction hypothesis there are Γ_{r}, T⃗^{r} and V_{r} such that Γ_{r} ⊢_{∧∨} t⃗ : T⃗^{r} and Γ_{r} ⊢_{∧∨} r[t⃗/x⃗]v⃗ : V_{r}. Now, taking Γ =_{def} ⋀_{r∈R(f)} Γ_{r}, T⃗ =_{def} ⋀_{r∈R(f)} T⃗^{r} and V =_{def} ⋁_{r∈R(f)} V_{r}, we have Γ ⊢_{∧∨} t⃗ : T⃗ and for all f(x⃗) ↦_{R} r, Γ ⊢_{∧∨} r[t⃗/x⃗]v⃗ : V. We conclude that Γ ⊢_{∧∨} f(t⃗)v⃗ : V thanks to Lem. A.4.(ii).

B. Typability in ⊢_{∧} (Sec 5.5)

In this appendix, we give the proofs of Sec. 5.5.

B.1. Proofs of Example 5.15

In this section, we prove the claim of Ex. 5.15: for the system of Ex. 2.2, intersection types are complete w.r.t. strong normalization.

Since by Ex. 2.2 this system breaks the safety of (∨ E), it follows that completeness of type assignment in ⊢_{∧} does not imply safe interaction. We use the preorder ≺ defined in Def.3.10.

Proposition B.1. Let R be the system of Ex. 2.2 and fv⃗ ∈ SN be such that every u ≺ fv⃗ is typable in ⊢_{∧}. Then fv⃗ is typable in ⊢_{∧}.

Proof. We reason by cases on |v⃗|. Let u_{1} =_{def} λxy.g(xaδ), u_{2} =_{def} λxy.g(yy) and recall that T_{S} = o ∧ (o ⇒ o).

|v⃗| = 0. This case is dealt with in Ex. 5.15.

|v⃗| = 1. Let v =_{def} v⃗. Since vaδ ≺ fv, we have Γ and T such that Γ ⊢_{∧} vaδ : T. Thanks to Prop. A.1.(ii) there are U_{1}, U_{2} such that Γ ⊢_{∧} v : U_{1} ⇒ U_{2} ⇒ T, Γ ⊢_{∧} a : U_{1} and Γ ⊢_{∧} δ : U_{2}. It follows that for all i ∈ {1, 2} we have

Γ ⊢_{∧} u_{i} : (U_{1} ⇒ U_{2} ⇒ T) ⇒ T_{S} ⇒ o .

Hence Γ ⊢_{∧} u_{i}v : T_{S} ⇒ o and Γ ⊢_{∧} fv : T_{S} → o.

|v⃗| ≥ 2. In this case, we show by induction on |v⃗| that for all T ∈ T , there exists Γ such that for all i ∈ {1, 2} we have Γ ⊢_{∧} u_{i}v⃗ : T. This implies Γ ⊢_{∧} fv⃗ : T.

The induction step easily follows from the induction hypothesis and Prop. A.1.(ii). We only detail the base case v⃗ = v_{1}v_{2}.

Since v_{1}aδ ≺ fv_{1}v_{2}, as in the case |v⃗| = 1, we have Γ_{1}, U_{1}, U_{2} U_{3} such that Γ_{1} ⊢_{∧} v_{1} : U_{1} ⇒ U_{2} ⇒ U_{3}, Γ_{1} ⊢_{∧} a : U_{1} and Γ_{1} ⊢_{∧} δ : U_{2}.

On the other hand, since v_{2}v_{2} ≺ fv_{1}v_{2}, there are Γ_{2}, V_{1}, V_{2} such that Γ_{2} ⊢_{∧} v_{2} : V_{1} ∧ (V_{1} ⇒ V_{2}).

It follows that for all T ∈ T_{∧} we have

Γ_{1}, x : U_{1} ⇒ U_{2} ⇒ U_{3} ⊢_{∧} g(xaδ) : T
and Γ_{2}, y : V_{1} ∧ (V_{1} ⇒ V_{2}) ⊢_{∧} g(yy) : T .

Hence Γ_{1} ∧ Γ_{2} ⊢_{∧} u_{i}v_{1}v_{2} : T for all i ∈ {1, 2}.

Theorem B.2 (Completeness). Let R be the system of Ex. 2.2. If t ∈ SN then t is typable in ⊢_{∧}.

Proof. We reason by induction on ≺ as for Thm. A.5, except when t is an applied symbol.

The result is trivial if either t = av⃗ or t = g(u)v⃗. Otherwise, we have t = fv⃗ and since by induction hypothesis every u ≺ t is typable in ⊢_{∧}, we conclude by Prop. B.1.

B.2. The System ⊢_{∧} and the P.R.P.

Now, we show that if R has the p.r.p., then every strongly normalizable term is typable in ⊢_{∧}.

In addition to the properties proved in Appendix A we have the following.

Proposition B.3. If ⋀_{i∈I}(U_{i} ⇒ T_{i}) ≤ U ⇒ T, then there is a non-empty J ⊆ I such that U ≤ ⋀_{j∈J} U_{j} and ⋀_{j∈J} T_{j} ≤ T.

Proof. See [3].

With intersection and union types, Prop. B.3 is proved in [7, 8] assuming the distributivity of (T , ≤, ∧, ∨). We can not assume it in our case, since it would break the soundness of the biorthogonal type interpretation. Now we can prove:

Proposition B.4 (Subject Reduction). If Γ ⊢_{∧} t : T and t → u then Γ ⊢_{∧} u : T.

Proof. By induction on Γ ⊢_{∧} t : T, using Prop. A.1.(iii) and Prop. B.3 when t ↦_{β} u.

The important technical property is following lemma. Recall that ≺ is defined in Def.3.10.

Lemma B.5. Let v ∈ SN such that every v′ ≺ v is typable in ⊢_{∧}. Then, for all t, u ≺ v, if u ⊑_{SN} t and Γ ⊢_{∧} t : T then there is Γ′ such that Γ′ ⊢_{∧} u : T.

Proof. Let t ≺ v such that Γ ⊢_{∧} t : T. We show by induction on ≺ that for all u, if u ⊑_{SN} t and u ≺ v then there exists Γ′ such that Γ′ ⊢_{∧} u : T.

If u ∉ N, then by definition we have t →^{∗} u , thus Γ ⊢_{∧} u : T by Subject Reduction (Prop. B.4). Otherwise, u is of the form hu⃗ where h is either a variable, an abstraction or a function.

h = x. In this case, u ∈ HN. Since u⃗ ≺ v, by assumption there are are Γ′ and U⃗ such that Γ′ ⊢_{∧} u⃗ : U⃗. Hence we have Γ′ ∧ (x : U⃗ ⇒ T) ⊢_{∧} xu⃗ : T.

h = (λx.u_{1})u_{2}. In this case, since u_{1}[u_{2}/x]u⃗ ⊑_{SN} t, and u_{1}[u_{2}/x]u⃗ ≺ u, by induction hypothesis there is Γ_{1} such that Γ_{1} ⊢_{∧} u_{1}[u_{2}/x]u⃗ : T. Moreover, since u_{2} ≺ v, by assumption there are Γ_{2} and U such that Γ_{2} ⊢_{∧} u_{2} : U. Therefore, by Lem. A.4.(i) we have Γ_{1} ∧ Γ_{2} ⊢_{∧} (λx.u_{1})u_{2}u⃗ : T.

h = f(t⃗). Since for all f(x⃗) ↦_{R} r we have r[t⃗/x⃗]u⃗ ≺ u and r[t⃗/x⃗]u⃗ ⊑_{SN} t, by induction hypothesis there is Γ_{1} such that for all f(x⃗) ↦_{R} r we have Γ_{1} ⊢_{∧} r[t⃗/x⃗]u⃗ : T. On the other hand, since t⃗ ≺ v, by assumption there are Γ_{2}, T⃗ such that Γ_{2} ⊢_{∧} t⃗: T⃗. Hence by Lem. A.4.(ii) we have Γ_{1} ∧ Γ_{2} ⊢_{∧} f(t⃗)u⃗ : T.

Theorem B.6 (Completeness). Assume that R has the p.r.p.. If t ∈ SN, then there are Γ and T such that Γ ⊢_{∧} t : T.

Proof. The proof is by induction on ≺. It is the same as the proof of Thm. A.5, except for the case t = f(t⃗)v⃗. We only detail this case.

First, note that we have t⃗ ≺ t. Since moreover for all f(x⃗) ↦_{R} r we have r[t⃗/x⃗]v⃗ ≺ t by induction hypothesis there are Γ_{r}, T⃗^{r} and V_{r} such that Γ_{r} ⊢_{∧} t⃗ : T⃗^{r} and Γ_{r} ⊢_{∧} r[t⃗/x⃗]v⃗ : V_{r}.

Now, by assumption, there is f(x⃗) ↦_{R} d such that for all f(x⃗) ↦_{R} r, r[t⃗/x⃗]v⃗ ⊑_{SN} d[t⃗/x⃗]v⃗. Since d[t⃗/x⃗]v⃗ ≺ t and for all f(x⃗) ↦_{R} r, r[t⃗/x⃗]v⃗ ≺ t, and moreover by induction hypothesis every v ≺ t is typable in ⊢_{∧}, by Lem. B.5 for all f(x⃗) ↦_{R} r, there is Γ′_{r} such that Γ′_{r} ⊢_{∧} r[t⃗/x⃗]v⃗ : T_{d}.

Let Γ =_{def} ⋀_{r∈R(f)}(Γ_{r} ∧ Γ′_{r}) and T⃗ =_{def} ⋀_{r∈R(f)} T⃗^{r}. We have Γ ⊢_{∧} t⃗: T⃗ and for all f(x⃗) ↦_{R} r, Γ ⊢_{∧} r[t⃗/x⃗]v⃗ : T_{d}. We get Γ ⊢_{∧} f(t⃗)v⃗ : T_{d} thanks to Lem. A.4.(ii).

C. HN -Biorthogonality (Sec. 6)

This appendix is devoted to the proofs of Sec. 6 concerning HN -biorthogonality. The development is similar to that of Sec. 4.

We show that the following properties are equivalents:

(∨ E) is HN -safe: If Γ ⊢_{∧⊻} t : o then t ∈ HN.

(Ip_{HN}) If f ∈ F, f(t⃗) ∈ SN and v[r[t⃗/x⃗]/y] ∈ HN for all f(x⃗) ↦_{R} r, then v[f(t⃗)/y] ∈ HN.

⦇ · ⦈_{HN} is sound: If Γ ⊢_{∧⊻} t : T and σ ⊧_{⦇ · ⦈_{HN}} Γ then tσ ∈ ⦇T ⦈_{HN}.

Theorem C.1. If (∨ E) is HN -safe, then (Ip_{HN}) holds.

Proof. The proof is similar to that of Thm. 4.2.

Let f(t⃗) ∈ SN and v such that for all f(x⃗) ↦_{R} r, v[r[t⃗/x⃗]/y] ∈ HN. Reasoning as in Thm. 6.2, there are Γ, (U_{r})_{r∈R(f)} such that Γ ⊢_{∧∨} f(t⃗) : ⋁_{r∈R(f)} U_{r} and for all r ∈ f(R), Γ ⊢_{∧∨} λy.v : U_{r} ⇒ o.

By Prop. 4.1, we have Γ ⊢_{∧⊻} (λy.v)f(t⃗) : o, hence v[f(t⃗)/y] ∈ HN since (∨ E) is HN -safe.

Proposition C.2 (Neutral Term Property). Let E[ ] ∈ SN and t ∈ N. If (Ip_{HN}) holds and ∀u(t → u ⇒ E[u] ∈ HN) then E[t] ∈ HN.

Proof. First, if t ∈ HN, since E[ ] ∈ SN, by Thm. 6.3 we have E[t] ∈ HN.

Otherwise, since t ∈ N, we have (t)_{→} ≠ ∅ and there are two cases. In the first one t = (λx.t_{1})t_{2}v⃗ and we conclude by Thm. 6.2. In the second one t = f(t⃗)v⃗ with f ∈ F and the result follows from (Ip_{HN}).

Then, as in Sec. 4.3, we obtain that biorthogonals of nonempty subsets of SN are reducibility candidates.

Lemma C.3. If A ⊆ SN is not empty, then (Ip_{HN}) implies A^{⊥⊥} ∈ CR.

Proof. As for Lem. 4.5, using Prop. C.2 instead of Prop. 4.4 and (Ip_{HN}) instead of (Ip).

We deduce that types are interpreted as biorthogonals, and the main result easily follows.

Lemma C.4. If (Ip_{HN}) then for all T ∈ T , ⦇T ⦈_{HN} ∈ CR.

Proof. Reason by induction on T, using Lem. C.3 in the case T = T_{1} ∨ T_{2}.

Theorem C.5. Let Γ ⊢_{∧⊻} t : T. If (Ip_{HN}) and σ ⊧_{⦇ · ⦈_{HN}} Γ then tσ ∈ ⦇T ⦈_{HN}.

Proof. By induction on Γ ⊢_{∧⊻} t : T. Thanks to Lem. C.4, using (Ip_{HN}), we have ⦇U⦈_{HN} ∈ CR for all U ∈ T . Then, once we have noted that t′ ⊥ E[(λx.c′)[ ]] implies c′[t′/x] ⊥ E[ ], the proof is exactly the same as for Thm. 4.8, using Thm. 6.2 instead of Thm. 3.13.