Modularity of Termination and Confluence in Combinations of Rewrite Systems with λ_{ω}

Franco Barbanera^{1}^{⋆} and Maribel Fernández^{2}

1 Dipartimento di Informatica, Corso Svizzera 185, 10149 Torino, Italy. E-mail: barba@di.unito.it 2 LRI Bât. 490, CNRS/Université de Paris-Sud, 91405 Orsay Cedex, France. E-mail: maribel@lri.fr

Abstract. We prove that termination and confluence are modular properties in combinations of the typed λ-calculus of order ω with (first or higher order) term rewrite systems, provided that the first order rewrite system is conservative (non-duplicating) and the higher order rewrite system satisfies some suitable conditions (the general schema) and does not introduce critical pairs.

1 Introduction

In the last years, many research efforts have been devoted to the study of the interactions between two closely related models of computation: the one based on β-reduction on λ-terms and the one formalized by means of rewrite rules on algebraic terms. Many interesting results (see [8], [9], [17], [3], [2], [14]) have been obtained concerning the modularity of strong normalization (or termination) and confluence of the combined relation. A property is called modular if the combination of two systems having this property inherits it.

Confluence and strong normalization are very useful properties in practice; strong normalization ensures that all reduction sequences are finite, whereas confluence establishes a kind of consistency of computations because it ensures that when two different terms u and v can be obtained by reducing some term t, there exists a common reduct of u and v. In [8] and [17] it is shown that the system obtained by combining a terminating first order many-sorted term rewrite system with the second order typed λ-calculus is again terminating with respect to β-reduction and the algebraic reductions induced by the rewrite rules, i.e. strong normalization is a modular property in this case. The same result is proven for confluence in [9]. In [14] both results are extended to combinations of first and higher order rewriting systems with second order λ-calculus, provided that suitable conditions are satisfied. Such conditions are that the higher order rules satisfy the so-called general schema (a generalization of primitive recursive definitions) and that the first order rules are conservative (also called non-duplicating), that is, the number of occurrences of each variable in the right

⋆ To Bianca and Massimo

hand side is less than or equal to the number of occurrences of the variable in the left hand side.^{3}

This last result is also valid when type assignment systems for λ-calculus are considered instead of explicitly typed calculi: in [4] it is shown that termination and confluence are modular properties of combinations of the intersection type assignment system (an extremely powerful system defined in [6]) with first and higher order algebraic rewrite systems, provided that the first order reductions are conservative and the higher order rules satisfy the general schema of Jouannaud and Okada. We rely on the results of [4] to obtain the main results of this paper.

Indeed the restriction to conservative reductions is also required to get modularity of termination in combinations of algebraic rewrite systems alone. In [20], Y. Toyama proved that confluence is modular for disjoint unions of term rewrite systems and conjectured that termination was also modular, but later H. Barendregt and J.W. Klop gave a counterexample to modularity of termination using a non-conservative rewrite system (see [19]). Modularity of termination for disjoint sums of conservative systems was proven in [18]. In practice, this restriction is not significative: most implementations of rewrite systems use sharing, and shared-reductions are always conservative since all the occurrences of a variable in a right hand side are shared.

A (practical) motivation for the investigation of combinations of λ-calculi with rewrite systems is that they provide an alternative for the design of new programming languages: the algebraic functional languages [14]. These languages allow algebraic definitions of data types and operators (as in equational languages like OBJ) and definition of higher order functions (as in functional languages like ML), in a unified framework. By the Curry-Howard isomorphism, some of these languages can also be seen as logical systems. From this point of view, it is better to consider more powerful type disciplines for λ-calculus than the ones considered up to now, such as the typed λ-calculus of order ω (Girard’s system F_{ω} [12]) or the Calculus of Constructions of Coquand and Huet [10]. As pointed out in [8], it would be useful to know whether the modularity results above hold also in these cases: confluence and termination ensure the consistency of the logical system.

We will show in this paper that this is true for the combination of the λcalculus of order ω (λ_{ω} in the following) with first and higher order rewrite systems, provided that the first order systems are conservative and the higher order systems satisfy the general schema of Jouannaud and Okada.

We will prove first the modularity of the strong normalization property. For this we give a proof based on a translation from λ_{ω} -terms to terms of the system described in [4], for which strong normalization is known. This mapping preserves all reduction sequences, and hence the strong normalization property of the former system is a direct consequence of the strong normalization property of the latter. Our proof of strong normalization generalizes to the problem discussed

