Jean-Pierre Jouannaud

Albert Rubio

Normal Higher-Order Termination

Keywords: F.4.1 [Mathematical Logic]: Lambda calculus and related systems; F.4.2 [Grammars and Other Rewriting Systems] Higher-order rewriting, higher-order orderings, higher-order patterns, typed lambda calculus

We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higherorder pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church's simply typed λ-calculus, and on the other hand, any use of eta, as a reduction, as an expansion or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.

INTRODUCTION

Rewrite rules are used in logical systems to describe computations over lambdaterms used as a suitable abstract syntax for encoding functional objects like programs or specifications. This approach has been pioneered in this context by Nipkow [START_REF] Mayr | Higher-Order Rewrite Systems and Their Confluence[END_REF]] and is available in Isabelle [START_REF] Nipkow | Isabelle-91[END_REF]. Its main feature is the use of higher-order pattern matching for firing rules. A generalization of Nipkow's setting allows using rewrite rules of higher type [Middeldorp et al. 2005;[START_REF] Jouannaud | Church-Rosser Properties of Normal Rewriting[END_REF]. Besides, it is shown there that using the extensionality rule as an expansion [START_REF] Nipkow | Higher-Order Critical Pairs[END_REF]] or as a reduction [START_REF] Jouannaud | Higher-Order Rewriting: Framework, Confluence and Termination[END_REF]] yields very similar confluence checks based on higher-order critical pairs.

A first contribution of this paper is a general setting for addressing termination of all variants of higher-order rewriting à la Nipkow, called normal termination, thanks to the notion of a normal higher-order reduction ordering. While higherorder reduction orderings target termination of higher-order rewriting based on plain pattern matching, hence must include β-reductions, normal higher-order or-derings target termination of higher-order rewriting based on higher-order pattern matching, hence must be compatible with βη-equality. We show however that, in general, monotonicity, stability, compatibility and well-foundedness cannot be satisfied at the same time. This leads to the definition that higher-order rewrite orderings are normal when they include a subrelation enjoying some stability property for terms in βη-normal form. Checking the rewrite rules against such a subrelation then ensures normal termination.

How to build normal higher-order reduction orderings from higher-order reduction orderings is our second contribution, that we illustrate with the case of the higher-order recursive path ordering HORPO [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], yielding its normal version NHORPO. Some examples of use are presented. The method would also apply to other similar orders, such as CPO [START_REF] Blanqui | The Computability Path Ordering: The End of a Quest[END_REF]].

This method does not work well in the presence of abstractions in the righthand side of rules. Our third contribution is an interpretation-based framework that solves this problem, at an abstract level first, where the properties of such interpretations are specified which imply preservation of normal termination, and then at a concrete level, by defining a particular termination-preserving interpretation, neutralization, whose role is to remove abstractions that can never be applied. Combining neutralization with NHORPO allows us to solve complex examples from the literature.

So far, these methods target the use of higher-order reduction orderings. In the recent years, other methods have popped up that allow us to show higher-order termination, like higher-order dependency pairs. The question arises whether these methods that aim at proving higher-order termination can also be turned into methods aiming at proving normal higher-order termination? Our fourth contribution is a transformation of a higher-order rewrite system R into a new system R containing β-reductions, such that R is normal terminating if R is terminating. Our second contribution then appears as a refinement of the latter when using a method based on a higher-order reduction ordering like HORPO.

We describe our framework for simply typed terms in Section 2, and for higherorder rewriting in Section 3. NHORPO is given in Section 4 and illustrated by an example. Termination-preserving interpretations, including neutralization, are introduced and studied in Section 5. Our implementation is described briefly in Section 7, several examples are carried out there. Section 6 covers weak polymorphism, and is illustrated by yet another example. Our general transformation reducing normal higher-order termination to higher-order termination is introduced and illustrated in Section 8. The relevant literature is discussed in Section 9 where it is compared with the present work whose significance is discussed at this occasion. Brief concluding remarks are given in Section 10.

Readers are assumed familiar with the basics of term rewriting [START_REF] Dershowitz | Rewrite Systems[END_REF][START_REF]Term Rewriting Systems[END_REF]] and typed lambda calculi [START_REF] Pieter | Higher-order dependency pairs[END_REF].

T S := s(T n S ) | (T S → T S ) for s : * n ⇒ * ∈ S
Types are functional when headed by the → symbol, and data types when headed by a sort symbol. As usual, → associates to the right. We will often make explicit the functional structure of an arbitrary type τ by writing it in the canonical form σ 1 → . . . → σ n → σ, with n ≥ 0, where n is the arity of τ and σ is a data type called canonical output type of τ . We use σ, τ, ρ, θ for arbitrary types.

We are given a set of function symbols denoted by the letters f, g, h, which are meant to be algebraic operators equipped with a fixed number n of arguments (called the arity) of respective types σ 1 ∈ T S , . . . , σ n ∈ T S , and output type σ ∈ T S . Let F = σ 1 ,...,σn,σ F σ 1 ×...×σn⇒σ be the set of all function symbols. The membership of a given function symbol f to a set F σ 1 ×...×σn⇒σ is called a type declaration and written f : σ 1 × . . . × σ n ⇒ σ. In case n = 0, the declaration is written f : σ. A type declaration is first-order if its constituent types are data types, and higherorder otherwise. F is said to be first-order if all its type declarations are first-order, and higher-order otherwise.

The pair S; F is called the signature. We say that the signature is first-order, higher-order when F satisfies the corresponding property.

Raw terms

The set T (F, X ) of raw algebraic λ-terms is generated from the signature F and a denumerable set X of variables according to the following grammar rules:

T := X | (λX : T S .T ) | @(T , T ) | F(T , . . . , T ).

Raw terms of the forms λx : σ.u, @(u, v), and f (t 1 , . . . , u n ) are respectively called abstractions, applications, and pre-algebraic. As a matter of convenience, we may sometimes omit the type σ in λx : σ.u and write @(u, v 1 , . . . , v n ) for @(. . . @(u, v 1 ), . . . , v n ), assuming n ≥ 1.

Our syntax requires using explicit applications for variables, since they cannot take arguments. In the examples, we shall however allow ourselves writing X(v 1 , . . . , v n ) for @(X, v 1 , . . . , v n ) when X is a higher-order variable. On the other hand, function symbols have arities, eliminating the need for an explicit application of a function symbol to its arguments. Currying a function symbol is possible by taking zero for its arity.

Raw terms are identified with finite labeled trees by considering λx : σ. , for each variable x and type σ, as a unary function symbol taking a raw term u as argument to construct the raw term λx : σ.u. We denote the set of free variables of the raw term t by Var(t), and its size (the number of symbols occurring in t) by |t|. A raw term is closed if it has no free variable. The notation s will be ambiguously used to denote a list, or a multiset, or a set of raw terms s 1 , . . . , s n .

Positions are strings of positive integers. Λ and • denote respectively the empty string (root position) and the concatenation of strings. We use Pos(t) for the set of positions in t, and > for the prefix ordering on positions. Incomparable positions are called disjoint. The subterm of t at position p is denoted by t| p , and we write t ¤ t| p for the subterm relationship. The result of replacing t| p at position p in t by u is denoted by t[u] p , and we denote it by t[u] p 1 ...pn if the same replacement is made in several positions p 1 . . . p n at once. Accordingly, we use t[x : σ] p for a raw term with a unique hole of type σ at position p, called a context (and respectively t[x : σ] p 1 ...pn when we have several holes). Both p and x : σ may be omitted.

Typing

Definition 2.1. An environment Γ is a finite set of pairs written as {x 1 : σ 1 , . . . , x n : σ n } such that x i ∈ X , σ i ∈ T S , and x i = x j for i = j. Var(Γ) = {x 1 , . . . , x n } is the set of variables of Γ. We may write Γ(x i ) for σ i . Given two environments Γ and Γ , their composition is the environment Γ

• Γ = Γ ∪ {x : σ ∈ Γ | x ∈ Var(Γ )}. Γ is compatible with Γ if Γ • Γ = Γ ∪ Γ .
We now collect all declarations into a single environment Σ; Γ, of which the signature Σ = S; F is the fixed part. We assume that there is exactly one declaration for each symbol in an environment Σ; Γ. We may omit Σ in our examples, using the word environment for Γ alone.

Typing rules restrict the set of raw terms by constraining them to follow a precise discipline. Our typing judgments are written as Γ Σ s : σ, and read "s has type σ in the environment Γ". The typing judgments are displayed in Figure 1.

Variables: x : σ ∈ Γ Γ Σ x : σ Abstraction: Γ • {x : σ} Σ t : τ Γ Σ (λx : σ.t) : σ → τ Application: Γ Σ s : τ → σ Γ Σ t : τ Γ Σ @(s, t) : σ Functions: f : σ 1 × . . . × σ n ⇒ σ ∈ F Γ Σ t 1 : σ 1 . . . Γ Σ t n : σ n Γ Σ f (t 1 , . . . , t n ) : σ Fig. 1.
Typing judgments in higher-order algebras Given an environment Σ; Γ, a raw term s has type σ if the judgment Γ Σ s : σ is provable in our type system. Given an environment Σ; Γ, a raw term s is typable, and said to be a term if there exists a type σ such that Γ Σ s : σ. Classically, we consider the proof of a given judgment as a tree whose nodes are labeled by the judgments derived in the proof and the edges by the names of the rules used in the proof. We use as usual Pos(P ) for the set of positions of the proof tree P . We can therefore speak of the rule used at a position p ∈ Pos(P ) whose conclusion labels the node at p while its premises, displayed above the conclusion, label its sons.

We shall use without mentioning that a term has a unique type in a given environment. We further recall two important typing properties of HOAs used later: LEMMA 2.2 (SUBTERM). Let P denote the proof of the judgment Γ Σ s : σ and p be a position in Pos(s). Then, there exists a unique position q ∈ Pos(P ) such that the subproof P | q is a proof of a judgment of the form Γ s|p Σ s| p : τ in which τ is the type of s| p in Γ s|p .

LEMMA 2.3 (REPLACEMENT). Assume given an environment Σ; Γ, two terms s and v, two types σ and τ , and a position p ∈ Pos(s) such that Γ Σ s : σ, Γ s|p Σ s| p : τ , and

Γ s|p Σ v : τ . Then, Γ Σ s[v] p : σ. 2.4. Substitutions Definition 2.4. A substitution γ = {x 1 → t 1 , . . . , x n → t n } is a finite set of pairs made of a variable in its domain Dom(γ) = {x 1 , . . . , x n } and a term in its range Ran(γ) = {t 1 , . . . , t n }, such that ∀i ∈ [1..n], t i = x i and ∀i = j ∈ [1..n],
x i = x j . We denote by γ \V the restriction of γ to the variables in Var(γ) \ V . We use the letter γ for substitutions and postfix notation for their application.

Definition 2.5. A substitution γ operates as an endomorphism on s and yields the term sγ defined as:

If s = x ∈ X and x ∈ Var(γ)

then sγ = x If s = x ∈ X and x → t ∈ γ then sγ = t If s = @(u, v) then sγ = @(uγ, vγ) If s = f (u 1 , . . . , u n ) then sγ = f (u 1 γ, . . . , u n γ) If s = λx : τ.u
then sγ = λz : τ.uγ x where γ x = γ \{x} ∪ {x → z} for some fresh variable z.

A notion of typed substitution is used in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. The present more convenient untyped notion is borrowed from [START_REF] Blanqui | The Computability Path Ordering[END_REF]]. As expected, substitutions preserve typability: LEMMA 2.6 (TYPE INVARIANCE). Let s, t be two terms and γ be a substitution such that t = sγ. Then, (i) if Γ Σ s : σ and ∀x ∈ Var(s), Θ Σ xγ : Γ(x) for some environments Γ, Θ and type σ, then Θ Σ sγ : σ.

(ii) if Γ Σ t : τ for some environment Γ and type τ , then there is some environment Θ such that Θ Σ s : τ and Γ Σ xγ : Θ(x) for all x ∈ Var(s).

Conversions

The following three equations originate from the (pure) λ-calculus, and are called α-, βand η-equality respectively:

λx : α.u = α λy : α.u{x → y} if y ∈ BV ar(v) ∪ (Var(v) \ {x}) @(λx : σ.v, w) = β v{x → w} λx : σ.@(u, x) = η u if x ∈ Var(u)
(usually called extensionality)

In the above equations, u, v and w stand for arbitrary terms to which substitutions {x → y} and {x → u} apply. We consider α-convertible terms as identical, and therefore omit α-conversions in the sequel. Both β and η-equalities can be oriented as rewrite rules. There are two possible choices for rewriting with η, either as a reduction (from left to right) or as an expansion (from right to left), in which case termination is ensured by restricting its use to positions other than the first argument of an application. Typed lambda-calculi have all termination and Church-Rosser properties one may need, as recalled below.

We consistently use the following important notations: u -→ β v for one β-rewrite step, u -→ * β v for its reflexive, transitive closure, and = β for its symmetric, reflexive, transitive closure, also called β-equality. Similarly u -→ η v, u -→ * η v, and = η are the corresponding notations for η used as a reduction. We also use u↓ β , u↓ η and u↓ βη for the β-normal form, η-normal form and βη-normal form of a typable term u. The notation u↓ is exclusively used as a short form of u↓ βη . We say that a term is β-normal (resp., η-normal, normal) if it is in normal form for β-reduction (resp., η-reduction, βη-reductions). We shall not need a notation for η-expansion, η-long forms or β-normal η-long forms. We shall use, possibly without mentioning, several related properties of the simply typed λ-calculus:

(1) Subject reduction: Assume Γ Σ s : σ and s -→ β t. Then, Γ Σ t : σ.

(2) η-preservation: Assume Γ Σ s : σ and s ←→ η t. Then, Γ Σ t : σ.

(3) Postponement of η:

(∀u, v, w) u = η v -→ β w, (∃v ) u -→ * β v = η w. (4) Church-Rosser property (i) of β-reductions: s = β t implies s↓ β = t↓ β (5) Church-Rosser property (ii) of η-reductions: s = η t implies s↓ η = t↓ η (6) Church-Rosser property (iii) of β-reductions modulo η: s = βη t iff s↓ β = η t↓ β (7) Church-Rosser property (iv) of βη-reductions: s = βη t iff s↓= t↓ (8) Closedness of η-normal forms by instantiation: (tγ)↓ η = t↓ η γ↓ η ,
a consequence of (5), since variables bound in t cannot occur free in γ.

NORMAL HIGHER-ORDER REWRITING OF HIGHER TYPE

Introduced in [START_REF] Nipkow | Higher-Order Critical Pairs[END_REF]], normal higher-order rewriting allows defining computations over λ-terms used as a suitable abstract syntax for encoding functional objects like programs or specifications. It differs from the more traditional definition of plain higher-order rewriting from [START_REF] Jouannaud | A Computation Model for Executable Higher-Order Algebraic Specification Languages[END_REF]:

Definition 3.1. A rewrite rule is a pair of terms written l → r, such that l ∈ X , Var(r) ⊆ Var(l) and (∀Θ, θ, γ) Θ Σ lγ : θ iff Θ Σ rγ : θ. A higher-order term rewriting system is a set of rules containing both rules β and η.

Given a higher-order term rewriting system R, an environment Γ, two higherorder terms s and t, and a type σ such that Γ Σ s : σ, we say that s rewrites to t at position p with the rule l → r and the term substitution γ, written Γ s -→ p R t, or s -→ p R t assuming Γ, if s| p = lγ and t = s[rγ] p . Nipkow's formulation of normal higher-order rewriting, uses β and η in two different ways, both as rules and equalities: given a term s to be rewritten with a set R of rules, s is first normalized, using η-long β-normal forms, before being searched for lefthand sides of rules in R via higher-order pattern matching [START_REF] Nipkow | Higher-Order Critical Pairs[END_REF][START_REF] Mayr | Higher-Order Rewrite Systems and Their Confluence[END_REF]]. In [Middeldorp et al. 2005;Jouannaud and Li 2012], Nipkow and Mayr's confluence result is generalized by allowing using η as a reduction on the one hand, and rules of higher type on the other hand.

