Union of Reducibility Candidates for Orthogonal Constructor Rewriting

Colin Riba

Projet Everest INRIA Sophia Antipolis^{⋆}

                        Colin.Riba@sophia.inria.fr

Abstract. We revisit Girard’s reducibility candidates by proposing a general of the notion of neutral terms. They are the terms which do not interact with some contexts called elimination contexts. We apply this framework to constructor rewriting, and show that for orthogonal constructor rewriting, Girard’s reducibility candidates are stable by union.

1 Introduction

The most flexible termination proof methods for various extensions of typed λcalculi use type interpretations [Abe06, BGP06, BJO02, BR06, Par97]. Among them we distinguish three families: Girard’s reducibility candidates [Gir72], Tait’s saturated sets [Tai75], and interpretations based on biorthogonality [Gir87, Par97]. An interesting way to compare different type interpretations is to study their stability by union. This is even a necessary property in some cases [Abe06, BR06, Tat07].

This paper concerns the extension of the simply-typed λ-calculus with constructor rewriting. We are not interested in termination criteria by themselves, but by the investigation of the closure properties of types interpretations that allow to formulate different termination criteria. We focus on Girard’s reducibility candidates and their stability by union.

We give a generalization of the notion of neutral terms that allows to define Girard’s reducibility candidates in a generic way. Neutral terms are the terms that do not interact with some contexts called elimination contexts. Terms which are not neutral are observable since they interact with some elimination contexts. We call them values. We instantiate this framework with constructor rewriting. In order to get interesting values, we use elimination contexts with destructors to eliminate the constructors.

Next, we study the question of stability by union. By instantiating the condition of [Rib07b], we show that reducibility candidates are stable by union for orthogonal constructor rewriting. The proof uses a result of [KOvO01] on the existence of external redexes for orthogonal Context-sensitive Conditional Expression Systems (CCERSs).

⋆ 2004 route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France.

The paper is organized as follows. We present our notations in Sect. 2.

Section 3 presents a general definition of reducibility families and type interpretations. We apply it by briefly discussing Tait’s saturated sets for the pure λ-calculus and one possible extension to deal with rewriting.

Section 4 is devoted to Girard’s reducibility candidates, of which we suggest a generalization in Sect. 4.1. We instantiate it in Sect. 4.2 to the framework of λ-calculus plus constructor rewriting.

We then discuss stability by union in Sect. 5. We first briefly present the key problems and known results. Section 5.1 recalls a necessary and sufficient condition for the stability by union of Girard’s candidates. In Sect. 5.2, we show that this condition is met with orthogonal constructor rewriting.

We assume familiarity with typed λ-calculus [Bar92], reducibility [Gal89, Kri90] and rewriting [Ter03]. Concerning CCERSs, we refer to [GKK05]. The paper (except Sect. 5.2) is based on parts of the Phd thesis of the author [Rib07a] (in French).

2 Simply Typed λ-Calculus with Constructor Rewriting

Given a set A, a⃗ denotes a finite sequence of elements of A of length |a⃗|.

Terms and types. A signature Σ is a family of sets (Σ_{n} )_{n∈ℕ} such that Σ_{n} contains algebraic symbols of arity n. We consider λ-terms with uncurried symbols f in a signature Σ and variables x ∈ X:

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

where f ∈ Σ_{n}. Let Λ be the set of pure λ-terms Λ(∅). A substitution is a function σ : X ) Λ(Σ) of finite domain. The capture avoiding application of σ to the term t is written tσ or t[σ(x_{1})/x_{1}, …, σ(x_{n} )/x_{n} ] if Dom(σ) = {x_{1}, …, x_{n} }.

Given base types B ∈ B, simple types are defined as usual:

T, U ∈ T (B) ::= B | U } T .

Typing contexts are functions Γ of finite domain from variables to types, written x_{1} : T_{1}, …, x_{n} : T_{n}. Given a type assignment τ : Π_{n∈ℕ} .Σ_{n} ) T (B)^{n+1} , the typing relation Γ ⊢_{τ} t : T is inductively defined by the following rules:

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

(Symb) \frac{Γ ⊢_{τ} t_{1} : T_{1} … Γ ⊢_{τ} t_{n} : T_{n}}{Γ ⊢_{τ} f(t_{1}, …, t_{n} ) : T}τ(f) = (T_{1}, …, T_{n} , T)

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

Constructor rewriting. Assume given a set C ⊆ Σ of constructor symbols c of type (T⃗, B) with B ∈ B. For normalization, B must occur only at positive positions in T⃗ [Men87]. As we are not interested in strong normalization conditions, we do not care of this restriction here.