3 Although not explicitly required in [14], the restriction to non-duplicating first order rules is necessary for the modularity of termination.

in this paper the proof in [2].

After proving the modularity of the strong normalization property, we will show that local confluence (or weak confluence) is also modular in combinations of λ_{ω} with first and higher order rewriting systems, provided that the higher order rules do not introduce critical pairs. To prove this we use an argument similar to the one used in [4] to prove the confluence of the combination of rewriting systems and type assignment systems. Since in strongly normalizing systems local confluence and confluence are equivalent, we get also a proof of confluence for the system λ_{ω} extended with first and higher order rewriting.

The modularity of strong normalization in combinations of λ_{ω} with first and higher order rewrite systems (a result interesting in itself) is also a first step towards proving the modularity of strong normalization in combinations of the Calculus of Constructions (λ_{C} in the following) with first and higher order rewrite systems: λ_{ω} is a subset of λ_{C} where types depending on terms are not allowed. An example of type depending on a term (taken from [5]) is A^{n} → B with n a natural number, defined by A^{0} → B = B; A^{n+1} → B = A → (A^{n} → B).

However, the generalization of this result to combinations of λ_{C} with rewrite systems is not straightforward. One of the difficulties concerns the Conversion Rule, which states that if a term t in λ_{C} has type T and T is convertible to T′ then t has also type T′. Of course, in the extension of λ_{C} with algebraic features the convertibility of types involves, besides β-conversion, the rewrite relation induced by the rewrite system, since types may depend on terms. Then one has to show that this relation has the same useful properties that β-conversion has. This problem will be the subject of future work.

2 Adding algebraic features to the typed λ-calculus of order ω

In the following we assume familiarity with typed λ-calculi and the way to present them used below (for more details see [5] and [7]). Let us define now λ_{ωRH} , the algebraic extension of the system λ_{ω} (called F_{ω} in [12]).

We consider a denumerable set S of sorts and define by induction the set T_{S} of arrow types based on S:

– If s ∈ S then s ∈ T_{S}

– If σ_{1}, …, σ_{n}, σ ∈ T_{S} then σ_{1} … σ_{n} → σ ∈ T_{S}. An extended signature F contains first and higher order function symbols:

F = ⋃_{τ∈T_{S}}F_{τ} where F_{τ} denotes a set of function symbols of type τ. We will

assume that F_{τ} ∩ F_{τ′} = ∅ if τ ≠ τ′. Let s_{1} … s_{n}, s ∈ S, and τ = s_{1} … s_{n} → s, then F_{τ} is a set of first order function symbols. We denote by Σ the set of all first order function symbols and by f, g its elements. We use F, G to denote higher order function symbols. When it is clear from the context, we use f to denote a generic (first or higher order) element of F.

System λ_{ωRH} is based on a set T of pseudo-expressions built out of variables (term and type variables), function symbols and sort symbols using application, abstraction and universal quantification. Pseudo-expressions are defined by the following abstract syntax:

T ::= x | ∗ | □ | f | s | T T | λx: T.T | Πx: T.T

where x ranges over the category of variables (divided into two groups: V ar^{∗} and V ar^{□} ), ∗ and □ are special constants (denoting respectively the set of types and the set of kinds of the system), s ranges over the set S of sorts and f ranges over the set F of function symbols. A declaration for a variable x is an expression of the form x : A, where A ∈ T. If A ∈ S we say that x is a first order variable.

In the following we shall denote simultaneous substitutions by {x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}}. Postfix notation will be used for their application, e.g. M{x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}} denotes the simultaneous substitution of N_{i} for x_{i} (1 ≤ i ≤ n) in M. When applying a substitution we must take care of bound variables, as usual. We shall use the symbol ϕ to denote a generic substitution.

On pseudo-expressions, the notions of β-reduction and β-conversion are defined by the contraction rule: (λu: A.B)C →_{β} B{u ↦ C}

In the following Γ will denote a context, that is, a finite sequence of declarations. The empty sequence will be denoted by ⟨⟩ and if Γ = ⟨x_{1} : A_{1}, …, x_{n} : A_{n}⟩ then Γ, x : B = ⟨x_{1} : A_{1}, …, x_{n} : A_{n}, x : B⟩.