We now define normal higher-order rewriting so as to capture the different ways in which a term can be βη-normalized before pattern-matching a subterm with a lefthand side of rule. This definition is not meant to be used for computing, as is the case of the previous just mentioned two. The fact that it has poor operational properties (including confluence) is therefore irrelevant. Its sole purpose is to study the termination properties of Nipkow's normal higher-order rewriting and its variants: by providing a method for proving termination of this more general relation, we do provide a method for all variants of higher-order rewriting based on higherorder pattern matching, independently of a particular orientation of extensionality.

From now on, by normal higher-order rewriting (possibly omitting normal), we mean the coming definition, while Nipkow's specific definition is systematically referred to as Nipkow's higher-order rewriting. Definition 3.2. A normal rewrite rule is a pair of β-normal terms written l → r, such that l↓ η ∈ X , Var(r) ⊆ Var(l) and (∀Θ, θ, γ) Θ Σ lγ↓ β : θ iff Θ Σ rγ↓ β : θ.

A normal term rewriting system is a set of normal rules. Given a normal term rewriting system R, an environment Γ, two β-normal terms s and t, and a type σ such that Γ Σ s : σ, we say that s rewrites to t at position p with the normal rule l → r and the β-normal term substitution γ, written Γ

s -→ p R βη t, or s -→ p R βη t assuming Γ, if s| p = βη lγ and t = η s[rγ] p ↓ β .
Note that our definition does not require rules to be typable, but does require that in case they are, then, their normalized instances have the same type. This property is weaker than usual, but suffices for our purpose and is indeed more convenient to work with. A key observation is:

LEMMA 3.3 (TYPE PRESERVATION). Let s be a β-normal term such that Γ Σ s : σ and Γ s -→ p R βη t. Then Γ Σ t : σ.
PROOF. By Lemma 2.2, Γ s|p Σ s| p : τ . Let l → r be the rule of R matching s| p , hence s| p = βη lγ. Since s is β-normal, so is s| p , hence, by Property (6) of untyped λ-calculus, (lγ)↓ β = η s| p . By η-preservation, Γ s|p Σ (lγ)↓ β : τ . By Definition 3.2, Γ s|p Σ (rγ)↓ β : τ . By Lemma 2.3, Γ Σ s[(rγ)↓ β ] p : τ . By confluence and subject reduction, Γ Σ s[rγ] p ↓ β : τ . We conclude by η-preservation.

We often consider type preserving higher-order rewriting as a relation on terms instead of on judgments, therefore simplifying our notations.

Example 3.4 (differentiation). We present here an encoding of symbolic derivation in which functions are represented by λ-terms of a functional type. We give two typical rules of higher type. The free variable F stands for a function over the reals, while x, y stand for real values. Let S = {real}, and

F = { sin, cos : real → real; diff : (real → real) → real → real +, × : (real → real) → (real → real) → real → real}
diff(λx. sin(@(F, x))) → λx. cos(@(F, x)) × diff(λx.@(F, x)) diff(λx.@(F, x) × λy.@(F, y)) → (diff(λx.@(F, x)) × λy.@(F, y))+ (λx.@(F, x) × diff(λy.@(F, y)))

This example makes sense when using normal higher-order rewriting, because using plain pattern matching instead would not allow for computing the derivative of all expressions: rewriting the expression diff(λx.sin(x)) does require higherorder pattern matching, since taking for F the identity substitution λy.y, we have diff(λx.sin(@(λy.y, x)) -→ β diff(λx.sin(x)). Note that we use η-expanded forms here. We shall give a mechanical termination proof of these two rules in Section 4.

Higher-Order Reduction Orderings

We shall use well-founded relations for proving strong normalization properties [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. For our purpose, these relations may not be transitive, but their transitive closures will be well-founded orderings, justifying our abuse of terminology. We shall consider two kinds of higher-order reduction orderings, dubbed plain when they include β-reductions and normal when they are compatible with βη-equivalence.

s : σ) (Γ Σ t : σ), then (Γ Σ u[s] : τ ) (Γ Σ u[t] : τ ); -functional iff for all terms s, t, t such that (Γ Σ s : σ) (Γ Σ t : σ) and (Γ Σ t : σ -→ β t : σ) then (Γ Σ s : σ) (Γ Σ t : σ).
Note that our definition of functionality here is slightly weaker than the one in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF] which does not assume that s t.

Coherence is a natural property ensuring that a comparison does not depend upon the type of the variables in the compared terms. For example @(x, y) y should not depend upon the type of x, y. HORPO and other similar orders are coherent.

Definition 3.6. A higher-order reduction ordering is a well-founded ordering of the set of judgments satisfying coherence, stability and monotonicity. A higherorder ordering is plain if it also satisfies functionality.

Plain higher-order orderings are an adequate tool for proving strong normalization of plain higher-order rewriting. One may wonder whether they should also include some form of extensionality, as in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. This is indeed not possible if one wants to be compatible with both syntactic choices of having extensionality as either η-reduction (our choice in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]) or η-expansion (Di Cosmo-Kesner's choice in [Cosmo and Kesner 1994], which includes a discussion of their respective advantages).

Normal Higher-Order Reduction Orderings

We would need higher-order orderings satisfying the compatibility property: ∀s , s, t, t s.t. (Γ Σ s : σ = βη s : σ), (Γ Σ t : σ = βη t : σ) and

(Γ Σ s : σ) (Γ Σ t : σ) then (Γ Σ s : σ) (Γ Σ t : σ)
Unfortunately, no ordering can satisfy monotonicity, stability, compatibility and well-foundedness together: assume s : σ t : σ (omitting judgments), where s : σ is in β-normal form. Given a variable X : σ → τ , @(X, s) is in β-normal form as well. By monotonicity, @(X, s) : τ @(X, t) : τ . Consider the substitution γ = {X → λy.a} where a : τ is a constant. By stability, @(λy.a, s) : τ @(λy.a, t) : τ . By compatibility, a : τ a : τ , contradicting well-foundedness.

We therefore introduce a new kind of ordering for the normal case:

Definition 3.7. A normal higher-order reduction ordering (normal ordering) is a pair >, of a plain higher-order reduction ordering and a relation > satisfying: (i) normal η-compatibility: for all β-normal typed terms s, s , t s.t. s = η s t there exists some β-normal term t such that s t = η t. (ii) normal stability: for all β-normal typed terms s, t and β-normal substitutions γ, s > t implies (sγ)↓ β (tγ)↓ β .

Normal stability is a property that combines: inclusion of > into hence wellfoundedness (by taking the identity substitution for γ) ; β-compatibility by taking β-normal forms ; and a form of stability by instantiation. THEOREM 3.8. Let R = {l i → r i } i be a normal higher-order rewrite system, and (>, ) be a normal higher-order reduction ordering satisfying the property (∀l → r ∈ R, ∀Γ, ∀σ) Γ l : σ implies l > r for some l = η l and r = η r. Then, the relation -→ R βη is strongly normalizing.

PROOF. First, strong normalization is true for arbitrary terms provided it is true for closed terms, since adding new constants at every type does not influence termination. Note that η-equivalence classes of closed terms contains only closed terms.

Let therefore s be a closed β-normal term such that Γ Σ s : σ. The result is by noetherian induction on s with , showing the property, that will be useful to have as our induction argument, that no term in the η-equivalence of s can originate an infinite sequence of R-reductions.

If s is in R βη -normal form, then so are all its subterms s| p , for p ∈ Pos(s). Now, all terms in the η-equivalence class of s| p are in R βη -normal form by definition of higher-order rewriting, and we are done with this case.

Otherwise, by definition of higher-order rewriting, s rewrites at some position p ∈ Pos(s) with rule l → r ∈ R and β-normal substitution γ, hence s| p = βη lγ and t = η s[rγ] p ↓ β . Because rewriting cannot introduce free variables, t must be closed as well. We then show that s t for some β-normal term t = η t. By induction hypothesis, no term in the η-equivalence class of t can originate an infinite sequence of R-reductions. The property is therefore true of t, hence of s.

We are left showing that Γ Σ s t for some t = η t. Since s is β-normal, by Church-Rosser property (iii) and η-postponement, we have s| p = η (lγ)↓ β , hence s = η s[(lγ) ↓ β ] p . Using additionally Church-Rosser property (i), t = η s[(rγ) ↓ β ] p ↓ β . By assumption, l > r for some l = η l and r = η r, hence, by normal stability applied with the β-normal

substitution γ ↓ β , (l γ ↓ β )↓ β (r γ ↓ β )↓ β . By the Church-Rosser property (i), (l γ ↓ β ) ↓ β = (l γ) ↓ β and (r γ ↓ β ) ↓ β = (r γ) ↓ β , hence (l γ)↓ β (r γ)↓ β . Since s is closed, s[(l γ)↓ β ] p is closed as well. Further, Var((r γ)↓ β ) ⊆ Var(r γ) ⊆ Var(l γ) since is stable, hence s[(l γ)↓ β ] p is closed. Therefore, by monotonicity of , s[(l γ)↓ β ] p s[(r γ)↓ β ] p and, by functionality, s[(l γ)↓ β ] p s[(r γ)↓ β ] p ↓ β . By Church-Rosser property (i) again s[(l γ)↓ β ] p s[r γ] p ↓ β . Finally, by normal η-compatibility, s t = η s[r γ] p ↓ β = η t
where t is β-normal and we are done.

The actual meaning of this result is that rules should be checked with the restriction > of the higher-order reduction ordering instead of with itself.

This result improves over [START_REF] Jouannaud | Higher-Order Orderings for Normal Rewriting[END_REF] in two different ways: it applies to all forms of plain higher-order rewriting, independently of the orientation of η for normalizing terms, and of the type of the rules, basic or functional; by using simpler properties, it requires simpler arguments to justify the construction of normal higher-order orderings, making it an easier task. Further, lefthand sides of rules need not be patterns, an assumption that only becomes necessary to check the Church-Rosser property of higher-order rewrite rules via the computation of their higher-order critical pairs [START_REF] Nipkow | Higher-Order Critical Pairs[END_REF][START_REF] Jouannaud | Church-Rosser Properties of Normal Rewriting[END_REF].

THE NORMAL HIGHER-ORDER RECURSIVE PATH ORDERING

Our purpose here is to define a particular normal ordering (>, ). There are several possible candidates for , notably HORPO [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], the computability closure ordering CCO [START_REF] Blanqui | Computability Closure: Ten Years Later[END_REF]], the computability path ordering CPO [START_REF] Blanqui | The Computability Path Ordering: The End of a Quest[END_REF]] and the recursive path and polynomial ordering RPPO [START_REF] Bofill | The recursive path and polynomial ordering for first-order and higher-order terms[END_REF].

Our choice here for is the higher-order recursive path ordering HORPO, and therefore, in the remainder of this section, denotes the ordering HORPO. The reason is that HORPO is the simplest one, but we believe that our techniques would apply to CPO and CCO (and probably RPPO) as well. As all these orderings, HORPO is not an appropriate answer per se, that is, the pair , is not a normal ordering: (i) HORPO does not satisfy normal η-compatibility: we shall enforce it easily by comparing η-normal forms of terms in the first place.

(ii) HORPO does not satisfy normal stability, in particular because of applications @(X, v) which become a redex if X is instantiated by an abstraction. We shall forbid such cases.

Definition 4.1. A β-normal term u = f (u) with f ∈ F ∪ {@, λ} is non-versatile if uγ↓= f ((uγ)↓
) for all normal substitutions γ. Other β-normal terms are versatile.

Variables are versatile. Here is a sufficient syntactic condition for non-versatility: LEMMA 4.2. The following terms are non-versatile: (i) β-normal F-headed terms; (ii) β-normal typable applications @(v, w) with non-versatile v; (iii) βηnormal typable abstractions λx.v with non-versatile application-headed subterms.

This lemma provides an inductive way of checking non-versatility, which terminates since terms it applies recursively to are of decreasing size, and is stronger than the definition of non-versatility in [START_REF] Jouannaud | Higher-Order Orderings for Normal Rewriting[END_REF].

PROOF. We consider the three possible cases in turn. The case of β-normal Fheaded term is straightforward.

Let u = @(v, v ). Since u is β-normal, v cannot be an abstraction. And since v is non-versatile, then (vγ)↓ is not an abstraction either, concluding the proof.

Let now u = λx.v, assuming without loss of generality that x ∈ Dom(γ). In this case we prove the stronger property that for every term βη-normal term t such that all its subterms headed by application are non-versatile, we have that tγ↓= t(γ↓).

We proceed by induction on the size of t. If t is a variable we are done. Otherwise, if t = f (t) with f ∈ F, we have tγ ↓= f ((tγ)↓) and we can conclude by induction. If t = @(t 1 , t 2 ), since it is non-versatile, we have tγ↓= @(t 1 γ↓, t 2 γ↓), and again we conclude by induction hypothesis. Finally, if t = λx.u, then, by induction hypothesis, we have that uγ↓= u(γ↓). Hence, since tγ = λx.(uγ) and t is in βη-normal form, we have that λx.u(γ↓) is βη-normal form.

Fortunately, a simple restriction > of suffices to take care of versatile terms. We assume given: a partition M ul Lex of F; a quasi-ordering ≥ F on F, called the precedence, such that > F is well-founded; a quasi-ordering ≥ T S on types, which is taken here to be a recursive path ordering RPO on the type structure generated by ≥ F modified so as to satisfy all conditions given in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF] 1 : → cannot be bigger than or equal to sorts, and the subterm and status cases must be restricted appropriately for →. Here is our restriction of HORPO: Definition 4.3 (NHORPO). Given two terms, s : σ and t : τ , we define:

s>t iff s is normal, non-versatile , σ≥ T S τ and (1) s = f (s) with f ∈ F, and u ≥ t for some u ∈ s (2) s = f (s), t = g(t) with f > F g, and A (3) s = f (s), t = g(t) with f = F g ∈ M ul, and s (>) mul t (4) s = f (s), t = g(t) with f = F g ∈ Lex, s > lex t, and A (5) s = f (s), t = @(u, v), and A (6) s = f (s), t = λx.v, x ∈ Var(v)
and s > v (7) s = @(u, v) and w ≥ t for some w ∈ {u, v} (8) s = @(u, v), t = @(u , v ), and {u, v} > mul {u , v } (9) s = λx : σ.u and u{x → z} ≥ t with z fresh (10) s = λx : α.u, t = λx : β.v, α=β and u>v (11) s = λx.u, t is not a variable nor an abstraction, and u{x → z}≥@(t, z), z fresh where • A = ∀v ∈ t s>v or u≥v for some u ∈ s

• s ≥ t iff s > t or s ≡ t where • ≡ is the congruence on typed terms generated by the following axiom schemas (typed in an appropriate environment):

f (x) = g(x) f = F g, f ∈ Lex, g ∈ Lex f (x) = g(ξ(x)) f = F g, f ∈ M ul, g ∈ M ul, ξ a permutation λx.u = λz.u{x → z} z ∈ Var(λx.u)
Although > is defined on arbitrary terms, the computation proceeds only in case s is normal. Note that s is non-versatile in Cases (1) to (6). It is therefore sufficient to check the non-versatility requirement for s in cases ( 7) to (11) only.

Besides forbidding versatile terms in lefthand sides of a comparison, we also abandon flattening of the lefthand sides as in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], which makes the obtained order slightly less powerful but simpler. On the other hand, Case 11 enhances NHORPO's strength by replacing η-reduction with a combination of Cases 10 and 9 (called the middle term trick in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]). This is indeed needed to ensure that recursive calls apply to β-normal terms. On the other hand, the equivalence associated to ≥ is the same as the one for .

We now define the pair (> η , η ) using an extra ordering T :

Definition 4.4. Given two typable terms s : σ and t : τ , we define:

s : σ T t : τ if s t and σ = τ .

-

s η t iff s ↓ η + T t ↓ η and if s ↓ η = @(u, x) and x is a free variable such that x / ∈ Var(u) then u η λx.t. -s : σ > η t : τ iff s ↓ η > t ↓ η , σ = τ and if s ↓ η = @(u, v) then either v is non-versatile or v is a variable x and u > η λx.t.
We use + T instead of + , which would suffice for transitivity, because we need η to be also monotonic, and is only monotonic on terms with the same type. Note that we could make > η marginally stronger by replacing u > η λx.t by u η λx.t. We prefer having this stand-alone definition at no practical cost. LEMMA 4.5. Let s , s, t and t be terms. Then s = η s η t = η t implies s η t .