A constructor rewrite system (or rewrite system) on C is a set R of rewrite rules f(l⃗) )_{R} r such that r ∈ Λ(Σ), FV(r) ⊆ FV(f(l⃗)), f ∈ Σ\C (defined symbols are not constructors) and l⃗ are terms of the grammar

p ::= x | c(p_{1}, …, p_{n} ) ,

where c ∈ C (hence, l⃗ are patterns).

A rewrite system R is typed if for each rewrite rule f(l⃗) )_{R} r with τ(f) = (T⃗, T), there exists a (necessarily unique) context Γ with Dom(Γ) = FV(f(l⃗)) such that

Γ ⊢_{τ} f(l⃗) : T  and  Γ ⊢_{τ} r : T .

Example 2.1. We consider the type Nat of Peano’s numbers, with constructors 0 : Nat and S : (Nat, Nat). The following system, defining addition, is a constructor rewrite system:

plus(x, 0) ) x plus(x, S(y)) ) plus(S(x), y) .

Reductions. A rewrite relation is a binary relation )_{R} ⊆(Λ(Σ) \ X ) × Λ(Σ ) which is stable by contexts and substitutions. We let (t)_{R} =_{def} {v | t )_{R} v} and say that a term t is R-reducible (or reducible) if (t)_{R} ≠ ∅. We define the product extension of )_{R} as (t_{1}, …, t_{n} ) )_{R} (u_{1}, …, u_{n} ) when there is k ∈ {1, …, n} such that t_{k} )_{R} u_{k} and t_{i} = u_{i} for all i ≠ k. We denote by SN_{R} the set of strongly normalizing terms for )_{R}, which is the smallest set of terms such that

∀t. (∀u. t )_{R} u =} u ∈ SN_{R}) =} t ∈ SN_{R} .

Given a constructor rewrite system R, we let )_{βR} be the smallest rewrite relation on Λ(Σ) containing )_{R} and β-reduction: (λx.t)u )_{β} t[u/x].

3 Reducibility Families

In this section, we present a general notion of reducibility family and of type interpretation. We then briefly take a look at their instantiation to deal with the pure λ-calculus and with the combination of λ-calculus with rewriting.

Definition 3.1. Let )_{R} be a rewrite relation on Λ(Σ).

(i) The function space is the function } : 𝒫(Λ(Σ))^{2} ) 𝒫(Λ(Σ)) defined as

A } B =_{def} {t | ∀u. u ∈ A =} t u ∈ B} .

(ii) A reducibility family for )_{R} is a set of sets ℛed ⊆ {A | X ⊆ A ⊆ SN_{R}} which is closed by intersections and by the function space.

(iii) A type interpretation in ℛed is a map ⟦ ⟧ : T (B) ) ℛed such that for all

T, U ∈ T (B) we have ⟦U } T⟧ = ⟦U⟧ } ⟦T⟧. (iv) A type interpretation ⟦ ⟧ is adequate if for all Γ, t, T and σ we have

(Γ ⊢_{τ} t : T ∧ σ ⊧_{⟦ ⟧} Γ) =} tσ ∈ ⟦T⟧ ,

where σ ⊧_{⟦ ⟧} Γ iff σ(x) ∈ ⟦Γ(x)⟧ for all x ∈ Dom(Γ).

Pure λ-calculus. Let ℛed be a reducibility family and ⟦ ⟧ : T (B) ) ℛed be a type interpretation. Let us see, in the case of the pure λ-calculus, some sufficient conditions to ensure that ⟦ ⟧ is adequate. As usual, we reason by induction on Γ ⊢ t : T and by cases on the last applied typing rule.

We only have to check the rules (Ax), (} E) and (} I). The rule (Ax) is trivial while (} E) is dealt with by definition of the function space } . Concerning the rule (}I), it is sufficient that for all A ∈ ℛed,

∀t, u ∈ Λ. (t[u/x] ∈ A ∧ u ∈ SN_{β} ) =} (λx.t)u ∈ A .  (1)

As for X ⊆ A ⊆ SN_{β} , condition (1) has to be preserved by } : ℛed^{2} ) ℛed. We can conveniently formulate this by using elimination contexts [Abe04]. For the pure λ-calculus, they are defined by the grammar

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

Then, we get the following clauses: for all E[ ] ∈ E, all x ∈ X and all t, u ∈ Λ,

E[ ] ∈ SN_{β} =} E[x] ∈ A ,  (2)
(E[t[u/x]] ∈ A ∧ u ∈ SN_{β} ) =} E[(λx.t)u] ∈ A .  (3)

The sets A ⊆ SN_{β} satisfying (2) and (3) are Tait’s saturated sets [Tai75]. The set of saturated sets, denoted by 𝒮𝒜𝒯_{β} , forms a reducibility family.

