Combining First and Higher Order Rewrite Systems with Type Assignment Systems

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.lri.fr

Abstract. General computational models obtained by integrating different specific models have recently become a stimulating and promising research subject for the computer science community. In particular, combinations of algebraic term rewriting systems and various λ-calculi, either typed or untyped, have been deeply investigated. In the present paper this subject is addressed from the point of view of type assignment. A powerful type assignment system, the one based on intersection types, is combined with term rewriting systems, first and higher order, and relevant properties of the resulting system, like strong normalization and confluence, are proved.

1 Introduction

The interactions between term rewriting systems and λ-calculus have been widely studied in the last years ([10], [16], [6], [7], [20], [3], [2], [15]). An important motivation of these works is the need of establishing a formal setting integrating two closely-related models of computation: the one based on algebraic reduction of algebraic terms and the one based on β-reduction of λ-terms.

Since both models are based on term reduction, the most natural combined model is given by the combination of the two kinds of reductions on mixed terms, i.e., on λ-algebraic-terms. An interesting question to investigate is under which conditions the properties of each reduction relation transfer to their combination. Confluence and strong normalization (or termination) are the most important properties of reductions: strong normalization ensures that all reduction sequences are finite, whereas confluence ensures determinacy, because if two different terms u and v can be obtained by reducing some term t, there must exist a common reduct of u and v. The question above is whether the combined reduction relation inherits these properties when they are true of each reduction relation alone.

If we consider untyped languages, the attempt to combine both sorts of computations raises serious problems. In [16] it is proved that in order to add a confluent term rewriting system to the untyped λ-calculus preserving confluence,

⋆ To Roberta Gottardi

restrictions have to be imposed on the term rewriting system. If such restrictions are omitted, it is proved in [10] that confluence and strong normalization of the combination hold only if we impose severe restrictions on the set of mixed terms. On the other hand, if we consider typed languages (typed versions of λ-calculus and typed term rewriting systems) things work out nicely: confluence and termination are modular properties in this case, that is, the system resulting from the combination of a confluent and terminating first-order many-sorted rewrite system and typed λ-calculus is again confluent and terminating. This result is shown in [7] and [20] for polymorphic (or second order) λ-calculus, by using the computability predicate method developed by Girard and Tait (see [11]).

In [3], types are considered from another perspective: the author investigated a version of λ-calculus where types are assigned to λ-terms by means of an inference system, showing that the same good properties that are preserved by combining typed λ-calculi with first order term rewriting systems hold even when dealing with type assignment systems. He considered in particular the intersection type discipline described in [4]. The strength of the intersection type assignment system lies in the fact that it yields a characterization of strongly normalizable terms as the class of terms having a type according to the rules of this type assignment system [21]. Besides, the strong normalization property of the combination of the intersection type assignment system and first order rewrite systems is used in [2] to extend Gallier and Breazu-Tannen’s result about modularity of strong normalization, to more powerful type disciplines, such as Girard’s system F_{w} and the Calculus of Constructions.

Briefly, at this point it is well-known that strong typing (either in typed languages or in type assignment systems) is the key for the modularity of confluence and termination in combinations of first order rewrite systems and λ-calculus.

Up to now we have only mentioned theoretical motivations for the combination of two computational models. But the combination of term rewriting systems and λ-calculus was also studied as an interesting alternative in the design of new programming languages. J-P. Jouannaud and M. Okada were the first to investigate from this point of view the combination of λ-calculus and term rewriting systems, defining a new programming paradigm that allows first order definitions of abstract data types and operators, as in equational languages like OBJ, and the full power of λ-calculus for defining functions of higher types, as in functional languages like ML.

The following example, taken from [15], shows a simple program that can not be written in one of the above-mentioned traditional languages alone, but can be written in the unified language.

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 nonrecursive), while the higher order function map is defined recursively on the structure of lists.

Adding λ-expressions to this kind of higher order rewrite systems (i.e., allowing to substitute a λ-term for higher order variables) we obtain the usual paradigm of functional programming languages extended with equational (algebraic) definitions of operators and types. This is what Jouannaud and Okada called “algebraic functional paradigm”, i.e., the combination of first order algebraic equations and λ-calculus enriched with higher order functional constants defined by higher order equations.

In [15] it is shown that for algebraic functional languages built upon typed versions of λ-calculus (simply typed λ-calculus or polymorphic λ-calculus) the combination with confluent and terminating rewrite rules is modular provided that the set of higher order rules satisfies certain conditions (the so-called general schema) and the first order rules are non-duplicating (that is, the number of occurrences of any variable in the right-hand side of a rule is less or equal than the number of occurrences in the left-hand side).^{3} But the authors left open the question of whether other type disciplines for λ-calculus interact as nicely with “well-behaved” term rewriting systems. In this paper we address the problem of the modularity of confluence and strong normalization properties for algebraic functional languages with type inference, a way of dealing with types that has several advantages in practice and is used in powerful functional programming languages, notably ML [12] and MIRANDA [23].