A well-formed term for λ_{ωRH} of type B in Γ is a pseudo-expression A such that it is possible to derive Γ ⊢ A : B using a subset of the term formation rules listed below. Axioms

⟨⟩ ⊢ ∗ : □
⟨⟩ ⊢ s : ∗ for each s ∈ S
⟨⟩ ⊢ f : σ_{1} → … → σ_{n} → σ for each f ∈ F_{σ_{1}...σ_{n}→σ}
(σ_{1} → … → σ_{n} → σ is short for
Πx_{1}: σ_{1}.Πx_{2}: σ_{2} … Πx_{n}: σ_{n}.σ).

General Rules

Start rule  \frac{Γ ⊢ A : p}{Γ, u : A ⊢ u : A}  if p ∈ \{∗, □\}, u ∈ V ar^{p} and u ∉ Γ

Weakening rule \frac{Γ ⊢ A : B Γ ⊢ C : p}{Γ, u : C ⊢ A : B} if p ∈ \{∗, □\}, u ∈ V ar^{p} and u ∉ Γ

Application rule \frac{Γ ⊢ F : Πu: A.B Γ ⊢ C : A}{Γ ⊢ F C : B\{u ↦ C\}}

Conversion rule \frac{Γ ⊢ A : B Γ ⊢ B′ : p B =_{β} B′}{Γ ⊢ A : B′} if p ∈ \{∗, □\}.

Specific rules The specific rules are all introduction rules and are parametrized by ∗ and □; more precisely, they are (p_{1}, p_{2}) rules, with p_{1}, p_{2} ∈ {∗, □}.

Π-intro \frac{Γ ⊢ A : p_{1} Γ, u : A ⊢ B : p_{2}}{Γ ⊢ Πu: A.B : p_{2}}

λ-intro \frac{Γ ⊢ A : p_{1} Γ, u : A ⊢ b : B Γ, u : A ⊢ B : p_{2}}{Γ ⊢ λu: A.b : Πu: A.B}

The term formation rules of λ_{ωRH} are all the axioms and general rules and a particular subset of the set of specific rules, namely (∗, ∗), (□, ∗), (□, □). The specific term-formation rules have the following informal meaning: (∗, ∗) allows of forming terms depending on terms, (∗, □) allows of forming types depending on terms, (□, ∗) allows of forming terms depending on types, (□, □) allows of forming types depending on types. The set of terms of λ_{ωRH} is denoted in the following by Λ_{ωRH}.

2.1 Algebraic terms and rewrite rules

The set of higher order algebraic terms of type σ in λ_{ωRH} is inductively defined by:

1. If f ∈ F_{σ_{1}...σ_{n}→σ} (either first or higher order) and M_{1}, …, M_{n} (n ≥ 0) are algebraic terms of type σ_{1}, …, σ_{n} in Γ then fM_{1} … M_{n} is an algebraic term of type σ in Γ.

2. If x : σ_{1} … σ_{n} → σ ∈ Γ, with σ_{1} … σ_{n} → σ ∈ T_{S}, and M_{1}, …, M_{n} (n ≥ 0) are algebraic terms of type σ_{1}, …, σ_{n} in Γ then xM_{1} … M_{n} is an algebraic term of type σ in Γ.

It is easy to see that if M is algebraic, and Γ ⊢ M : σ, then the β-normal form of σ belongs to T_{S}. First order algebraic terms are algebraic terms in which only first order function symbols and first order variables occur.

We define now two sets of rewrite rules on algebraic terms:

1. a set R of first order rewrite rules whose elements are denoted by r : t → t′ where t, t′ are first order algebraic terms of the same sort in some context Γ, i.e. the rewriting rules of R are assumed sound with respect to types. Besides, in r : t → t′, t cannot be a variable and the set of variables in t′ must be a subset of the variables in t. R is conservative (also called non-duplicating) if for all r : t → t′ ∈ R and for all variables x in t, the number of occurrences of x in t′ is less than or equal to the number of occurrences of x in t.

2. a set HOR of higher order rewrite rules satisfying the general schema ([14]):

F l⃗[X⃗, x⃗] Y⃗ y⃗ → v[(F r⃗_{1}[X⃗, x⃗] Y⃗ y⃗), …, (F r⃗_{m}[X⃗, x⃗] Y⃗ y⃗), X⃗, x⃗, Y⃗ , y⃗]