Remark 3.2. Note that properties (2) and (3) use call-by-name evaluation contexts to prove strong normalization of the full reduction )_{β} .

Showing that 𝒮𝒜𝒯_{β} is not empty amounts to showing that SN_{β} ∈ 𝒮𝒜𝒯_{β} . We must check properties (2) and (3) with A = SN_{β} , which in this case are consequences of two important facts. First, a reduction step from a term of the form E[(λx.t)u] (resp. E[x]) occurs either in the elimination context E[ ] or in the term (λx.t)u, but involves no interaction between them:

∀v. E[x] )_{β} v =} (v = E′[x] with E[ ] )_{β} E′[ ])  (4)
∀v. E[(λx.t)u] )_{β} v =} (v = E′[s] with (E[ ], (λx.t)u) )_{β} (E′[ ], s))  (5)

Second, property (3) follows from (5) and the fact that (λx.t)u ∈ SN_{β} as soon as t[u/x] ∈ SN_{β} and u ∈ SN_{β} . This property holds in turn thanks to the Weak Standardization Lemma, which was used in [Alt93] for extensions of the Calculus of Constructions. It is obvious for the pure λ-calculus.

Lemma 3.3 (Weak Standardization). A reduct of a β-redex (λx.t)u is either t[u/x] or a β-redex (λx.t′)u′ with (t, u) )_{β} (t′, u′). λ-calculus with rewriting. To deal with rewriting, we must consider the rule (Symb). For constructors, we have to use specific interpretations of base types (eg. using inductive types, as in [BJO02]). We concentrate on symbols f ∈ Σ \ C. Given f of type (T⃗, T) and t⃗ ∈ ⟦T⃗⟧, we have to make sure that f(t⃗) ∈ ⟦T⟧. Sufficient conditions for this are given by termination criteria, a subject that we do not treat in this paper (see for instance [BJO02, Abe04, Abe06, BGP06, BR06]).

Here, we are interested in the exploration of reducibility families that allow to formulate termination criteria. As for the λ-calculus, we can use a non-interaction property similar to (5):

∀v. E[f(t⃗)] )_{βR} v =} (v = E′[s] with (E[ ], f(t⃗)) )_{βR} (E′[ ], s)) . (6)

But rewrite systems do not satisfy in general the weak standardization lemma. Therefore, in order to get f(t⃗) ∈ SN_{βR} , we need v ∈ SN_{βR} for all v such that f(t⃗) )_{βR} v. This is subsumed by the clause

(∀v. E[f(t⃗)] )_{βR} v =} v ∈ A)  =} E[f(t⃗)] ∈ A .  (7)

In this case, we also need saturated sets to be stable by reduction: if t ∈ A and t )_{βR} u then u ∈ A.

4 Neutral Terms and Reducibility Candidates

We now turn to Girard’s reducibility candidates [Gir72]. They form a reducibility family in which properties (3) and (7) can be formulated in a uniform and elegant way. This is due to neutral terms, that enjoy non-interaction properties such as (4), (5) and (6).

We first give a general formulation, and then apply it to constructor rewriting.

4.1 A General Formulation

We give a generalization of the original notion of neutral terms that allows to define reducibility candidates in a generic way. The key idea is that neutral terms are the terms that do not interact with elimination contexts. In the whole section, we assume given a rewrite relation )_{R}.

Elimination contexts will be defined as a special case of evaluation contexts.

Definition 4.1 (Evaluation Contexts). Let [ ] ∈ X be a distinguished variable. A set of evaluation contexts for )_{R} is a set E of terms E[ ] which is

(i) stable by reduction: if E[ ] ∈ E and E[ ] )_{R} t then t = F[ ] ∈ E; (ii) stable by composition: if E[ ] ∈ E and F[ ] ∈ E then E[F[ ]] ∈ E, where

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

We now assume given a set E of evaluation contexts for )_{R}.

Definition 4.2 (Neutral Terms). A term t is neutral for )_{R} in E if for all E[ ] ∈ E,

∀v. E[t] )_{R} v =} (v = E′[t′] with (E[ ], t) )_{R} (E′[ ], t′)) .

We denote by N_{RE} the set of neutral terms for )_{R} in E.

The terms that are not neutral interact with evaluation contexts. They are therefore observable, and we think of them as being values.

Definition 4.3 (Values). A value for )_{R} in E is a term which is not neutral. We denote by V_{RE} the set of values for )_{R} in E.

Example 4.4. For the pure λ-calculus, taking E} as evaluation contexts, the values are exactly the terms of the form λx.t. Hence values are determined by the shape of evaluation contexts. Thanks to Weak Standardization (Lem. 3.3), we can use call-by-name evaluation contexts to prove the strong normalization of the full β-reduction (see also Rem. 3.2).