PROOF. We proceed by induction on the size of s. Since η is a plain higher-order reduction ordering of the set of terms. PROOF. The relation η is clearly a well founded relation of the set of terms, since so is . Coherence is clear. We are left with four properties proved in turn.

s η t, s ↓ η = s↓ η + T t ↓ η = t ↓ η . In case s ↓ η = @(u, x) with x / ∈ Var(u), then s ↓ η = @(u,
Monotonicity: if s :

σ η t : σ then u[s] η u[t]
for all u, s and t. We proceed by induction on the size of u, using monotonicity of HORPO [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. If u is empty we are done otherwise there are four cases:

(1) u[] = f (. . . u [] . . .) with f ∈ F. By induction hypothesis, u [s] η u [t], hence u [s]↓ η + T u [t]↓ η . The result follows by monotonicity of HORPO. (2) u[] = @(u [], v). By induction hypothesis, u [s] η u [t], hence u [s] ↓ η + T u [t] ↓ η . Therefore @(u [s], v) ↓ η = @(u [s] ↓ η , v ↓ η ) + T @(u [t] ↓ η , v ↓ η ) = @(u [t], v)↓ η , by monotonicity of HORPO. Assume @(u [s], v)↓ η = @(u [s]↓ η , v↓ η ) with v↓ η = x / ∈ Var(u [s]↓ η ) ⊆ Var(u [t]↓ η
) by stability of HORPO. We then further need to show that u [s]↓ η η λx.@(u [t], v). This follows from the fact that u [s] η u [t] = η λx.@(u [t], x) and Lemma 4.5.

(3) u[] = @(v, u []). This case is similar to the first part of the previous case.

(4) u[] = λx.u []. By induction hypothesis, u [s] η u [t], hence u [s]↓ η + T u [t]↓ η . By Church-Rosser property (ii), (λx.u [s])↓ η =(λx.u [s]↓ η )↓ η . We get two cases: -(λx.u [s] ↓ η ) ↓ η = λx.(u [s] ↓ η ).By monotonicity of HORPO, we have λx.(u [s]↓ η ) + T λx.(u [t]↓ η ), hence (λx.u [s]↓ η )↓ η + T (λx.u [t]↓ η )↓ η
, since HORPO includes η-reductions, which preserve types, and we are done.

u [s↓ η ] = @(u, x), where x is a free variable such that x / ∈ Var(u [s]↓ η ) and

(λx.u [s]↓ η )↓ η = u. Then u η λx.u [t], and since λx.u [t] = η (λx.u [t]↓ η )↓ η , then u η (λx.u [t]↓ η )↓ η by Lemma 4.5

, and we are done again

Transitivity: s η t η u implies s η u. The proof is by induction on the size of s. By definition s ↓ η

+ T t ↓ η + T u ↓ η , hence s ↓ η + T u ↓ η . Assuming s↓ η = @(w, x) with x /
∈ Var(w), then w η λx.t. By monotonicity, λx.t η λx.u. Hence w η λx.t η λx.u. By induction hypothesis, w η λx.u, and we are done.

Stability follows from the property, given s and γ, that sγ↓ η = (s↓ η )(γ↓ η ). Functionality: assuming s η t -→ β u, we prove that s η u by induction on the size of s. By definition, s↓ η + T t↓ η and t -→ β u. By Church-Rosser property (iii), t ↓ η -→ * βη u ↓ η , and since HORPO includes βand η-reductions [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], and both preserve types, then s↓ η + T u↓ η . Assume that s↓ η = @(w, x) with x / ∈ Var(w). Then w η λx.t. Therefore w η λx.t -→ β λx.u, hence, by induction hypothesis, w η λx.u and we are done. THEOREM 4.7. The pair (> η , η ) is a normal higher-order reduction ordering.

PROOF. Using Lemma 4.6, we are left proving normal η-compatibility, which follows from Lemma 4.5, and normal stability: for all β-normal terms s : σ, t : τ and β-normal substitutions γ, s : σ > η t : τ implies (sγ)↓ β : σ η (tγ)↓ β : τ . We proceed by induction on the size of s. By definition of η , this requires (sγ)↓ β ↓ η + T (tγ)↓ β ↓ η and if (sγ)↓ β ↓ η = @(u , y) and y is a free variable such that y / ∈ Var(u ) then u η λy.((tγ)↓ β ). We first prove the second part.

Assume (sγ)↓ β ↓ η = @(u , y) and y is a free variable such that y / ∈ Var(u ). By Church-Rosser properties (ii)-(iv), we have that (s↓ η γ)↓= (sγ)↓ β ↓ η , and since s ↓ η > t ↓ η implies that s ↓ η is non-versatile, we have that if (s ↓ η γ) ↓= @(u , y) then s↓ η = @(u, v), with (uγ)↓= u and (vγ)↓= y. Moreover, since s > η t and s↓ η = @(u, v), we have that either v is non-versatile or v is a variabe x and u > η λx.t. Since (vγ)↓= y, we have that v cannot be non-versatile, and hence v must be a free variable x and x(γ↓) = y, which, by Church-Rosser property (iii), implies that x(γ ↓ β ) = η y, and hence, by confluence, (t{x → y}γ)

↓ β = η (tγ) ↓ β . Then, by induction hypothesis, (uγ)↓ β η ((λx.t)γ)↓ β , which is, by α-conversion, equal to ((λy.t{x → y})γ) ↓ β = (λy.(t{x → y}γ)) ↓ β = λy.((t{x → y}γ) ↓ β ) = η λy.((tγ)↓ β ), and by η-compatibility, (uγ)↓ β ↓ η η λy.((tγ)↓ β ).
We are left with proving that (sγ)

↓ β ↓ η + T (tγ) ↓ β ↓ η , that is (sγ) ↓ +
T (tγ) ↓ under the assumption that s ↓ η > t ↓ η and σ = τ . Since (sγ) ↓: σ and (tγ) ↓: τ and, by confluence, (sγ)↓= (s↓ η γ)↓ and (tγ)↓= (t↓ η γ)↓, we can prove (sγ)↓: σ + T (tγ)↓: σ under the assumption that s : σ > tσ for normal terms s and t. Additionally, since HORPO includes βand η-reductions [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF] and both preserve types, it suffices to show the following property: (i) s > t implies (sγ)↓ w for some w such that tγ -→ * βη w. Showing (i) will need (ii) s ≡ t implies (sγ)↓≡ (sγ)↓. Further, (i) and (ii) both together imply (iii) s ≥ t implies (sγ)↓ w for some w such that tγ -→ * βη w. We prove (ii) by induction on the size of s. Assume s ≡ t. There are four cases.

s = t. Then (sγ)↓= (tγ)↓ and we are done.

s = f (s), t = g(t), f = F g, f ∈ Lex, g ∈ Lex and s ≡ t. Then, by induction hypothesis, (sγ)↓≡ (tγ)↓ and therefore (sγ We now prove (i) by induction on the pair s, t ordered lexicographically by size. There are 11 cases according to the definition of NHORPO:

)↓= f ((sγ)↓) ≡ g((sγ)↓) = (tγ)↓. -s = f (s), t = g(ξ(s)), f = F g, f ∈ M ul, g ∈ M ul, ξ a permutation. Similarly, (sγ)↓= f ((sγ)↓) ≡ g(ξ(sγ)↓) = (tγ)↓. -s = λx.u, t = λz.v{x → z} with z ∈ Var(λx.v),
(1) s = f (s) with f ∈ F, and u ≥ t for some u ∈ s. By, induction hypothesis (i) and property (ii), (uγ)↓ w for some w such that tγ -→ * βη w, and since (f (s)γ)↓= f ((sγ)↓), we conclude by Case 1 of HORPO.

(2) s = f (s), t = g(t) with f > F g, and for all v i ∈ t, s > v i or u ≥ v i for some u ∈ s. By induction hypothesis (i) and property (ii), for all v i ∈ t, (sγ)↓ w i or (uγ)↓ w i for some w such that

v i γ -→ * βη w i . Since (f (s)γ)↓= f ((sγ) ↓), then (sγ) ↓ g(w 1 γ, . . . , w i ) = w by Case 2 of HORPO. Since tγ = g(v 1 γ, . . . , v n γ) -→ *
βη w, we are done with this case. (3) s = f (s), t = g(t) with f = F g ∈ M ul, and s (>) mul t. Then, by induction hypothesis on (i) and property (ii), (sγ)↓ ( ) mul w for some w such that t -→ * βη w. We conclude by Case 3 of HORPO. (4) s = f (s), t = g(t) with f = F g ∈ Lex, s > lex t, and for all v i ∈ t, then s > v i or u ≥ v i for some u ∈ s. This case is similar to Case 2. (5) s = f (s), t = @(t 1 , t 2 ), and for all t i , then s > t i or u ≥ t i for some u ∈ s. By induction hypothesis (i) and property (ii), for all t i , then (sγ)↓ w i or (uγ)↓ w i for some w i such that t i -→ * βη w i . We conclude thanks to Case 5 of HORPO. (6) s = f (s), t = λx.v, x ∈ Var(v) and s > v. By induction hypothesis (i), (sγ)↓ w with vγ -→ * βη w . Since, (f (s)γ)↓= f ((sγ)↓), we conclude as in case 3.

(7) s = @(u, v) is non-versatile and s ≥ t for some s ∈ {u, v}. Since s is non-versatile then (sγ)↓= @((uγ)↓, (vγ)↓), and we conclude as in Case 3. (8) s = @(u, v), t = @(u , v ), and {u, v} > mul {u , v }. Since s is non-versatile, then (sγ)↓= @((uγ)↓, (vγ)↓) and we conclude as in Case 3. (9) s = λx : σ.u and u{x → z} ≥ t with z fresh. Since s is non-versatile, then (sγ) ↓= λx.((uγ) ↓). By, induction hypothesis (i) and property (ii), (u{x → z}γ)↓ w with tγ -→ * βη w, and, since z is fresh, (u{x → z}γ)↓= ((uγ)↓ ){x → z}. We conclude as in case 3. (10) s = λx : α.u, t = λx : β.v, α = β and u > v. Since s is non-versatile, then (sγ)↓= λx.((uγ)↓). By induction hypothesis (i), (uγ)↓ w for some w such that vγ -→ * βη w , and we conclude as in Case 3. (11) s = λx.u, t is not an abstraction and u{x → z} ≥ @(t, z), z fresh. Since s is non-versatile, then (sγ) ↓= λx.((uγ) ↓). By induction hypothesis (i) and property (ii), (u{x → z}γ) ↓ w with @(t, z)γ -→ * βη w . Since z is fresh, (u{x → z}γ) ↓= (uγ) ↓ {x → z}. Since t is not a variable nor an abstraction, w = @(w, z) and tγ -→ * βη w. Therefore, (uγ) ↓ {x → z} @(w, z), which implies by monotonicity and α-conversion λx.(uγ) ↓ λx.@(w, x). Since HORPO includes η-reduction, we get (sγ)↓= λx.(uγ)↓ w. We assume here that this can be done with HORPO in one step, which could be achieved by adding the necessary case without modifying HORPO as an order.

We can therefore use (> η , η ) as our normal higher-order ordering for checking whether a given higher-order rewrite system R is terminating. However, note that the lefthand side l of a rule l → r ∈ R must be in β-normal form in order to use NHORPO via η , since NHORPO needs lefthand sides of comparisons to be normal to have a chance of success, which will be the case by η-postponement.

We strongly believe that the very same changes as done here work equally well for similarly defined higher-order reduction orderings such as CPO [START_REF] Blanqui | The Computability Path Ordering: The End of a Quest[END_REF], with a similar proof as for HORPO, although details have not checked.

Example 4.8 (differentiation continued). Symbols have multiset status, sin and cos are equal in the precedence, diff is bigger than all others. We consider only the first rule. Our goal is: diff(λx. sin(@(F, x))) > λx. cos(@(F, x)) × diff(F), which, by Case 2, yields two subgoals:

Subgoal 1: diff(λx. sin(@(F, x))) > λx. cos(@(F, x)) which succeeds by Case 1 since λx. sin(@(F, x)) = λx. cos(@(F, x)), sin and cos having the same precedence.

Subgoal 2: diff(λx. sin(@(F, x))) > diff(F) which, by Case 3 yields Subgoal 3: λx. sin(@(F, x)) > F. We cannot apply Case 9 here as one might have expected, the type of F is too large. We use instead Case 11, which yields: Subgoal 4: sin(@(F, x)) > @(F, x) which succeeds by Case 1. Since η , > is a normal higher-order reduction ordering, we conclude normal termination of (the first rule of) our example by using theorems 3.8 and 4.7 together.

Many examples cannot be treated by normal HORPO, because the only rule able to handle abstractions on the righthand side are the weak Rule 6 and the monotonicity Rule 10. Some of these examples would work with normal CPO, which was designed to remedy this very weakness of HORPO. This question is indeed at the heart of the next section, where a powerful technique is presented that makes it possible to solve complex goals, even when CPO itself would fail.

INTERPRETATIONS FOR NORMAL HIGHER-ORDER REWRITING

The profusion of abstractions on both the lefthand and righthand sides of rules in normal higher-order rewrite rules is a challenge for termination proofs, even when using CPO instead of HORPO. This is the question addressed in this section. To this end, we introduce neutrlization, a particular higher-order interpretation aimed at eliminating abstractions which cannot originate reductions. Higher-order term interpretations that preserve termination of higher-order rewriting are studied first, making no assumption whatsoever on the method used for carrying out such a termination proof. On the other hand, we make an assumption on higher-order rules: their lefthand side is either of basic type or headed by an algebraic function symbol.

Definition 5.1. A higher-order interpretation is a mapping from higher-order terms to higher-order terms which is the identity on free variables and preserves types in a given environment: (∀Γ, u, σ) such that Γ Σ u : σ, then Γ Σ I(u) : σ.

Higher-order interpretations are extended to terms, substitutions, rewrite rules, and rewrite systems in the natural way.

The role of our assumption that types are preserved ensures that term manipulations in interpreted terms preserve typability. More general assumptions are of course possible, provided they achieve the same property and ensure that if two terms the same type σ, then their interpretations have the same type τ for some τ .

Definition 5.2. A higher-order interpretation I : T (F, X ) → T (F , X ) is normal if it satisfies the following properties:

β-compatibility: s = β t implies I(s) = β I(t) for every two typed terms s and t ; -η-compatibility: s = η t implies I(s) = η I(t) for every two typed terms s and t ; -preservation of β-normal forms: I(t) is β-normal whenever t is ; -preservation of algebraic head:

I(t) is F -headed if t is F-headed ; -monotonicity: ∀β-normal u, ∀p ∈ Pos(u), there exists a set {q 1 , . . . , q n } n>0 of disjoint positions in I(u) such that, ∀β-normal t, I(u[t] p ) = βη I(u)[I(t)
] q 1 ...qn ; -stability: for all β-normal term t and substitution γ, I(tγ) = βη I(t)I(γ).

LEMMA 5.3. Let t and u be higher-order terms. Then, for every set {p 1 . . . p m } of disjoint positions in Pos(t) there is a set {q 1 , . . . , q n } of disjoint positions in Pos(t↓ β ) such that t[u] p 1 ...pm ↓ β = (t↓ β [u↓ β ] q 1 ,...,qn )↓ β . Further, if u has a basic type or is headed by an algebraic symbol, then t

[u] p 1 ...pm ↓ β = t↓ β [u↓ β ] q 1 ...qn .
PROOF. Follows from the Church-Rosser property of β-reductions, and the fact that u↓ β has a basic type or is headed by an algebraic symbol if this is true of u.

LEMMA 5.4. Let u be a β-normal term, R a terminating higher-order rewrite system whose lefthand sides are either headed by an algebraic symbol or of base type, p be a non-empty sequence of disjoint positions of Pos(u), and l → r a rule in R such that (∀p ∈ p) u| p = βη lγ. Then u -→ + R u[rγ] p ↓ β . PROOF. The difficulty is that higher-order rewriting does not satisfy the socalled disjoint redex axiom because of the β-normalization which applies at each step, but all β-normalization steps can indeed be postponed and grouped together.

Since l hence lγ is not an abstraction and u| p is β-normal and it is not an abstraction either,

u = η u[z] p {z → lγ ↓ β } where z is a fresh variable, p is a set of disjoint positions in Pos(u[z] p ) and u[z] p is β-normal. We prove that u = η u[z] p {z → lγ ↓ β } -→ + R (u[z] p {z → rγ}) ↓ β by induction on u compared in the well-founded order -→ + R . If |p| = 1,
the result is clear. Otherwise, p = p, q. We choose to rewrite p first:

u -→ p R v = η (u[z] p {z → rγ}[z] q {z → lγ ↓ β })↓ β = (u[rγ] p [z] q {z → lγ ↓ β })↓ β . Because lγ↓ β is not an abstraction and is β-normal, v = η (u[rγ] p [z] q )↓ β {z → lγ↓ β }, and z occurs at a non-empty set q of disjoint positions of Pos(u[rγ] p [z] q ↓ β ). By induction hypothesis, v -→ + R v = η ((u[rγ] p [z] q )↓ β {z → rγ})↓ β . By confluence of β, v = η ((u[rγ] p [z] q )↓ β {z → rγ})↓ β = u[z] p,q {z →
rγ}↓ β and we are done. THEOREM 5.5. Let R be a normal higher-order rewrite system all whose lefthand sides are either headed by an algebraic symbol or have a basic type, and I be a normal higher-order interpretation. Then termination of I(R) implies termination of R. PROOF. Let s be a β-normal term such that s -→ R t. By definition of higherorder rewriting, s = s ↓ β , s| p = βη lγ for some position p, β-normal substitution γ and rule l → r ∈ R, and t is a β-normal term such that t = η s[rγ] p ↓ β . By definition of an interpretation, I(s) and I(t) are β-normal. We now show that I(s) -→ + I(R) I(t), which implies termination of R assuming termination of I(R). The assumption that interpretations preserve types ensures that all terms constructed in the coming proof are typable: environments can be dispensed with.

Since s, hence s| p is β-normal, and s| p = βη lγ, by confluence of β-reductions modulo η, lγ -→ * β lγ↓ β = η s| p . By assumption, l is headed by an algebraic symbol or is a term of basic type, hence so are lγ and therefore lγ↓ β . It follows that s| p = λx.@(s| q , x) and x ∩ Var(s| q ) = ∅, and either s| q has basic type or s| q = f (u). Now, s| q = η lγ ↓ β , hence s -→ q t = η (s[λx.@(rγ, x)] p ) ↓ β . Further, s| q and lγ being βη-equivalent, Var(lγ) = Var(s| q ), and therefore Var(lγ) ∩ x = ∅. Since Var(r) ⊆ Var(l), Var(rγ) ⊆ Var(lγ), implying that Var(rγ

) ∩ x = ∅. It follows that t = η (s[rγ] q )↓ β = η (s[rγ] p )↓ β = η t.
We proceed with the calculation of I(s) first and then I(t), which are both βnormal since I preserves β-normal forms.

By monotonicity of I, there are disjoint positions q 1 . . . q n (depending on s and q only) such that I(s) = βη I(s)[I(s| q )] q 1 ...qm . By preservation of β-normal forms I(s) and I(s| q ) are β-normal. Further, since s| q has basic type or is headed by an algebraic symbol, the same is true of I(s| q ) by preservation of either types or algebraic symbols. Hence, by Lemma 5.3, since I(s) and I(s| q ) are β-normal, we have I(s) = η I(s)[I(s| q )] q 1 ...qn .

By η-compatibility and β-compatibility, I(s| q ) = βη I(lγ). By stability, I(lγ) = βη I(l)I(γ). Hence I(s| q ) = βη I(l)I(γ). Hence I(s) -→ + I(R) I(s)[I(r)I(γ)] q 1 ...qn ↓ β by Lemma 5.4.

We move to I(t). By successively η-compatibility and β-compatibility of I, we get

I(t) = η I(s[rγ] q ↓ β ) = β I(s↓ β [(rγ)↓ β ] q ). Further, by monotonicity of I, I(s↓ β [rγ ↓ β ] q ) = βη I(s ↓ β )[I((rγ) ↓ β )] q 1 ,
...,qn . Finally, by stability and β-compatibility of I, it follows that I(t) = βη I(s ↓ β )[I(r)I(γ)] q 1 ,...,qn . Since t is β-normal and I preserves normal forms, and β is Church-Rosser modulo η, we finally get I(t) = η I(s)[I(r)I(γ)] q 1 ,...,qn ↓ β , which achieves the proof.

Neutralization and Normalization

We present now a particular example of termination-preserving interpretation for normal rewriting, originally introduced in [START_REF] Jouannaud | Higher-Order Orderings for Normal Rewriting[END_REF]]. The construction relies on a specific treatment, called neutralization, of those abstractions which should not be involved in a beta-redex, that is, which should not be or become after reductions the first argument of an application. To this end, a term built from the signature F is transformed into a term built from an enlarged signature F new obtained from F by adding (if necessary) a minimal constant type o, a coercion symbol m σ : σ → o for every type σ to the minimal type o, a function symbol ⊥ n σ : τ 1 ×. . .×τ n → τ for every type σ = τ 1 → . . . → τ n → τ , and a function symbol f new for some of the function symbols in F. We omit the superscript n in ⊥ n σ when it is clear from the context. The higher-order rules to be proved terminating are of course built from terms in T (F, X ), not in T (F new , X ).

Definition 5.6. The neutralization of level i (i-neutralization for short) of a typable term t ∈ T (F new , X ) with respect to the list of (typable) terms u 1 : θ 1 , . . . , u n : θ n in T (F new , X ), is the term N i (t, u 1 , . . . , u n ) defined as follows:

(1)

N i (t : τ, u 1 , . . . , u n ) = m τ (t) if i < 0; (2) N 0 (t : τ, u 1 , . . . , u n ) = t; (3) N i+1 (t : τ, u 1 , . . . , u n ) = t if τ is a data type; (4) N i+1 (t : σ → τ, u 1 , . . . , u n ) = N i (@(t, ⊥ n θ 1 →...→θn→σ (u 1 , . . . , u n ))
). Terms of a functional type are neutralized by applying them to the ⊥-expression of the appropriate type, therefore reducing their functionality as long as the level is non-zero. The role of N -1 is specific to HORPO, we shall understand it in examples. The role of the sequence of terms u 1 : θ 1 , . . . , u n : θ n is to become arguments of ⊥ n σ in case that symbol has a functional type. Note also that neutralization is the identity function if all levels are 0. Further, for each function symbol, we control which arguments of a functional type can be neutralized: Definition 5.7. To each symbol f : σ 1 × . . . × σ n → σ ∈ F and each argument position j ∈ [1.

.n], we associate:

-an integer nl j f ≤ ar(σ j ), called neutralization level of f at position j. We call neutralized (respectively, active, coerced) those positions j for which nl j f > 0 (respectively,

nl j f = 0, nl j f < 0), -a subset A j f ⊆ [1.
.n] of argument positions of f used to filter out its list of arguments t by defining t

j f = t k | k ∈ A j f .
We now neutralize terms recursively. To this end, for each symbol f :

σ 1 × . . . × σ n → σ such that σ i = τ 1 → . . . → τ k → τ ,
where τ is a basic type, we add to the signature a new function symbol

f new : σ 1 × . . . × σ n → σ such that σ i = τ q+1 → . . . → τ k → τ if nl i f = q < k and σ i = τ if nl i f = k. Definition 5.8. The full neutralization of a term t is the term FN (t) s.t. FN (x) = x if x ∈ X FN (λx.u) = λx.FN (u) FN (@(t 1 , t 2 )) = @(FN (t 1 ), FN (t 2 )) FN (f (t 1 , . . . , t n )) = f new (N nl 1 f (FN (t 1 ), FN (t 1 f )), . . . , N nl n f (FN (t n ), FN (t n f ))) where FN ( u 1 , . . . , u n ) = FN (u 1 ), . . . , FN (u n ) .
Our definition makes sense since, in all cases, FN (t) is typable with the same type as t. Note also that the filtered list of arguments t i f is itself recursively neutralized before using it to neutralize t i in the last case.

Example 5.9 (differentiation continued). We illustrate here the full neutralization of the lefthand and righthand sides of the rules of Example 3.4. To this end, we choose a neutralization level for each function symbol and argument position. The associated subsets of argument positions are chosen empty, hence ⊥ 0 real is a constant abbreviated as ⊥:

L 1 diff = 1 L 1 sin = 0 L 1 cos = 0 A 1 diff = {} A 1 sin = {} A 1 cos = {} L 1 × = 1 L 2 × = 1 L 1 + = 1 L 2 + = 1 A 1 × = {} A 2 × = {} A 1 + = {} A 2 + = {} (1) t is a variable x. Then FN (xγ) = xFN (γ) = FN (x)FN (γ).
(2) t = λx.u. Then FN (tγ) = FN (λx.uγ) = λx.FN (uγ). By induction hypothesis, FN (uγ) = FN (u)FN (γ), and therefore λx.FN (uγ) = λx.FN (u)FN (γ) = (λx.FN (u))FN (γ), since x is not occurring in Ran(FN (γ)), and which is equal to FN (λx.u)FN (γ) = FN (t)FN (γ).

(3) t = @(t 1 , t 2 ). Then FN (tγ) = FN (@(t 1 , t 2 )γ) = FN (@(t 1 γ, t 2 γ)) = @(FN (t 1 γ), FN (t 2 γ)). By induction hypothesis, it is equal to @(FN (t 1 )FN (γ), FN (t 2 )FN (γ)) = @(FN (t 1 )FN (γ),

FN (t 2 )FN (γ)) = @(FN (t 1 ), FN (t 2 ))FN (γ) = FN (@(t 1 , t 2 ))FN (γ) = FN (t)FN (γ) (4) t = f (t 1 , . . . , t n ) with f ∈ F. Then FN (tγ) = FN (f (t 1 , . . . , t n )γ) = FN (f (t 1 γ, . . . , t n γ)) = f new (N nl 1 f (FN (t 1 γ), FN (t 1 f γ)), . . . , N nl n f (FN (t n γ), FN (t n f γ))). By induction hypothesis, this is equal to f new (N nl 1 f (FN (t 1 )FN (γ), FN (t 1 f )FN (γ)), . . . , N nl n f (FN (t n )FN (γ), FN (t n f )FN (γ)))
, and, by Lemma 5.10, to

f new (N nl 1 f (FN (t 1 ), FN (t 1 f ))FN (γ), . . . , N nl n f (FN (t n ), FN (t n f ))FN (γ)) = f new (N nl 1 f (FN (t 1 ), FN (t 1 f )), . . . , N nl n f (FN (t n ), FN (t n f )))FN (γ) = FN (f (t 1 , . . . , t n ))FN (γ) = FN (t)FN (γ)
LEMMA 5.12. Let s, t, u 1 , . . . , u m and w be higher-order terms and let p be a position in t and q 1 . . . q n positions in FN (t), such that FN (t[w] p ) = FN (t)[FN (w)] q 1 ...qn . Then we have that there are disjoint positions r 1 . . . r o such that

-N i (FN (t[w] p ), FN (u 1 ), . . . , FN (t[w] p ), . . . , FN (u m ) ) = N i (FN (t), FN (u 1 ), . . . , FN (t), . . . , FN (u m ) )[FN (w)] r 1 ...ro if t : τ 1 → . . . → τ k → τ and i ≤ k. -N i (FN (t[w] p ), FN (u 1 ), . . . , FN (u m ) ) = N i (FN (t), FN (u 1 ), . . . , FN (u m ) )[FN (w)] r 1 ...ro if t : τ 1 → . . . → τ k → τ and i ≤ k. -N i (FN (s), FN (u 1 ), . . . , FN (t[w] p ), . . . , FN (u m ) ) = N i (FN (s), FN (u 1 ), . . . , FN (t), . . . , FN (u m ) )[FN (w)] r 1 ...ro if s : τ 1 → . . . → τ k → τ and i ≤ k.
PROOF. We only provide the proof of the first case, the other two are easily obtained from this one. N i (FN (t[w] p ), FN (u 1 ), . . . , FN (t[w] p ), . . . , FN (u m ) ) = @(. . . @(FN (t[w] p ), ⊥ τ 1 (FN (u 1 ), . . . , FN (t[w] p ), . . . , FN (u m ))), . . .

⊥ τ i (FN (u 1 ), . . . , FN (t[w] p ), . . . , FN (u m ))))
By assumption, we have that FN (t[w] p ) = FN (t)[FN (w)] q 1 ...qn , hence is equal to @(. . . @(FN (t)[FN (w)] q1...qn ), ⊥ τ1 (FN (u 1 ), . . . , FN (t)[FN (w)] q1...qn , . . . , FN (u m ))), . . . ⊥ τi (FN (u 1 ), . . . , FN (t)[FN (w)] q1...qn , . . . , FN (u m ))))