More precisely, we consider the combination of first and higher order rewriting systems with type assignment systems for λ-calculus, and we prove that the same good properties that are preserved when combining simple and polymorphic λcalculus with rewrite systems in algebraic functional languages hold even when dealing with types in this modified perspective. We consider in particular the intersection type assignment system, since it is a very expressive and powerful system, as already mentioned.

Our proof of strong normalization is based on the computability predicate method. We use a predicate that results from the generalization to our type assignment system of the one defined in [15]. For the proof of confluence however, we didn’t apply the same method (although a proof based on computability predicates can be done as suggested in [15]). Instead, we give a simple proof using the strong normalization result proved previously.

The results we present here can be seen on one hand as a generalization of [15] because of the introduction of type assignment systems, and on the other hand as a generalization of [3] by taking into account higher order rewrite systems. It is also interesting to note that our modularity results extend Dougherty’s results for untyped systems [10], since there are sets of mixed terms that do not satisfy Dougherty’s conditions but are typeable in our system.

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

2 Type assignment systems

Type assignment systems (also called type inference systems) are formal systems for assigning types to untyped terms. These systems are defined by specifying a set of terms, a set of types one assigns to terms and a set of type-inference rules. We shall refer to [5] and [14] for all the notions about λ-calculus we do not define explicitly, and to [9] for definitions and notations for term rewriting systems.

2.1 The intersection type assignment system

In this section we present a variant of the intersection type assignment system (⊢^{∧}) defined in [4], [21]. See also [8] and [13] for motivations and applications of intersection systems.

The set T_{∧} of intersection types is inductively defined by:

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

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

3. σ, τ ∈ T_{∧} ⇒ σ ∧ τ ∈ T_{∧} (intersection types).

The elements of T_{∧} are considered modulo associativity, commutativity and idempotency of ∧. In the following ⋀_{i∈I}σ_{i}, where I = {i_{1}, …, i_{n}}, will be a short-

hand for σ_{i_{1}} ∧ … ∧ σ_{i_{n}}.

The terms we assign types to are the terms of the pure λ-calculus (Λ). A statement is an expression of the form M : σ where σ ∈ T_{∧} and M ∈ Λ. M is the subject of the statement. A basis (the set of assumptions a statement depends on) is a set of statements with only variables as subjects. Without loss of generality we assume that in a basis there are no two statements with the same subject. If x does not occur in the basis B then B, x : σ denotes the basis B ∪ {x : σ}.

The axioms and type inference rules of the intersection type assignment system ⊢^{∧} are the following :

(Ax) B, x : σ ⊢^{∧} x : σ