To build reducibility candidates, we are interested in neutral terms and evaluation contexts that enjoy some properties. This leads to the notion of elimination contexts.

Definition 4.5 (Elimination Contexts). Let E be a set of evaluation contexts for )_{R}. Then E is a set of elimination contexts for )_{R} if

(i) all variables are neutral: X ⊆ N_{RE}, (ii) if t ∈ N_{RE} and E[ ] ∈ E then E[t] ∈ N_{RE}.

Example 4.6. For the pure λ-calculus, E} is a set of elimination contexts.

We now define reducibility candidates in the usual way: our generalization regards neutral terms and their definition using elimination contexts. Assume that E is a set of elimination contexts for )_{R}.

Definition 4.7 (Reducibility Candidates). The set 𝒞ℛ_{RE} of reducibility candidates for )_{R} in E is the set of all C ⊆ SN_{R} such that

(𝒞ℛ0) if t ∈ C and t )_{R} u then u ∈ C, (𝒞ℛ1) if t ∈ N_{RE} and ∀u. t )_{R} u =} u ∈ C then t ∈ C.

Note that 𝒞ℛ_{RE} is a complete lattice for ⊆ whose top element is SN_{R} and whose greatest lower bounds are intersections. In order to verify that X is contained in any candidate, it is interesting to look at the least reducibility candidate. This is HN_{RE}, the set of hereditary neutral terms, defined as the smallest set of terms such that

∀t ∈ N_{RE}. (∀u. t )_{R} u =} u ∈ HN_{RE}) =} t ∈ HN_{RE} .

Since variables are neutral terms in normal form (recall that by assumption )_{R} ⊆(Λ(Σ) \ X ) × Λ(Σ )), we have X ⊆ HN_{RE} ⊆ C for every C ∈ 𝒞ℛ_{RE}.

The non-interaction between neutral terms and elimination contexts has the following simple but fundamental consequence.

Lemma 4.8. Let t ∈ N_{RE} and E[ ] ∈ E ∩ SN_{R}. Then, for all C ∈ 𝒞ℛ_{RE},

(∀u. t )_{R} u =} E[u] ∈ C) =} E[t] ∈ C .

Proof. First, since t ∈ N_{RE} and E[ ] ∈ E, we have E[t] ∈ N_{RE} by Def. 4.5.(ii). Hence, we only have to show that (E[t])_{R} ⊆ C.

We reason by induction on E[ ] ∈ SN_{R}. Let v such that E[t] )_{R} v. Since t is neutral, we have v = E′[t′] with (E[ ], t) )_{R} (E′[ ], t′), and there are two cases.

Case of E[ ] )_{R} E′[ ]. We have E′[ ] ∈ E by Def. 4.1.(i) and E′[ ] ∈ SN_{R} since E[ ] ∈ SN_{R}. For all u ∈ (t)_{R}, since E[u] )_{R} E′[u] and E[u] ∈ C, we have E′[u] ∈ C by (𝒞ℛ0). Hence, we can apply the induction hypothesis on E′[ ] and we conclude that E′[t] ∈ C.

Case of t )_{R} t′. In this case, we have E[t′] ∈ C by assumption. ⊓ ⊔

We now give a sufficient condition for 𝒞ℛ_{RE} to be a reducibility family (in the sense of Def. 3.1) when E contains [ ]t for all t ∈ SN_{R}. The key point is to show that } is a function from 𝒞ℛ_{RE}^{2} to 𝒞ℛ_{RE}. We rely on Lem. 4.8.

Lemma 4.9. If E contains [ ] t for all t ∈ SN_{R} and moreover [ ]t ∈ SN_{R} for all t ∈ SN_{R}, then 𝒞ℛ_{RE} is a reducibility family.

Proof. It remains to show that } : 𝒞ℛ_{RE}^{2} ) 𝒞ℛ_{RE}. Let A, B ∈ 𝒞ℛ_{RE}. First, we have A } B ⊆ SN_{R}: for all t ∈ A } B, since X ⊆ A we have tx ∈ B ⊆ SN_{R}, hence t ∈ SN_{R}. Let us now check the clauses (𝒞ℛ0) and (𝒞ℛ1).

(𝒞ℛ0) Let t ∈ A } B and u ∈ (t)_{R}. For all a ∈ A, we have ta ∈ B, hence ua ∈ B

by (𝒞ℛ0) applied to B. It follows that u ∈ A } B. (𝒞ℛ1) Let t ∈ N_{RE} such that (t)_{R} ⊆ A } B and let a ∈ A. For all u ∈ (t)_{R}, we

have ua ∈ B. Since [ ] a ∈ SN_{R}, it follows from Lem. 4.8 that ta ∈ B. We conclude that t ∈ A } B. ⊓ ⊔