Now adding the corresponding prefixes p 0 , p 1 , . . . , p i , which are the disjoint positions of the i + 1 occurrences of FN (t) we are considering, this is equal to @(. . . @(FN (t), ⊥ τ 1 (FN (u 1 ), . . . , FN (t), . . . , FN (u m ))), . . . ⊥ τ i (FN (u 1 ), . . . , FN (t), . . . , FN (u m ))))[FN (w)] r 1 ...ro where r 1 . . . r o is the set of disjoint positions p 0 • q 1 . . . p 0 • q n , p 1 • q 1 . . . p 1 • q n , . . . , p i • q 1 . . . p i • q n . LEMMA 5.13. Let t, w be higher-order terms. For every position p in t there are disjoint positions {q 1 , . . . , q n } n>0 in FN (t) such that FN (t[w] p ) = FN (t)[FN (w)] q 1 ...qn .

PROOF. We proceed by induction on |p|. If p is Λ, it trivially holds. Otherwise, there are three cases:

(1) t = λx.u. Then p = 1 • p and FN (λx.u) = λx.FN (u). By induction hypothesis, there are disjoint positions {q 1 . . . q n } n>0 such that FN (u[w] p ) = FN (u)[FN (w)] q 1 ...q n , and therefore, taking

q i = 1 • q i for all i ∈ {1 . . . n}, we have FN (λx.u[w] p ) = λx.FN (u[w] p ) = λx.FN (u)[FN (w)] q 1 ...q n = FN (λx.u)[FN (w)] q 1 ...qn . (2) t = @(t 1 , t 2 ). Let p = 1 • p (the case p = 2 • p is analogous). Then
FN (@(t 1 , t 2 )) = @(FN (t 1 ), FN (t 2 )). By induction hypothesis, there are disjoint positions {q 1 . . . q n } n>0 such that FN (t 1 [w] p ) = FN (t 1 )[FN (w)] q 1 ...q n , and therefore, taking q i = 1 • q i for all i ∈ {1 . . . n}, we have FN (@(t 1 , t 2 )[w] p ) = FN (@(t 1 [w] p , t 2 )) = @(FN (t 1 [w] p ), FN (t 2 )) = @(FN (t 1 )[FN (w)] q 1 ...q n , FN (t 2 )) = @(FN (t 1 ), FN (t 2 ))[FN (w)] q 1 ...qn = FN (@(t

1 , t 2 ))[FN (w)] q 1 ...qn . (3) t = f (t 1 , . . . , t m ) with f ∈ F. Let p = i • p for some i ∈ {1 . . . m}. Then FN (f (t 1 , . . . , t m )) = f new (N nl 1 f (FN (t 1 ), FN (t 1 f )), . . . , N nl m f (FN (t m ), FN (t m f )))
. By induction hypothesis, there are disjoint positions {q 1 . . . q n } n>0 such that

FN (t i [w] p ) = FN (t i )[FN (w)] q 1 ...q n .
Then by Lemma 5.12, we have that for every t j with j ∈ {1 . . . m} there are disjoint positions q j 1 . . . q j n j such that -if i = j and i ∈ A j f and i j is the position of t i in t