where X⃗, Y⃗ are sequences of higher order variables; x⃗, y⃗ are sequences of first order variables; F is a higher order function symbol that can not appear in l⃗, v, r⃗_{1}, …, r⃗_{m}; both sides of the rule have the same type in some context Γ, the left hand side is an algebraic term and the right hand side v is a term in λ_{ωRH} ; l⃗, r⃗_{1}, …, r⃗_{m} are all terms of sort-type; X⃗ ⊆ Y⃗ and ∀i ∈ [1..m], l⃗ >_{mul} r⃗_{i} (where < denotes strict subterm ordering and >_{mul} denotes the multiset extension of >). The notation t[t_{1}, …, t_{n}] means that t_{1}, …, t_{n} are subterms of t.

The higher-order rules can be considered as definitions of new functionals of the language. There is a restriction that we have to impose on the set HOR: mutually recursive definitions are forbidden. This restriction, however, together with the one that the higher order variables in l⃗ must be included in Y⃗, could easily be removed (the first by introducing product types and packing mutually recursive definitions in a same product and the second by reasoning on a transformed version of F). The restriction that terms in r⃗_{i} are subterms of terms in l⃗, however, is essential in the proof of strong normalization of the combined language (see also [14] and [4]).

Although restricted, the general schema is interesting from a practical point of view: it allows for the introduction of functionals by primitive recursion on a first order data structure, as in the definition of the functional map in the following example (taken from [14]):

append nil l = l

append (cons x l) l′ = cons x (append l l′)

append (append l l′) l′′ = append l (append l′ l′′)

map X nil = nil

map X (cons x l) = cons (X x) (map X l) Here, the first order function append is defined algebraically (the third rule establishes the associativity of append on lists, and makes the definition non-primitive recursive), while the higher order function map is defined recursively on the structure of lists. See [14] for more examples and applications of the general schema.

Each rule in R and HOR induces a rewrite relation in λ_{ωRH} : Let M, M′ ∈ λ_{ωRH} , r : t → t′ ∈ R (resp. r : t → t′ ∈ HOR). Then M →^{r} M′ if there exists a subterm P of M such that P ≡ t{x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}} (where obviously N_{1}, …, N_{n} ∈ λ_{ωRH} ) and M′ is obtained from M by replacing the term t′{x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}} for P. Notice that since N_{1}, …, N_{n} ∈ λ_{ωRH} these can contain λ-terms. We write M →_{R} M′ (resp. M →_{HOR} M′) if M →^{r} M′ for some r : t → t′ ∈ R (resp. r : t → t′ ∈ HOR). By →_{R}^{∗}, →_{HOR}^{∗} we denote the reflexive and transitive closure of →_{R}, →_{HOR} respectively.

In the following →_{mix} denotes the reduction relation on terms of λ_{ωRH} obtained by the union of →_{β}, →_{R} and →_{HOR}. →_{mix}^{∗} denotes its transitive and reflexive closure, as usual.

2.2 Basic properties of λ_{ωRH}

We will use the notation Γ ⊢ M : A to denote the fact that indeed we can derive Γ ⊢ M : A in the system λ_{ωRH} . We let Γ ⊢ A : B : C stand for Γ ⊢ A : B and Γ ⊢ B : C. A → B is short for Πu: A.B when u is not a free variable in B. Finally, we denote by Context(λ_{ωRH} ) the set of all sequences of declarations for λ_{ωRH} .

If Γ ⊢ A : B : ∗, then A is called an object and B is called a type. The set of all objects in λ_{ωRH} is denoted in the following by Object(λ_{ωRH} ), and the set of all types by Type(λ_{ωRH} ). If Γ ⊢ A : B : □ then A is called a constructor and B is called a kind. The set of all the constructors in λ_{ωRH} is denoted in the following by Constructor(λ_{ωRH} ), and the set of all the kinds by Kind(λ_{ωRH} ). Notice that ∗ is a particular kind and that types are particular constructors. It can be shown that a term is either an object, a constructor or a kind.

Let Γ ∈ Context(λ_{ωRH} ), and Πz:B_{1}.B_{2}, λz: B_{1}.B_{2}, B_{1}, B_{2} ∈ Λ_{ωRH}. In the following we use the terminology:

1. Πz: B_{1}.B_{2} is formed by (p_{1}, p_{2}) in Γ if there are specific rules (p_{1}, p_{2}) ∈ λ_{ωRH} such that Γ ⊢ B_{1}: p_{1} and Γ, x: B_{1} ⊢ B_{2}: p_{2}.