Example 4.10. For the pure λ-calculus, 𝒞ℛ_{βE}} is the usual set of reducibility candidates. In particular, each C ∈ 𝒞ℛ_{βE}} satisfies property (3).

4.2 Application to Constructor Rewriting

Let R be a constructor rewrite system on C. If we use elimination contexts of the form E} , then the values are the terms of the form λx.t.

However, we would like to build values from constructors. This is particularly useful with inductive types [BJO02]. According to Def. 4.3, we have to make them observable. To this end, we introduce appropriate destructors in elimination contexts. To each c ∈ C of type (T⃗, B) with |T⃗| > 0 and each i ∈ {1, …, |T⃗|}, we associate a new unary destructor symbol d_{c,i} defined by the rewrite rule

d_{c,i} (c(x_{1}, …, x_{n} )) )_{D} x_{i} .

Let ℧ be a new nullary symbol. For the elimination of a nullary constructor c, we use a new unary destructor d_{c} defined by the rewrite rule

d_{c}(c) )_{D} ℧ .

Lemma 4.11. Let E_{}C} be the set of terms defined by the grammar

E[ ] ∈ E_{}C} ::= [ ] | E[ ] t | d(E[ ]) ,

where d is a destructor of a constructor of C. Then,

(i) E_{}C} is a set of evaluation contexts for )_{βRD} . (ii) The values in E_{}C} for )_{βRD} are exactly the terms of the form

– λx.t; or

– c(t⃗) with c ∈ C. (iii) E_{}C} is a set of elimination contexts for )_{βRD} . (iv) Each C ∈ 𝒞ℛ_{βRDE}C} satisfies properties (3) and (7).

Proof.

(i) It is clear that E_{}C} is a set of evaluation contexts for )_{βRD} . (ii) It is clear that the terms of (ii) are values. We check that if t is a value,

then it is in one of these forms. Assume now that E[ ] ∈ E_{}C} is a minimal context that interacts with t. Note that the top symbol of E[ ] is either an application or a destructor d. We consider these two cases: The top symbol of E[ ] is an application. In this case, E[ ] is of the

form F[ ] u. By minimality, F[ ] = [ ] and t is an abstraction. The top symbol of E[ ] is a destructor. In this case, E[ ] is of the form

d(F[ ]). By minimality, F[ ] = [ ] and t is a constructor. (iii) The fact that E_{}C} is a set elimination contexts is a direct consequence of

the shape of values (ii). (iv) From (ii) we know that terms of the form (λx.t)u and f(t⃗) with f ∈ Σ \ C

are neutral. Properties (3) and (7) then follow from Lem. 4.8. ⊓ ⊔

Example 4.12. Consider the system presented at example 2.1. Its values are the terms of the form

λx.t  S(t)  0 .

Indeed, we have

(λx.t) u )_{β} t[u/x]  d_{S,1} (S(t)) )_{D} t  d_{0}(0) )_{D} ℧ .

5 Stability by Union

A reducibility family ℛed is stable by union if

∀ℛ. ℛ ⊆ ℛed  =}  ⋃ ℛ ∈ ℛed .

The main question on stability by union is the following: given a rewrite relation )_{R}, does there exists a reducibility family ℛed for )_{R} which is stable by union and leads to an adequate type interpretation?

For the pure λ-calculus, it is well-known that the answer is positive: Tait’s saturated sets (presented in Sect. 3) are stable by union and lead to an adequate type interpretation. This has been exploited for instance in [Abe06, Tat07].

The question becomes more difficult with rewriting. We have seen in Sect. 3 that rewrite systems do not satisfy in general the weak standardization lemma (Lem. 3.3), and that we need a reducibility family satisfying a clause like (7). But this is precisely what makes stability by union difficult. Assume given ℛ ⊆ ℛed such that for all v ∈ (E[f(t⃗)])_{βR} , we have v ∈ ⋃ ℛ. Then, unless we find some A ∈ ℛ such that (E[f(t⃗)])_{βR} ⊆ A, there is no reason to have E[f(t⃗)] ∈ ⋃ ℛ.

Besides, using intersection and union types, we have shown in [Rib07c] that there are confluent typed rewrite systems for which no reducibility family that is stable by union leads to an adequate type interpretation.

However, we can in some cases obtain a reducibility family which is stable by union. In [Rib07b], we have given a necessary and sufficient condition for reducibility candidates to be stable by union; and in [Rib07c], we have given a necessary and sufficient condition for the closure by union of biorthogonals [Gir87, Par97, DK00] to be reducibility candidates. The second condition is strictly more general than the first one.

We now recall the condition established in [Rib07b] for the stability by union of reducibility candidates, and then show that it is met with orthogonal constructor rewriting.