j f then N nl j f (FN (t j [w] p ), FN (t j f [w] i j •p )) = N nl j f (FN (t j ), FN (t j f ))[FN (w)] q j 1 ...q j n j -if i = j and i ∈ A j f and i j is the position of t i in t j f then N nl j f (FN (t j ), FN (t j f [w] i j •p )) = N nl j f (FN (t j ), FN (t j f ))[FN (w)] q j -if i = j and i ∈ A j f and i j is the position of t i in t j f then N nl j f (FN (t j ), FN (t j f [w] i j •p )) = N nl j f (FN (t j ), FN (t j f ))[FN (w)] q j 1 ...q j n j Therefore FN (f (t 1 , . . . , t i [w] p , . . . , t m )) = FN (f (t 1 , . . . , t i , . . . , t m ))[FN (w)] 1•q 1 1 ...1•q 1 n 1 ...m•q m 1 ...m•q m nm
Now we prove ηand β-compatibility of FN .

LEMMA 5.14. Let s, t be higher-order terms. If s = η t, then FN (s) = η FN (t).

PROOF. First, we prove that if x / ∈ Var(u) then FN (λx.@(u, x)) = η FN (λx.@(u, x)). By definition of FN , we have that FN (λx.@(u, x)) = λx.@(FN (u), x). Since FN preserves the set of free variables, we have that x / ∈ Var(FN (u)), and hence λx.@(FN (u), x) = η FN (u). Now, assume we have s[λx.@(u, x)] p = η s[u] p for some position p, then by Lemma 5.13, there are disjoint positions q 1 , . . . , q n in FN (s) such that we have that FN (s[λx.@(u, x)] p ) = FN (t)[FN (λx.@(u, x))] q 1 ...qn and FN (s[u] p ) = FN (t)[FN (u)] q 1 ...qn . Therefore, since, FN (t)[FN (λx.@(u, x))] q 1 ...qn = η FN (t)[FN (u)] q 1 ...qn , we conclude that FN (s[λx.@(u, x)] p ) = η FN (s[u] p ).

We conclude by induction on the number of η-equality steps applied in s = η t.

LEMMA 5.15. Let s, t be higher-order terms. If s = β t, then FN (s) = β FN (t).

PROOF. First, we prove that FN (@(λx.u, v)) = β FN (u{x → v}). By definition of FN , we have that FN (@(λx.u, v)) = @(λx.FN (u), FN (v)), which is β-equivalent to FN (u){x → FN (v)}, and by Lemma 5.11, it is equal to FN (u{x → v}). We then conclude that FN (s) = β FN (t), proceeding as in the proof of the previous lemma, using Lemma 5.13 and induction on the number of β-equality steps afterward.

The coming two lemmas follow easily: LEMMA 5.16. Let t : τ be a higher-order term. Then FN (t) : τ . LEMMA 5.17. Let t be a higher-order term. Then FN (t) is headed by an algebraic symbol whenever t is.

Neutralization as an interpretation

Definition 5.18. We define the interpretation N as N (s) = FN (s)↓ β . THEOREM 5.19. N is a normal higher-order interpretation.

PROOF. By definition and Lemma 5.16, N is a higher-order interpretation. Since β-normalization preserves both ηand β-equivalence, by Lemma 5.15 we obtain β-compatibility and by Lemma 5.14 we obtain η-compatibility. Preservation of βnormalization trivially holds by definition. Lemma 5.17 implies preservation of algebraic heads. Finally, Lemma 5.11 implies stability and Lemma 5.13 monotonicity. Therefore N is a normal higher-order interpretation.

Full normalization combined with neutralization can be used in conjunction with any normal higher-order reduction ordering. Of course, we then need to define the precedence on function symbols for the extended signature. In practice, we shall make ⊥ σ -functions symbols small, as done now to prove our starting example.

Example 5.20 (differentiation end). We consider again the differentiation example, using now neutralization. Let diff new > F {× new , + new , cos} and diff new ∈ Mul. First rule: diff new (sin(@(F, ⊥))) > cos(@(F, ⊥)) × new @(diff new (@(F, ⊥)), ⊥) Applying first case 2, we recursively obtain two subgoals: (i) diff new (sin(@(F, ⊥))) > cos(@(F, ⊥)) (ii) diff new (sin(@(F, ⊥))) > @(diff new (@(F, ⊥)), ⊥). (i): applying Case 2 yields diff new (sin(@(F, ⊥))) > @(F, ⊥) shown by Case 1 twice. (ii): applying Case 5 generates two new subgoals (iii) diff new (sin(@(F, ⊥))) > diff new (@(F, ⊥)) ,which holds by case 3, then case 1. (iv) diff new (sin(@(F, ⊥))) > ⊥ ,which holds by case 1 twice and then case 7. Second rule: diff new (@(@(F,⊥) × new @(F,⊥),⊥)) > @(@(diff new (@(F,⊥)),⊥) × new @(F,⊥),⊥)

+ new @(@(F,⊥) × new @(diff new (@(F,⊥)),⊥),⊥) Case 2 generates two subgoals: (i) diff new (@(@(F,⊥)× new @(F,⊥),⊥)) > @(@(diff new (@(F,⊥)),⊥)× new @(F,⊥),⊥) (ii) diff new (@(@(F,⊥)× new @(F,⊥),⊥)) > @(@(F,⊥)× new @(diff new (@(F,⊥)),⊥),⊥) We only prove (i), as (ii) is shown exactly in the same way. By Case 5, (i) generates two new subgoals: (iii) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > @(diff new (@(F, ⊥)), ⊥) × new @(F, ⊥) (iv) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > ⊥. The latter holds by case 1 and then case 7. By Case 2, (iii) yields two subgoals: (v) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > @(diff new (@(F, ⊥)), ⊥) (vi) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > @(F, ⊥), solved by applying successively Case 1, 7 and 1. By Case 5, (v) generates (vii) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > diff new (@(F, ⊥)) (viii) diff new (@(@(F, ⊥) × new @(F, ⊥), ⊥)) > ⊥ solved by Case 1 first, then 7. Finally, (vii) is solved by Case 3, 7, and 1 successively.

POLYMORPHIC NORMAL REWRITING

We investigate here the case of polymorphic rewriting defined by polymorphic rewrite rules. Polymorphism is introduced via type variables, quantifiers being omitted, hence is weak in the usual sense. We shall not mention further this "weakness" which is present throughout this section. Since types are first-order expres-sions, type instantiation is the usual notion of substitution, acting as a homomorphism of expressions generated by its action on type variables. This applies to terms too via the type of variables in abstractions.

The idea is of course to reduce polymorphic rewriting to monomorphic rewriting by considering all ground type-instances of a given polymorphic rewrite rule. Example 7.5 taken from [START_REF] Van De Pol | Termination of Higher-Order Rewrite Systems[END_REF]] describes an encoding of natural deduction by means of a polymorphic rewriting system whose difficult normal termination proof can be automatically carried out in full.

Polymorphic algebras

We first recall the basics of polymorphic algebras introduced in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. We are now given a set S ∀ of distinguished type constants called type variables. We use T S ∀ for the set of types, and T S , as before, for the set of ground types. Signatures may now contain type variables. Types, declarations and signatures are said to be polymorphic if they contain type variables, and monomorphic otherwise. As before, we collect all declarations into a single environment Σ; Γ, where the signature Σ = S; S ∀ ; F is the fixed part of the environment, and the variable part Γ collects the type declarations for (term) variables.

The typing judgments are displayed in Figure 2. Since the last two rules introduce a type substitution ξ, we have considered, for uniformity reason, that the first two introduce the identity type substitution ι.

Variables:

x : σ ∈ Γ Γ c Σ x : σι Abstraction: Γ • {x : σ} c Σ t : τ Γ c Σ (λx : σ.t) : (σ → τ )ι Application: Γ c Σ s : σ Γ c Σ t : τ ξ most general unifier of α → β = σ ∧ α = τ Γξ c Σ @(s, t)ξ : βξ Functions: f : σ 1 × . . . × σ n ⇒ σ ∈ F Γ c Σ t 1 : τ 1 . . . Γ c Σ t n : τ n ξ most general unifier of σ 1 = τ 1 ∧ . . . ∧ σ n = τ n Γξ c Σ f (t 1 , . . . , t n )ξ : σξ Fig. 2.
Typing judgments in polymorphic algebras Definition 6.1. Given an environment Σ; Γ, a raw term s is typable with principal type σ, written Γ Σ s : σ, iff the judgment Γ c Σ s : σ is provable in the system of Figure 2.

Two key properties of this typing system are [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]: (i) every typable term has a (unique) principal type; (ii) if Γ Σ s : σ, then Γξ Σ sξ : σξ.

Polymorphic Rewriting

In this section, we consider polymorphic rewriting for terms of a monomorphic type, which is easily extensible to terms of a polymorphic type by considering the type variables in the environment of the term as new constant types. Definition 6.2. A polymorphic normal rewrite rule is a normal rewrite rule Γ l → r : σ such that l and r are higher-order terms in β-normal form having the same principal type σ in the environment Γ. A polymorphic normal rewrite system is a set of such rules. Given a polymorphic normal rewrite system R, we define the set R g = {Rξ} ξ of type instances of R by some ground substitution ξ. Given now a term s of a ground type, we define s -→ p R t iff s -→ p Rg t. Given a polymorphic normal rewrite rule Γ l → r : σ and a ground type substitution ξ, then Γξ lξ → rξ : σξ is a monomorphic normal rewrite rule by the property (ii) of the polymorphic type system, justifying our definition of polymorphic rewriting. This would not be true for a definition like Nipkow's which requires l and r to be in η-long form, a property which is not closed under type instantiation.

Let now s = s[lγ] p , where Γ l → r is a polymorphic rule. There are two kinds of redexes lγ:

-Those for which γ replaces a variable x : σ ∈ Γ by a term of type σ. Those substitutions act as in the monomorphic case, they do not change the type of terms. As a consequence, if is a stable ordering such that l r, then lγ rγ. -Those for which γ replaces some variable x : σ ∈ Γ by a term of type σξ. Such substitutions instantiate both the term and its type.

Definition 6.3. Let γ be a substitution {x i → t i } i and Γ be an environment such that (∀i) Γ c Σ x i : σ i . Then γ is type preserving in Γ if and only if f (∀i) Γ c Σ t i : σ i and γ is a specialization by the type instantiation ξ (possibly the identity) in Γ if and only if (∀i) Γξ c Σ t i : σ i ξ. An ordering of the set of higher-order terms is called stable if it is stable under type preserving substitutions, and polymorphic if it is stable under specializations.

Note that a stable order is a particular case of a polymorphic order. A polymorphic higher-order reduction ordering makes it possible to compare all instances of the lefthand and righthand side of a rewrite rule l → r by doing the single comparison l r.

In [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], we show that HORPO is polymorphic: this is so because types do not influence the choice of rules in an ordering computation, provided the type ordering is extended to type variables in a way that is compatible with substitutions, that is σ ≥ T S τ implies σξ ≥ T S τ ξ for any ground type substitution ξ. Of course, the restricted version > of HORPO introduced here is polymorphic as well. We now define polymorphic interpretations: Definition 6.4. A higher-order interpretation I is polymorphic if it preserves polymorphism, that is, I(sξ) = η I(s)ξ. THEOREM 6.5. Let R be a normal higher-order rewrite system whose lefthand sides are all either headed by an algebraic symbol or have a non variable basic type and I a polymorphic normal higher-order interpretation. Then termination of I(R) implies termination of R.

PROOF. We show that s -→ R t implies I(s) -→ + I(R) I(t). By definition of polymorphic rewriting, s -→ ξ Rξ t, ξ denoting a monomorphic type substitution. By Theorem 5.5, I(s) -→ + I( ξ Rξ) I(t). Now I( ξ IRξ) = ξ I(Rξ) = η ξ I(R)ξ by preservation of polymorphism. Hence, I(s) -→ + I(R) I(t) by definition of polymorphic rewriting.

We are left showing that neutralization preserves polymorphism. Note that we could take advantage of polymorphism to eliminate (part of) type decorations from coercions and bottom symbols. We will however not do this, so as to facilitate the reading of complex expressions in proofs or examples. LEMMA 6.6. Let t : σ be a higher-order term and ξ a type substitution. Then tξ↓ β = t↓ β ξ.

PROOF. Note first that tξ → β t if and only if there is some t with t → β t and t = t ξ. The result follows by induction on the derivation tξ -→ * β (tξ)↓ β .

Since the neutralization level nl j f of an argument of f is smaller than or equal to the arity of its type, we have the following properties: LEMMA 6.7. Let t : τ and u 1 : θ 1 , . . . , u n : θ n be higher-order terms and ξ a type substitution. Then, (∀i ≤ ar(τ )) N i (tξ, u 1 ξ, . . . , u n ξ ) = N i (t, u 1 , . . . , u n )ξ.

PROOF. We proceed by induction on i. There are three cases.

(1

) If i < 0 then N i (tξ, u 1 ξ, . . . , u n ξ ) = m τ ξ (tξ) = N 0 (t, u 1 , . . . , u n )ξ. (2) If i = 0 then N 0 (tξ, u 1 ξ, . . . , u n ξ ) = tξ = N 0 (t, u 1 , . . . , u n )ξ. (3) If i > 0 then, by assumption τ = σ → ρ, hence tξ : σξ → ρξ. Then, N i (tξ, u 1 ξ, . . . , u n ξ ) = N i-1 (@(tξ, ⊥ θ 1 ξ→...→θnξ→σξ (u 1 ξ, . . . , u n ξ))) = N i-1 (@(t, ⊥ θ 1 →...→θn→σ (u 1 , . . . , u n ))ξ). Since i -1 ≤ ar(ρ), by induction hypothesis, this is equal to N i-1 (@(t, ⊥ θ 1 →...→θn→σ (u 1 , . . . , u n )))ξ = N i (t, u 1 , . . . , u n )ξ.
THEOREM 6.8. Full neutralization is polymorphic.

PROOF. Let t : σ be a higher-order term and ξ a type substitution. By Lemma 6.6, it is enough to show that FN (tξ) = FN (t)ξ, we we do by induction on |t|. There are four cases. If t is a variable x, the result is clear. Otherwise, (1) t = λx : τ.u. Then FN (tξ) = FN (λx : τ ξ.uξ) = λx : τ ξ. FN (uξ).

By induction hypothesis, FN (uξ) = FN (u)ξ, which yields the result. (2) t = @(t 1 , . . . , t n ). Then FN (tξ) = FN (@(t 1 ξ, . . . , t n ξ)) = @(FN (t 1 ξ), . . . , FN (t n ξ)) = @(FN (t 1 ξ), . . . , FN (t n ξ)).

By induction hypothesis, this is equal to @(FN (t 1 )ξ, . . . ,

FN (t n )ξ) = @(FN (t 1 ), . . . , FN (t n ))ξ = FN (@(t 1 , . . . , t n ))ξ = FN (t)ξ. (3) t = f (t 1 , . . . , t n ) with f ∈ F. Then FN (tξ) = FN (f (t 1 , . . . , t n )ξ) = FN (f (t 1 ξ, . . . , t n ξ)) = f new (N nl 1 f (FN (t 1 ξ), FN (t 1 f ξ)), . . . , N nl n f (FN (t n ξ), FN (t n f ξ))). By induction hypothesis, this is equal to f new (N nl 1 f (FN (t 1 )ξ, FN (t 1 f )ξ)), . . . , N nl n f (FN (t n )ξ, FN (t n f )ξ))) = f new (N nl 1 f (FN (t 1 ), FN (t 1 f ))ξ, . . . , N nl n f (FN (t n ), FN (t n f
))ξ), by using lemma 6.7. Extracting the type substitution we get

f new (N nl 1 f (FN (t 1 , FN (t 1 f ))), . . . , N nl n f (FN (t n , FN (t n f ))))ξ = FN (f (t 1 , . . . , t n ))ξ = FN (t)ξ.

EXAMPLES

We present here several complex examples whose termination is proved with normal HORPO in conjunction with neutralization. For all of them, we give the necessary ingredients for computing the appropriate neutralizations and comparisons. As a convention, missing neutralization levels are equal to 0, in which case the corresponding subset of argument positions will be empty. In all examples, we use as type ordering ≥ T S an RPO as the one described just above Definition 4.3 where, additionally, we equate all sort symbols in the precedence on sort. The precedence on function symbols and statuses will be given in full.