2. λz: B_{1}.B_{2} is formed by (p_{1}, p_{2}) in Γ if there are specific rules (p_{1}, p_{2}) ∈ λ_{ωRH} such that Γ ⊢ λz: B_{1}.B_{2} : Πz: C_{1}.C_{2} and Πz: C_{1}.C_{2} is formed by (p_{1}, p_{2}) in Γ.

3. B_{1}B_{2} is formed by (p_{1}, p_{2}) in Γ if there are specific rules (p_{1}, p_{2}) ∈ λ_{ωRH} such that Γ ⊢ B_{1} : Πz: C_{1}.C_{2} and Πz: C_{1}.C_{2} is formed by (p_{1}, p_{2}) in Γ.

The following lemmas were proved in [11] for General Type Systems and hold also for the system in which we are interested (i.e. λ_{ωRH} ).

Lemma 1 Unicity of formation. Let Γ ∈ Context(λ_{ωRH} ), B ∈ Λ_{ωRH}. If B is formed by (p_{1}, p_{2}) in Γ and B is formed by (p′_{1}, p′_{2}) in Γ′ then p_{1} ≡ p′_{1} and p_{2} ≡ p′_{2}.

The Unicity of Formation Lemma allows us to use the terminology “formed by” without mentioning the context Γ.

Lemma 2. Let Γ ∈ Context(λ_{ωRH} ), t ∈ Λ_{ωRH}, and K be the set inductively defined by:

– ∗ ∈ K

– k_{1}, k_{2} ∈ K ⇒ k_{1} → k_{2} ∈ K.

then t ∈ Kind(λ_{ωRH} ) implies t ∈ K and ⟨⟩ ⊢ t : □.

Lemma 3. Let A, t ∈ Λ_{ωRH}. If A ∈ Constructor(λ_{ωRH} ) and t is a subexpression of A then t ∈ Kind(λ_{ωRH} ) or t ∈ Constructor(λ_{ωRH} ).

The relation →_{mix} enjoys the following important property:

Theorem 4 Generalized Subject Reduction for λ_{ωRH} . Let B, B′, C in Λ_{ωRH} and Γ ∈ Context(λ_{ωRH} ). Then Γ ⊢ B : C and B →_{mix}^{∗} B′ implies Γ ⊢ B′ : C.

3 Strong Normalization and Confluence of →_{mix} in λ_{ωRH}

The strong normalization of the combination of typed λ-calculus of order ω with terminating first order rewrite systems was proved in [2]. In this section we will extend that result, showing that λ_{ω} , enriched with first and higher order rewriting, is strongly normalizing whenever the first order rewrite system is terminating and conservative, and the higher order rewrite system satisfies the general schema. Moreover, we will prove that if the first order rewrite system is also confluent and the higher order rules do not introduce critical pairs then λ_{ωRH} is also confluent.

3.1 Strong Normalization of →_{mix}

The following lemma was proved in [12] for λ_{ω} (i.e. without algebraic features), but it holds also for λ_{ωRH} because the function symbols in F can be seen as free variables in β-reductions.

Lemma 5 [12]. If M ∈ Λ_{ωRH} then M is β-strongly normalizable.

In order to show that each term of λ_{ωRH} is →_{mix}-strongly normalizable we use the type assignment system ∧T RH of [4]. This system, but for its algebraic component, is the system devised in [6] without the universal type and the ≤ relation on types. It is a very powerful system indeed, since it can type precisely the set of strongly normalizable λ-terms (for a detailed proof see [1]).

Let us recall briefly the system ∧T RH. A type assignment system is defined by specifying a set of terms, a set of types and a set of type inference rules. For ∧T RH we have

1. The set T_{∧RH} of types is inductively defined by:

(a) α_{1}, α_{2}, … ∈ T_{∧RH} (type variables, a denumerable set which we shall denote by V_{T})

(b) S (the set of sorts) is included in T_{∧RH}

(c) σ, τ ∈ T_{∧RH} ⇒ σ → τ ∈ T_{∧RH} (arrow types).

(d) σ, τ ∈ T_{∧RH} ⇒ σ ∧ τ ∈ T_{∧RH} (intersection types). Intersection is

associative, commutative and idempotent.

2. The terms we consider are pure λ-terms built out of a denumerable set of variables and a set of constants. The set of constants has exactly the function symbols of F as elements.