5.1 Reducibility Candidates

The study of stability by union of reducibility candidates of [Rib07b] carries over to our generalization of neutral terms and elimination contexts. The key observation is a characterization of the membership of a term to a candidate using a weak observational preorder.

Definition 5.1. Let t ≲_{N} u if and only if t, u ∈ SN_{R} and

∀v ∈ V_{RE}. t )_{R}^{∗} v =} u )_{R}^{∗} v .

Every candidate C ∈ 𝒞ℛ_{RE} is a non-empty subset of SN_{R} which is downwardclosed wrt. ≲_{N}. Reducibility candidates are stable by union exactly when the converse is also true.

Theorem 5.2 ([Rib07b]). The following are equivalent:

(i) 𝒞ℛ_{RE} is stable by union; (ii) 𝒞ℛ_{RE} is the set of all non-empty C ⊆ SN_{R} which are downward-closed wrt.

the preorder ≲_{N}; (iii) every strongly normalizable neutral term t which is reducible has a reduct

u such that t ≲_{N} u. Such u is a strong principal reduct^{1}of t.

1 Called ”principal reduct” in [Rib07b].

Proof. For each t ∈ SN_{R}, we let 𝒞ℛ(t) be the smallest reducibility candidate containing t. Note that 𝒞ℛ(t) = {u | u ≲_{N} t}.

(i) =} (ii). Let C ⊆ SN_{R} be a non-empty set downward-closed wrt. ≲_{N}. Since 𝒞ℛ(t) is downward closed wrt. ≲_{N} for all t ∈ SN_{R}, C = ⋃{𝒞ℛ(t) | t ∈ C}. Hence C ∈ 𝒞ℛ because 𝒞ℛ is stable by union.

(ii) =} (iii). Let t ∈ N ∩ SN_{R} be reducible. For all u ∈ (t)_{R}, the set 𝒞ℛ(u) is non-empty and downward-closed wrt. ≲. Therefore, the set C of all v such that v ∈ 𝒞ℛ(u) for some u ∈ (t)_{R} is non-empty and downward-closed wrt. ≲_{N}. It follows that C ∈ 𝒞ℛ and that t ∈ C since (t)_{R} ⊆ C. Hence there is u ∈ (t)_{R} such that t ≲_{N} u.

(iii) =} (i). Let ∅ ≠ C ⊆ 𝒞ℛ. In order to show ⋃ C ∈ 𝒞ℛ, the key-point is to show that if t ∈ N is such that (t)_{R} ⊆ ⋃ C then t ∈ ⋃ C. If (t)_{R} = ∅ then t ∈ C for all C ∈ C and we are done. Otherwise, we have t ∈ SN_{R} since (t)_{R} ⊆ ⋃ C ⊆ SN_{R}. Let u be a strong principal reduct of t. There is C ∈ C such that u ∈ C, and since t ≲_{N} u and C is downward-closed wrt. ≲_{N}, we have t ∈ C, hence t ∈ ⋃ C. ⊓ ⊔

Example 5.3 ([Rib07b, Tat07]). For the pure λ-calculus, thanks to the weak standardization lemma (Lem. 3.3), 𝒞ℛ_{βE}} is stable by union.

5.2 Application to Orthogonal Constructor Rewriting

Recall that a rewrite system R is orthogonal if it is left-linear and has no critical pairs [Ter03]. For instance, the system of Ex. 2.1 is orthogonal.

In this section, we show that if R is an orthogonal constructor rewrite system, then 𝒞ℛ_{βRDE}C} is stable by union. According to Thm. 5.2, this amounts to showing that every strongly normalizing reducible neutral term has a strong principal reduct. We prove it by using a general theorem on external redexes [KOvO01] (see also [GKK05]). This result applies to the framework of orthogonal CCERSs, of which our higher-order rewrite systems β ∪ R ∪ D are an instance.

To prove our result, we need some machinery to deal with the term structure. We use the following standard notations: a position in a term t is a finite word on ℕ \ {0}, ϕ · ψ denotes the concatenations of the words ϕ and ψ. Moreover, t|_{ϕ} is the subterm of t at position ϕ, and t[u]_{ϕ} is the term t in which the subterm of t at position ϕ is textually replaced by u.

The notion of descendant, which is standard in rewriting theory, is used to trace terms during reduction. We do not detail the definition which is quite technical and can be found in standard textbooks [Ter03], but we provide an example.

Example 5.4. Consider the derivation

P : (λx.plus(x, 0)) 0 plus(y, S(z)) )_{β} plus(0, 0) plus(y, S(z))

– The β-redex (λx.plus(x, 0)) 0 has no descendant along P.