(→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 shall express the fact that it is possible to derive B ⊢^{∧} M : σ in system ⊢^{∧} by simply stating B ⊢^{∧} M : σ. A term will be called typeable in ⊢^{∧} if there exists a basis B and a type σ such that B ⊢^{∧} M : σ.

Using system ⊢^{∧} it is possible to characterize λ-terms having a relevant functional property, namely β-strong normalization.

Theorem 1 [21], [17]. A term of the pure λ-calculus is β-strongly normalizable if and only if it is typeable in the intersection type assignment system.

2.2 The ∧T RH type assignment system

As stated in the introduction we now extend the system ⊢^{∧} with algebraic rewriting capabilities. First of all, we consider a denumerable set S of sorts and we define by induction the set T_{S} of arrow ground types based on S:

1. If s ∈ S then s ∈ T_{S}.

2. 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 the set of function symbols of type τ (τ ≠ τ′

implies F_{τ} ∩ F_{τ′} = ∅). In case τ ≡ s_{1} … s_{n} → s where s_{1}, …, s_{n}, s ∈ S, 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.

Let X = ⋃_{τ∈T_{S}}X_{τ}, where X_{τ} denotes a denumerable set of variables of type τ

(τ ≠ τ′ implies X_{τ} ∩X_{τ′} = ∅). X contains first order variables, i.e. variables whose type is a sort, and higher order variables. We use x, y, … to denote variables and X, Y, … when we want to emphasize that they are higher order variables.

The set T (F, X)_{σ} of higher order algebraic terms of type σ is inductively defined by:

1. If f ∈ F_{σ_{1}...σ_{n}→σ}, t_{1} ∈ T (F, X)_{σ_{1}}, …, t_{n} ∈ T (F, X)_{σ_{n}} (n ≥ 0) then ft_{1} … t_{n} ∈ T (F, X)_{σ}.

2. If X ∈ X_{σ_{1}...σ_{n}→σ}, t_{1} ∈ T (F, X)_{σ_{1}}, …, t_{n} ∈ T (F, X)_{σ_{n}} (n ≥ 0) then Xt_{1} … t_{n} ∈ T (F, X)_{σ}.

The set of higher order algebraic terms is T (F, X) = ⋃_{τ}T (F, X)_{τ}. It includes

the set T (Σ, X) = ⋃_{s∈S}T (Σ, X)_{s} of first order algebraic terms.

The rewriting systems we consider are composed of:

1. a set R of first order rewrite rules whose elements are denoted by r : t → t′ (t, t′ ∈ T (Σ, X)). Obviously, in order to have a reasonable system, for each rewriting rule r : t → t′ there exists s ∈ S such that t, t′ ∈ T (Σ, X)_{s}, 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.

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

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 (i.e. they belong to T (F, X)_{τ} for some τ), l⃗, r⃗_{1}, …, r⃗_{m} are all terms of sort type, X⃗ ⊆ Y⃗ and ∀i ∈ [1..m], l⃗ >_{mul} r⃗_{i} (where < is the strict subterm ordering and mul denotes multiset extension).

The reduction rules above can be considered as the definitions of new functionals of the (programming) language. There is a restriction 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 also appear in the left hand side definition of F could be easily 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⃗ instead is essential in the proof of strong normalization of the combined language, as we shall see later.

Although restricted, this schema is interesting from a practical point of view: it allows, for example, the introduction of functional constants of higher order types by primitive recursion (or structural induction) on a first order data structure, as the function map showed in the introduction (see [15] for more examples and applications). Moreover, for higher order systems satisfying the general schema all the properties we are interested in are valid also when simply typed λ-terms are allowed in right-hand sides. So, from now on we consider an extended version of higher order systems whose rules satisfy the general schema above, but where there may be simply typed λ-terms built from X and F in v. See [14] for missing definitions on simply typed λ-calculus.

Let us describe now the extended type assignment system ∧T RH (∧T RH stands for intersection type assignment system with an algebraic rewrite system R ∪ HOR). Let S be the set of sorts and F the S-sorted algebraic signature of R ∪ HOR. ∧T RH is the type assignment system obtained by extending the intersection type assignment system as follows:

1. The set T_{∧RH} of types is defined by adding to case 1 of the inductive definition of T_{∧} a constant type s for each sort s ∈ S.

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. Note that we do not consider the types of function symbols and variables here. This means that even if S = {int, bool} and f ∈ F_{int→int}, a term such as λx.f T rue is well-formed, although it can not be given a type.

3. For each function symbol f ∈ F_{σ_{1}...σ_{n}→σ} we add to the axioms of the inter-

section type assignment system the following axiom: (Ax) B ⊢ f : σ_{1} → … → σ_{n} → σ for all bases B.

This axiom states that f can be given only its right type. Indeed what we assign to f is the curryfication of its type since in λ-calculus all functions are thought of as unary higher order functions.

4. The inference rules and the definition of basis are the same as in the intersection type assignment system.

We shall use “⊢” as deduction symbol for ∧T RH. Note that ∧T RH does not treat function symbols as variables. Instead, it assigns to each function symbol the very ground type it has in the typed signature we consider, avoiding in this way the problems dealt with in [1] for the preservation of types along rewriting. In the following section we prove that our rewriting relation preserves types.

We say that a term M is typeable if there exist a basis B and a type σ such that B ⊢ M : σ. The set of typeable terms is denoted by Λ_{∧RH}.

The ∧-algebraic terms (a subset of Λ_{∧RH}) are inductively defined by:

1. If f ∈ F_{σ_{1}...σ_{n}→σ} (n ≥ 0), M_{1}, …, M_{n} are ∧-algebraic terms and fM_{1} … M_{n} is typeable then fM_{1} … M_{n} is a ∧-algebraic term.

2. If X ∈ X and M_{1}, …, M_{n} (n ≥ 0) are ∧-algebraic terms, then XM_{1} … M_{n} is a ∧-algebraic term.

We define in the obvious way the set of first order ∧-algebraic terms.

Note that in the definition of ∧-algebraic terms the variables are considered untyped. It is not difficult to check that each (first order) ∧-algebraic term is typeable (with a sort type) by means of a deduction in which rule (∧I) is not used, and rule (∧E) is applied only as first rule. Rule (∧E) is necessary since in a ∧-algebraic term the same variable can occur whereas in the corresponding term of T (F, X) different variables are required. For example, if f ∈ F_{int,bool→int} then fxx is a ∧-algebraic term (it can be assigned the type int in a basis where x has type int ∧ bool) but it is not an algebraic term.

Terms in T (F, X) can be seen as ∧-algebraic if types are not taken into consideration (to emphasize this change of perspective, the ∧-algebraic term corresponding to t ∈ T (F, X) will be denoted by t), but for the converse a renaming of variables may be necessary in order to avoid type conflicts. Let us formally define the mapping ς : ∧-algebraic terms → T (F, X). Let P be a ∧- algebraic term and let ρ_{P} be a renaming of occurrences of variables such that if x occurs in P in positions where arguments of different types τ_{1}, …, τ_{q} are required (to get a term in T (F, X)), then, for i = 1 … q, ρ replaces x by the new variable x_{i} of type τ_{i} in all the positions where an argument of type τ_{i} is required. We define ς(P) = P ρ_{P}. For example, if f ∈ F_{int,bool→int} then ς(fxx) = fxy.

Of course, there are many ways of defining ρ_{P} and each possible ρ_{P} gives a different ς(P), but it is sufficient to choose a canonical ρ_{P} for each P to have ς uniquely defined on ∧-algebraic terms.

On terms in Λ_{∧RH} the β-reduction relation, denoted by →_{β}, is defined as usual. Moreover for terms in Λ_{∧RH} we can define new reduction relations, each of them induced by an algebraic or higher order rewriting rule.

In the following we denote substitutions by {x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}}. Postfix notation is used for their application. When applying a substitution to a λ-term we must take care of bound variables, as usual.