3. A basis is a set of statements of the form x : σ, where x is a variable and σ ∈ T_{∧RH}. If x does not occur in the basis B, then B, x : σ denotes the basis B ∪ {x : σ}. The type inference rules are the following :

(Ax) B, x : σ ⊢ x : σ (Ax) B ⊢ f : σ, if f ∈ F_{σ}

(→I) \frac{B, x : σ ⊢ M : τ}{B ⊢ λx.M : σ → τ} (→E) \frac{B ⊢ M : σ → τ B ⊢ N : σ}{B ⊢ (MN) : τ}

(∧I) \frac{B ⊢ M : σ B ⊢ M : τ}{B ⊢ M : σ ∧ τ} (∧E) \frac{B ⊢ M : σ ∧ τ}{B ⊢ M : σ}

We will express that it is possible to derive B ⊢ M : σ in system ∧T RH by simply stating B ⊢ M : σ. A term will be called typeable in T_{∧RH} if there exists a basis B and a type σ such that B ⊢ M : σ.

Briefly, the idea of the strong normalization proof is the following: We define a “type erasing” function on terms of λ_{ωRH} that gives pure λ-terms as result and then we prove that erased terms are typeable in ∧T RH (this is done in three steps: first we reduce the complexity of the λ_{ω} structure of a term M by reducing it in β-normal form, then we prove that the erasures of terms in normal form are typeable in ∧T RH, finally we exploit the preservation of intersection types by β-expansion to prove that the erasure of M too is typeable in ∧T RH). After that we show that an infinite →_{mix}-reduction sequence on a term of λ_{ωRH} induces an infinite reduction sequence on the corresponding erased term. Since we know that ∧T RH is strongly normalizing, we deduce that λ_{ωRH} is strongly normalizing.

The erasing function | | : Object(λ_{ωRH} ) → Λ is inductively defined by

1. |x| = x if x ∈ V ar^{∗}.

2. |f| = f if f ∈ F.

3. |λx: A.q| = λx.|q| if λx: A.q is formed by (∗, ∗).

4. |λx: A.q| = |q| if λx: A.q is formed by (□, ∗).

5. |pq| = |p||q| if pq is formed by (∗, ∗)

6. |pQ| = |p| if pQ is formed by (□, ∗).

We shall prove that |M| ∈ Λ_{∧RH} (the set of typeable terms in ∧T RH) whenever M ∈ Object(λ_{ωRH} ) (Theorem 9 below). To do this we use some lemmas. In the following a type A will be called arrow-ground if its β-normal form A↓_{β} belongs to T_{S}.

Lemma 6. Let M ∈ Object(λ_{ωRH} ) such that Γ ⊢ M : A and |M| is in βnormal form. Then there exist B and σ such that B ⊢ |M| : σ. Moreover,

1. if A is an arrow-ground type then σ ≡ A↓_{β}

2. if x : δ ∈ Γ with δ an arrow-ground type, then x : δ ↓_{β} ∈ B.

Lemma 7. Let M ∈ Object(λ_{ωRH} ), |M| ≡ Q{x ↦ P }, where P is a term such that

1. if x is not a free variable in Q then P is in β-normal form and

2. ∃P′ ∈ Object(λ_{ωRH} ) s.t. |P′| ≡ P.

Then ∃B, σ s.t. B ⊢ Q{x ↦ P } : σ ⇒ ∃B′ s.t. B′ ⊢ (λx.Q)P : σ

We can now prove that the erasure of a term M ∈ Object(λ_{ωRH} ) is β-strongly normalizable, by showing that a β-reduction on |M| induces a β-reduction on M. The β-strong normalization of |M| is crucial to prove that indeed |M| ∈ Λ_{∧RH} and, from this, that M is →_{mix}-strongly normalizable.

Lemma 8. Let M ∈ Object(λ_{ωRH} ). If |M| →_{β} N then there exists M′ ∈ Object(λ_{ωRH} ) such that N ≡ |M′| and M →_{β} M′.

Theorem 9. If M ∈ Object(λ_{ωRH} ), then there exist B, σ s. t. B ⊢ |M| : σ.