– The first occurrence of 0 in plus(0, 0) is the only descendant along P of the argument 0 of the β-redex (λx.plus(x, 0)) 0.

– plus(0, 0) is the only descendant of plus(x, 0) along P.

– plus(y, S(z)) is the only descendant of plus(y, S(z)) along P.

We use the notions of redex-arguments and of external redexes of [KOvO01, GKK05].

Definition 5.5. A term u is a redex-argument of t if either

(i) t has a subterm of the form (λx.t_{1})t_{2} and u is a subterm of t_{1} or t_{2}, or (ii) t has a subterm of the form lσ, where l )_{R} r is a rewrite rule and σ a

substitution, and there is a variable x of l such that u is a subterm of σ(x).

The key notion is that of external redex.

Definition 5.6. A redex at position ϕ in a term t is external if for any derivation P : t )_{βRD}^{∗} v, no descendant of ϕ along P appears inside redex-arguments.

Hence every descendant of an external redex is external. Note that every external redex is outermost, but the converse is false.

Using external redexes, we have the following weak standardization lemma. We apply it in Lem. 5.8 to show that every neutral term which has an external redex has a strong principal reduct.

Lemma 5.7 (Weak Standardization). Assume that R is orthogonal. Let t )_{βRD} u by contracting an external redex of t. If t )_{βRD} v by contracting a different redex, then there is w such that u )_{βRD}^{∗} w and v )_{βRD} w by contracting a descendant of t )_{βRD} u (which is therefore external in v).

Proof. Let ϕ and ψ be the respective positions of the redexes contracted in t )_{βRD} u and t )_{βRD} v. We show that there exists w such that the redex contracted in v )_{βRD} w is a descendant of ϕ. It is an external redex of v because ϕ is external in t.

Note that since ϕ is external in t, for every ϕ_{1}, ϕ_{2} such that ϕ = ϕ_{1} · ϕ_{2}, ϕ_{2} is external in t|_{ϕ_{1}} : if a descendant ϕ′_{2} of ϕ_{2} appears in a redex argument of a reduct u of t|_{ϕ_{1}} , then ϕ_{1} · ϕ′_{2}, which is a descendant of ϕ, appears in a redex argument of t[u]_{ϕ_{1}} , which is a reduct of t.

We now reason by induction on t.

t ∈ X. Not possible. t = λx.t_{1}. In this case, u = λx.u_{1} and v = λx.v_{1}. Moreover we have ϕ = 1 · ϕ_{1},

ψ = 1 · ψ_{1}, t_{1} )_{βRD} u_{1} by contracting ϕ_{1} and t_{1} )_{βRD} v_{1} by contracting ψ_{1}. Since ϕ_{1} is external in t_{1}, by induction hypothesis there is w_{1} such that u_{1} )_{βRD}^{∗} w_{1} and v_{1} )_{βRD} w_{1} by contracting a descendant of ϕ_{1}. It follows that u )_{βRD}^{∗} λx.w_{1} and v )_{βRD} λx.w_{1} by contracting a descendant of ϕ.

t = t_{1} t_{2} with t_{1} not an abstraction. There are i, j ∈ {1, 2} such that ϕ = i · ϕ_{1} and ψ = j · ψ_{1}. Moreover, u = u_{1} u_{2} and v = v_{1} v_{2} with t_{i} )_{βRD} u_{i}, t_{j} )_{βRD} v_{j}, u_{j} = t_{j} and v_{i} = t_{i}. There are two cases. If i = j, then we reason as in the case of t = λx.t_{1}.

Otherwise i ≠ j. Let w = w_{1} w_{2} with w_{i} = u_{i} and w_{j} = v_{j}. We have

u )_{βRD} w and v )_{βRD} w by contracting a descendant of ϕ.

t = (λx.t_{1})t_{2}. Since ϕ is external in t, ϕ is the root β-redex of t. Therefore u = t_{1}[t_{2}/x] and v = (λx.t′_{1})t′_{2} with (t_{1}, t_{2}) )_{βRD} (t′_{1}, t′_{2}). We are done by taking w =_{def} t′_{1}[t′_{2}/x] since (λx.t′_{1})t′_{2} is a descendant of (λx.t_{1})t_{2} and

t_{1}[t_{2}/x] )_{βRD}^{∗} t′_{1}[t′_{2}/x].

t = f(t⃗) and t is not a RD-redex. We reason as in the case of t_{1} t_{2} with t_{1}

not an abstraction. t = f(t⃗) and t is a RD-redex. Since ϕ is external in t, it is the roof RD-redex

of t. Hence there is a rule l )_{RD} r and a substitution σ such that t = lσ and u = rσ. Because l is linear, there is a substitution σ′ such that σ )_{βRD} σ′ and v = lσ′. We are done by taking w =_{def} rσ′ since lσ′ is a descendant of lσ and rσ )_{βRD}^{∗} rσ′. ⊓ ⊔