The rules are first given in a format aiming at an easier reading by writing F (X) for @(F, X). When it comes to the computations, we make the contrary choice, to make clear that @ is the top function symbol of the term F (X). Since these computations are complex, all examples have been checked by our implementation, which is available from the web at the following url:

www.lsi.upc.edu/ ˜albert/normal.html. Consequently, we will allow ourselves to skip the computation part in most cases.

Example 7.1. The coming encoding of first-order prenex normal forms is adapted from [START_REF] Nipkow | Higher-Order Critical Pairs[END_REF], where its local confluence is proved via the computation of its (higher-order) critical pairs. Formulas are represented as λ-terms Here, + stands for the choice operator, • for sequential composition, δ for deadlock, and Σ for the data dependent choice. The rules are the following:

{x : proc} x + x → x {x, y, z : proc} (x + y) • z → (x • z) + (y • z) {x, y, z : proc} (x • y) • z → x • (y • z) {x : proc} x + δ → x {x : proc} δ • x → δ {x : proc} Σ(λd.x) → x {D : data, P : data → proc} Σ(λd.P (d)) + P (D) → Σ(λd.P (d)) {P, Q : data → proc}      Σ(λd.P (d) + Q(d)) → Σ(λd.P (d)) + Σ(λd.Q(d)) {x : proc, P : data → proc} Σ(λd.P (d)) • x → Σ(λd.(P (d) • x))
Example 7.4. Monomorphic encoding of natural deduction, from [START_REF] Van De Pol | Termination of Higher-Order Rewrite Systems[END_REF]]. Let S = {o, c : * × * → * }. The signature and rules follow, parametrized by three arbitrary types σ, τ and ρ, making them infinite. The coming calculations are not meant to be automated.

F = { app σ,τ : (σ → τ ) × σ → τ ; abs σ,τ : (σ → τ ) → (σ → τ ); Π σ,τ : σ × τ → c(σ, τ ); Π 0 σ,τ : c(σ, τ ) → σ; Π 1 σ,τ : c(σ, τ ) → τ ; ∃ + σ : o × σ → c(o, σ); ∃ - σ,τ : c(o, σ) × (o → σ → τ ) → τ } X = { X : σ; Y : τ ; Z : o; T : c(o, ρ), F : σ → τ ; G : o → σ → τ, H : o → ρ → (σ → τ ), I : o → ρ → c(σ, τ ), J : o → ρ → c(o, σ)} app σ,τ (abs σ,τ (F ), X) → F (X) ∃ - σ,τ (∃ + σ (Z, X), G) → G(Z, X) Π 0 σ,τ (Π σ,τ (X, Y )) → X Π 1 σ,τ (Π σ,τ (X, Y )) → Y app σ,τ (∃ - ρ,σ→τ (T, H), X) → ∃ - ρ,τ (T, λx : o y : ρ.app σ,τ (H(x, y), X)) Π 0 σ,τ (∃ - ρ,c(σ,τ ) (T, I)) → ∃ - ρ,τ (T, λx : o y : ρ.Π 0 σ,τ (I(x, y))) Π 1 σ,τ (∃ - ρ,c(σ,τ ) (T, I)) → ∃ - ρ,τ (T, λx : o y : ρ.Π 1 σ,τ (I(x, y))) ∃ - σ,τ (∃ - ρ,c(o,σ) (T, J), G) → ∃ - ρ,τ (T, λx : o y : ρ.∃ - σ,τ (J(x, y), G)) Neutralization:L 1 ∃ - σ,τ = -1,L 2 ∃ - σ,τ = 2 and A 2 ∃ - σ,τ ={1}for all types σ, τ . Statuses: ∃ - new σ,τ ∈ Lex and app σ,τ , Π 0 σ,τ , Π 1 σ,τ ∈ Mul for all types ρ, σ, τ ; Precedence: (∀ρ, σ, τ ) {app σ,τ , Π 0 σ,τ , Π 1 σ,τ } > F ∃ - new ρ,τ and ∃ - new ρ,τ = ∃ - new σ,τ
We carry out the computation for the most difficult rule, the last. The βnormalization of the full neutralization of both sides is:

FN (∃ - σ,τ (∃ - ρ,c(o,σ) (T, J), G))↓ β = ∃ - new σ,τ ( m c(o,σ) (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), @(G, ⊥ c(o,σ)→o (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), ⊥ c(o,σ)→σ (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))))))
and,

FN (∃ - ρ,τ (T, λx : o y : ρ.∃ - σ,τ (@(J, x, y), G)))↓ β = ∃ - new ρ,τ (m c(o,ρ) (T ), ∃ - new σ,τ ( m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), @(G, ⊥ c(o,σ)→o (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), ⊥ c(o,σ)→σ (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))))))
We prove s > t by case 4, yielding two subgoals:

(i) ∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))) > m c(o,ρ) (T ), and (ii) s > ∃ - new σ,τ ( m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), @(G, ⊥ c(o,σ)→o (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), ⊥ c(o,σ)→σ (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))
)) For (i) we apply case 1 twice (note that m c(o,ρ) (T ) has minimal type). For (ii) we apply case 4 again which leads us to two new subgoals:

(iii) m c(o,σ) (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))) > m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), and (iv) @(G, ⊥ c(o,σ)→o (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), ⊥ c(o,σ)→σ (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))))) ≥ @(G, ⊥ c(o,σ)→o (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), ⊥ c(o,σ)→σ (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))
)) For (iii) we apply case 3 first and then case 1, and for (iv) we apply case 8, which leads us to prove:

⊥ c(o,σ)→o (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))) ≥ ⊥ c(o,σ)→o (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))).
which holds by case 3 and 1.

Example 7.5. The previous encoding of natural deduction is now made polymorphic. As a result, it becomes finite, hence amenable to automation. Let S = {o, c : * × * → * }, and S ∀ = {σ, τ, ρ}. Signature and rules follow.

F = { app : (σ → τ ) × σ → τ ; abs : (σ → τ ) → (σ → τ ); Π : σ × τ → c(σ, τ ); Π 0 : c(σ, τ ) → σ; Π 1 : c(σ, τ ) → τ ; ∃ + : o × σ → c(o, σ); ∃ -: c(o, σ) × (o → σ → τ ) → τ } X = { X : σ; Y : τ ; Z : o; T : c(o, ρ), F : σ → τ ; G : o → σ → τ, H : o → ρ → (σ → τ ), I : o → ρ → c(σ, τ ), J : o → ρ → c(o, σ)} app(abs(F ), X) → F (X) ∃ -(∃ + (Z, X), G) → G(Z, X) Π 0 (Π(X, Y )) → X Π 1 (Π(X, Y )) → Y app(∃ -(T, H), X) → ∃ -(T, λx : o y : ρ.app(H(x, y), X)) Π 0 (∃ -(T, I)) → ∃ -(T, λx : o y : ρ.Π 0 (I(x, y))) Π 1 (∃ -(T, I)) → ∃ -(T, λx : o y : ρ.Π 1 (I(x, y))) ∃ -(∃ -(T, J), G) → ∃ -(T, λx : o y : ρ.∃ -(J(x, y), G)) Statuses: ∃ - new ∈ Lex and app, Π 0 , Π 1 ∈ Mul. Precedence: {app, Π 0 , Π 1 } > F ∃ - new . Neutralization:L 1 ∃ -= -1,L 2 ∃ -= 2 and A 2 ∃ -={1}.
The computations are now exactly the same as for the monomorphic encoding of natural deduction done in Example 7.4.

REDUCING NORMAL TO PLAIN HIGHER-ORDER TERMINATION

In this section, we introduce a transformation that reduces the problem of normal higher-order termination to that of plain higher-order termination. Such a transformation is of course most useful since it allows one to prove normal termination by using already existing tools that can prove plain higher-order termination.

We proceed in two steps. First, we reduce normal termination of R to termination of the union of β-reduction and (S) modulo η, where S simulates R in a way that we are going to describe next. Here rewriting modulo η means rewriting on ηequivalence classes. Second, we show that termination of the union of β-reduction and (S) modulo η can itself be reduced to termination of S ∪ βη, where S is obtained from S, although in most cases S will be S itself. Moreover, we also show that, under some restrictions, termination of (S) modulo η union β-reduction can also be reduced to termination of S ∪ β, where S is an η-expansion of S that operates on η-long forms. Let us give a precise definition of rewriting modulo η: Definition 8.1. Given a set of higher-order rewrite rules R, we denote by (R) η the rewrite relation defined as

s -→ (R)η t if s = η s -→ R t = η t .

Rigid simulation

We know that normal termination differs from plain termination because of the existence of versatile terms (or subterms). Our transformation will therefore eliminate these versatile subterms when possible. Definition 8.2. A term l in β-normal form is a rigid pattern if (i) l is not a variable nor an abstraction; (ii) no subterm of l is a versatile application. A higherorder rewrite rule is rigid if its lefthand side is a rigid pattern. A higher-order rewrite system is rigid if so are its rewrite rules.

Being a rigid pattern is different from being a higher-order pattern [START_REF] Miller | A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification[END_REF]], for which variables must be applied to different bound variables, resulting in versatile applications. This superficial difference will be understood later.

LEMMA 8.3. If l is a rigid pattern and t an arbitrary β-normal term s.t. p ∈ Pos(t), then t[lγ] p is β-normal for every β-normal substitution γ.

PROOF. The absence of a β-redex in lγ follows from the absence of a versatile subterm in l. Since l is not a variable nor an abstraction, t[lγ] p has no β-redex.

Term rewriting systems whose lefthand sides are not rigid patterns will be simulated by rigid systems: Definition 8.4. A normal higher-order rewrite system R is simulated by a rigid system R A iff, for any rule l → r ∈ R, there is a pair made of a rigid rule u → v in R A and an abstracting substitution γ, such that uγ = η l and vγ -→ * R A ∪β r = η r. Abstraction by fresh free variables is the main tool to obtain a rigid system from one which is not, therefore explaining our notation R A .

Example 8.5. Consider the system R = {f (λx.h(@(H, c(x)))) → g(H)}, in which H : α → β is the only free variable. R can be abstracted by

R A = {f (X) → g(X), h(Y ) → Y, c(z) → z}
The rule in R is abstracted by the rule f (X) → g(X) added to R A with {X → λz.h(@(H, c(z)))} as abstracting substitution, requiring that λz.h(@(H, c(z))) -→ * R A λz.@(H, z) = η H. Considering this property as a new rule, it is abstracted in turn by the rule h(Y ) → Y in R A with {Y → @(H, c(z))} as abstracting substitution, requiring that @(H, c(z)) -→ * R A @(H, z). This new requirement is satisfied with the versatile subterm free rule c(z) → z added to R A .

LEMMA 8.6. Let R be a rigid system and s, t terms s.t. THEOREM 8.7. Let R be a normal higher-order rewrite system simulated by a rigid system S. Then -→ R βη is terminating if -→ (S)η∪β is terminating.

PROOF. Assume that S ∪ β is terminating modulo η. Let then be the higherorder reduction ordering -→ + (S)η∪β and > be defined as s > t iff there exist u → v ∈ S and γ such that s = uγ and vγ -→ * S∪β t. Note that this implies that >⊆ + . By Theorem 3.8, we need to show that ( , >) is a normal higher-order ordering, and for all l → r ∈ R then l > r for some l = η l and r = η r.

Since S simulates R, then for every rule l → r ∈ R there exists u → v ∈ S and a substitution γ s.t. l = uγ = η l and vγ -→ * S∪β r for some r = η r, which implies l > r by definition of >.

We now show that is normal η-compatible, which means that for all βnormal typed terms s, s , t such that s = η s -→ + (S)η∪β t there exists some β-normal term t = η t such that s -→ + (S)η∪β t . Since s is β-normal, we have that s = η s -→ (S)η w -→ * (S)η∪β t for some term w and, by definition of -→ (S)η , we have s -→ (S)η w, which directly implies that s -→ + (S)η∪β t, hence we take t as t . We are left showing that it is normal stable when equipped with the relation . Assume that s > t. By assumption, there is l → r and γ s. Example 8.8. Consider the rules of Example 7.4 (we could take the polymorphic version of Example 7.5 as well). By Theorem 5.19, we can apply first neutralization as an interpretation and then Theorem 8.7 to transform the resulting system to a new one whose plain termination implies that of normal rewriting with the original one.

Using the same neutralization as in Example 7.4, and new variables V τ : τ for all types τ , the rules resulting from abstraction are the following:

app σ,τ (abs σ,τ (F ), X) → F (X) ∃ - new σ,τ (m c(o,σ) (∃ + σ (Z, X)), V τ ) → V τ Π 0 σ,τ (Π σ,τ (X, Y )) → X Π 1 σ,τ (Π σ,τ (X, Y )) → Y ⊥ c(o,σ)→o (∃ + σ (Z, X)) → Z ⊥ c(o,σ)→σ (∃ + σ (Z, X)) → X app σ,τ (∃ - new ρ,σ→τ (m c(o,ρ) (T ), V σ→τ ), X) → ∃ - new ρ,τ (m c(o,ρ) (T ), app σ,τ (V σ→τ , X)) Π 0 σ,τ (∃ - new ρ,c(σ,τ ) (m c(o,ρ) (T ), V c(σ,τ ) )) → ∃ - new ρ,τ (m c(o,ρ) (T ), Π 0 σ,τ (V c(σ,τ ) )) Π 1 σ,τ (∃ - new ρ,c(σ,τ ) (m c(o,ρ) (T ), V c(σ,τ ) )) → ∃ - new ρ,τ (m c(o,ρ) (T ), Π 1 σ,τ (V c(σ,τ ) )) ∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), V c(o,σ) )) → V c(o,σ) ∃ - new σ,τ (m c(o,σ) (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), V c(o,σ) )), V τ ) → ∃ - new ρ,τ (m c(o,ρ) (T ), ∃ - new σ,τ (m c(o,σ) (V c(o,σ) ), V τ ))
This system can be easily proved terminating by most of the existing tools for proving termination of higher-order rewriting.

Let us show in detail how the last rule of the original example is transformed into the last two given above. The original rule is

∃ - σ,τ (∃ - ρ,c(o,σ) (T, J), G) → ∃ - ρ,τ (
T, λx : o y : ρ.∃ - σ,τ (J(x, y), G)) and after applying the same neutralization as in Example 7.4 to both sides of the rule, we obtain

∃ - new σ,τ ( m c(o,σ) (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), @(G, ⊥ c(o,σ)→o (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), ⊥ c(o,σ)→σ (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))))) → ∃ - new ρ,τ (m c(o,ρ) (T ), ∃ - new σ,τ ( m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), @(G, ⊥ c(o,σ)→o (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), ⊥ c(o,σ)→σ (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))))))
Then the rule is abstracted by

∃ - new σ,τ (m c(o,σ) (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), V c(o,σ) )), V τ ) → ∃ - new ρ,τ (m c(o,ρ) (T ), ∃ - new σ,τ (m c(o,σ) (V c(o,σ) ), V τ ))
with the abstracting substitution γ

   V c(o,σ) → @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )) V τ → @(G, ⊥ c(o,σ)→o (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))), ⊥ c(o,σ)→σ (∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )))))   
Following Definition 8.4, we need to add rules ensuring that the new righthand side instantiated by γ, namely

∃ - new ρ,τ (m c(o,ρ) (T ), ∃ - new σ,τ (m c(o,σ) (V c(o,σ) ), V τ ))
γ, rewrites to a term η-equivalent to the original righthand side. No middle ηequivalent term is needed. Adding rules to the simulating system S so that

∃ - new ρ,τ ( m c(o,ρ) (T ), ∃ - new σ,τ (m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )), @(G, ⊥ c(o,σ)→o ( ∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))) ), ⊥ c(o,σ)→σ ( ∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))) )))))
rewrites to

∃ - new ρ,τ ( m c(o,ρ) (T ), ∃ - new σ,τ (m c(o,σ) (@(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))), @(G, ⊥ c(o,σ)→o ( @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )) ), ⊥ c(o,σ)→σ ( @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T )) ))))
is enough, which can be achieved with the rule

∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))) → @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))
Since its lefthand side is not a rigid pattern, it must be abstracted again by the rule