Proof. |M| is →_{β}-strongly normalizable by Lemma 5 and Lemma 8. Then all the reduction strategies allow us to obtain the β-normal form of |M|, in particular the rightmost-innermost reduction strategy, according to which a contraction (λx.Q)P →_{β} Q{x ↦ P } is performed only if P is in β-normal form. Hence we can find B and σ by applying Lemma 6 to the β-normal form of |M| and iterating Lemma 7 backward along the chain of reduction steps which leads from |M| to its β-normal form. □

So, we have proved that if M ∈ Object(λ_{ωRH} ) then |M| ∈ Λ_{∧RH}. In fact we can also prove that for algebraic terms we can obtain the same type:

Lemma 10. If Γ ⊢ M : τ is an algebraic term in λ_{ωRH} , then |M| ∈ Λ_{∧RH}, and |M| is typeable with τ ↓_{β} from a basis B such that: if x : τ′ ∈ Γ, then x : τ′ ↓_{β}∈ B.

Each rule r : A → B ∈ R ∪ HOR in λ_{ωRH} induces a reduction relation →_{∧RH}^{r} on Λ_{∧RH}: |A|ϕ →_{∧T RH}^{r} |B|ϕ for any substitution ϕ in ∧T RH such that if Γ is the context for A and B and x : σ′ ∈ Γ then xϕ is typeable with type σ′ ↓_{β}. Lemma 10 ensures that this is a good definition.

We define →_{R_{(∧T RH)}}= ⋃_{r∈R} →_{∧T RH}^{r}, →_{HOR_{(∧T RH)}}= ⋃_{r∈HOR} →_{∧T RH}^{r} and

→_{mix_{(∧T RH)}}=→_{β} ∪ →_{R_{(∧T RH)}} ∪ →_{HOR_{(∧T RH)}} Since it will always be clear from the context, we shall denote in the same way a reduction on terms of λ_{ωRH} and the corresponding one on terms in Λ_{∧RH}, i.e. we shall omit the subscript (∧T RH). The following theorem is fundamental for the proof that λ_{ωRH} terms are →_{mix}-strongly normalizing.

Theorem 11 [4]. →_{mix} is strongly normalizing on terms of Λ_{∧RH} if R is conservative and HOR satisfies the general schema.

Conservativity of R is essential here. A counterexample to this theorem in the case of non-conservativity is shown in [4].

We can now prove the main theorem of this section. A β-reduction on a λ_{ωRH} term such that the β-redex is formed by (p_{1}, p_{2}), will be called, in the following, a β(p_{1}, p_{2})-reduction.

Theorem 12. Assume that R is conservative and that HOR satisfies the general schema. If M ∈ Λ_{ωRH} then M is →_{mix}-strongly normalizable.

Proof. By Lemma 2, we only need to consider the cases M ∈ Constructor(λ_{ωRH} ) and M ∈ Object(λ_{ωRH} ). If M ∈ Constructor(λ_{ωRH} ), then, since λ_{ωRH} objects can not occur in constructors (Lemma 3), each reduction in M is actually a β-reduction. Hence, strong normalization of M follows from Lemma 5. If M ∈ Object(λ_{ωRH} ), then we assign to M the pair I(M) = ⟨|M|, M⟩. By Theorem 9, |M| ∈ Λ_{∧RH} and then by Theorem 11 |M| is →_{mix}-strongly normalizing. By Lemma 5, M is →_{β}-strongly normalizable. Then the ordering >≡ (→_{mix}, →_{β(□,□)} ∪ →_{β(∗,□)} )_{lex} is well founded on these pairs. Moreover, M →_{mix} M′ implies I(M) > I(M′), so there is no infinite reduction sequence. □

The second order λ-calculus is included in λ_{ω} . Then, as a by-product of Theorem 12 we also obtain the →_{mix}-strong normalization of the second order λ-calculus enriched with first and higher order rewriting. This property was already proved in [14] using the classical method of candidates of reducibility.

3.2 Confluence of →_{mix}

We first recall the definition of confluence: a reduction relation → is called confluent if for all t such that t →^{∗} v_{1} and t →^{∗} v_{2} for some v_{1}, v_{2}, there exists v_{3} such that v_{1} →^{∗} v_{3} and v_{2} →^{∗} v_{3}. Local confluence is a closely related (weaker) property: → is called locally confluent if for all t such that t → v_{1} and t → v_{2} for some v_{1}, v_{2}, there exists v_{3} such that v_{1} →^{∗} v_{3} and v_{2} →^{∗} v_{3}. For strongly normalizing relations, local confluence is equivalent to confluence (Newman’s Lemma [15]). So we shall prove in the rest of this subsection that →_{mix} is locally confluent on λ_{ωRH} . The following lemmas show that the confluence of →_{R} for algebraic terms transfers to λ_{ωRH} -terms, and that for the class of higher order rewrite systems which we consider, the absence of critical pairs implies confluence (note that this is not true for arbitrary higher order rewrite systems, as shown in [16]). Due to lack of space we can not include the proofs of these lemmas here.