Lemma 5.8. Assume that R is orthogonal and let t ∈ N_{βRDE}C} . If t )_{βRD}^{∗} v with v ∈ V_{βRDE}C} , then for all u such that t )_{βRD} u by contracting an external redex of t, we have u )_{βRD}^{∗} v.

Proof. Let u such that t )_{βRD} u by contracting an external redex of t and let v ∈ V_{βRDE}C} such that t )_{βRD}^{∗} v. Since t is neutral, we have t )_{βRD}^{+} v. We reason by induction on the length of the derivation.

Base Case. Since t is neutral, it follows from Lem. 4.11.(ii) that t )_{βRD} v by contracting a top redex of t. Since every external redex is outermost, it follows that every external redex of t is a root redex of t. By orthogonality, this is the redex contracted in t )_{βRD} v, and we have u = v.

Induction Case. Assume that t )_{βRD} s )_{βRD}^{∗} v. If s is a value, then reasoning as in the base case we have s = u, hence u )_{βRD}^{∗} v. Otherwise s is neutral. If s is obtained from t by contracting the same redex as in t )_{βRD} u, then s = u and u )_{βRD}^{∗} v. Otherwise, by weak standardization (Lem. 5.7), there is w such that u )_{βRD}^{∗} w and s )_{βRD} w by contracting an external redex of s. We then have w )_{βRD}^{∗} v by induction hypothesis, hence u )_{βRD}^{∗} v. ⊓ ⊔

If t is neutral and t )_{βRD} u by contracting an external redex of t, then we have t ≲_{N} u. Hence u is a strong principal reduct of t. Then, by Thm. 5.2 𝒞ℛ_{βRDE}C} is stable by union if all neutral terms have external redexes. It remains to show this last property, which follows from the next theorem, proved in [KOvO01]. We can apply it because the CCERS β ∪ R ∪ D is orthogonal as soon as the rewrite system R is orthogonal.

Theorem 5.9 ([KOvO01, GKK05]). If R is orthogonal then every reducible term has an external redex.

Theorem 5.10. If R is orthogonal then 𝒞ℛ_{βRDE}C} is stable by union.

References

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

[Abe06] A. Abel. Semi-Continuous Sized Types and Termination. In Proceedings of CSL’06, volume 4207 of LNCS, pages 72–88. Springer, 2006. 1, 5, 9

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

[Bar92] H.P. 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

[BGP06] G. Barthe, B. Grégoire, and F. Pastawski. Type-Based Termination of Recursives Definitions in the Calculus of Inductive Constructions. In Proceedings of LPAR’06, pages 257–271, 2006. 1, 5

[BJO02] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-Data-Types Systems. Theoretical Computer Science, 271:41–68, 2002. 1, 5, 7

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

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

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

[Gir72] J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur. PhD thesis, Université Paris 7, 1972. 1, 5

[Gir87] J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1–102, 1987. 1, 9

[GKK05] J. Glauert, D. Kesner, and Z. Khasidashvili. Expression Reduction Systems and Extensions: An Overview. In Processes, Terms and Cycles: Steps to the Road of Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of LNCS, pages 496–553. Springer, 2005. 2, 10, 11, 12

[KOvO01] Z. Khasidashvili, M. Ogawa, and V. van Oostrom. Perpetuality ans Uniform Normalization in Orthogonal Rewrite Systems. Information and Computation, 164(1):118–152, 2001. 1, 10, 11, 12

[Kri90] J.-L. Krivine. Lambda-Calcul, Types et Modèles. Masson, 1990. 2

[Men87] N. P. Mendler. Recursive Types and Type Constraints in Second Order Lambda-Calculus. In Proceedings of LiCS’87, pages 30–36. IEEE Computer Society, 1987. 3

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

[Rib07a] C. Riba. Definitions par Réécriture dans le λ-Calcul: Confluence, Réductibilité et Typage. PhD thesis, INPL, 2007. 2

[Rib07b] C. Riba. On the Stability by Union of Reducibility Candidates. In Proceedings of FoSSaCS’07, volume 4423 of LNCS, 2007. 1, 9, 10 [Rib07c] C. Riba. Strong Normalization as Safe Interaction. In Proceedings of

LiCS’07, pages 13–22. IEEE Computer Society, 2007. 9

[Tai75] W. W. Tait. A Realizability Interpretation of the Theory of Species. In R. Parikh, editor, Logic Colloquium, volume 453 of LNCS, pages 240–251, 1975. 1, 4

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

[Ter03] Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. M. Bezem, J.W. Klop and R.C. de Vrijer, eds. 2, 10