∃ - new ρ,c(o,σ) (m c(o,ρ) (T ), V c(o,σ) )) → V c(o,σ)
with the abstracting substitution {V c(o,σ) → @(J, ⊥ c(o,ρ)→o (T ), ⊥ c(o,ρ)→ρ (T ))}, and we are done since the new righthand side with the substitution applied coincides with the original one. Hence framed rules a part of the simulating system.

Our result allows one to show normal termination of R by checking for higherorder termination of the rules of the rigid system S modulo η.

Computing a rigid system S simulating a given non-rigid system R is not always possible, but succeeds often in practice. The way used in the previous examples is the following: abstract by a fresh free variable the smallest subterm of l containing an outermost versatile subterm, and whose free variables are included in that of l. This defines the abstracting substitution γ. Then, the righthand side is constructed so as to ensure the (stronger than needed) property vγ -→ R A r = η r in Definition 8.4. Here is one more example using this transformation strategy:

Example 8.9. Let H : α → β → ρ, x : α and y : β be variables, and R = {f (h 1 (g(x, y)), @(@(H, h 2 (g(x, y))), h 3 (g(x, y)))) → @(@(H, x), y)} which can be abstracted by the three rules

{f (h 1 (g(x, y)), Z 1 ) → Z 1 , h 2 (g(x, y))) → x, h 3 (g(x, y)))) → y}
Let us now consider a new system with a much bigger rule:

f 1 (m 1 (f 2 (m 2 (T ), @(J, h 1 (T ), h 2 (T )))), @(G, h 3 (f 2 (m 2 (T ), @(J, h 1 (T ), h 2 (T )))), h 4 (f 2 (m 2 (T ), @(J, h 1 (T ), h 2 (T )))))) → f 3 (m 3 (T ), f 1 (m 1 (@(J, h 1 (T ), h 2 (T ))), @(G, h 3 (@(J, h 1 (T ), h 2 (T ))), h 4 (@(J, h 1 (T ), h 2 (T ))))))
which contains the free variables J : α → β → ρ and T : o. The abstraction includes the following additional three rigid rules:

{f 1 (m 1 (f 2 (m 2 (T ), X J )), X G ) → f 3 (m 3 (T ), f 1 (m 1 (X J ), X G )), h 3 (f 2 (m 2 (T ), X J )) → h 3 (X J ), h 4 (f 2 (m 2 (T ), X J )) → h 4 (X J )}

From termination modulo η to termination union η-reduction

We now turn to η-compatibility. Regarding termination, η-compatibility can easily be replaced by one-side η-compatibility, that is, either s = η s t implies s t or s t = η t implies s t . This fact is used to show that termination modulo η can be guaranteed by showing termination union η-reduction (after some minor transformation). Therefore, we can apply any technique that ensures termination union η-reduction, which is the case of orderings like HORPO or CPO, in order to show termination modulo η of the original system. As shown below, since the result is proved by working on η-normalized terms, we only have to η-normalize both sides of the rules and add a few rules needed to catch η-reductions that may involve part of the rule and part of the context. For instance if we have a rule @(a, x) → b in our rewrite system, then λx.@(a, x) can be rewritten into λx.b, but its η-normalization a cannot be rewritten by the η-normalization of @(a, x) → b which is the same rule. We therefore need to extend the set of rules by adding the η-normalization of the rules with all possible contexts which create η-redexes on top, and then η-normalize these rules. Apart from the extra η-normalization phase, these extensions are similar in spirit to Peterson and Stickel's notion of associative commutative extension [START_REF] Peterson | Complete Sets of Reductions for Some Equational Theories[END_REF], and its generalization by Jouannaud and Kirchner [START_REF] Jouannaud | Completion of a Set of Rules Modulo a Set of Equations[END_REF].

Definition 8.10. Let R be a higher-order term rewrite system. Let

R↓ η = {l↓ η → r↓ η | l → r ∈ R} R η = R↓ η ∪{ (λx i . . . x n .l)↓ η → (λx i . . . x n .r)↓ η | l → r ∈ R, i ∈ [1..n],
l = @(l , x 1 , . . . , x n ), (∀j = k) x j = x k , and (∀j) x j / ∈ Var(l )}

For example, if R contains a rule @(a, x, y) → b then R η contains the rules {@(a, x, y) → b, @(a, x) → λy.b, a → λxy.b} THEOREM 8.11. Let R be a higher-order term rewrite system. Then -→

(R)η∪β is terminating if -→ R η ∪β∪η is terminating. PROOF. We show that s = η s -→ R t = η t implies s ↓ η -→ + R η ∪η t ↓ η and s = η s -→ β t = η t implies s ↓ η -→ * β∪η t ↓ η .
By confluence of η, s ↓ η = s ↓ η and t ↓ η = t ↓ η . We therefore need to show that s -→ R t and s -→ β t imply s ↓ η -→ + R η ∪η t↓ η and s↓ η -→ * β∪η t↓ η respectively. -Suppose s = s[lσ] p and t = s[rσ] p for some rule l → r in R, substitution σ and position p in s. We proceed by induction on the size of s.

-If p = Λ then it holds since, by Property 8 of λ-calculus, we have lσ↓ η = l↓ η σ↓ η and rσ↓ η = r↓ η σ↓ η and l↓ η → r↓ η in R η . -If s = λx i . . . x n .lσ and l = @(l , x 1 , . . . , x n ), where n > 0, all x j are different, x j / ∈ Var(l ) and x j / ∈ Dom(σ), there is a rule @(l , x 1 , . . . ,

x i-1 )↓ η → λx i . . . x n .r ↓ η in R η . It follows that s ↓ η = @(l , x 1 , . . . , x i-1 )σ ↓ η = @(l , x 1 , . . . , x i-1 )↓ η σ↓ η → R η λx i . . . x n .r↓ η σ↓ η = s[rσ]↓ η . -If s = λx.@(s [lσ] p , x) with x / ∈ Var(s [lσ] p ) then s↓ η = s [lσ] p ↓ η .
= f (s 1 ↓ η . . . s [lσ] p ↓ η . . . s n ↓ η ) -→ + R η ∪η f (s 1 ↓ η . . . s [rσ] p ↓ η . . . s n ↓ η ) = t↓ η . -If s = @(s [lσ] p , s 2 ) or s = @(s 1 , s [lσ] p ) it
holds as in the previous case.

-Suppose s = s[@(λx.u, v)] p and t = s[u{x → v}] p for some position p in s.

There are two cases.

-If u = @(u , x) with x / ∈ Var(u ) then, by confluence of η-reduction, s↓ η = s[@(u , v)] p ↓ η , and since t = s[@(u , x){x → v}] p = s[@(u , v)] p , we have that s↓ η = t↓ η and thus trivially,

s↓ η -→ * β∪η t↓ η . -Otherwise s ↓ η = s[z] p ↓ η {z → @(λx.u ↓ η , v ↓ η )}, for a fresh variable z ∈ Var(s[z] p ↓ η ) by property of η. It follows that s↓ η -→ β s[z] p ↓ η {z → u↓ η {x → v↓ η }}.
Therefore, by confluence of η-reductions, s↓ η -→ + β∪η t↓ η . To conclude, we show that if -→ R η ∪β∪η is terminating then there cannot be an infinite sequence with -→ (R)η∪β . Assume there is an infinite sequence s 0 -→ (R)η∪β s 1 -→ (R)η∪β . . .. By the previous property, we get an infinite sequence s 0 ↓ η -→ * R η ∪β∪η s 1 ↓ η -→ * R η ∪β∪η . . .. Since β-reduction is terminating there must be infinitely many R η -steps, hence infinitely many (R) η -steps in the original sequence, contradicting our assumption.

From termination modulo η to plain termination on η-long forms

We reduce here termination modulo η to plain termination again, but using this time η-expanded forms. The question was first considered in Kop's PhD thesis [START_REF] Kop | Higher Order Termination[END_REF]], Sections 2.2 and 2.3, where it is shown that termination of R modulo η can be ensured by proving termination of some η-expansion of R, provided the lefthand sides of rules in R are higher-order patterns.

Once R is η-expanded, any termination technique for plain higher-order systems can be used. But since η-expansion relies on types, and type instantiation does not preserve η-long forms, these results do not accomodate polymorphism.

Kop considers a restricted form of η-expansion where a subterm u is expanded inside its superterm s, denoted s[u] → η s[λx.@(u, x)] if x : σ is a fresh variable; -u : σ → τ is not (i) a free variable; (ii) an abstraction; (iii) the left argument of an application;

(iv) an application of the form @(y, t 1 , . . . , t n ) where y is free in s and n > 0;

(v) any of the t i 's in @(y, t 1 , . . . , t n ) whenever y is free in s.

The η-long form of s, denoted by s↑ η , is the normal form of s with respect to restricted η-expansion. The η-long form of a rewrite system R is the set LEMMA 8.12. Let R be a set of rules in η-long form, whose lefthand sides are patterns not headed by λ. Then s -→ (R∪β) t implies s↑ η -→ + R↑ η ∪β t↑ η . We shall now reduce termination modulo η to plain termination via the computation of η-long forms in Kop's sense, hence allowing us to use Lemma 8.12. A nontrivial obstacle is that different η-equivalent terms may have different η-long forms. The reason originates in the syntactic restrictions in the definition of η-expansion that ensure termination, when the subterm of arrow type to be expanded is a free variable or the first argument of an application. For an example, @(λx.@(a, x), b) and @(a, b) are different η-equivalent η-long forms (in her sense).