We will denote by →_{R} and →_{HOR} the reduction relations induced by R and HOR respectively in T (F, X). R and HOR also induce reductions relation in Λ_{∧RH}. Since it will be always clear from the context, we shall use the same notation for reductions on algebraic terms and on terms in Λ_{∧RH}. Let us define the →_{R} and →_{HOR} reduction relations on Λ_{∧RH}:

Let M, M′ ∈ Λ_{∧RH} and r : t → t′ ∈ R ∪ HOR. M →^{r} M′ iff 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 out of M by replacing the term t′{x_{1} ↦ N_{1}, …, x_{n} ↦ N_{n}} for P. Note that since N_{1}, …, N_{n} ∈ Λ_{∧RH} they can contain λ-terms. M →_{R} M′ (resp. M →_{HOR} M′) iff 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.^{4}

Property 1 For each reduction M →_{R} N (resp. M →_{HOR} N) where M, N are ∧-algebraic terms, there exists a reduction ς(M) →_{R} ς(N) (resp. ς(M) →_{HOR} ς(N)).

Theorem 2 (Termination of →_{R} and →_{HOR} on ∧-algebraic terms). If R (resp. HOR) is a terminating rewrite system, i.e. strongly normalizing on algebraic terms, then →_{R} (resp. →_{HOR}) is strongly normalizing on ∧-algebraic terms.

Theorem 2 is a direct consequence of Property 1. Note that the definition of the reduction relations only for typeable terms is crucial for strong normalization to hold. If we defined algebraic reductions without care of the typability of terms we could have terms in Λ_{∧RH} not strongly normalizable even if R and HOR are strongly normalizing systems: it is in fact easy to find strongly normalizing manysorted term rewrite systems which fail to be strongly normalizing if we do not take types into consideration i.e. if all sorts are identified. See [22] for examples.

Now, to prove a similar result about confluence we need one more property.

Property 2 Let M be a ∧-algebraic term and N an algebraic term such that ς(M) →_{R} N (resp. ς(M) →_{HOR} N), then M →_{R} Nρ_{M}^{−1} (resp. M →_{HOR} Nρ_{M}^{−1}).

As a consequence of Properties 1, 2 and the fact that for ∧-algebraic terms M, N such that M →_{R∪HOR} N we can use either ρ_{M} or ρ_{N} in ς(N), we have

Theorem 3 (Confluence of →_{R} and →_{HOR} on ∧-algebraic terms). If R (resp. HOR) is confluent then →_{R} (resp. →_{HOR}) is confluent on ∧-algebraic terms.

In the following →_{mix} will denote the reduction relation on terms of Λ_{∧RH} obtained by the union of →_{β}, →_{R} and →_{HOR}. →_{mix}^{∗} will denote its reflexive and transitive closure.

Now we are going to show an important property of →_{mix}, the so-called Subject Reduction property, which states that →_{mix} preserves the types of terms.

4 We have chosen to define first algebraic terms and reductions on them, and later to include this sort of reductions on terms of our type assignments by using a translation from algebraic terms to ∧-algebraic terms. A different approach, more frequent in the literature, would have been that of first defining the set Λ_{∧RH} of terms and then the reduction relations on ∧-algebraic terms. We have refrained from this latter choice since, by being in an intersection type assignment context it would have led, in our opinion, to a more cumbersome definition.

Lemma 4 (Rewriting preserves types). If B ⊢ M : τ and M →_{R∪HOR} M′ then B ⊢ M′ : τ.

The assumption of ground types for the symbols in F is crucial for rewriting to be type preserving. If we accept non-ground types with the possibility of instantiating the type variables, then rewriting is not type preserving in general, as shown in [1].

Theorem 5 (Subject Reduction). If B ⊢ M : τ and M →_{mix}^{∗} N then B ⊢ N : τ.

3 Strong Normalization and Confluence of →_{mix}

In [3] it is shown that →_{R} ∪ →_{β} is confluent and strongly normalizing in Λ_{∧RH} whenever R is confluent and strongly normalizing on algebraic terms. But unfortunately, to extend this result to →_{R} ∪ →_{HOR} ∪ →_{β} we have to require one extra condition on the first order rewrite system R: for each rule r : t → t′ ∈ R, each variable must “appear less” in t′ than in t, more precisely, the number of occurrences of each variable in t′ must be less or equal than its number of occurrences in t. This is because otherwise we could easily code Toyama’s example of non-termination [22] by using a first order rule where this condition is not satisfied: Consider the system