Lemma 13. If R is confluent and strongly normalizing on the set of algebraic terms of λ_{ωRH} then →_{R} is locally confluent on Λ_{ωRH}.

Lemma 14. Let HOR be a higher order rewrite system satisfying the general schema. If there is no critical pair, then →_{HOR} is confluent on λ_{ωRH} .

Now let us prove that →_{mix} is locally confluent.

Theorem 15 Local Confluence of →_{mix} in λ_{ωRH} . If R is confluent over the set of algebraic terms, and there are no critical pairs between rules in R and HOR and between rules in HOR, then →_{mix} is locally confluent on λ_{ωRH} .

Proof. It suffices to show the commutativity of β-, →_{R}- and →_{HOR}-reductions on overlapping redexes. But since →_{β} is confluent, →_{HOR} is confluent (by Lemma 14) and →_{R} is confluent (by Lemma 13), it is sufficient to prove that, for all t such that t →_{mix} v_{1} at position p using one of the reduction relations, and t →_{mix} v_{2} at position p.q using a different reduction relation, there exists a v_{3} such that v_{1} →_{mix}^{∗} v_{3} and v_{2} →_{mix}^{∗} v_{3}.

Let t′ be the term obtained from t by replacing the subterm at position p.q by a new variable x. Since there are no critical pairs, t′ is still reducible at position p: t′ →_{mix} v′. If x appears in v′ at positions m_{1}, …, m_{n} then t|_{p.q} appears in v_{1} at the same positions. Let t′′ be the term obtained after reducing v_{1} at positions m_{1}, …, m_{n}. Then v_{2} →_{mix} t′′ at position p. □

For example, the class of higher order rewriting systems defining higher order functions by primitive recursion (structured recursion) on first order data structures, verify the required hypothesis and then →_{mix} is confluent in this case.

4 Conclusions and further work

The results proved here allow for the use of the well known principle of Divide et Impera to prove consistency of logical systems based on combinations of λ_{ω} with algebraic rewrite systems (both first and higher order), provided that the first order reductions are conservative, and that higher order rules satisfy the general schema. Unfortunately, the extension of these results to more powerful systems such as the Calculus of Constructions is not straightforward. This is no doubt a topic worth of further investigation.

References

1. S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102:135-163, 1992.

2. F. Barbanera. Adding algebraic rewriting to the calculus of constructions: Strong normalization preserved. In Proc. of the 2nd Int. Workshop on Conditional and Typed Rewriting, LNCS 514, 1990.

3. F. Barbanera. Combining term rewriting and type assignment systems. International Journal of Foundations of Computer Science, 1:165–184, 1990.

4. Franco Barbanera and Maribel Fernández. Combining first and higher order rewrite systems with type assignment systems. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Utrecht, Holland, LNCS 664, 1993.

5. H. Barendregt. Introduction to generalised type systems. Journal of Functional Programming, 1991.

6. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter λ-model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

7. S. Berardi. Type dependence and constructive mathematics. PhD thesis, Mathematical Institute, Torino, Italy, 1990.

8. Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 1990. to appear.

9. Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation, 1992. to appear.

10. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, February 1988.

11. H. Geuvers and M.J. Nederhof. Modular proof of the strong normalization for the calculus of constructions. Journal of Functional Programming, vol.1 (2), 1991.

12. J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse d’Etat, Univ. Paris VII, France, 1972.

13. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

14. Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350–361, 1991.

15. M. H. A. Newman. On theories with a combinatorial definition of ‘equivalence’. Ann. Math., 43(2):223–243, 1942.

16. T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.

17. Mitsuhiro Okada. Strong normalizability for the combined system of the types lambda calculus and an arbitrary convergent term rewrite system. In Proc. ISSAC 89, Portland, Oregon, 1989.

18. Michaël Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters, 26:65–70, 1987.

19. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, April 1987.

20. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, April 1987.

This article was processed using the L TEX macro package with LLNCS style