R↑ η = { @(l, z 1 , . . . , z n )↑ η → @(r, z 1 , . . . , z n )↑ η : l → r ∈ R l : τ 1 → . . . τ n → o,
In order to avoid the problem with free variables we show termination by proving the absence of infinite sequences of closed terms, as already done in Theorem 3.8.

To conclude, from u -→ η u implies u ↑ η = u ↑ η , since u is also closed and normal with respect to β ∩ η, we have by easy induction that u↑ η = u↓ η ↑ η , for every closed term and normal with respect to β ∩ η. Therefore, we have u↑ η = u↓ η ↑ η and v↑ η = v↓ η ↑ η , and s↓ η = v↓ η , since u = η v, and we conclude.

We are now ready for the main result of this section: THEOREM 8.17. Let R be a higher-order term rewrite system, where all lefthand sides are rigid patterns. Then -→ (R)η∪β is terminating if -→ R↑ η ∪β is terminating on terms in η-long form. PROOF. Let s and t be two closed terms. First we show that if s -→ (R)η t then s↓ β∩η ↑ η -→ + R↑ η ∪β t↓ β∩η ↑ η . By definition, s = η s -→ R t = η t and, by Lemma 8.14, s ↓ β∩η -→ + R∪β t ↓ β∩η . This implies that s↓ β∩η = η s ↓ β∩η -→ + R∪β t ↓ β∩η = η t↓ β∩η , and by Lemma 8.12 and 8.16, s↓ β∩η ↑ η = s ↓ β∩η ↑ η -→ + (R↑ η ∪β) t ↓ β∩η ↑ η = t↓ β∩η ↑ η . Similarly, by Lemma 8.15 first and then Lemma 8.12, we conclude that s -→ β t implies s↓ β∩η ↑ η -→ * R↑ η ∪β t↓ β∩η ↑ η . We now show the absence of infinite sequences of closed terms. Let s 0 -→ (R)η∪β s 1 -→ (R)η∪β . . . be one. Since β alone is terminating, there must be infinitely many R-steps. By the previous two properties, we get an infinite sequence s i 0 ↓ β∩η ↑ η -→ + (R↑ η ∪β) s i 1 ↓ β∩η ↑ η -→ + (R↑ η ∪β) . . . with j ≤ i j < i j+1 for all j, contradicting the termination assumption of -→ R↑ η ∪β on terms in η-long form.

The method based on η-expansions has indeed several drawbacks: termination proof methods are better suited to η-reductions than η-expansions, which introduces abstractions; it requires lefthand sides of rules to be rigid patterns, a property which may not be compatible with other transformation methods and, moreover, it is not compatible with polymorphism. Despite the fact that η-long normal forms are often used in the implementations we are aware of, we believe that this method has less potential than the one based on η-reductions.

RELATED WORK

Proving termination properties of Nipkow's rewriting was considered first in [van de [START_REF] Van De Pol | Strict Functionals for Termination Proofs[END_REF], then in [START_REF] Jouannaud | Higher-Order Orderings for Normal Rewriting[END_REF], and later in [START_REF] Blanqui | Computability Closure: Ten Years Later[END_REF][START_REF] Kusakari | Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems[END_REF]Blanqui 2006]. Related investigations are carried out in [START_REF] Femke Van Raamsdonk | On Termination of Higher-Order Rewriting[END_REF].

Van de Pol was the first to look for and propose a solution to the problem of normal higher-order termination [van de [START_REF] Van De Pol | Strict Functionals for Termination Proofs[END_REF]. His solution, however, is a methodology needing important user-interaction to build an interpretation-based ordering first, and then prove that the ordering constructed has the required compatibility, monotonicity, and stability properties. As a methodology, it is quite powerful: van de Pol was able to prove many difficult terminating examples, some of which are listed in this paper. Although there is no hope to succeed automating this technique, a partial, powerful approximation is presented in [START_REF] Fuhs | Polynomial Interpretations for Higher-Order Rewriting[END_REF] for the case of simple types, where automatable higherorder polynomial interpretations are considered. How to extend this technique to polymorphic types, which are needed in example 7.5, is however unclear.

Inspired by van de Pol's work, we then developed a dedicated version of HORPO, which was indeed the first automatable, implemented method [START_REF] Jouannaud | Higher-Order Orderings for Normal Rewriting[END_REF]. Most ingredients of the present work were introduced there, in a form that was strongly tied to HORPO.

A third method is based on the notion of general schema as formulated in [START_REF] Blanqui | The Calculus of algebraic Constructions[END_REF][START_REF] Blanqui | Inductive-data-type systems[END_REF] where the notion of computability closure was introduced. The computability closure of a term l is a set C(l) such that a set of higher-order rules R including β is terminating provided r ∈ C(l) for each rule l → r ∈ R \ β. In [START_REF] Blanqui | Computability Closure: Ten Years Later[END_REF]], Blanqui shows that the computability closure makes it possible to define a well-founded order that contains the very first version of HORPO, where the order on types was just a congruence [START_REF] Jouannaud | The Higher-Order Recursive Path Ordering[END_REF], and can also be adapted to consider normal termination of higher-order rules whose lefthand sides are patterns in Miller's sense [START_REF] Miller | A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification[END_REF]], an assumption which is fundamental in his work. On the other hand, it is shown in [START_REF] Blanqui | The Computability Path Ordering[END_REF]] that HORPO enhanced with the computability closure [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], an order named CHORPO, is included in CPO, the computability path ordering [START_REF] Blanqui | The Computability Path Ordering: The End of a Quest[END_REF][START_REF] Blanqui | The Computability Path Ordering[END_REF]. Since these orderings are much easier to use and implement than the computability closure whose implementation involves search, we believe that the methods presented here, which can be easily adapted to CPO, overrun those based on the direct use of the computability closure.

Finally, higher-order dependency pairs have also been used for normal termination in [START_REF] Sakai | An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems[END_REF][START_REF] Sakai | On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems[END_REF][START_REF] Kusakari | Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems[END_REF][START_REF] Suzuki | Argument filterings and usable rules in higher-order rewrite systems[END_REF]Blanqui 2006;[START_REF] Kop | Higher-order dependency pairs with argument filterings[END_REF]. Patterns play an important role there too. A good survey of all these techniques is given in [START_REF] Kop | Higher Order Termination[END_REF], where the author also presents a general framework based on transforming different higher-order formalisms, including pattern higher-order systems, into a single one, namely algebraic functional systems with meta-variables. However, as is the case of the computability closure, methods based on dependency pairs require lefthand sides of rules to be headed by a function symbol, a restriction that we do not have and believe can be too restrictive for practice.

We do not really know how the dependency pairs method compares with ours. Comparing NHORPO with dependency pairs is not really fair as NHORPO inherits all known weaknesses of RPO that are far improved by the dependency pairs method. Still, as far as we know, the monomorphic version of Example 7.5 cannot be proved with the existing dependency pairs techniques. For the most part, this is due to the notion of neutralization which allowed us to carry out many quite difficult normal termination proofs. Neutralization is a general technique, as we have shown here, that is applied to transform the rewrite system before proving termination and hence other methods can benefit from its use. It could indeed be applied before using the dependency pair method or even try to include it as a processor to enhance the strength of dependency pairs framework in the higher-order setting. However, neutralization may transform a pattern into a non-pattern, as we have seen with Example 7.1, and hence it cannot be used with its full strength by methods which require lefthand sides of rules to be patterns, as is the case of all methods described above but ours. Note however that in all such cases, the bound variable argument of a free higher-order variable becomes a constant ⊥ of the same type after neutralization. It is quite possible that the definition of a higher-order pattern can be extended to handle such a simple case without loosing its numerous virtues. In particular, note that the most general unifier of the equation X(⊥) = v is X = λx.v, where x ∈ Var(v), which also is the most general unifier of the equation X(x) = v, with x ∈ Var(v), found in pattern unification.

Note finally that the results given in Section 8 provide a way to combine neutralization with higher-order dependency pairs techniques, since the transformed systems fulfill the pattern condition. Generally speaking, an important part of our work can be seen as develop ping preprocessors for proving termination of higher-order rewriting. Neutralization and the transformation techniques described in Section 8 are such preprocessors which allow the user to use existing techniques aiming at proving termination of higher-order rewriting as a back-end. They are also compatible with weak polymorphism, a key, novel feature of our work. We have shown how powerful these preprocessors are.

CONCLUSION

The methods we have presented here for normal termination of a set of higher-order rewrite rules are very general and provide easily implementable normal higherorder orderings. The user has to provide a precedence and statuses as is usual with the recursive path ordering. He or she may also provide neutralization levels together with filters selecting appropriate arguments for each function symbol. This requires some expertise, but can be automated by searching non-deterministically for appropriate neutralization levels and filters, as done by many implementations for the precedence and statuses required by the recursive path ordering. The list of examples given in the paper shows the strength of our approach. Some are indeed complex enough so that their termination is by no means obvious even to the expert. Some of our methods are based on reduction orderings but others are just transformations techniques applied to the rewrite system before using any other termination technique such as those based on the computational closure or on higher-order dependency pairs. Implementating these techniques will show which are most useful.

We believe that there is room for carrying out this research further. Much can be done to improve the techniques for showing higher-order termination, which will then benefit to normal higher-order termination. Indeed the higher-order recursive path ordering itself has been already generalized, to semantic precedences [START_REF] Borralleras | A Monotonic Higher-Order Semantic Path Ordering[END_REF], and to the calculus of constructions [START_REF] Walukiewicz-Chrzaszcz | Termination of rewriting in the Calculus of Constructions[END_REF]. Generalization of all existing techniques to handle richer type disciplines should be a next step. Search for effective transformations reducing normal termination to plain higher-order termination should also be carried on.

  and u ≡ v. By induction hypothesis, (uγ)↓≡ (vγ)↓, and since z ∈ Var(λx.(vγ)↓), it follows that (sγ)↓= λx.(uγ)↓≡ λz.(vγ)↓ {x → z} = λz.(v{x → z}γ)↓= (tγ)↓.

t

  for some p ∈ Pos(s). Then, s↓ β -→ * R∪β t↓ β (with s↓ β -→ + R∪β t↓ β in case p = Λ). is a rule u → v in R and a substitution γ, such that s| p = uγ and t = s[vγ] p . Since u is a rigid pattern, then (uγ) ↓ β = u(γ ↓ β ) by Lemma 8.3, and u(γ↓ β ) -→ + R v(γ↓ β ) -→ * β v(γ↓ β )↓ β = (vγ)↓ β . If p = Λ we are done. Otherwise, u is not an abstraction since R is a rigid system. Moreover, uγ is not an abstraction either since u is not a variable, hence s↓ β = (s[uγ] p )↓ β = s↓ β [uγ↓ β ] P where P is the (possibly empty) set of positions of z in s[z] p ↓ β . Since (uγ)↓ β -→ + R∪β (vγ)↓ β , then s↓ β [uγ↓ β ] P -→ * R∪β s↓ β [vγ↓ β ] P -→ * β (s↓ β [vγ↓ β ] P )↓ β = (s[vγ])↓ β .

  monotonic iff for all environments Γ, contexts u[], variable x, type σ and terms s, t s.t. Γ • {x : σ} Σ u[x : σ] : τ and (Γ Σ

	Definition 3.5. A binary relation on the set of judgments is
	-coherent iff for all terms s, t such that (Γ	Σ s : σ)	(Γ	Σ t : σ),
	and for all environment Γ such that Γ		Σ s : σ and Γ	Σ t : σ, then
	(Γ Σ s : σ) (Γ Σ t : σ);
	-stable iff for all terms s, t such that (Γ	Σ s : σ)	(Γ	Σ t : σ), and all
	substitutions γ such that ∀x ∈ Var(s), Θ Σ xγ : Γ(x) for some environment
	Θ, then (Θ Σ sγ : σ) (Θ Σ tγ : σ);

  t. s = lγ -→ Λ S rγ -→ * S∪β t. Given an arbitrary normal substitution θ, sθ -→ Λ S rγθ -→ * S∪β tθ. By Lemma 8.6, sθ↓ β -→ + S∪β rγθ↓ β and rγθ↓ β -→ * S∪β tθ↓ β , therefore sθ↓ β -→ + S∪β rγθ↓ β -→ * S∪β tθ↓ β , hence, by definition, since -→ S∪β is included in -→ (S)η∪β , we have sθ↓ β tθ↓ β .

  Further, since rewriting cannot introduce new variables, t = λx.@(s [rσ] p , x) with x / ∈ Var(s [rσ] p ), hence t↓ η = s [rσ] p ↓ η . Induction hypothesis concludes. -Otherwise, if s = λx.s [lσ] p then s↓ η = λx.(s [lσ] p ↓ η ), and t = λx.s [rσ] p with t ↓ η = λx.(s [rσ] p ↓ η ) ↓ η , by confluence of η-reduction. Now, by induction hypothesis, we have s [lσ] p ↓ η -→ + R η ∪η s [rσ] p ↓ η , and hence s↓ η = λx.(s [lσ] p ↓ η ) -→ + R η ∪η λx.(s [rσ] p ↓ η ) -→ * η t↓ η . -If s = f (s 1 . . . s [lσ] p . . . s n ) then s↓ η = f (s 1 ↓ η . . . s [lσ] p ↓ η . . . s n ↓

η ), and t = f (s 1 . . . s [rσ] p . . . s n ) with t↓ η = f (s 1 ↓ η . . . s [rσ] p ↓ η . . . s n ↓ η ). Now, by induction hypothesis, we have s [lσ] p ↓ η -→ + R η ∪η s [rσ] p ↓ η , and hence s↓ η

ACM Journal Name, Vol. 79, No. 3, Article 3, Publication date: May 2014.

This is Definition 5.1 there. The proof of transitivity is missing, but follows the same scheme as that of RPO[START_REF] Dershowitz | Orderings for Term-Rewriting Systems[END_REF]].ACM Journal Name, Vol. 79, No. 3, Article 3, Publication date: May

...q j n j ACM Journal Name, Vol. 79, No. 3, Article 3, Publication date: May

Acknowledgments: The referees pointed out a few inaccuracies, imprecise definitions and proofs. We thank them warmly. We also thank Cynthia Kop for scrutinizing the paper as nobody else would have done.

This work has been partly carried out in the INRIA-LIAMA project Formes and the UPC projects SweetLogics and DAMAS, supported by Spanish MEC/MICINN grants TIN2010-21062-C02-01 and TIN2013-45732-C4-3-P respectively. The first author is now Professor emeritus at Université Paris-Sud, although still working at École Polytechnique. This paper is based on a preliminary version published

We can now compute the full neutralizations of both sides of the first rule: FN ( diff ( λx.sin(@(F, x))

) ) = diff new ( @( λx. sin(@(F, x)) , ⊥) )

FN ( λx. cos(@(F, x)) × diff ( λx.@(F, x) ) ) = @( λx. cos(@(F, x)) , ⊥) × new @( diff new ( @( λx.@(F, x) , ⊥) ) , ⊥)

and normalizing both sides we get diff new (sin(@(F, ⊥))) → cos(@(F, ⊥)) × new @(diff new (@(F, ⊥)), ⊥)

and of the second rule: FN ( diff ( λx.@(F, x) × λy.@(F, y)

) ) = diff new ( @( @( λx.@(F, x) , ⊥) × new @( λx.@(F, x) , ⊥) , ⊥) )

FN ((diff(λx.@(F, x)) × λy.@(F, y))+(λx.@(F, x) × diff(λy.@(F, y)))) = @(@(diff new (@(λx.@(F, x), ⊥)), ⊥) × new @(λy.@(F, y), ⊥), ⊥) + new @(@(λx.@(F, x), ⊥) × new @(diff new (@(λy.@(F, y), ⊥)), ⊥), ⊥)

and normalizing both sides we get

An example with a non-empty set of argument positions is given at Example 7.2.

Properties of neutralization

We investigate here the interactions between neutralization, monotonicity and instantiation.

LEMMA 5.10. Let t : τ and u 1 , . . . , u n be higher-order terms and γ be a substitution. Then N i (tγ, u 1 γ, . . . , u n γ ) = N i (t, u 1 , . . . , u n )γ.

PROOF. We proceed by induction on i. There are three cases.

(1) If i < 0. Then, we have tγ : τ , and hence

(2) If i = 0 or τ is a data type. Then, we have tγ : τ , and hence

By induction hypothesis, this is equal to

LEMMA 5.11. Let t be a higher-order term and γ be a substitution. Then FN (tγ) = FN (t)FN (γ).

PROOF. We proceed by induction on |t|. There are four cases:

with sort f orm. The idea is that quantifiers are higher-order constructors binding a variable via the use of a functional argument.

We carry out the proof of the first rule, abbreviating ⊥ f orm as ⊥ and making application symbols explicit. First, we compute the full neutralization of both sides:

Second, we show that

. By case 2 we need to show P ∧ ∀ new (@(Q, ⊥)) > P ∧ @(Q, ⊥), and by case 3 we need {P, ∀ new (@(Q, ⊥))}(>) mul {P, @(Q, ⊥)}. This requires ∀ new (@(Q, ⊥)) > @(Q, ⊥) which holds by case 1.

Example 7.2. This example of surjective disjoint union is from [van de [START_REF] Van De Pol | Strict Functionals for Termination Proofs[END_REF]. The monomorphic signature and rules are parametrized by α ∈ S = {A, B, U } for sake of conciseness.

Statuses are multiset and precedence is equality. We sketch the proof of the first rule, computing first the β-normalization of the full neutralizations of both sides:

The proof that s > t uses successively cases 1, 8, and then 1 twice.

The second problem is more delicate, and that is where we need to introduce a new tool. Let β ∩ η be a new rewrite system encoding the intersection of β and η reductions via their two critical pairs:

λx.@(λy.u, x) → λy.u if x ∈ Var(λy.u) .

Clearly, β ∩η-reductions is included in βand η-reductions. We now investigate the properties of this rewrite system. LEMMA 8.13 (DIAMOND). The rewrite system β ∩η is strongly confluent.

PROOF. Using Huet's characterization of strong confluence for linear systems [Huet 1980], we need to prove that the 4 critical pairs are strongly confluent.

(1) First rule with itself. The superposition term is s = @(λx.@(λy.@(u, y), x), v), with x ∈ Var(λy.@(u, y)) and y ∈ Var(u). Then s -→ @(λx.@(u, x), v) and s -→ @(λy.@(u, y), v), both terms rewriting in one step to @(u, v).

(2) Second rule with itself. The superposition term is s = λx.@(λy.@(λz.u, y), x), with x, y ∈ Var(λz.u). Then s -→ λx.@(λz.u, x) and s -→ λy.@(λz.u, y), both terms rewriting in one step to λz.u.

(3) Second rule inside the first. The superposition term is s = @(λx.@(λy.u, x), v), with x ∈ Var(λy.u). Then s rewrites to @(λy.u, v) in both cases. (4) First rule inside the second. The superposition term is s = λx.@(λy.@(u, y), x), with x ∈ Var(λy.@(u, y)) and y ∈ Var(u). Then s rewrites to λx.@(u, x) with the first rule and λy.@(u, y) with the second, both terms being equal up to α-renaming.

Being confluent and terminating, the rewrite system β∩η enjoys the unique normal form property. We denote by u↓ β∩η the normal form of u with respect to β ∩ η.

LEMMA 8.14. Let u, v be two terms such that u -→ R v, where R is a higherorder rewrite system whose lefthand sides are patterns. Then, u↓ β∩η -→ + R∪β v↓ β∩η . PROOF. The proof is by induction on u compared with -→

If u = u ↓ β∩η , we are done. Otherwise, u q -→ β∩η u . We show by cases on p, q that u -→ R v and v -→ β∩η v for some v and conclude y induction hypothesis on u and confluence of β ∩ η which ensures that u↓ β∩η = u ↓ β∩η and v↓ β∩η = v ↓ β∩η .

(1) If p and q are disjoint, both steps commute as needed.

(2) p ≥ q. Since lefthand sides of rules in R are rigid patterns, their lefthand side is not an abstraction nor a β-redex, hence no overlap with β ∩ η is possible. Therefore, the R-redex is inside the substitution of the other redex, and since β ∩η is linear, both steps must commute and the result holds as above.

Normal Higher-Order Termination 3:41

(3) q > p, hence p = q • m for some position m. This is the difficult case. Assume first that m ∈ Pos(l) and l| m is an application, hence there is an overlap between the R-rule and the first rule in β ∩ η. Then l| m σ = @(λx.@(w 1 , x), w 2 ). Since lefthand sides of rules in R are β-normal, l| m cannot have an abstraction as first argument of the application, hence it can only be a variable. But this is impossible too by our assumption that l is a rigid pattern. Assume now that m ∈ Pos(l) and l| m is an abstraction, implying an overlap between the R-rule and the second rule in β ∩η. Then l| m σ = λx.@(λy.w, x) with x ∈ Var(λy.u). Higher-order substitutions do not capture variables, hence l| m = λx.@(w , x), and w must be an abstraction or a free variable. Impossible. We are left with the case where no overlap occurs, which holds as before.

LEMMA 8.15. Given two terms u, v such that u -→ β v then u↓ β∩η -→ * β v↓ β∩η .

PROOF. Let u p -→ β v, hence u| p = @(λx.s , t ). The proof is by induction on u. If u = u↓ β∩η , we are done. Otherwise, u q -→ β∩η u for some term u and position q. We show that u -→ β v and v -→ * β∩η v and conclude by induction hypothesis on u .

(1) If the position q is disjoint from p, or at a strict prefix of p without overlapping p, or inside s , or inside t , then the same β∩η-rewrite takes place in v (possibly many times in the latter case), yielding the result. (2) If u| q = @(λy.@(λx.s , y), t), with t = y ∈ Var(λx.s ). Then u and v are equal up to variable renaming. (3) If u| q = λy.@(λx.s , y), that is, t = y ∈ Var(λx.s ). Then u and v are equal up to variable renaming again.

LEMMA 8.16. Let u, v be η-equivalent, β ∩η-normal closed terms. Then u↑ η = v↑ η .

PROOF. We first prove that if u is closed and normal with respect to β ∩ η and u -→ η u then u↑ η = u ↑ η .

By assumption we have that there is a position p in u such that u| p = λx.@(w, x) with x ∈ Var(w) and u = u[w] p . Moreover, u is also closed and normal with respect to β ∩ η. Now, we show that, u = u[w] → η u[λx.@(w, x)] = u, which implies that u↑ η = u ↑ η .

Assume that the step u[w] → η u[λx.@(w, x)] cannot be applied, then, since u is closed there are only two possible reasons.

-If w is an abstraction of the form λy.s then, we have that u| p = λx.@(λy.s, x), which contradicts the fact that u is normal with respect to β ∩ η. -If w is the left argument of an application then, with q the position just above p, we have that u q = @(λx.@(w, x), w ) for some w , which again contradicts the fact that u is normal with respect to β ∩ η.