f01x → fxxx

F X → 1

F X → 0 where F is a higher order function symbol, f is a first order function symbol, 0, 1 are first order constants and X, x are variables. There is an infinite reduction sequence out of the term f(F X)(F X)(F X):

f(F X)(F X)(F X) → f0(F X)(F X) → f01(F X) → f(F X)(F X)(F X) …

Confluence of HOR does not suffice to restore the strong normalization property. This can be seen by coding the example of Barendregt and Klop (see [22]).

We will say that R is non-duplicating (or conservative) when it satisfies the condition above. What we shall prove in the following is that if R is nonduplicating, confluent and strongly normalizing, and HOR is confluent (and satisfies the general schema), →_{mix} is confluent and strongly normalizing. More precisely, we shall prove that all terms in Λ_{∧RH} are →_{mix}-strongly normalizable and that →_{mix} is a confluent reduction relation for terms in Λ_{∧RH} provided that there are no critical pairs between rules in HOR and between rules in R and HOR (that is, only R can have critical pairs).

Remark that these properties extend [10]: D.J. Dougherty showed that strong normalization and confluence are modular properties for sets of “stable terms”. Intuitively, stability means that algebraic rewriting can not create new abstractions. Formally, if a set T of terms is R-stable then for all M ∈ T such that M is in β-normal form and M →_{R} N, N is in β-normal form. But Λ_{∧RH} is not R∪HORstable in general: Consider the rewriting system HOR containing only one rule F X0 → X, where F ∈ F_{(int→int),int→(int→int)} and 0 ∈ F_{int}. This is a higher order system satisfying the general schema. Let M ≡ (F (λx.x)0)0 ∈ Λ_{∧RH}. M is in β-normal form, but M →_{HOR} (λx.x)0 →_{β} 0.

3.1 Strong Normalization of →_{mix}

Our proof is a generalization of the proof given in [15]. It is done in two parts: in the first one we give the definition of a predicate Red on types and terms, usually called computability predicate, and prove some properties of Red, the most important one stating that if Red holds for a term then the term is strongly normalizable. In the second part Red is shown to hold for each term in Λ_{∧RH}.

We shall call base type a type in S ∪ V_{T}. Let t be a term and τ a type. Red(t, τ) holds if there exists a basis B such that B ⊢ t : τ and

1. τ = τ_{1} ∧ τ_{2} Red(t, τ_{1}) and Red(t, τ_{2}).

2. τ ≠ τ_{1} ∧ τ_{2}

(a) t = λx.v (then τ = σ → ρ) for all w such that Red(w, σ) we have Red(v{x ↦ w}, ρ).

(b) t ≠ λx.v (such a t will be called neutral) either τ is a base type and t is strongly normalizable or for all v such that t →_{mix} v, Red(v, τ).

Note that by the Knaster-Tarski Theorem, this recursive definition has a least fixpoint since the underlying functional is monotonic.

We say that a term t is computable if ∃τ such that Red(t, τ).

Property 3 Red satisfies the standard properties of computability predicates:

- (Fact 1) A term of a base type is computable if and only if it is strongly normalizable.

- (C1) Red(u, τ) implies u is strongly normalizable.

- (C2) If Red(u, τ) and u →_{mix}^{∗} v then Red(v, τ).

- (C3) If u is neutral, B ⊢ u : σ for some B, σ (i.e., u is typeable) and for all v such that u →_{mix} v, Red(v, σ) holds, then also Red(u, σ) holds.

The proofs are by induction on the definition of Red.

We need in the following the notions of alien subterm and cap, which we define as in [15]: Let u be a Λ_{∧RH}-term. An alien subterm of u is a maximal subterm of u which is not of the form ft_{1} … t_{n} for some f ∈ Σ_{s_{1}...s_{n}→s}. We denote by alien(t) the multiset of alien subterms of t. The cap of u is the ∧-algebraic term obtained by replacing alien subterms by variables (the same variable for equal alien subterms). In other words, the cap of u is the ∧-algebraic term u[x_{1}]_{p_{1}} … [x_{n}]_{p_{n}} where x_{1}, …, x_{n} are new variables, alien(u) = [u|_{p_{1}}, …, u|_{p_{n}}] where square brackets denote multiset, and x_{i} = x_{j} if u|_{p_{i}} ≡ u|_{p_{j}}. For example, the cap of (λx.M)N is z and the cap of f(λy.y)(λy.y) is fzz if f ∈ Σ.

The following lemma will be used in the proof of the Strong Normalization Theorem.

Lemma 6 (Principal Case). If R is conservative and strongly normalizing, any Λ_{∧RH}-term of the form ft_{1} … t_{n}, where f ∈ Σ, is →_{mix}-strongly normalizable whenever its alien subterms are →_{mix}-strongly normalizable.

Proof. We interpret a term t by the pair (alien(t), cap(t)) of the multiset of its alien subterms and its cap. Multisets of alien subterms are compared in the multiset extension of →_{mix} ∪ > (recall that < is the strict subterm relation), and caps are compared in the algebraic reduction ordering →_{R}. This is a well-founded ordering since →_{mix} is strongly normalizing on alien subterms by hypothesis and →_{R} is strongly normalizing on ∧-algebraic terms.

Now, assume t →_{mix} t′. We have two cases:

1. If t →_{mix} t′ in a position inside an alien subterm then alien(t) (→_{mix} ∪ >)_{mul} alien(t′). Note that we need to consider > since the result of reducing an alien subterm of t can be a term whose root belongs to Σ and so only its strict subterms can be alien subterms of t′.

2. If t →_{mix} t′ in a cap position (it is an algebraic reduction) then alien(t′) ⊆ alien(t) since R is conservative, and cap(t) →_{R} cap(t′).

In both cases the interpretation decreases (strictly). Hence there is no infinite reduction sequence. □

Theorem 7 (Strong Normalization of →_{mix} in Λ_{∧RH}). If R is conservative and strongly normalizing and HOR satisfies the general schema then →_{mix} is strongly normalizing on Λ_{∧RH}.

Proof. We say that a substitution {x_{1} ↦ u_{1}, …, x_{n} ↦ u_{n}} is computable in a basis B = x_{1} : σ_{1}, …, x_{n} : σ_{n} if Red(u_{1}, σ_{1}), …, Red(u_{n}, σ_{n}) hold. In order to prove the theorem we shall prove a stronger property: For any term u with free variables x_{1}, …, x_{n} and such that x_{1} : σ_{1}, …, x_{n} : σ_{n} ⊢ u : σ, if γ = {x_{1} ↦ u_{1}, …, x_{n} ↦ u_{n}} is computable in B = x_{1} : σ_{1}, …, x_{n} : σ_{n} then Red(w, σ) holds for w = uγ. The theorem follows by C1, putting u_{i} = x_{i}.

To prove the property we apply noetherian induction. Let F_{1}, …, F_{n} be the higher order function symbols of F. We interpret the term w = uγ by the triple < i, u, {γ} >, where i is the maximal index of the functional constants belonging to u and {γ} is the multiset {xγ | x ∈ V ar(u)}. These triples are compared in the ordering (>_{N}, ◇, (→_{mix} ∪ >)_{mul})_{lex}, denoted by ≫ in the following and by ≫_{n} when we want to indicate that the nth element of the triple has decreased but not the (n−1) first ones. Here, >_{N} denotes the standard ordering on natural numbers, ◇ stands for the well-founded encompassment ordering, that is, u◇v if u ≠ v and u|_{p} = vδ for some position p ∈ u and substitution δ, and lex, mul denote respectively the lexicographic and multiset extension of an ordering. Note that encompassment contains strict subterm. Besides, since γ is computable, →_{mix} is well-founded on γ by property (C1), and because the union of the strict subterm relationship ( >) with a terminating rewrite relation is well-founded [9], the relation (→_{mix} ∪ >)_{mul} is well-founded on γ. Hence, ≫ is a well-founded ordering on the triples.

The induction hypothesis is: For all v ≡ tγ′ such that w ≫ v, y_{1}, …, y_{m} are the free variables of t, y_{1} : τ_{1}, …, y_{m} : τ_{m} ⊢ t : τ and γ′ is computable in y_{1} : τ_{1}, …, y_{m} : τ_{m}, Red(v, τ) holds.

There are ten cases in the proof, depending upon the properties of w = uγ.

1. Let u = λx.v, hence w = λx.vγ. We know that B ⊢ λx.v : σ, then there exist τ_{i}, ρ_{i} such that B, x : τ_{i} ⊢ v : ρ_{i} and σ = ⋀_{i∈I}τ_{i} → ρ_{i}. Assume that

t is a computable term of type τ_{i}, and define γ′ = γ ∪ {x ↦ t}, hence γ′ is computable in B, x : τ_{i}. Now, uγ ≫_{2} vγ′, hence Red(vγ′, ρ_{i}) holds by the induction hypothesis. Therefore, by definition of Red, for all i ∈ I Red(w, τ_{i} → ρ_{i}) holds, and then Red(w, σ) holds.

2. Let u ≠ λx.v. If w is irreducible, then Red(w, σ) holds by definition of Red. Otherwise, let w →_{mix} w′ at position p. We must show Red(w, σ) itself, or (by property (C3)) Red(w′, σ).

(a) Let p ∉ FDom(u), where FDom(u) is the set of positions of function symbols in u union the set of non-leaf variable positions (i.e. positions of higher order variables applied to some arguments). This means that the reduction w →_{mix} w′ takes place inside the substitution γ, in this case p is a position of a leaf variable in u or it is not a position in u. Note that this case takes care of the case where u is a variable. Let p = qp′, u|_{q} = x_{i} ∈ X, u′ = u[z]_{q} where z is a new variable. If x_{i} occurs only once in u then we consider γ′ = γ|_{dom(γ)−{x_{i}}} ∪ {z ↦ w′|_{q}}, otherwise γ′ = γ ∪ {z ↦ w′|_{q}}. Note that w|_{q} →_{mix} w′|_{q} at position p′. Since w|_{q} ∈ {γ}, Red(w|_{q}, σ_{i}) holds by assumption, then Red(w′|_{q}, σ_{i}) by property (C2), hence γ′ is computable in B, z_{i} : σ_{i}. Now, u = u′ modulo renaming of variables if the variable u|_{q} has exactly one occurrence in u, otherwise u◇u′. In the first case uγ ≫_{3} u′γ′, and uγ ≫_{2} u′γ′ in the second case. In both cases Red(u′γ′, σ) holds, and u′γ′ ≡ w′.

(b) Let p ∈ FDom(u), with p ≠ ε (p is not the root position). Then u◇u|_{p}, hence uγ ≫_{2} (u|_{p})γ = (uγ)|_{p}. Let τ_{i} be the types assigned to u|_{p} in the derivation of B ⊢ u : σ, then Red((uγ)|_{p}, τ_{i}) holds by the induction hypothesis and hence by definition of Red, Red((uγ)|_{p}, ⋀ τ_{i}). Let u′ = u[z]_{p} for some new variable z, and γ′ = γ ∪ {z ↦ (uγ)|_{p}}, then γ′ is computable in B, z : ⋀ τ_{i}, and B, z : ⋀ τ_{i} ⊢ u′ : σ. Now u◇u′, hence uγ ≫_{2} u′γ′ = w, hence Red(w, σ).

(c) Let p ∈ FDom(u) and p = ε. We distinguish now the cases:

i. u = (λx.v)t and w = (λx.vγ)tγ. Hence u◇t, hence uγ ≫_{2} tγ, and by the induction hypothesis we get Red(tγ, τ_{i}) where τ_{i} are the types assigned to t in B ⊢ u : σ, and hence Red(tγ, ⋀ τ_{i}). Let now γ′ = γ ∪ {x ↦ tγ}, hence γ′ is computable in B, x : ⋀ τ_{i}. Now u◇v, hence uγ ≫_{2} vγ′ = w′ and Red(w′, σ) holds.

ii. u = yt and yγ = λx.v. Hence w = (λx.v)(tγ) and w′ = vγ′ where xγ′ = tγ. Since u◇t, uγ ≫_{2} tγ, hence γ′ is computable in B, x : ⋀ τ_{i} where τ_{i} are the types assigned to t in the derivation of B ⊢ u : σ. Now, λx.v is computable by assumption (Red(λx.v, σ_{i}) holds), hence by definition of Red, we have Red(vγ′, σ). Hence, Red(w′, σ).

iii. w = uγ →^{r} w′, where r ∈ R ∪ HOR. Assume that u(ε) = V is an arbitrary algebraic symbol or a higher-order variable, and that u◇V z_{1} … z_{q} but u is not equal to V z_{1} … z_{q} up to renaming of variables (cases 2(c)iv, 2(c)v and 2(c)vi below deal with u = V z_{1} … z_{q}). Let u′_{i} = u|_{i} and z_{i}γ′ = u′_{i}γ. u◇u′_{i}, hence uγ ≫_{2} u′_{i}γ. Then, if B ⊢ u′_{i} : σ′_{i}, Red(u′_{i}γ, σ′_{i}) holds. Hence γ′ is computable in B, z_{1} : σ′_{1}, …, z_{q} : σ′_{q}. But uγ ≫_{2} (V z_{1} … z_{q})γ′ = w and B, z_{1} : σ′_{1}, …, z_{q} : σ′_{q} ⊢ V z_{1} … z_{q} : σ. Hence Red(w, σ).

iv. u = F_{k}z_{1} … z_{q} and w = uγ →^{r} w′ at the root. Then i (the first component of the interpretation) is k. Hence w = (F_{k}z_{1} … z_{q})γ = F_{k}l⃗[M⃗, s⃗]N⃗t⃗ →^{r} v[(F_{k}r⃗_{1}[M⃗, s⃗]N⃗t⃗), …, (F_{k}r⃗_{m}[M⃗, s⃗]N⃗t⃗), M⃗, s⃗, N⃗, t⃗]. l⃗[M⃗, s⃗], M⃗ ⊆ N⃗, N⃗, t⃗ are all terms in {γ}, hence are computable by hypothesis. Then terms in l⃗[M⃗, s⃗] are strongly normalizable by Fact 1 since they are of base type by definition of HOR. Terms in s⃗ are of base type and strongly normalizable as subterms of strongly normalizable terms, hence they are computable by Fact 1. Let X⃗γ′ = M⃗ and x⃗γ′ = s⃗. Since M⃗ and s⃗ are computable, γ′ is computable. Now ∀j ∈ [1..m], F_{k} ∉ r⃗_{j} (by definition of HOR), hence (F_{k}z_{1} … z_{q})γ ≫_{1} r_{j}γ′, hence r_{j}γ′ is computable. Let now γ′′ be the computable substitution such that uγ′′ = (F_{k}r⃗_{j}[X⃗, x⃗]Y⃗ y⃗)γ′. Since l⃗ >_{mul} r⃗_{j}, and > is closed under substitution, then l⃗γ′ >_{mul}r⃗_{j}γ′, hence (F_{k}z_{1} … z_{q})γ ≫_{3} (F_{k}z_{1} … z_{q})γ′′, hence (F_{k}z_{1} … z_{q})γ′′ is computable. Let now γ′′′ be the substitution such that uγ →^{r} vγ′′′ and that we have just proved to be computable. Since F_{j} ∈ v implies j < i (by definition of HOR) then uγ ≫_{1} vγ′′′, hence w′ = vγ′′′ is computable and we get Red(w′, σ) (σ is the only type that can be assigned to w′).

v. Let u = fz_{1} … z_{q} and w = uγ. Since uγ is of base type, it is computable iff it is strongly normalizable. The latter property follows from Lemma 6 (Principal Case).

vi. Finally, let u = Xx_{1} … x_{q} and w = uγ → w′ at the root.

Then w is either (fx_{1} … x_{q})γ or (F_{k}x_{1} … x_{q})γ or (without loss of generality γ can be assumed idempotent) (ft_{1} … t_{j}x_{1} … x_{q})γ or (F_{k}t_{1} … t_{j}x_{1} … x_{q})γ, which have already been shown computable. This finishes the proof.

3.2 Confluence of →_{mix}

We recall first the definition of confluence. A reduction relation → is 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 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 [18]). So, since we have already proved that →_{mix} is strongly normalizing on Λ_{∧RH}, it is sufficient to prove local confluence.

First we have to prove that the confluence of →_{R} for algebraic terms transfers to terms in Λ_{∧RH}, and that HOR is confluent when there are no critical pairs. Lemma 8. If R is confluent and strongly normalizing on the set of algebraic terms then →_{R} is locally confluent on Λ_{∧RH}.

For terminating first order rewrite systems it is well-known that the absence of critical pairs implies confluence. The same property holds for the class of higher order rewrite systems we consider (Lemma 9 below). However, it is not true for arbitrary higher order rewrite systems, as shown in [19]. There the same lemma is proved for another class of higher order rewrite systems that differ from ours in that rules are required to be of base type and λ-terms are allowed in left-hand sides of rules. We do not need to impose the first restriction because we are assuming that all left-hand sides are algebraic. Lemma 9. Let HOR be a higher order rewrite system satisfying the general schema. If there is no critical pair then →_{HOR} is confluent on Λ_{∧RH}.

Theorem 10 (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. Since on Λ_{∧RH} →_{β} is confluent, →_{HOR} is confluent (by Lemma 9) and →_{R} is confluent (by Lemma 8), 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 v_{3} such that v_{1} →_{mix}^{∗} v_{3} and v_{2} →_{mix}^{∗} v_{3}.

Let t′ be the term obtained out of 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, satisfies the hypothesis and then →_{mix} is confluent in this case.

Acknowledgments: We would like to thank Val Breazu-Tannen for his comments on the proof of confluence. Special thanks to Jean-Pierre Jouannaud and Mariangiola Dezani for many fruitful discussions and for reading a previous version of this paper. Thanks also to Giuseppe Castagna for his help in proving strong normalization, and to Delia Kesner and Walid Sadfi for their support.

References

1. S. van Bakel, S. Smetsers, and S. Brock. Type assignment in left linear applicative term rewriting systems. In Proc. of CAAP’92. Colloquium on Trees in Algebra and Programming, Rennes, France, 1992, 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, 1990.

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

4. 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.

5. H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 2nd ed., 1984.

6. Val Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.

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

8. F. Cardone and M. Coppo. Two extensions of Curry’s type inference system. In P. Odifreddi, editor, Logic and Computer Sciennce. Academic Press, 1990.

9. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243– 309. North-Holland, 1990.

10. Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.

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

12. M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. Lecture Notes in Computer Science, 78, 1979.

13. R. Hindley. Types with intersection, an introduction. Formal aspects of Computing, 1990.

14. R. Hindley and J. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.

15. 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.

16. J. W. Klop. Term rewriting systems: a tutorial. EATCS Bulletin, 32:143–182, June 1987.

17. D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51–68, 1986.

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

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

20. 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.

21. G. Pottinger. A type assignment for the strongly normalizable λ-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 561– 578. Academic Press, 1980.

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

23. D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In Functional Programming Languages and Computer Architecture, Nancy, LNCS 201. Springer-Verlag, September 1985.

This article was processed using the LaTEX macro package with LLNCS style