Frédéric Blanqui

Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

Keywords: termination, rewriting, λ-calculus, types, Girard's reducibility, rewriting modulo, matching modulo βη, patterns à la Miller

In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting modulo some equational theory and rewriting with matching modulo βη, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.

Introduction

This paper addresses the problem of checking the termination of various kinds of rewrite relations on simply typed λ-terms.

First-order rewriting [KB70, DJ90] and λ-calculus [START_REF] Church | A formulation of the simple theory of types[END_REF][START_REF] Barendregt | The lambda calculus: its syntax and semantics[END_REF] are two general (Turing-complete) computational frameworks with different strengths and limitations.

The λ-calculus is a language for expressing arbitrary functions based on a few primitives (abstraction over some variable and application of a function to an argument). Computation is done by repeatedly substituting formal arguments by actual ones (β-reduction) [START_REF] Church | A formulation of the simple theory of types[END_REF].

In first-order rewriting, one considers a fixed set of function symbols and a fixed set of term transformation rules. Computation is done by repeatedly substituting the left-hand side of a rule by the corresponding righthand side [START_REF] Knuth | Simple word problems in universal algebra[END_REF].

Hence, in λ-calculus, there is only one computation rule and it is unconditional while, in rewriting, a computation step occurs only if a term matches a pattern (possibly modulo some equational theory).

But first-order rewriting cannot express in a simple way anonymous functions or patterns with bound variables. See for instance the works on Combinatory Logic [START_REF] Curry | Combinatory logic[END_REF], first-order definitions of a substitution operation compatible with α-equivalence [dB78, ACCL91, Kes07] (to cite just a few, for the amount of publications on this subject is very important), or first-order encodings of higher-order rewriting [START_REF] Bonelli | Relating higher-order and first-order rewriting[END_REF].

Rewriting on λ-terms, or higher-order rewriting, aims at unifying these two languages. Several approaches exist like Klop's Combinatory Reduction Systems (CRSs) [Klo80, KvOvR93], Khasidashvili's Expression Reduction Systems (ERSs) [Kha90, GKK05], Nipkow's Higher-order Rewrite Systems (HRSs) [START_REF] Nipkow | Higher-order critical pairs[END_REF][START_REF] Mayr | Higher-order rewrite systems and their confluence[END_REF], or Jouannaud and Okada's higher-order algebraic specification languages (HALs) [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF][START_REF] Jouannaud | Abstract data type systems[END_REF]. Van Oostrom and van Raamsdonk studied the relations between CRSs and HRSs [START_REF] Van Oostrom | Comparing combinatory reduction systems and higher-order rewrite systems[END_REF] and developed a general framework (HORSs) that subsumes most of the previous approaches [vO94, vR96].

1 Hosted from July 2012 to August 2013 by the Institute of Software of the Chinese Academy of Sciences, Beijing, China.

Interpretation. For the simply-typed λ-calculus again, Gandy showed that λI-terms (λ-terms where, in every subterm λxt, x has at least one free occurrence in t), can be interpreted by hereditarily monotone functionals on N [START_REF] Gandy | Proofs of strong normalization[END_REF]. Then, van de Pol showed that there is a transformation from λ-terms to λIterms that strictly decreases when there is a β-reduction, and extended this to higher-order rewriting and other domains than N [vdP96]. Finally, Hamana developed a categorical semantics for terms with bound variables [START_REF] Hamana | An initial algebra approach to term rewriting systems with variable binders[END_REF] based on the work of Fiore, Plotkin and Turi [START_REF] Fiore | Abstract syntax and variable binding[END_REF], that is complete for termination (which is not the case of van de Pol's interpretations), and extended to higher-order terms the technique of semantic labeling [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF] introduced for first-order terms by Zantema [START_REF] Zantema | Termination of term rewriting by semantic labelling[END_REF]. However, Roux showed that its application to β-reduction itself is not immediate since the interpretation of β-reduction is not β-reduction [START_REF] Blanqui | On the relation between sized-types based termination and semantic labelling[END_REF][START_REF] Roux | Size-based termination: semantics and generalizations[END_REF].

Computability. The last technique, not limited to simply-typed λ-calculus, is based on Tait and Girard's notions of computability2 introduced by Tait [START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF] for the weak normalization of the simply-typed λ-calculus, and extended by Girard to polymorphic types [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse e[END_REF] and strong normalization [START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF].

There are however relations between these techniques. For instance, van de Pol proved that his interpretations on N can be obtained from a computability proof by adding information on the length of reductions [vdP96]. Conversely, the author and Roux proved that size-based termination [Gim98, Abe04, BFG + 04, Bla04], which is a refinement of computability, can to some extent be seen as an instance of Hamana's higher-order semantic labeling technique [START_REF] Blanqui | On the relation between sized-types based termination and semantic labelling[END_REF].

In this paper, we will consider a technique based on computability. Computability has been first used for proving the termination of the combination of β-reduction, in the simply typed or polymorphic λ-calculus, together with a first-order rewrite system that is terminating on first-order terms, by Tannen and Gallier [START_REF] Breazu-Tannen | Polymorphic rewriting conserves algebraic strong normalization[END_REF][START_REF] Breazu-Tannen | Polymorphic rewriting conserves algebraic strong normalization[END_REF] and Okada [START_REF] Okada | Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite[END_REF] independently. It was noticed later by Dougherty that, with first-order rewriting, a proof can be given that is independent of the proof of termination of β-reduction [START_REF] Dougherty | Adding algebraic rewriting to the untyped lambda calculus[END_REF][START_REF] Dougherty | Adding algebraic rewriting to the untyped lambda calculus[END_REF], because first-order rewriting cannot create β-redexes (but just duplicate them). But this does not extend to higher-order rewriting or to function symbols with polymorphic types.

In [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF][START_REF] Jouannaud | Abstract data type systems[END_REF], Jouannaud and Okada extended computability to higher-order rewrite rules following a schema extending Gödel' system T recursion schema on Peano integers [START_REF] Gödel | über einer bisher noch nicht benützte erweiterung des finiten standpunktes[END_REF] to arbitrary first-order data types. This work was then extended to Coquand and Huet's Calculus of Constructions [START_REF] Coquand | A theory of constructions[END_REF][START_REF] Coquand | The calculus of constructions[END_REF] in a series of papers culminating in [START_REF] Barbanera | Modularity of strong normalization in the algebraic-λ-cube[END_REF].

In [START_REF] Jouannaud | Inductive data type systems: strong normalization and all that[END_REF], Jouannaud and Okada reformulated this general schema as an inductively defined set called computability closure. This notion was then extended with the author to strictly positive inductive types [START_REF] Blanqui | The calculus of algebraic constructions[END_REF][START_REF] Blanqui | Inductive-data-type systems[END_REF] and to the Calculus of Algebraic Constructions, that is an extension of the Calculus of Constructions where types equivalent modulo user-defined rewrite rules are identified and function symbols can be given polymorphic and dependent types [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF].

In this paper, we provide a new presentation of the notion of computability closure for standard rewriting and show how to extend it for dealing with rewriting modulo some equational theory and higher-order pattern-matching, by providing detailed proofs of results sketched in [START_REF] Blanqui | Rewriting modulo in deduction modulo[END_REF][START_REF] Blanqui | Computability closure: ten years later[END_REF]. We do it in a progressive way by showing, step by step, how the notion of computability closure can be extended to cope with new term constructions or new rewriting mechanisms. To avoid unnecessary technicalities related to the type discipline, we do it in the simply typed λ-calculus but this work could be conducted in the Calculus of Algebraic Constructions as well, following the lines of [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF].

The paper is organized as follows. In Section 2, we define the set of terms that will be considered, introduce our notations and recall some general results on well-founded relations. In Section 3, we present the different definitions of computability introduced so far and discuss their relations and applicability to rewriting. In Section 4, we show how Girard's definition of computability can be extended to deal with rewriting with matching modulo α-equivalence by introducing the notion of computability closure, and provide a first core definition of such a computability closure. Then follows a number of subsections and sections showing how to extend this core definition to deal with new constructions or more general notions of rewriting: abstraction and bound variables, basic subterms, recursive functions, higher-order subterms, matching on defined symbols, rewriting modulo an equational theory and rewriting with matching modulo βη. We finally explain why our results apply to HRSs and simply typed CRSs as well.

Parts of this work have already been formalized in the Coq proof assistant [START_REF] Blanqui | A formalization in Coq of the notion of computability closure for proving the termination of rewrite relations on λ-term[END_REF]. See the conclusion for more details about that.

Definitions and notations

We first recall some definitions and notations about simply-typed λ-terms, rewriting and well-founded relations. See for instance [DJ90, [START_REF] Barendregt | Lambda calculi with types[END_REF][START_REF]Term rewriting systems[END_REF] for more details.

Notations for sequences

Given a set A, let A * be the free monoid generated from A, i.e. the set of finite sequences of elements of A or words on A. We denote the empty word by ε, word concatenation by juxtaposition, and the length of a word w by |w|. We often denote a word a 1 . . . a n by a. A word p is a prefix of a word q, written p ≤ q, if there is r such that q = pr. The prefix relation is a partial ordering. We write p#q if p and q are not comparable or disjoint.

Simple types

We assume given a set B of type constants. As usual, the set T of (simple) types is defined recursively as follows [START_REF] Church | A formulation of the simple theory of types[END_REF]:

• a type constant B ∈ B is a type;

• if T and U are types, then T ⇒ U is a type.

Terms

All over the paper, we only consider simply typed λ-terms (terms are always well-typed).

We follow Pottinger's approach [START_REF] Pottinger | Proofs of the normalization and Church-Rosser theorems for the typed λ-calculus[END_REF], that is, we assume that every variable or function symbol comes equipped with a fixed (simple) type and that α-equivalence replaces a variable by another variable of the same type only (assuming an infinite set of variable for each type). Hence, we do not have to consider untyped terms and introduce typing environments (finite map from variables to types) for terms and rules: it is like working in a fixed infinite typing environment.

Let X be an infinite set of variables and F be a set of function symbols disjoint from X , and assume that each variable or function symbol s is equipped with a type τ (s) so that there is an infinite number of variable of each type.

The family (L T ) T ∈T of the sets of raw terms of type T is inductively defined as follows:

• if s ∈ X ∪ F , then s ∈ L τ (s) ;

• if x ∈ X , T ∈ T and t ∈ L T , then λxt ∈ L τ (x)⇒T ;

• if U, V ∈ T , t ∈ L U⇒V and u ∈ L U , then tu ∈ L V .

For every type T , the set L T of terms of type T is the quotient of L T by type-preserving α-equivalence, that is, λxt = α λyu only if τ (x) = τ (y) [START_REF] Pottinger | Proofs of the normalization and Church-Rosser theorems for the typed λ-calculus[END_REF]. Let L = T ∈T L T be the set of all (typed) terms. We write t : T or τ (t) = T if the α-equivalence class of t belongs to L T . A relation R on terms preserves types if τ (t) = τ (u) whenever (t, u) ∈ R, written tRu (e.g. α-equivalence).

Note that function symbols do not have to be applied to any argument nor any fixed number of arguments. Hence, f, fx, fxy, etc. are legal terms (as long as they are well-typed). However, in some examples, for convenience, we may use infix notations, like x + y for denoting +xy.

Let FV(t) be the set of variables having a free occurrence in t (i.e. not bound by a λ), and BV(t) be the set of binding variables of a raw term t (e.g. BV(λxy) = {x}).

A term is linear if no variable has more than one free occurrence in it.

A term is algebraic if it contains no subterm of the form λxt or xt.

A type-preserving relation R on terms is monotone if, for all t, u, v, x such that tRu, one has (λxt)R(λxu), (tv)R(uv) whenever tv is well-typed, and (vt)R(vu) whenever vt is well-typed.

Substitution

A substitution σ is a map from X to L such that (1) for all x ∈ X , τ (σ(x)) = τ (x), and (2) its domain dom(σ) = {x ∈ X | σ(x) = x} is finite. In particular, we write u

x for the substitution σ such that σ(x) = u and σ(y

) = y if y = x. Let FV(σ) = {FV(σ(x)) | x ∈ dom(σ)}. A substitution σ is away from X ⊆ X if (dom(σ) ∪ FV(σ)) ∩ X = ∅.
Given a term t and a substitution σ, we denote by tσ the term obtained by replacing in t each free occurrence of a variable x by σ(x) by renaming, if necessary, variables bound in t so that no variable free in σ(x) becomes bound [START_REF] Curry | Combinatory logic[END_REF]. Note that substitution preserves typing: τ (tσ) = τ (t).

A relation R is stable by substitution (away from X) if (tσ)R(uσ) whenever tRu (and σ is away from X). It is a congruence if it is an equivalence relation that is monotone and stable by substitution.

Stable subterm ordering

The notion of sub-raw-term is not compatible with α-equivalence. Instead, we consider the notion of stable subterm: t s u if t is a sub-raw-term of u and FV(t) ⊆ FV(u). The relation s is a partial ordering stable by substitution. Let ⊳ s be its strict part and s (resp. ⊲ s ) be the inverse of s (resp. ⊳ s ).

Positions

The set of positions in a (raw) term t, Pos(t), is the subset of {0, 1} * such that:

• Pos(x) = Pos(f) = {ε} if x ∈ X and f ∈ F • Pos(tu) = {ε} ∪ {0w | w ∈ Pos(t)} ∪ {1w | w ∈ Pos(u)} • Pos(λxt) = {ε} ∪ {0w | w ∈ Pos(t)}
Given a (raw) term t, we denote by t| p its sub-raw-term at position p ∈ Pos(t), and by t[u] p the (raw) term obtained by replacing it by u.

A term t is η-long if every variable or function symbol occurring in it is maximally applied, that is, for all p ∈ Pos(t), if t| p ∈ X ∪ F and t| p : T ⇒ A, then there are q ∈ Pos(t) and t such that p = q0 | T | and t| q = t| p t [START_REF] Huet | Résolution d'équations dans les langages d[END_REF].

Given a term t and p ∈ Pos(t), the set BV(t, p) of binding variables above t| p is defined as follows:

• BV(t, ε) = ∅ • BV(tu, 0p) = BV(t, p) • BV(tu, 1p) = BV(u, p) • BV(λxt, 0p) = {x} ∪ BV(t, p)
For instance, Pos(λxfx) = {ε, 0, 00, 01} and BV(λxfx, 0) = {x}.

Rewriting

The relation of β-reduction (resp. η-reduction), → β (resp. → η ), is the monotone closure of {((λxt)u,

t u x ) | t, u ∈ L, x ∈ X } (resp. {(λx(tx), t) | t ∈ L, x ∈ X , x /
∈ FV(t)}). We write t x ] p , and similarly for t p → η u. Note that the relation → βη = → β ∪ → η preserves typing: if t : T and t → βη t ′ , then t ′ : T .

An equation is a pair of terms (l, r), written l = r, such that τ (l) = τ (r). A (rewrite) rule is a pair of terms (l, r), written l → r, such that τ (l) = τ (r), l is of the form f l and FV(r) ⊆ FV(l).

We assume neither that, if f l → r is a rule, then every occurrence of f in r comes applied to | l| arguments, nor that, if f l → r and f m → s are two distinct rules, then | l| = | m|. And, indeed, we will give examples of systems that do not satisfy these constraints in Section 4.6 (function ex) and Section 6 (after Lemma 20). Such systems are necessary for dealing with matching modulo βη because we use curried symbols. In contrast, in HRSs [START_REF] Nipkow | Higher-order critical pairs[END_REF], function symbols are always maximally applied (wrt their types) since terms are in η-long form and rules are of the form f l → r with f l of base type. Note however that, in [vdP96], van de Pol considers rules not necessarily in η-long form nor of base type.

The rewriting relation generated by a set of rules R, written → R , is the closure by monotony and substitution of R. Hence, t → R u if there are p ∈ Pos(t), l → r ∈ R and σ such that t| p = lσ and u = t[rσ] p . For instance, with R = {fx → x}, we have λxfxy → R λxxy. Note that rewriting preserves typing: if t : T and t → R t ′ , then t ′ : T .

Given a set of rules R, let D(R) = {f ∈ F | ∃ l, ∃r, f l → r ∈ R} be the subset of symbols defined by R, and α f = sup{| l| | ∃r, f l → r ∈ R}. Note that α f is finite even if R is infinite for f l is simply typed by assumption.3

Notations for relations

Given a relation R on a set A, let R(t) = {u ∈ A | tRu} be the set of reducts or successors of t. An element t such that R(t) = ∅ is said to be in normal form or irreducible.

Given a relation R, let R = be the reflexive closure of R, R + its transitive closure, R * its reflexive and transitive closure, and R -1 its inverse (xR -1 y iff yRx).

However, we will denote by ← β , ← η and ← R the inverse relations of → β , → η and → R respectively; by ↔ β , ↔ η and ↔ βη the symmetric closures of → β , → η and → βη respectively (i.e. → β ∪ ← β , etc.); and by = η and = βη the reflexive and transitive closures of ↔ η and ↔ βη respectively.

Given two relations R and S, we denote their composition by juxtaposition and say that R commutes with

S if RS ⊆ SR. For instance, if R is monotone, then ⊲ s commutes with R. A relation R is strongly confluent if R -1 R ⊆ (R = )(R = ) -1 , locally confluent if R -1 R ⊆ R * (R -1 ) * , and confluent if (R -1 ) * R * ⊆ R * (R -1 ) * .
For instance, the relations → η , → β and their union → βη are all confluent [START_REF] Pottinger | Proofs of the normalization and Church-Rosser theorems for the typed λ-calculus[END_REF].

Notations for quasi-orderings

Given an equivalence relation R on a set A, we denote by [t] R the equivalence class of an element t, and by A/R the set of equivalence classes modulo R.

Given a quasi-ordering ≥ on a set A (transitive and reflexive relation), let ≃ = ≥ ∩ ≥ -1 be its associated equivalence relation and > = ≥ -≥ -1 be its strict part (transitive and irreflexive relation).

Well-founded relations

Given a set A, an element a ∈ A is strongly normalizing wrt a relation R on A if there is no infinite sequence a = a 0 Ra 1 R . . . The relation R terminates (or is noetherian or well-founded4 ) on A if every element of A is strongly normalizing wrt R. Let SN(R) be the set of elements of A that are strongly normalizing wrt R. By abuse of language, we sometimes say that a quasi-ordering ≥ is well-founded when its strict part so is.

If R terminates (resp. is confluent) then every element has at least (resp. at most) one normal form. In particular, we will denote by t↓ η the unique normal form of t wrt → η .

Note that, if R is monotone, then R ∪ ⊲ s terminates iff R terminates.

In this paper, we are interested in the termination of the relation → β ∪ → R , or variants thereof. Note that → β terminates on well-typed terms [START_REF] Sanchis | Functionals defined by recursion[END_REF]. However, since termination is not a modular property (already in the first-order case) [START_REF] Toyama | Counterexamples to termination for the direct sum of term rewriting systems[END_REF], the termination of → R is generally not sufficient to guarantee the termination of → β ∪ → R . Moreover, considering → R alone does not make sense when, in a right-hand side of a rule, a free variable is applied to a term. This is not the case in CRSs and HRSs since, in these systems, the definition of rewriting includes some β-reductions after a rule application [START_REF] Van Oostrom | Comparing combinatory reduction systems and higher-order rewrite systems[END_REF].

Product quasi-ordering

The product of n relations R 1 , . . . , R n on the sets A 1 , . . . , A n respectively is the relation

(R 1 , . . . , R n ) prod on A 1 × . . . × A n such that x (R 1 , . . . , R n ) prod y if, for all i ∈ [1, n], x i R i y i .
If each R i is a quasi-ordering, then (R 1 , . . . , R n ) prod is a quasi-ordering too. If, moreover, the strict parts of R 1 , . . . , R n are well-founded, then the strict part of (R 1 , . . . , R n ) prod is well-founded too.

Given a quasi-ordering ≥ on a set A, let also ≥ prod denote the product quasi-ordering on A n with each component ordered by ≥.

Multiset quasi-ordering

Given a set A, let M = M(A) be the set of finite multisets on A (functions from A to N with finite support) [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF]. Given a quasi-ordering ≥ A on A, the extension of ≥ A on finite multisets is the smallest quasi-ordering ≥ M containing > 1 M ∪ ≃ M where ≃ M and > 1 M are defined as follows [START_REF] Comon | Les termes en logique et en programmation[END_REF]:

• ∅ ≃ M ∅, and M + {|x|} ≃ M N + {|y|} if M ≃ M N and x ≃ A y; 5 • M + {|x|} > 1 M M + {|y 1 , . . . , y n |} (n ≥ 0) if, for every i ∈ [0, n], x > A y i ;
where ≃ A (resp. > A ) is the equivalence relation associated to (resp. strict part of) ≥ A . Its associated equivalence relation is

≃ M . Its strict part > M is (> 1 M ) + ≃ M . It is well-founded if > A is well-founded.
Finally, let ≥ mul be the quasi-ordering on A * such that x ≥ mul y if {| x|} ≥ M {| y|}.

Lexicographic quasi-ordering

Given quasi-orderings ≥ 1 , . . . , ≥ n on sets A 1 , . . . , A n , the lexicographic quasi-ordering on A 1 × . . . × A n , written (≥ 1 , . . . , ≥ n ) lex , is the union of the following two relations:

• (≃ 1 , . . . , ≃ n ) prod ; • x > y if there is i ∈ [1, n] such that x i > i y i and, for all j < i, x j ≃ j y j ;
where ≃ i (resp. > i ) is the equivalence relation associated to (resp. strict part of) ≥ i . If > 1 , . . . , > n are well-founded, then > is well-founded too.

Given a quasi-ordering ≥ on a set A, let ≥ lex also denote the lexicographic quasi-ordering on A n with each component ordered by ≥.

Dependent lexicographic quasi-ordering

Given two sets A and B and, for each x ∈ A, a set B x ⊆ B, the dependent product of A and (B x ) x∈A is the set Σ x∈A B x of pairs (x, y) ∈ A × B such that y ∈ B x . In the following, we use in many places a generalization to dependent products of the lexicographic quasi-ordering (generalizing to quasi-orderings Paulson's lexicographic ordering on dependent pairs [START_REF] Paulson | Constructing recursion operators in intuitionistic type theory[END_REF]):

Definition 1 (Dependent lexicographic quasi-ordering). The dependent lexicographic quasi-ordering (DLQO) on a dependent product Σ x∈A B x associated to:

• a quasi-ordering ≥ A on A;

• for each equivalence class E modulo ≃ A , a set C E equipped with a quasi-ordering ≥ E ;

• for each x ∈ A, a partial function ψ x : B x → C [x]≃ A ;
is the union of the following two relations:

• (x, y) ≃ (x ′ , y ′ ) if x ≃ A x ′ ∧ ψ x (y) ≃ [x]≃ A ψ x ′ (y ′ ); • (x, y) > (x ′ , y ′ ) if x > A x ′ ∨ (x ≃ A x ′ ∧ ψ x (y) > [x]≃ A ψ x ′ (y ′ )); where ≃ A (resp. ≃ E ) is the equivalence relation associated to ≥ A (resp. ≥ E ), and > A (resp. > E ) the strict part of ≥ A (resp. ≥ E ).
If > A and each > E are well-founded, then > is well-founded too. Various examples of DLQOs will be given and used in the paper (in particular, in Sections 4.5.1 and 5.1).

Computability

The computability method was introduced by Tait to prove the weak normalization of (i.e. the existence of a normal form wrt) β-reduction in some extensions of the simply typed λ-calculus [START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF], and was later extended by Girard for dealing with polymorphic types [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse e[END_REF] and strong normalization [START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Girard | Proofs and types[END_REF]. This method consists of: 1. defining a domain Cand ⊆ P(SN(→ β )) of computability candidates for interpreting types; 6 2. interpreting each type T by a candidate [[T ]] ∈ Cand; 3. proving that each term of type T is computable, i.e. belongs to [[T ]], from which it follows that every typed term is strongly normalizing wrt → β .

In this section, we will see the various definitions that have been proposed for Cand so far, and discuss which ones are best suited for extension to arbitrary, and in particular non-orthogonal 7 , rewrite systems. However, all those definitions satisfy the following properties:

• variables are computable: for every P ∈ Cand, X ⊆ P ;

• Cand is stable by the operation ∝: P(L) × P(L) → P(L) defined by:

∝ (P, Q) = {v ∈ L | ∀t ∈ P, vt ∈ Q} i.e. if P, Q ∈ Cand, then ∝ (P, Q) ∈ Cand;
• Cand is stable by arbitrary 8 non-empty intersection:

if (A i ) i∈I is a non-empty family of candidates, then i∈I A i ∈ Cand;

• Cand contains SN(→ β ).

The last two conditions imply that Cand has a structure of complete lattice for inclusion, 9 the greatest lower bound of a set P ⊆ Cand being given by the intersection P if P = ∅, and SN(→ β ) if P = ∅. However, its lowest upper bound (the smallest candidate containing the union) is not necessarily the union [START_REF] Riba | On the stability by union of reducibility candidates[END_REF].

The intersection allows one to interpret quantification on types (polymorphism) or inductive types (see Section 4.6), while ∝ allows one to interpret ⇒ so that, by definition, vt ∈

[[V ]] if v ∈ [[T ⇒ U ]] and t ∈ [[T ]],
which is the main problem when trying to prove the termination of β-reduction.

We now see every definition we are aware of:

• Red: Girard' set of reducibility candidates [START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Girard | Proofs and types[END_REF] 6 In the following, like Girard in [Gir72, GLT88], we will in fact consider a domain Cand T ⊆ P(L T ) for each type T , but this is not relevant in this section.

7 A rewrite system is orthogonal if it is left-linear and non-ambiguous (i.e. has no critical pair). This is in particular the case of ML-like programs. An important property of orthogonal systems is their confluence [START_REF] Huet | Confluent reductions: abstract properties and applications to term-rewriting systems[END_REF][START_REF] Klop | Combinatory reduction systems[END_REF][START_REF] Van Oostrom | Confluence for abstract and higher-order rewriting[END_REF].

8 Finite or infinite. 9 An inf-complete lattice L that has a biggest element is complete. The supremum of a set P ⊆ L is indeed glb(ub(P )) where glb is the greatest lower bound and ub(P ) is the non-empty set of all the upper bounds of P .

10 Called "simple" in [START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF] and "neutral" in [START_REF] Girard | Proofs and types[END_REF].

8

In λ-calculus with no function symbols, a term is neutral if it is not an abstraction. Neutral terms satisfy the following key property: if t is neutral then, for all terms u, → β (tu

) = {t ′ u | t → β t ′ } ∪ {tu ′ | u → β u ′ },
∝ * (E, Q) = {v ∈ L | ∀ t ∈ E, v t ∈ Q}
Note that a sequence t ∈ L * can be seen as the context [] t. Hence,

∝ * (E, Q) = {v ∈ L | ∀e ∈ E, e[v] ∈ Q}.
Reducibility candidates and saturated sets are studied in [START_REF] Gallier | On Girard's "candidats de réductibilité[END_REF]. In particular, every reducibility candidate is a saturated set: Red ⊆ Sat. The converse does not hold in general since a saturated set does not need to be stable by reduction: for instance, the smallest saturated set containing λx(λyy)x does not contain λxx. However, Riba showed that every saturated set stable by reduction is a reducibility candidate [START_REF] Riba | On the stability by union of reducibility candidates[END_REF]. Hence, Red = Sat → = {P ∈ Sat | → β (P ) ⊆ P }. In [START_REF] Parigot | Proofs of strong normalization for second order classical natural deduction[END_REF], Parigot showed that every element of SatInd is a bi-orthogonal: SatInd ⊆ Bi. Finally, Riba showed that every bi-orthogonal is a reducibility candidate [START_REF] Riba | Strong normalization as safe interaction[END_REF]: Bi ⊆ Red. In particular, bi-orthogonals are stable by reduction. On the other hand, I don't know whether SatInd, Bi and Red are distinct. In conclusion, we currently have the following relations:

SatInd ⊆ Bi ⊆ Red = Sat → Sat
A natural question is then to know to which extent each one of these sets can be used to handle rewriting, and if a set allows to show the termination of more systems than the others. All these definitions rely on the form of redexes (reducible expressions): Red uses the notion of neutral term, a set P ∈ Sat has to be stable by head-expansion (inverse relation of head-reduction), and Bi is defined as the set of bi-orthogonals wrt a relation between terms and contexts that allows one to build redexes.

• Bi being exclusively based on the notion of context, it does not seem possible to extend it to nonorthogonal rewrite relations.

• The saturated sets could perhaps be extended by adding:

(S4) if l → r ∈ R, rσ t ∈ P and σ ∈ SN(→ β ∪ → R ), then lσ t ∈ P .
In order to have SN(

→ β ∪ → R ) ∈ Sat R , one has then to prove that lσ t ∈ SN(→ β ∪ → R ) if rσ t ∈ SN(→ β ∪ → R ) and σ ∈ SN(→ β ∪ → R )
, which is generally not the case if R is not orthogonal. This problem could perhaps be solved by considering all the head-reducts of lσ, but then we would arrive at a condition similar to (R3).

• In contrast to the previous domains, Girard's reducibility candidates seem easy to extend to arbitrary rewrite relations. This is therefore the notion of computability that we will use in the following.

Rewriting with matching modulo α-equivalence

In this section, we provide a survey on the notion of computability closure for standard rewriting (that is in fact rewriting modulo α-equivalence, because terms are defined modulo α-equivalence) first introduced in [START_REF] Blanqui | The calculus of algebraic constructions[END_REF][START_REF] Blanqui | Inductive-data-type systems[END_REF]. We present the computability closure progressively by showing at each step how it has to be extended to handle new term constructions. Omitted proofs can be found in [START_REF] Blanqui | Inductive-data-type systems[END_REF][START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]. For dealing with recursive function definitions (Section 4.5 below), we introduce a new more general rule based on the notion of F -quasi-ordering compatible with application (Definition 6) and provide various examples of such F -quasi-orderings in Section 4.5.1 (and later in Section 5.1).

Definition of computability

To extend to rewriting Girard's definition of computability predicates [START_REF] Girard | Proofs and types[END_REF], we first have to define the set of neutral terms. By analogy with abstractions, a term of the form f t with f ∈ D(R) should be neutral only if f is applied to enough arguments wrt R, i.e. | t| ≥ α f . Otherwise, f tu could be head-reducible and the key property of neutral terms, that

→ (tu) = {t ′ u | t → t ′ } ∪ {tu ′ | u → u ′ }
whenever t is neutral, would not hold. Now, what about terms of the form f t with f ∈ F -D(R) (undefined symbols)? We could a priori consider them as neutral. However, for dealing with higher-order subterms in Sections 4.6 and 4.7, we will consider type interpretations for which it seems difficult to prove (R3) if such terms are neutral. We therefore exclude them from neutral terms:

Definition 2 (Computability candidates). Given a set R of rewrite rules of the form f l → r, a term is neutral 13 if it is of the form x v, (λxt)u v or f v with f ∈ D(R) and | v| ≥ α f = sup{| l| | ∃r, f l → r ∈ R}.
Given a type T , let Red T R be the set of all the sets P ⊆ L T such that: (R1) P ⊆ SN(→) where → = → β ∪ → R ; (R2) P is stable by reduction: if t ∈ P and t → u, then u ∈ P ; (R3) if t : T is neutral and → (t) ⊆ P , then t ∈ P .

Given P ∈ Red T R and Q ∈ Red U R , let ∝ (P, Q) = {v : T ⇒ U | ∀t ∈ P, vt ∈ Q}.
Note that computability predicates are sets of well-typed terms and that all the elements of a computability predicate have the same type.

For the sake of simplicity, in all the remaining of the paper, we write SN instead of SN(→), but → will have different meanings in sections 5 and 6.

We now check that the family (Red T R ) T ∈T has the properties described in Section 3:

Lemma 1 For every type T , Red T R is stable by non-empty intersection and admits SN T = {t : T | t ∈ SN} as greatest element. Moreover, for all T, U ∈ T ,

P ∈ Red T R and Q ∈ Red U R , ∝ (P, Q) ∈ Red T ⇒U R .
Proof. The fact that SN T ∈ Red R and the stability by non-empty intersection are easily proved. We only detail the stability by

∝. Let T, U ∈ T , P ∈ Red T R and Q ∈ Red U R . Every element of ∝ (P, Q) is of type T ⇒ U . (R1) Let v ∈ ∝ (P, Q). Let x be a variable of type T . By (R3), x ∈ P . By definition of ∝, vx ∈ Q. By (R1), vx ∈ SN. Thus, v ∈ SN. (R2) Let v ∈ ∝ (P, Q), v ′ ∈ → (v) and t ∈ P . By definition of ∝, vt ∈ Q. By (R2), v ′ t ∈ Q.
(R3) Let v : T ⇒ U neutral such that → (v) ⊆ ∝ (P, Q), and t ∈ P . We show that vt ∈ Q by well-founded induction on t with → as well-founded relation (t ∈ SN by (R1)). Since v is neutral, vt is neutral too. Hence, by (R3), it is sufficient to show that → (vt) ⊆ Q. Let w ∈ → (vt). We first prove (a): either w = v ′ t with v → v ′ , or w = vt ′ with t → t ′ . We proceed by case on vt → w:

• vt → β w. Since v is neutral, v is not an abstraction and (a) is satisfied.

• vt → R w. If there are f ll → r ∈ R and σ such that vt = f lσlσ and w = rσ, then v = f lσ and | l| < | ll| ≤ α f . Since v is neutral, this is not possible. Thus (a) is verified.

We now show that w ∈ Q.

• Case w = v ′ t with v → v ′ .
By assumption, v ′ ∈ ∝ (P, Q). As t ∈ P , we have w ∈ Q.

• Case w = vt ′ with t → t ′ . By (R2), t ′ ∈ P . Thus, by the induction hypothesis, w ∈ Q.

Therefore, as already mentioned in Section 3, every Red T R is a complete lattice for inclusion. Now, one can easily check Tait's property (S3) described in the previous section (implying that elements of Red T R are Tait saturated sets with SN(→ β ) replaced by SN(→ β ∪ → R )):

Lemma 2 Given T ∈ T and P ∈ Red T R , (λxt)u v ∈ P iff (λxt)u v : T , t u x v ∈ P and u ∈ SN. Proof. Assume that (λxt)u v ∈ P . Then, (λxt)u v : T . By (R2), t u x v ∈ P . By (R1), (λxt)u v ∈ SN. Therefore, u ∈ SN.
Assume now that (λxt)u v : T , t u x v ∈ P and u ∈ SN. By (R1), t u x v ∈ SN. Therefore, v ∈ SN, t u x ∈ SN and t ∈ SN. We now prove that, for all t, u, v ∈ SN, (λxt)u v ∈ P , by induction on → prod . Since (λxt)u v : T and (λxt)u v is neutral, by (R3), it suffices to prove that every reduct w of (λxt)u v belongs to P . Since rules are of the form f l → r, there are two possible cases:

• w = t u x v.
Then, w ∈ P by assumption.

• w = (λxt ′ )u ′ v ′ and tu v → prod t ′ u ′ v ′ .
Then, w ∈ P by the induction hypothesis.

Corollary 1 Given T, U ∈ T , P ∈ Red T R and Q ∈ Red U R , λxt ∈ ∝ (Q, P ) iff λxt : U ⇒ T and, for all u ∈ Q, t u
x ∈ P . Proof. Assume that λxt ∈ ∝ (Q, P ) and u ∈ Q. Then, by definition of ∝, λxt : U ⇒ T and (λxt)u ∈ P . Therefore, by (R2), t u x ∈ P . Assume now that λxt : U ⇒ T and, for all u ∈ P , t u x ∈ P . By definition, λxt ∈ ∝ (Q, P ) if, for all u ∈ Q, (λxt)u ∈ P . So, let u ∈ Q. By (R1), u ∈ SN. Therefore, by Lemma 2, (λxt)u ∈ P .

Given two sets A and B and, for each

x ∈ A, a set B x ⊆ B, let Π x∈A B x = P(Σ x∈A B x ) be the set of partial functions f : A → B such that, for all x ∈ dom(f ), f (x) ∈ B x .
Given an interpretation of type constants

I ∈ Π B∈B Red B R , the interpretation of types [[ ]] I ∈ Π T ∈T Red T R
is defined as follows:

•

[[B]] I = I(B) if B ∈ B, • [[T ⇒ U ]] I = ∝ ([[T ]] I , [[U ]] I ).
We say that a type constant B is basic if its interpretation is SN B , and that a symbol f :

T ⇒ B is basic if B is basic. Let the basic interpretation be the interpretation I such that I(B) = SN B for all B ∈ B.
We say that a term t : T is computable wrt a base type interpretation

I if t ∈ [[T ]] I . A substitution σ is computable wrt a base type interpretation I if, for all x ∈ X , xσ ∈ [[τ (x)]] I .
Note that, by (R3), variables are computable. Therefore, the identity substitution is always computable.

By definition of the interpretation of arrow types, a symbol f :

T ⇒ U is computable wrt a base type interpretation I if, for all t ∈ [[ T ]] I , f t ∈ [[U ]] I . So, let Σ I be the set of pairs (f, t) such that f : T ⇒ U and t ∈ [[ T ]] I (f
may be partially applied in f t), and let Σ I max be the subset of Σ I made of the pairs (f, t) such that U ∈ B, that is, when f is maximally applied.

In the following, we may drop the exponent I when it is clear from the context.

Theorem 1 The relation → β ∪ → R terminates on well-typed terms if there is I ∈ Π B∈B Red B R such that every non-basic undefined symbol and every defined symbol is computable.

Proof. It suffices to prove that every well-typed term is computable. For dealing with abstraction, we prove the more general statement that, for all t : T and computable σ, tσ ∈ [[T ]], by induction on t. This indeed implies that every well-typed term is computable since the identity substitution is computable by (R3). We proceed by case on t:

• t = x ∈ X . Then, tσ = xσ ∈ [[T ]] since σ is computable. • t = uv. By the induction hypothesis, uσ ∈ [[τ (v) ⇒ T ]] and vσ ∈ [[τ (v)]]. Therefore, by definition of [[ ]], tσ = (uσ)(vσ) ∈ [[T ]]. • t = f : T ⇒ A. If f is a defined symbol or a non-basic undefined symbol, then tσ = f is computable by assumption. Otherwise, f is a basic undefined symbol. By definition, it is computable if, for all t ∈ [[ T ]], f t ∈ [[A]]. Since f is basic, [[A]] =
SN. Now, one can easily prove that f t ∈ SN, by induction on t with → prod as well-founded relation ( t ∈ SN by (R1)).

• t = λxu. Wlog we can assume that σ is away from {x}. Hence, tσ = λx(uσ).

By Corollary 1, λx(uσ) ∈ [[T ]] = [[τ (x) ⇒ τ (u)]] if λx(uσ) : τ (x) ⇒ τ (U ) and (uσ) v x ∈ [[τ (u)]] for all v ∈ [[τ (x)]]. Since σ is away from {x}, we have (uσ) v x = uθ where xθ = v and yθ = yσ if y = x. Since θ is computable, by induction hypothesis, uθ ∈ [[τ (u)]].
Note that, with the basic interpretation, there is no non-basic undefined symbol. In Section 4.4, we will see another interpretation with which non-basic undefined symbols are computable.

Core computability closure

The next step consists then in proving that every defined symbol is computable,

i.e. f ∈ [[τ (f)]] I for all f ∈ D(R). Assume that τ (f) = T ⇒ A. As just seen above, f is computable if, for all t ∈ [[ T ]] I , f t ∈ I(A). Since f ∈ D(R) and | t| ≥ α f , f t is
neutral and, by (R3), belongs to I(A) if all its reducts so do. The notion of computability closure enforces this property.

Definition 3 (Computability closure).

A computability closure is a function CC mapping every f ∈ D(R) and l ∈ L * such that f l is well-typed to a set of well-typed terms.

Definition 4 (Valid computability closure -first definition).14 A computability closure CC is valid wrt a base type interpretation I if it satisfies the following properties:

• it is stable by substitution: tσ ∈ CC f ( lσ) whenever t ∈ CC f ( l);

• it preserves computability wrt I: every element of CC f ( l) is computable whenever l so are.

Theorem 2 Given I ∈ Π B∈B Red B R , every defined symbol is computable if there is a valid computability closure CC such that, for every rule f l → r ∈ R, we have r ∈ CC f ( l).
Proof. As just explained, it is sufficient to prove that, for all (f, t) ∈ Σ max with f ∈ D(R) and f : T ⇒ A, every reduct t of f t belongs to [[A]]. We proceed by well-founded induction on t with → prod as well-founded relation ( t ∈ SN by (R1)). There are two possible cases:

• There is u such that t = f u and t → prod u. By (R2), u ∈ [[ T ]]. Therefore, by the induction hypothesis, f u ∈ [[A]].
• There are w, f l → r ∈ R and σ such that t = lσ w and t = rσ w. Since r ∈ CC f ( l) and CC is stable by substitution, we have rσ ∈ CC f ( lσ). Since lσ are computable and CC preserves computability, we have rσ computable. Finally, since w is computable, we have t computable.

Hence, the termination of → β ∪ → R can be reduced to finding computability-preserving operations to define a computability closure. Among such operations, one can consider the ones of Figure 1 that directly follow from the definition or properties of computability.

(arg) { l} ⊆ CC f ( l) (app) if t ∈ CC f ( l), t : U ⇒ V , u ∈ CC f ( l) and u : U , then tu ∈ CC f ( l) (red) if t ∈ CC f ( l) and t → u, then u ∈ CC f ( l) (undef-basic) if g ∈ F -D(R), g : T ⇒ B, B ∈ B and [[B]] = SN B , then g ∈ CC f ( l)
Theorem 3 For all I ∈ Π B∈B Red B R , the smallest computability closure closed by the operations I is valid.

Proof. • Stability by substitution. We prove that, for all t ∈ CC f ( l), we have tσ ∈ CC f ( lσ), by induction on the definition of CC f ( l).

(arg) By (arg), { lσ} ⊆ CC f ( lσ).

(app) By the induction hypothesis, {tσ, uσ} ⊆ CC f ( lσ). Therefore, by (app), (tu)σ = (tσ)(uσ) ∈ CC f ( lσ).

(red) By the induction hypothesis, tσ ∈ CC f ( lσ). Since → is stable by substitution, tσ → uσ. Therefore, by (red), uσ ∈ CC f ( lσ).

(undef-basic) By (undef-basic), gσ = g ∈ CC f ( lσ).

• Preservation of computability. Assume that l are computable. We prove that, for all t ∈ CC f ( l), t is computable, by induction on the definition of CC f ( l).

(arg) l are computable by assumption.

(app) By the induction hypothesis, t and u are computable. Therefore, by definition of [[U ⇒ V ]], tu is computable.

(red) By the induction hypothesis, t is computable. Therefore, by (R2), u is computable.

(undef-basic) After the proof of Theorem 1, g is computable.

Therefore, using for I the basic interpretation, we get:

Corollary 2 The relation → β ∪ → R terminates on well-typed terms if, for every rule f l → r ∈ R, we have r ∈ CC f ( l),
where CC is the smallest computability closure closed by the operations I.

Handling abstractions and bound variables

Consider now the following symbol definition, where T , U and V are any type:

o : (U ⇒ V ) ⇒ (T ⇒ U ) ⇒ (T ⇒ V ) f o g → λx f (g x)
It cannot be handled by the operations I. By Corollary 1, a term λxt is computable if, for all u ∈ [[τ (x)]], t u x is computable. We can therefore extend the previous core definition of CC by the rules of Figure 2 if we generalize validity as follows:

Definition 5 (Valid computability closure -extended definition). 15 A computability closure CC is valid wrt a base type interpretation I if:

• it is stable by substitution: tσ ∈ CC f ( lσ) whenever t ∈ CC f ( l) and σ is away from FV(t) -FV( l);

• it preserves computability wrt I: tθ is computable whenever t ∈ CC f ( l), l are computable, θ is computable and dom(θ) ⊆ FV(t) -FV( l).

Note that, if FV(t) ⊆ FV( l) as it is required for the right-hand side of a rule, then the above conditions reduce to the ones of Definition 4.

(var) X -FV( l) ⊆ CC f ( l) (abs) if t ∈ CC f ( l) and x ∈ X -FV( l), then λxt ∈ CC f ( l) Theorem 4 For all I ∈ Π B∈B Red B
R , the smallest computability closure CC closed by the operations I and II is valid.

Proof. We proceed as in Theorem 3 but only detail the new cases.

• Stability by substitution. We prove that, for all t ∈ CC f ( l) and σ away from FV(t) -FV( l), we have tσ ∈ CC f ( lσ), by induction on the definition of CC f ( l).

(var) Let x ∈ X -FV( l). Since σ is away from FV(x) -FV( l), we have xσ = x and x ∈ X -FV( lσ). Therefore, by (var), x ∈ CC f ( lσ).

(abs) Wlog we can assume that σ is away from {x}. Hence, (λxt)σ = λx(tσ) and, since x ∈ X -FV( l), we have x ∈ X -FV( lσ). Therefore, by (abs), λx(tσ) ∈ CC f ( lσ) for, by the induction hypothesis, tσ ∈ CC f ( lσ).

• Preservation of computability. Assume that l are computable. We prove that, for all t ∈ CC f ( l) and computable θ such that dom(θ) ⊆ FV(t) -FV( l), we have tθ computable, by induction on CC f ( l).

(var) Let x ∈ X -FV( l). Then, xθ is computable by assumption.

(abs) Wlog we can assume that θ is away from {x}. Hence, (λxt)θ = λx(tθ). Now, by Corollary 1, λx(tθ) is computable if, for all computable u : τ (x), (tθ) u x is computable. Since θ is away from {x}, (tθ) u x = tσ where xσ = u and yθ = yσ if y = x. Now, σ is computable and dom(σ) ⊆ FV(t) -FV( l) for dom(θ) ⊆ FV(λxt) -FV( l). Therefore, by the induction hypothesis, tσ is computable.

For instance, we have {f, g} ⊆ CC o by (arg), x ∈ CC o by (var), f (gx) ∈ CC o (f, g) by (app) twice, and λxf (gx) ∈ CC o (f, g) by (abs).

Handling basic subterms

Consider now the following definition on unary natural numbers (Peano integers):

z : N; s : N ⇒ N pred z → z pred (s x) → x
In order to handle this definition, we need to extend the computability closure with some subterm operation. Unfortunately, ⊲ s does not always preserve computability as shown by the following example:

16 f : A ⇒ (A ⇒ B); c : (A ⇒ B) ⇒ A f (c y) → y Indeed, with w = λxfxx, we have w(cw) → β f(cw)(cw) → R w(cw) → β . . . [Men87]. Therefore, cw ∈ SN but w /
∈ ∝ (SN, SN) since w(cw) / ∈ SN. On the other hand, ⊲ s preserves termination. Hence, we can add the operation of Figure 3 for basic subterms (we omit the proof).

(subterm-basic) if t ∈ CC f ( l), t ⊲ s u : B ∈ B and [[B]] = SN B , then u ∈ CC f ( l)
Hence, to handle the above predecessor function definition, it is enough to take I(N) = SN N . In Sections 4.6 and 6, we will see other computability-preserving subterm operations.

Handling recursive functions

Consider now a simple recursive function definition:

+ : N ⇒ N ⇒ N z + y → y (s x) + y → s (x + y)
For handling such a recursive definition, and more generally mutually recursively defined functions, we need to extend CC f ( l) with terms of the form g m. In order to ensure termination, we can try to use some well-founded DLQO ≥ on Σ (DLQOs are defined in Definition 1 and Σ just before Theorem 1) so that (f, l) > (g, m) and prove by induction on > that CC preserves computability and defined function symbols are computable. However, we cannot consider arbitrary DLQOs. Indeed, since we consider curried symbols and, by (app), adding arguments preserves termination, the number of arguments is not a valid termination criterion as shown by the following example:

val : (N ⇒ N) ⇒ N; f : N ⇒ (N ⇒ N) val x → x z f x z → val (f x) where f x z → val (f x) → f x z → . . .
We therefore need to consider DLQOs compatible with application:

Definition 6 (F -quasi-ordering). An F -quasi-ordering is a DLQO on Σ. A relation R on Σ is:

• compatible with application if, for all (f, l v), (g, m w) ∈ Σ max , (f, l v)R(g, m w) whenever (f, l)R(g, m);

• stable by substitution if (f, lσ)R(g, mσ) whenever (f, l)R(g, m), σ is away from FV( m) -FV( l) and lσ, mσ are computable.

A simple way to get an F -quasi-ordering compatible with application is to restrict comparisons to pairs (f, t) such that f is maximally applied in f t. For instance, given a quasi-ordering ≥ on terms, the DLQO associated to:

• the identity relation on F ;

• for each equivalence class E modulo identity, the quasi-ordering ≥ prod (resp. ≥ mul );

• for each symbol f, the identity function

ψ f ( t) = t if f is maximally applied in f t;
is an F -quasi-ordering compatible with application, that is stable by substitution if ≥ so is. For the sake of simplicity, we also denote such a DLQO by ≥ prod (resp. ≥ mul ) and its strict part by > prod (resp. > mul ). Hence, → * prod , ( s ) mul and, more generally, (→ * s ) mul17 are F -quasi-orderings compatible with application and stable by substitution. For the sake of simplicity, we will denote (→ + ) prod by → prod .

Definition 7 (Valid F -quasi-ordering). A quasi-ordering ≥ on terms is compatible with reduction if > ∪ → is well-founded, where > is the strict part of ≥. It is valid if, moreover, > and the equivalence relation associated to ≥ are both stable by substitution.

An F -quasi-ordering ≥ is compatible with reduction if > ∪ → prod is well-founded on Σ max , where > is the strict part of ≥. It is valid if, moreover, > and the equivalence relation associated to ≥ are both stable by substitution and compatible with application.

Note that > ∪ → prod is required to be well-founded on Σ max , that is, on pairs (f, t) such that f : T ⇒ A, A ∈ B and t ∈ [[ T ]]. Note also that, by (R1), → prod is well-founded on computable terms.

For instance, ≥ prod and ≥ mul are both valid if ≥ so is. In particular, → * prod and (→ * s ) mul are both valid (⊲ s commutes with → since → is monotone).

In the next subsection, we will give another example of valid F -quasi-ordering. With a valid F -quasi-ordering, we can add the operation of Figure 4.

(rec) if g : M ⇒ U , m : M , m ∈ CC f ( l) and (f, l) > (g, m), then g m ∈ CC f ( l)
Lemma 3 Let ≥ be a valid F -quasi-ordering, (f, t) ∈ Σ max and assume that, for all (g, u) ∈ Σ max such that (f, t) > (g, u), g u is computable. Then, for all l, w, t and θ such that t = l w, θ is computable, dom(θ) ⊆ FV(t) -FV( l) and t ∈ CC f ( l), where CC is the smallest computability closure closed by the operations I to IV, we have tθ computable.

Proof. We proceed as for Theorem 4 by proving that, for all t ∈ CC f ( l) and computable θ such that dom(θ) ⊆ FV(t) -FV( l), tθ is computable, by induction on CC, but only detail the new case:

(rec) We have mθ computable by the induction hypothesis. Since dom(θ) ⊆ FV(g m) -FV( l), lθ = l. Since > is stable by substitution, we have (f, l) > (g, mθ). Assume now that

U = V ⇒ B and let v ∈ [[ V ]].
Since > is compatible with application, we have (f, l w) > (g, mθ v). Hence, by assumption, g mθ v is computable. Therefore, g mθ is computable.

Theorem 5 The relation → β ∪ → R terminates on well-typed terms if there are I ∈ Π B∈B Red B R and a valid F -quasi-ordering ≥ such that:

• every non-basic undefined symbol is computable;

• for every rule f l → r ∈ R, we have r ∈ CC f ( l), where CC is the smallest computability closure closed by the operations I to IV.

Proof. We follow the proof of Theorem 2 that, for all (f, t) ∈ Σ max with f ∈ D(R), every reduct t of f t is computable, but proceed by induction on > ∪ → prod . There are two cases:

• There is u such that t = f u and t → prod u. By (R2), u is computable. Therefore, by the induction hypothesis, f u is computable.

• There are w, f l → r ∈ R and σ such that t = lσ w and t = rσ w. Since r ∈ CC f ( l) and CC is stable by substitution (for > is stable by substitution), we have rσ ∈ CC f ( lσ). Thus, by Lemma 3, rσ is computable since, for all (g, u) ∈ Σ max , if (f, t) > (g, u), then g u is computable by the induction hypothesis.

As a consequence, by taking the basic interpretation for I, we get:

Corollary 3 The relation → β ∪ → R terminates on well-typed terms if, for every rule f l → r ∈ R, we have r ∈ CC f ( l),
where CC is the smallest computability closure closed by the operations I to IV, and ≥ is any F -quasi-ordering valid wrt the basic interpretation.

In the first paper implicitly using the notion of computability closure for higher-order rewriting [JO91, JO97a], Jouannaud and Okada take the basic interpretation for I and define for CC a schema generalizing Gödel' system T recursion schema on Peano integers [START_REF] Gödel | über einer bisher noch nicht benützte erweiterung des finiten standpunktes[END_REF] to arbitrary first-order data types. This schema is included in any computability closure closed by the operations I to IV with the F -quasi-ordering ( s ) stat defined in the next subsection. The present inductive formulation first appeared in [START_REF] Blanqui | The calculus of algebraic constructions[END_REF][START_REF] Blanqui | Inductive-data-type systems[END_REF]. In Section 4.5.2, we provide various examples of systems that can be proved terminating by using this corollary.

Examples of valid F -quasi-orderings

We have seen that a simple way to get an F -quasi-ordering compatible with application is to only compare terms of base type. Another way is to always compare the same fixed subset of arguments by using a particular case of arguments filtering system (AFS) [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]:

Definition 8 (Arguments filtering system). A filter is a word on N -{0}. The arity of a filter ϕ = k 1 . . . k n is ϕ ∞ = max{0, k 1 , . . . , k n }. A word w is compatible with a filter ϕ if |w| ≥ ϕ ∞ . We denote by ϕ A the function mapping every word a ∈ A * compatible with ϕ = k 1 . . . k n to a k1 . . . a kn . An arguments filtering system (AFS) is a function ϕ providing, for each f ∈ D(R), a filter ϕ f of arity ϕ f ∞ ≤ α f .
An AFS describes, for each symbol f, which arguments, and in which order, these arguments must be compared. For instance, if ϕ f = 322, then ϕ L f (t 1 t 2 t 3 . . .) = t 3 t 2 t 2 . Hence, when comparing (f, t 1 t 2 t 3 ) and (f, u 1 u 2 u 3 u 4 ), one in fact compares t 3 t 2 t 2 and u 3 u 2 u 2 only.

Following [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF][START_REF] Kamin | Attempts for generalizing the recursive path orderings[END_REF], here is an F -quasi-ordering allowing both multiset and lexicographic comparisons depending on a function stat : F → {lex, mul}: Definition 9 (Status F -quasi-ordering). Given a quasi-ordering ≥ on terms, a quasi-ordering ≥ F on F , an AFS ϕ and a function stat : F → {lex, mul} compatible with ≃ F , i.e. such that:

• stat f = stat g whenever f ≃ F g; • |ϕ f | = |ϕ g | whenever f ≃ F g and stat f = lex;
let ≥ stat be the DLQO associated to:

• the quasi-ordering ≥ F on F ;

• for each equivalence class E modulo ≃ F of status mul (resp. lex), the quasi-ordering ≥ mul (resp. ≥ lex );

• for each symbol f, the function ψ f ( t) = ϕ L f ( t).
The F -quasi-ordering ≥ stat is valid whenever ≥ so is. In particular, (→ * s ) stat is valid.

Examples of termination proofs based on computability closure

With the above closure operations, one can already prove the termination of a large class of rewrite systems including:

• Gödel system T [Göd58]: rec T N : N ⇒ T ⇒ (N ⇒ T ⇒ T ) ⇒ T , for every type T rec T N z u v → u rec T N (s x) u v → v x (rec T N x u v)
To give an example, let us detail why the right-hand side of the second rule is in the computability closure of the left-hand. We take the identity relation on F for ≥ F , ϕ rec T N = 1 as AFS (only the first argument of rec T N will be used in comparisons), and stat rec T N = lex. Then, we have {s x, u, v} ⊆ CC = CC rec T N (s x, u, v) by (arg), x ∈ CC by (subterm-basic), rec T N x u v ∈ CC by (rec) for s x ⊲ s x, and v x (rec T N x u v) ∈ CC by (app) twice.

• Ackermann's function:

ack : N ⇒ N ⇒ N ack z n → s n ack (s m) z → ack m (s z) ack (s m) (s n) → ack m (ack (s m) n)
One can easily check that, for each rule, its right-hand side is in the computability closure of its left-hand side by taking ϕ ack = 12 and stat ack = lex.

• The following non-orthogonal set of rules for subtraction on unary natural numbers:

-: N ⇒ N ⇒ N z -x → z x -z → x (s x) -(s y) → x -y x -x → z
can also be proved terminating by taking ϕ sub = 1 and stat sub = lex.

• Here is an example of a rule for computing subtyping constraints on simple types that requires multiset comparisons (take ϕ ≤ = 12 and stat ≤ = mul):

arrow : T ⇒ T ⇒ T; ≤ : T ⇒ T ⇒ C; ∧ : C ⇒ C ⇒ C arrow x y ≤ arrow x ′ y ′ → x ′ ≤ x ∧ y ≤ y ′
• Here is an example of mutually defined functions requiring a true quasi-ordering on function symbols (height T ≃ F height F ):

nil : F; cons : T ⇒ F ⇒ F; leaf : T; node : F ⇒ T; height T : T ⇒ N; height F : F ⇒ N height F nil → z height F (cons t f ) → max (height T t) (height F f ) height T leaf → z height T (node f ) → s (height F f )
• Finally, here is an example showing that the operations I to IV can already handle rules with matching on basic defined symbols (we will see the case of non-basic defined symbols in Section 4.7):

× : N ⇒ N ⇒ N z + y → y (s x) + y → x + (s y) (x + y) + z → x + (y + z) z × y → z (s x) × y → (x × y) + y (x + y) × z → (x × z) + (y × z)

Handling higher-order subterms

The closure operations presented so far do not enable us to deal with functions defined by induction on higher-order inductive types, that is, on inductive types with constructors taking functions as arguments.

Here are some examples:

• The "addition" on the following (type theoretic) ordinal notation [START_REF] Coquand | Inductively defined types[END_REF]:

zero : O suc : O ⇒ O lim : (N ⇒ O) ⇒ O + : O ⇒ O ⇒ O zero + y → y (suc x) + y → suc (x + y) (lim x) + y → lim (λn (x n) + y)
• The computation of the prenex normal form in the predicate calculus [START_REF] Mayr | Higher-order rewrite systems and their confluence[END_REF]:

⊥, ⊤ : F; ¬ : F ⇒ F; ∧, ∨ : F ⇒ F ⇒ F; ∀, ∃ : (T ⇒ F) ⇒ F (∀ P ) ∧ Q → ∀ (λx (P x) ∧ Q) ¬ (∀ P ) → ∃ (λx ¬ (P x)) . . .
• The list of labels of a tree in breadth-first order using continuations (we only give the definition of one of the functions) [START_REF] Hofmann | Approaches to recursive data types -a case study[END_REF]:

nil : L; cons : N ⇒ L → L; d : C; c : ((C ⇒ L) ⇒ L) → C; ex : C ⇒ L ex d → nil ex (c x) → x ex
Indeed, in all these examples, there are two problems. First, we need the higher-order arguments of a computable function-headed term to be computable, e.g. x in (lim x). Second, we need to have a DLQO in which (lim x) is bigger than (x n), where n is a bound variable.

But we have already seen in Section 4.4 that the first property is not always satisfied. Fortunately, under some conditions, it is possible to define an interpretation I satisfying this property by using the fact that Red R is a complete lattice (as seen in Section 3) on which, therefore, any monotone function has a fixpoint [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF]. Following [START_REF] Matthes | Extensions of system F by iteration and primitive recursion on monotone inductive types[END_REF], two different definitions are possible that we illustrate with the type O of ordinals:18

• An elimination-based definition using recursor symbols. For instance, for O, one can define the family of recursor symbols rec T O indexed by T ∈ T as follows:

rec T O : O ⇒ T ⇒ (O ⇒ T ⇒ T ) ⇒ ((N ⇒ O) ⇒ (N ⇒ T ) ⇒ T ) ⇒ T rec T O zero u v w → u rec T O (suc x) u v w → v x (rec T O x u v w) rec T O (lim x) u v w → w x (λn rec T O (x n) u v w)
and define I(O) as some fixpoint of the following monotone function:

F O (X) = {t ∈ L | ∀T ∈ T , ∀P ∈ Red T R , ∀u ∈ [[A]] J , ∀v ∈ [[O ⇒ A ⇒ A]] J , ∀w ∈ [[(N ⇒ O) ⇒ (N ⇒ A) ⇒ A]] J , rec T O t u v w ∈ [[A]] J }
where A is a type constant distinct from O and N19 ,

J(A) = P , J(O) = X and J(N) = I(N)
The computability of rec T O directly follows from the definition of I(O). And for proving that x is computable if (lim x) so is, it suffices to take T = O and w = λxλyx which is clearly computable. Indeed, in this case, rec O O (lim x)uvw → wx(λnrec O O (xn)uvw) → x and we can conclude by (R2). Finally, proving that constructors are computable is no more complicated.

• An introduction-based definition using constructors only. In this approach, I(O) is defined as some fixpoint of the following monotone function:

F O (X) = {t ∈ SN | ∀u, (t → * suc u ⇒ u ∈ X) ∧ (t → * lim u ⇒ u ∈ [[N ⇒ O]] J )}
where J(O) = X and J(N) = I(N)

In this case, the computability of constructor arguments directly follows from the definition of I(O).

In [START_REF] Matthes | Extensions of system F by iteration and primitive recursion on monotone inductive types[END_REF], p. 116-117, Matthes proves that, when using saturated sets, the introduction-based interpretation is included into the elimination-based interpretation and provides an example of type for which the two interpretations are distinct, by using the fact that some saturated sets are not stable by reduction. It is not too difficult to check that this cannot happen with reducibility candidates.

Anyway, in both cases, the monotony of F O is due to the fact that O occurs only positively in the types of the arguments of the constructors of O, knowing that A occurs positively in B ⇒ A and negatively in A ⇒ B.

More formally:

Definition 10 (Positive and negative positions). Given a type T , the positive (resp. negative) positions of T , Pos + (T ) (resp. Pos -(T )), are the subsets of {0, 1} * defined as follows:

• Pos + (B) = {ε} • Pos -(B) = ∅ • Pos + (T ⇒ U ) = {0w | w ∈ Pos -(T )} ∪ {1w | w ∈ Pos + (U )} • Pos -(T ⇒ U ) = {0w | w ∈ Pos + (T )} ∪ {1w | w ∈ Pos -(U )}
And the positions in a type T of the occurrences of a type constant B, Pos(B, T ), are:

• Pos(B, B) = {ε} • Pos(B, C) = ∅ if B = C • Pos(B, T ⇒ U ) = {0w | w ∈ Pos(B, T )} ∪ {1w | w ∈ Pos(B, U )}
This leads to the following common restrictions one can for instance find in the Calculus of Inductive Constructions (CIC)20 [CPM88, Wer94] and proof assistants based on CIC like Agda [START_REF] Bove | A brief overview of Agda -a functional language with dependent types[END_REF], Coq [START_REF] Inria | The Coq reference manual[END_REF] or Matita [START_REF] Asperti | The Matita interactive theorem prover[END_REF]:

Definition 11 (Standard inductive system). Given a set R of rewrite rules, the set of type constants B and the set of undefined function symbols F -D(R) (constructors) form a standard inductive system if there is a well-founded quasi-ordering ≥ B on B such that, for all

B ∈ B, c ∈ F -D(R), c : T ⇒ B, i ∈ [1, | T |] and C occurring in T i , either C < B B or else C ≃ B B and Pos(C, T i ) ⊆ Pos + (T i ).
Taking a quasi-ordering instead of an ordering allows us to deal with mutually defined inductive types. However, in this case, one has to reason on equivalence classes modulo ≃ B because, if B ≃ B C, then the interpretation of B and the interpretation of C have to be defined at the same time.

In such a system, one can define I ∈ Π B∈B Red B R by induction on > B and, for each equivalence class E modulo ≃ B , as some fixpoint S E of a monotone function F E (similar to the function F O above) on the complete lattice E → Red R ordered point-wise by inclusion (I ≤ J if, for all B ∈ E, I(B) ⊆ J(B)). See Lemma 14 in [START_REF] Blanqui | Inductive-data-type systems[END_REF] or Section 6.3 in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF] for more details about that. For each type constant B, I(B) is then defined as

S [B]≃ B (B).
With this interpretation, all the symbols f ∈ F -D(R) (constructors) are computable and one can add to the computability closure the operations of Figure 5.

(undef) F -D(R) ⊆ CC f ( l) (subterm-undef) if g t ∈ CC f ( l), g t : B and g ∈ F -D(R), then { t} ⊆ CC f ( l)
However, the stable subterm ordering is not sufficient to prove the termination of the systems given above. For instance, for the addition on O, starting from an argument of the form (lim x), we have a recursive call with an argument of the form (x n) where n is a bound variable. Although x is a subterm of (lim x), (x n) is not. In the case of continuations, this is even worse: starting from an argument of the form (c x), the function ex is applied to no argument but is itself argument of x. . . If, for S E , we take the smallest fixpoint of F E (the set of fixpoints is itself a complete lattice [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF]), then it can be obtained by transfinite iteration [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF]: there is an ordinal a such that, for all B ∈ E, S E = F a E (⊥ E ) where ⊥ E is the smallest element of E → Red R and F a E is defined by transfinite induction:

• F 0 E (X) = X • F a+1 E (X) = F E (F a E (X)) • F l E (X) = {F a E (X) | a < l} if l is a limit ordinal
This provides us with a notion of rank to compare computable terms:

Definition 12 (Rank of a computable term). The rank of a term t ∈ I(B), rk B (t), is the smallest ordinal

a such that t ∈ F a [B]≃ B (⊥ [B]≃ B )(B). Let B be the quasi-ordering on I(B) such that t B u if rk B (t) ≥ rk B (u).
Note that some terms may have a rank bigger than ω. For instance, with i : N ⇒ O defined by the rules i z → zero and i(s

n) → suc(i n), we have rk O (lim i) = ω + 1.
The relation ≻ B is compatible with reduction since t B u whenever t ∈ [[B]] and t → u (reduction cannot increase the rank of a term by (R2)). However, it is not stable by substitution. For instance, s z > O y for rk O (s z) = 1 and rk O (y) = 0, but s z < O s (s z) for rk O (s (s z)) = 2. Restricting t ≻ B u to the cases where FV(u) ⊆ FV(t) is not a solution since, with the addition on O, we have to compare (lim x) and (x n). Instead, we will consider a sub-quasi-ordering of B due to Coquand [Coq92] that is valid (in a sense that will be precised after the definition) and, in which, (lim x) is bigger than (x n):

Definition 13 (Structural subterm ordering). The i-th argument of c : T ⇒ B is strictly positive if T i is of the form U ⇒ C with C ≃ B and, for all D occurring in U , D < B B. Let ⊲ acc s be the smallest sub-ordering of ⊲ s such that, for all c : T ⇒ B, t : T and i ∈ [1, | t|], we have c t ⊲ acc s t i if the i-th argument of c is strictly positive. Given a term of the form f l, a term t : T is structurally bigger than a term u : U , written t > f l s u, if T and U are equivalent type constants and there are v and x ∈ X -FV( l) such that t ⊲ acc s v and u = v x. 21 Finally, let ≥ f l s be the reflexive closure of > f l s .

For instance, lim x > (lim x)+y s

x n for lim x : O, x n : O, lim x ⊲ acc s x and n ∈ X -FV((lim x) + y). The relation > f l s is valid in the following generalized sense. First, l i σ > f lσ s uσ whenever l i > f l s u, dom(σ) ⊆ FV( l) and σ is away from FV(u) -FV( l). Second, if l i > f l s u, l i : B is computable, θ is computable and dom(θ) ⊆ FV(u)-FV( l), then uθ : B is computable and l i ≻ B uθ (see Lemma 18 in [START_REF] Blanqui | Inductive-data-type systems[END_REF] or Lemma 54 in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]). Hence, by adapting Lemma 3, we can provide an instance of Theorem 5 able to handle functions defined by induction on the structural subterm ordering, by using a status F -quasi-ordering compatible with the rank ordering (that is defined on terms of the same computability predicate only): Definition 14. An AFS ϕ and a map stat : F → {lex, mul} compatible with an equivalence relation ≃ F on F are compatible with the rank ordering when the following conditions are satisfied:

• if E is an equivalence class modulo ≃ F of status mul, then there is a constant type B E such that, for all f ∈ E with f : T ⇒ A and

ϕ f = k 1 . . . k n , we have T ki = B E for every i ∈ [1, n];
• if E is an equivalence class modulo ≃ F of status lex, then there is a sequence of constant types B E such that, for all f ∈ E with f :

T ⇒ A, we have ϕ T f ( T ) = B E .
Theorem 6 In a standard inductive system, the relation → β ∪ → R terminates on well-typed terms if there are a well-founded quasi-ordering ≥ F on F , an AFS ϕ and a status map stat compatible with ≃ F and the rank ordering such that, for every rule f l → r ∈ R, we have r ∈ CC f ( l), where CC is the smallest computability closure closed by the operations I to V with, in (rec), > = (→ * ≥ f l s ) stat .22

Proof. By adapting Lemma 3, we can follow the proof of Theorem 5 but proceed by induction on the DLQO ≻ stat associated to:

• the quasi-ordering ≥ F on F ;

• for each equivalence class E modulo ≃ F of status mul (resp. lex with

| B E | = n), the quasi-ordering (≻ B E ) mul (resp. (≻ B E 1 , . . . , ≻ B E n ) lex ); • for each symbol f, the function ψ f ( t) = ϕ L f ( t)
, which is compatible with application and reduction.

Using this theorem, we can prove the termination of the first two examples given at the beginning of this section, or the rules defining the recursor on O. For instance, if we take ϕ + = 1 and stat + = lex, then {lim x, y} ⊆ CC = CC + (lim x, y) by (arg), n ∈ CC by (var) for n ∈ X -FV(lim x, y), x ∈ CC by (subtermundef), (x n) + y ∈ CC by (rec) for lim x > (lim x)+y s

x n, λn(x n) + y ∈ CC by (abs) for n ∈ X -FV(lim x, y), and lim (λn(x n) + y) ∈ CC by (undef). This is however not sufficient to orient the rules defining the function ex above since the type for continuations is not strictly positive. To deal with non-strictly positive types, one needs to consider type constants with size annotations [Abe04, BFG + 04, BR06].

Handling matching on non-basic defined symbols

We have already seen at the end of Section 4.5 that the rule (subterm-basic) allows to handle matching on basic defined symbols and not only undefined symbols (constructors) as in the previous section. Consider now the following set of rules on the strictly-positive type O of ordinals:

+ : O ⇒ O ⇒ O zero + y → y (suc x) + y → suc (x + y) (lim x) + y → lim (λn (x n) + y) (x + y) + z → x + (y + z)
For handling the last rule (associativity), we need x and y to be computable whenever x + y so is. But this does not follow from the interpretation of types in standard inductive systems which ensures that all the arguments of a computable term of the form f t are computable if f is an undefined symbol (constructor) and some positivity conditions are satisfied. However, the introduction-based interpretation of types can be easily extended to include other symbols as long as the positivity conditions are satisfied. Moreover, these conditions can be checked for each argument independently. Hence the following definitions: Definition 15 (Accessible argument). Given a well-founded quasi-ordering ≥ B on B, the set of accessible positions of a symbol f :

T ⇒ B, Acc(f), is the set of integers i ∈ [1, | T |] such that, for all C occurring in T i , either C < B B or else C ≃ B B and Pos(C, T i ) ⊆ Pos + (T i ).
Let M(R) be the set of symbols f that are strict subterms of a left-hand side of a rule and for which Acc(f) is not empty (matched symbols with accessible arguments).

Then, for I(O), we can take:

F O (X) = {t ∈ SN | ∀f ∈ M(R), ∀ T , ∀ u, τ (f) = T ⇒ O ∧ | T | = | u| ∧ t → * f u ⇒ ∀i ∈ Acc(f), u i ∈ [[T i ]] J } 23
where J(O) = X and J(N) = I(N). But, for F O (X) to satisfy the property (R3), we need to exclude from the set of neutral terms the terms of the form f t with f ∈ M(R):

Definition 16 (Neutral term -New definition). Given a set R of rewrite rules, a term is

neutral 24 if it is of the form x v, (λxt)u v or f v with f ∈ D(R) -M(R) and | v| ≥ α f = sup{| l| | ∃r, f l → r ∈ R}.
Then, we have the following property:

Lemma 4 A term a : A is computable iff all its reducts are computable and, for all f ∈ M(R), i ∈ Acc(f) and a such that a = f a, a i is computable.

Proof. The only-if part directly follows from (R2) and the definition of the interpretation. For the if-part, first note that a ∈ SN for all its reducts are computable and [[A]] ⊆ SN by (R1). Now, let f ∈ M(R), i ∈ Acc(f) and a such that a → * f a. If a = f a, then a i is computable by assumption. Otherwise, there is a ′ such that a → a ′ → * f a and, since a ′ is computable by assumption, a i is computable.

(undef) F -D(R) ⊆ CC f ( l) (subterm-acc) if g t ∈ CC f ( l), g ∈ M(R), g t : B ∈ B and i ∈ Acc(g), then t i ∈ CC f ( l)
We can then generalize the closure operations of Figure 5 for standard inductive systems to the closure operations of Figure 6 (we omit the proof).

In addition, we can also give a syntactic criterion for the condition [[B]] = SN used in (undef-basic) and (subterm-basic) (see Lemma 16 in [START_REF] Blanqui | Inductive-data-type systems[END_REF] and Lemma 49 in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]):

Definition 17 (Basic type). A type constant is basic if its equivalence class modulo ≃ B is basic. An equivalence class E is basic if for all B ∈ E, f ∈ M(R), f : T ⇒ B, i ∈ Acc(f), T i is a type constant C such that C ∈ E or else C < B B and [C] ≃B is basic.
In particular, all first-order data types (natural numbers, lists of natural numbers, trees, etc.) are basic.

Rewriting modulo an equational theory

Rewriting theory has been initially introduced as a decision tool for equational theories [START_REF] Knuth | Simple word problems in universal algebra[END_REF]. Indeed, an equational theory = E , i.e. the smallest congruence containing E, is decidable if there is a set R of rewrite rules such that → R terminates, is confluent, correct (R ⊆ = E ) and complete (E ⊆ = R ). Knuth and Bendix invented a completion procedure that, in case of success, builds such a set from E. This procedure consists in orienting the equations of E (and those generated in the course of the procedure) in order to use them as rewrite rules.

Yet, some equations or sets of equations, like commutativity, or associativity and commutativity together (associativity alone is orientable), are not orientable (no orientation leads to a terminating relation). A solution consists then in reasoning modulo these unorientable equations E and consider class rewriting modulo E, i.e. the relation 25

t = E → R u if there is t ′ such that t = E t ′ and t ′ → R u [LB77, Hue80].
Another solution, preferred in practice since it makes rewriting more tractable, consists in considering rewriting with matching modulo E, i.e. the relation t → R,E u if there are a position p ∈ Pos(t), a rule l → r ∈ R and a substitution σ such that t| p = E lσ and u = t[rσ] p [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF][START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]. Efficient implementations of rewriting with matching modulo some equational theories like associativity and commutativity have been developed [START_REF] Eker | Fast matching in combinations of regular equational theories[END_REF][START_REF] Kirchner | Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs[END_REF] that are for instance used to simulate and verify systems modeling chemical reactions or cryptographic protocols. 26However, we will only consider class rewriting in this paper. But, since rewriting with matching modulo is included in class rewriting, the termination of class rewriting implies the termination of rewriting with matching modulo. Moreover, many confluence results for rewriting with matching modulo relies on termination of class rewriting [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF].

We now show how the notions of computability and computability closure can be adapted to prove the termination of the relation → = → β ∪ = E → R for an important class of equational theories = E .

First note that, if there is a non-regular27 equation (e.g. x × 0 = 0), then the relation = E → R does not terminate. Indeed, if there are g

= d ∈ E, x ∈ FV(g) -FV(d) and l → r ∈ R, then d = d l x = E g l x → + R g r x = E d r x = d [JK86].
Similarly, if there is a regular non-linear28 collapsing29 equation (e.g. x ∧ x = x), then = E → R does not terminate either. Indeed, assume that t = x ∈ E and x freely occurs at two positions p and q in t, and let

t ′ = t[y] p where y / ∈ FV(t). If l → r ∈ R, then l = E t( l x ) = t ′ ( l x )( l y ) → R t ′ ( l x )( r y ) . . . [JK86]
. We will therefore restrict our attention to regular and non-collapsing equations, thus excluding regular, linear and collapsing equations like x + 0 = x, which are easily oriented though.

We now extend the notion of neutral term by taking equations into account:

Definition 18 (Neutral term modulo equations). Given a set R of rewrite rules of the form f l → r and a set E of equations of the form

f l = g m, a term is neutral if it is of the form x v, (λxt)u v or f v with f ∈ D(R ∪ E ∪ E -1 ) -M(R ∪ E ∪ E -1 ) 30 and | v| ≥ α f = sup{| l| | ∃r, f l → r ∈ R ∪ E ∪ E -1 }. An equation l = r is neutral if l is of the form f l,
r is of the form g m, and both l and r are neutral. A set of equations E is neutral if every equation of E is neutral.

Note that this definition generalizes Definition 16 for they are identical if E = ∅. Note also that, if

f ll = r ∈ E, then f l is not neutral.
Next, we need the set of neutral terms to be stable by = E . It is not sufficient to require that, for each equation l = r ∈ E, l is neutral iff r is neutral, as shown by the following counter-example: for each equation l = r ∈ E = {f = g, f x = h, g x y = k}, l is neutral iff r is neutral (f and g are not neutral, f x and h are neutral, and g x y and k are neutral), but f x = E g x, f x is neutral and g x is not neutral because α f = 1, α g = 2 and α h = α k = 0. However, it is sufficient to require E to be neutral:

Lemma 5 If E is neutral, then the set of neutral terms is stable by = E .

Proof. Note that = E is the reflexive and transitive closure of ↔ E = → E ∪ ← E (the symmetric closure of → E ). We can therefore proceed by induction on the number of ↔ E steps, and prove that the set of neutral terms is stable by ↔ E . So, let t be a neutral term and assume that t ↔ E t ′ . We check that t ′ is neutral:

• x v ↔ E t ′ . Since equations are of the form f l = g m, t ′ is of the form x v ′ with v(↔ E ) prod v ′ . • (λxt)u v ↔ E t ′ . Since equations are of the form f l = g m, t ′ is of the form (λxt ′ )u ′ v ′ with tu v(↔ E ) prod t ′ u ′ v ′ . • f v ↔ E t ′ with f ∈ D(R ∪ E ∪ E -1 ) and | v| ≥ α f . Either t ′ = f v ′ and v(↔ E ) prod v ′ , or there are w, f l = g m ∈ E and σ such that v = lσ w and t ′ = g mσ w. Since E is neutral, | l| ≥ α f and | m| ≥ α g . Thus, t ′ is neutral.
Finally, we need SN(→) and thus SN(→ β ) to be stable by = E . This can be achieved by requiring = E to commute with → β . Putting every thing together, we get: Definition 19 (Admissible theory). A set of equations E is admissible if E is made of regular, noncollapsing and neutral equations only, and = E commutes with → β .

In particular, = E commutes with → β if: Lemma 6 Given a set of equations E of the form f l = g m, = E commutes with → β if E satisfies all the following conditions:

• E is linear: ∀l = r ∈ E, l and r are linear;

• E is regular: ∀l = r ∈ E, FV(l) = FV(r);

• E is algebraic: ∀l = r ∈ E, l and r are algebraic 31 .

Proof. We proceed by induction on the number of ↔ E -steps and show that, if

t p ← E u q → β v, then t → β = E v. The case → E → β ⊆ → β = E is
similar for conditions on equations are symmetric.

• p#q. Then, t → β ← E v.

• p < q. Then, there are l → r and σ such that u| p = lσ and t = u[rσ] p . Since r is algebraic and linear, there is

x ∈ FV(l) such that v = u[lσ ′ ] p , xσ → β xσ ′
and, for all y = x, yσ ′ = yσ. Since r is regular and linear, t

→ β u[rσ ′ ] ← E v.
• p = q. Not possible for equations are of the form f l = g m.

• p > q. There are x, a, b such that u| q = (λxa)b and v = u[a b x ] q . Since equations are of the form f l = g m:

-Either there is a ′ such that a → E a ′ and t = u[(λxa ′ )b] q . Then, t → β u[a ′ b x ] q ← E v. -Or there is b ′ such that b → E b ′ and t = u[(λxa)b ′ ] q . Then, t → β u[a b ′ x ] q ← * E v.
The condition of algebraicity could be slightly relaxed. For instance, the commutation of quantifiers necessary for ensuring the confluence of the rewrite rules computing the prenex normal form of a formula [START_REF] Mayr | Higher-order rewrite systems and their confluence[END_REF] commutes with → β :

∀(λx∀(λyP xy)) = ∀(λy∀(λxP xy))
Now, we generalize the notion of computability to rewriting modulo some admissible theory: Definition 20 (Computability predicates for rewriting modulo equations). Given an admissible set of equations E and a type T , let Red T R/E be the set of all the sets P ⊆ L T such that:

(R1) P ⊆ SN(→) where → = → β ∪ = E → R ; (R2) P is stable by → ∪ = E ; (R3) if t : T is neutral and → (t) ⊆ P , then t ∈ P . Note that Red T R/∅ = Red T R .
We now check that the family (Red T R/E ) T ∈T has all the required properties:

Lemma 7 If E is an admissible set of equations and T ∈ T , then Red T R/E is stable by non-empty intersection and admits SN T as greatest element. Moreover, for all T, U ∈ T ,

P ∈ Red T R/E and Q ∈ Red U R/E , ∝ (P, Q) ∈ Red T ⇒U R/E .
31 They contain no subterm of the form λxt or xt.

Proof. The proof is similar to the one of Lemma 1. We only detail the cases that are different. We have SN T ∈ Red T R/E for = E commutes with → β and thus with →. For the stability by ∝, we only detail (R3). Let T, U ∈ T , P ∈ Red T R/E and Q ∈ Red U R/E , v : T ⇒ U neutral with → (v) ⊆ ∝ (P, Q), and t ∈ P . We prove that vt ∈ Q by well-founded induction on t ordered by → (t ∈ SN by (R1)). Since vt is neutral, by (R3), it suffices to prove that, for all w ′ such that vt → w ′ , we have w ′ ∈ Q.

We first prove (a): there are v ′ and t ′ such that w ′ = v ′ t ′ with either v → v ′ and t = E t ′ , or v = E v ′ and t → t ′ . We proceed by case on vt → w ′ :

• vt → β w ′ . Since v is neutral, it is not an abstraction and either w ′ = v ′ t with v → β v ′ , or w ′ = vt ′ with t → β t ′ . Hence, (a) is satisfied.

• vt = E w → R w ′ .
We prove (a) by induction on the number of ↔ E -steps. If vt = w, then we are done. Assume now that, vt

↔ E w = E → R w ′ .
The term w can neither be a variable nor an abstraction for equations are of the form f l = g m.

Assume that there are f l = g m ∈ E and σ such that w = f lσ and vt = g mσ. Since vt = g mσ, there are k and k such that m = kk and v = g kσ. But, then, v cannot be neutral for

| k| < | m| ≤ α g .
Therefore, there are a and b such that w = ab, t = E a and u = E b. Now, by the induction hypothesis, there are v ′ and t ′ such that

w ′ = v ′ t ′ with either a → R v ′ and b = E t ′ , or a = E v ′ and b → R t ′ . Hence, (a) holds. If v → v ′ and t = E t ′ , then w ′ = v ′ t ′ ∈ Q for v ′ ∈ ∝ (P, Q)
by assumption and t ′ ∈ P by (R2). Otherwise, v = E v ′ and t → t ′ . Then, t ′ ∈ P by (R2), and v ′ is neutral since neutral terms are stable by = E . Assume now that v ′ → v ′′ . Since E is admissible, = E commutes with → β and thus with →. Hence, there is e such that v → e = E v ′′ , and v ′′ ∈ ∝ (P, Q) for e ∈ ∝ (P, Q) by assumption and ∝ (P, Q) satisfies (R2). Therefore, → (v ′ ) ⊆ ∝ (P, Q) and, by the induction hypothesis on t ′ , w ′ = v ′ t ′ ∈ Q. (mod) if t ∈ CC f ( l) and t = E u, then u ∈ CC f ( l)

We now show how to extend Theorem 5.

Theorem 7 Given a set of rules R and an admissible set of equations E, the relation → = → β ∪ = E → R terminates on well-typed terms if there are I ∈ Π B∈B Red B R/E and a valid F -quasi-ordering ≥ containing (= E ) prod such that:

• every non-basic undefined symbol is computable;

• for every equation f l = g m ∈ E, m ∈ CC f ( l), l ∈ CC g ( m) and (f, l) ≃ (g, m); • for every rule f l → r ∈ R, r ∈ CC f ( l);
where CC is the smallest computability closure closed by the operations I to IV, and I'.

Proof. We proceed as for Theorem 5 and show that, for all (f, t) ∈ Σ max , every reduct t of f t is computable, by induction on > ∪ → prod . There are two cases:

1. t = f u with t (→ β ) prod u. By (R2), u is computable. Therefore, by the induction hypothesis, t is computable.

2. Otherwise, f t = E u → R t. We first prove by induction on the number of equational steps between f t and u, that u is of the form g u with u computable and (f, t) ≃ (g, u). If there is no equational step, this is immediate. So, assume that f t = E u ′ ↔ E u. By the induction hypothesis, u ′ is of the form g u with u computable and (f, t) ≃ (g, u). The conditions on rules being symmetric, the case of ← E is similar to the one of → E for which there are two cases:

(a) u = g v with u (→ E ) prod v. By (R2), v is computable and (g, u) ≃ (g, v) since ≃ contains (= E ) prod . Therefore, by transitivity, (f, t) ≃ (g, v). (b) There are g l = h m ∈ E, σ and w such that u = lσ w and u = h mσ w. By assumption, m ∈ CC g ( l)

and (g, l) ≃ (h, m). Since ≃ is stable by substitution, (g, lσ) ≃ (h, mσ). Since ≃ is compatible with application, (g, lσ w) ≃ (h, mσ w) and, by transitivity, (f, t) ≃ (h, mσ w). Now, since > is stable by substitution, CC is stable by substitution and mσ ∈ CC g ( lσ). Hence, by Lemma 3 and induction hypothesis, mσ is computable. Now, for t, there are two possibilities:

(a) t = g v with u (→ R ) prod v. By (R2), v is computable and, by the induction hypothesis, t is computable. (b) There are g l → r ∈ R, σ and w such that u = lσ w and t = rσ w. By assumption, r ∈ CC g ( l). Since CC is stable by substitution, we have rσ ∈ CC g ( lσ). Hence, by Lemma 3 and induction hypothesis, rσ is computable.

F -quasi-ordering compatible with permutative theories

We now define an F -quasi-ordering satisfying the previous conditions for a general class of equational theories including permutative 32 axioms like associativity and commutativity together [START_REF] Lankford | Decision procedures for simple equational theories with commutative-associative axioms: complete Technical Report ATP-039[END_REF]. It is based on the notion of alien subterm used when studying the preservation (modularity) of properties like confluence and termination of the disjoint union of two rewrite systems [START_REF] Gramlich | A structural analysis of modular termination of term rewriting systems[END_REF][START_REF] Gramlich | Generalized sufficient conditions for modular termination of rewriting[END_REF][START_REF] Fernández | Modular termination of term rewriting systems revisited[END_REF].

Definition 21 (Alien subterms). Let M = M(SN) be the set of finite multisets on SN. Given a set E ⊆ F , the E-alien subterms (E-aliens for short) of a multiset M ∈ M, Aliens E (M ), is the multiset of terms defined by induction on ⊲ M as follows:

• Aliens E (∅) = ∅;

• Aliens E (M + N ) = Aliens E (M ) + Aliens E (N );

• Aliens E ({|t|}) = Aliens E ({| t|}) if t = f t and f ∈ E, • Aliens E ({|t|}) = {|t|} otherwise. Given an equivalence ≃ F on F , a set of equations E is compatible with ≃ F -aliens if every equation of E is of the form f l = g m with f ≃ F g and Aliens [f]≃ F ( l) = Aliens [g]≃ F ( m).
Note that {|t|} M Aliens E (t). For instance, Aliens {+} ((x + y) + (z × (t + u))) = {|x, y, z × (t + u)|}. Note also that, for all F -quasi-orderings ≥, if E is compatible with ≃ F -aliens then, for all equations f l = g m ∈ E, (f, l) ≃ (g, m), as required in Theorem 7.

We now prove some properties of aliens:

Lemma 8 If θ is a substitution, then Aliens E (M θ) = ϕ θ E (Aliens E (M ))
, where ϕ θ E (M ) is defined by induction on ⊲ M as follows:

• ϕ θ E (∅) = ∅;
32 An equation l = r is permutative if every variable or function symbol has the same number of occurrences in l than it has in r. Such equations appear in algebra (permutative semi-groups), category theory (middle four exchange rule of Mac Lane), linear logic, the calculus of structures (medial rule) [START_REF] Straßburger | A characterisation of Medial as rewriting rule[END_REF], automated deduction, . . .

• ϕ θ E (M + N ) = ϕ θ E (M ) + ϕ θ E (N ); • ϕ θ E ({|x u|}) = Aliens E ({| t|}) + ϕ θ E (Aliens E ({| u|})) if x ∈ X , xθ = f t and f ∈ E; • ϕ θ E ({|a|}) = {|aθ|} otherwise.
Proof. By induction on M with ⊲ M as well-founded relation.

In the following, we assume given a quasi-ordering ≥ F on F , a set of equations E compatible with ≃ F -aliens, and an equivalence class E modulo ≃ F .

Lemma 9 If M (= E ) M N , then Aliens E (M ) (= E ) M Aliens E (N ).
Proof. We proceed by induction on M with ⊲ M as well-founded relation:

• M = N = ∅. Then, Aliens E (M ) = ∅ = Aliens E (N ). • M = P + {|a|}, N = Q + {|b|}, P (= E ) M Q and a = E b. By the induction hypothesis, Aliens E (P ) (= E ) M Aliens E (Q).
We now prove that Aliens E ({|a|}) (= E ) M Aliens E ({|b|}), by induction on the number of ↔ E steps. And since conditions on equations are symmetric, it sufficient to prove that, if a → E b, then Aliens E ({|a|}) (= E ) M Aliens E ({|b|}):

-a = x u. Since equations are of the form f l = g m, there is v such that b = x v. Therefore, Aliens E ({|a|}) = {|a|} (= E ) M {|b|} = Aliens E ({|b|}).
a = (λxs) u. Since equations are of the form f l = g m, there are t and v such that b = (λxt) v. Therefore,

Aliens E ({|a|}) = {|a|} (= E ) M {|b|} = Aliens E ({|b|}). -a = f u, b = f v and u (→ E ) prod v. * f ∈ E. By the induction hypothesis, Aliens E ({| u|}) (= E ) M Aliens E ({| v|}). Therefore, Aliens E ({|a|}) (= E ) M Aliens E ({|b|}). * f / ∈ E. Then, Aliens E ({|a|}) = {|a|} (= E ) M {|b|} = Aliens E ({|b|}).
-There are w, f l = g m ∈ E and σ such that a = f lσ w and b = g mσ w. Since E is compatible with

≃ F -aliens, f ≃ F g and Aliens E ( l) = Aliens E ( m). * f ∈ E. Then, [f] ≃F = E, Aliens E ({|a|}) = Aliens E ({| lσ|}) + Aliens E ( w) and Aliens E ({|b|}) = Aliens E ({| mσ|})+Aliens E ( w). By Lemma 8, Aliens E ({| lσ|}) = ϕ σ E (Aliens E ({| l|})) and Aliens E ({| mσ|}) = ϕ σ E (Aliens E ({| m|})). Therefore, Aliens E ({|a|}) = Aliens E ({|b|}). * f / ∈ E. Then, g / ∈ E and Aliens E ({|a|}) = {|a|} (= E ) M {|b|} = Aliens E ({|b|}). Lemma 10 If M (= E ) M N , then ϕ θ E (M ) (= E ) M ϕ θ E (N ).
Proof. We proceed by induction on M with ⊲ M as well-founded relation:

• M = N = ∅. Then, ϕ θ E (M ) = ∅ = ϕ θ E (N ). • M = P + {|a|}, N = Q + {|b|}, P (= E ) M Q and a = E b. By the induction hypothesis, ϕ θ E (P ) (= E ) M ϕ θ E (Q). We now prove that ϕ θ E (a) (= E ) M ϕ θ E (b):
-Assume that a = x u, xθ = f w and f ∈ E. Since equations are of the form f l = g m, there is v such that b = x v and u(= E ) prod v. Hence, {| u|} (= E ) M {| v|} and, by Lemma 9, Aliens E ({| u|})

(= E ) M Aliens E ({| v|}). By the induction hypothesis, ϕ θ E (Aliens E ({| u|})) (= E ) M ϕ θ E (Aliens E ({| v|})). Therefore, we have ϕ θ E (a) = Aliens E ({| w|}) + ϕ θ E (Aliens E ({| u|})) (= E ) M Aliens E ({| w|}) + ϕ θ E (Aliens E ({| v|})) = ϕ θ E (b). -Otherwise, ϕ θ E (a) = {|a|} (= E ) M {|b|} = ϕ θ E (b).
The ordering on terms that compares the alien subterms with (⊲ s ) M is not stable by substitution as shown by the following example: Aliens {f} ({|xy|}) = {|xy|} (⊲ s ) M {|y|} = Aliens {f} ({|y|}) and Aliens {f} ({|fy|}) = {|y|}. Therefore, we consider the following restriction of ⊲ s : Definition 22. Let ⊲ alg s be the smallest sub-ordering of ⊲ s such that, for all f : T ⇒ U , t : T and i ∈ [1, | t|], f t ⊲ alg s t i . Let alg s be its reflexive closure.

Lemma 11 Let ≥ F be a quasi-ordering on F and E a set of equations such that:

• E is admissible and compatible with ≃ F -aliens;

• in each equivalence class modulo = E , the size of terms is bounded.

Then, the DLQO ≥ associated to:

• the quasi-ordering ≃ F on F ;

• for each equivalence class E modulo ≃ F , the quasi-ordering

(= E alg s ) M ; • for each symbol f, the function ψ f ( t) = Aliens [f]≃ F ({| t|}) if f is maximally applied in f t; is a valid F -quasi-ordering containing (= E ) prod .
Proof. The relation = E ⊲ alg s is well-founded since ⊲ alg s commutes with = E (for = E is monotone) and, in each equivalence class modulo = E , the size of terms is bounded (see the proof of Proposition 15 in [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]).

Therefore, the strict part of

≥ = (= E alg s ) is > = (= E ⊲ alg s )
, which is well-founded, and its associated equivalence relation is = E .

Let > be the strict part of ≥ and ≃ be its associated equivalence relation.

• Compatibility of > with application. The relation > is compatible with application for it only compares pairs (f, t) such that f is maximally applied in f t.

• Compatibility of > with reduction. The relation ⊲ alg s commutes with → for → is monotone. The relation = E commutes with → β for E is admissible. The relation = E trivially commutes with = E → R . Therefore, > commutes with →. Since both > and → are well-founded on SN, > ∪ → is well-founded on SN. Hence, > ∪ → prod is well-founded on Σ max .

• Stability of ≃ by substitution. It follows from the lemmas 8, 9 and 10.

• Stability of > by substitution. Let E be an ≃ F -equivalence class, and assume that Aliens E ({| t|}) > M Aliens E ({| u|}). Then, there are M , P = ∅, N and Q such that Aliens E ({| t|}) = M + P , Aliens E ({| u|}) = N + Q, M (= E ) M N and, (*) for all q ∈ Q, there is p ∈ P such that p > q. Now, let θ be a substitution. By Lemma 8, Aliens

E ({| tθ|}) = ϕ θ E (M ) + ϕ θ E (P ) and Aliens E ({| uθ|}) = ϕ θ E (N ) + ϕ θ E (Q). By Lemma 10, ϕ θ E (M ) (= E ) M ϕ θ E (N ). We now prove that ϕ θ E (P ) > M ϕ θ E (Q).
To this end, it suffices to prove that, for all q ∈ Q, there is p ∈ P such that ϕ θ E ({|p|}) > M ϕ θ E ({|q|}), that is, Aliens E ({|pθ|}) > M Aliens E ({|qθ|}). So, let q ∈ Q. After (*), there is p ∈ P such that p > q. By definition of >, there are w and i ∈ [1, | w|] such that p = E k w and w i alg s q. Since equations are of the form f l = g m, there are h and v such that p = h v. Since p is an E-alien, h / ∈ E and Aliens E ({|pθ|}) = {|pθ|}. Since > is stable by substitution, pθ > qθ and thus {|pθ|} > M {|qθ|}. By definition of aliens, {|qθ|} (⊲ alg s ) M Aliens E ({|qθ|}). Therefore, by transitivity, Aliens E ({|pθ|}) > M Aliens E ({|qθ|}).

Note that the terms of an equivalence class modulo E are of bounded size if, for instance, the equivalence classes modulo E are of finite cardinality. This is in particular the case of associativity and commutativity together.

Example of termination proof

As an example, we check that the conditions of Theorem 7 are satisfied by the set R of rules defining the addition on Peano integers given at the beginning of Section 4.5, and the following set E of equations (associativity and commutativity):

(x + y) + z = x + (y + z)
x + y = y + x by taking the identity relation for ≃ F and the F -quasi-ordering ≥ of Lemma 11. The set of equations E is neutral. By Lemma 6, = E commutes with → β since E is linear, regular and algebraic. Therefore, E is admissible.

The set of equations E is compatible with ≃ F -aliens since, for the associativity equation, we have + ≃ F + and Aliens {+} ({|x + y, z|}) = {|x, y, z|} = Aliens {+} ({|x, y + z|}), and for the commutativity equation, we have + ≃ F + and Aliens {+} ({|x, y|}) = {|x, y|} = Aliens {+} ({|y, x|}).

Hence, by Lemma 11, ≥ is a valid F -quasi-ordering containing (= E ) prod for, in each equivalence class modulo = E , the size of terms is bounded.

We now check the conditions on rules and equations: 33

• For the first rule defining addition, we have x ∈ CC + (0, x) by (arg).

• For the second rule defining addition, we have x + y ∈ CC + (x, suc y) by (rec) since Aliens {+} (x, suc y) = {|x, suc y|} > M Aliens {+} (x, y) = {|x, y|}, and thus suc (x + y) ∈ CC + (x, suc y) by (undef) and (app).

• For the commutativity equation, we have {y, x} ⊆ CC + (x, y) and {x, y} ⊆ CC + (y, x) by (arg).

• Finally, for the associativity equation, we have x ∈ CC + (x + y, z) by (arg) and (subterm-acc), and y + z ∈ CC + (x + y, z) by (rec) since Aliens {+} (x + y, z) = {|x, y, z|} > M {|y, z|} = Aliens {+} (y, z). Similarly, we have x + y ∈ CC + (x, y + z) and z ∈ CC + (x, y + z).

Rewriting with matching modulo βη

In this section, we extend the results of Section 4 to rewriting with matching modulo βη. Consider the following rewrite rule used for defining a formal derivation operator:

sin, cos : R ⇒ R; × : R ⇒ R ⇒ R; D : (R ⇒ R) ⇒ (R ⇒ R) D (λx sin (F x)) → λx (D F x) × (cos (F x))
Using matching modulo α-equivalence only, this rule can be applied neither to D(sin) nor to D(λx sin x). But it can be applied to D(λx sin x) if we use matching modulo β-equivalence, since x ← β (λxx)x, 34 and to D(sin) if we use matching modulo βη-equivalence, since sin ← η λx sin x.

Although matching modulo βη is decidable [START_REF] Stirling | Decidability of higher-order matching[END_REF], it is of non-elementary complexity [START_REF] Statman | The typed λ-calculus is not elementary recursive[END_REF] (while unification modulo βη [START_REF] Huet | Résolution d'équations dans les langages d[END_REF] and matching modulo β are both undecidable [START_REF] Loader | Higher-order β-matching is undecidable[END_REF]). There is however an important fragment for which the complexity is linear: the class of β-normal η-long terms in which every free variable is applied to distinct bound variables, introduced by Miller for λProlog [START_REF] Miller | A logic programming language with lambda-abstraction, function variables, and simple unification[END_REF][START_REF] Qian | Linear unification of higher-order patterns[END_REF]. For instance, λx sin(F x), λxλyF yx and λxx(F x) are patterns (if they are in η-long form), while F x and λxF xx are not patterns. However, in this paper, we will consider a slightly different class of terms: Definition 23 (Patterns). A term t is a pattern if t ∈ P FV(t) where P V is defined as follows:

33 As already remarked, the condition (f, l) ≃ (g, m) for every equation f l = g m follows from compatibility with ≃ F -aliens. 34 In contrast with a common practice (Barendregt's variable convention [START_REF] Barendregt | Lambda calculi with types[END_REF]), we often use the same variable name for both a bound and a free variable. Although it may be confusing at first sight, it has the advantage of avoiding some variable renamings.

• if t ∈ P V , then λxt ∈ P V -{x} ;

• if f ∈ F , f : T ⇒ U , t : T and t ∈ P V , then f t ∈ P V ;

• if x ∈ V , x : T ⇒ U , t : T and t η-reduces to pairwise distinct variables not in V , then x t ∈ P V .

Our definition excludes Miller patterns where a bound variable is applied to a free variable like λxx(F x), which is not very common in practice. On the other hand, our patterns do not need to be in η-long form.

To apply the computability closure technique to rewriting with matching modulo βη, we need to prove that, if f t = βη f lσ → R rσ and t are computable, then lσ is computable, so that rσ is computable if r ∈ CC f ( l). By confluence of → βη [START_REF] Pottinger | Proofs of the normalization and Church-Rosser theorems for the typed λ-calculus[END_REF] and η-postponement

(→ * βη ⊆ → * β → * η ) [CF58, Tak95], for each i ∈ [1, | l|], there is u i such that t i → * β u i = η ← * β l i σ.
By (R2), u i is computable. Therefore, we are left to prove that, if u i is computable and u i = η ← * β l i σ, then l i σ is computable. While computability is preserved by η-equivalence (see Lemma 20 below), it cannot be the case for arbitrary β-expansions because β-expansion may introduce non-terminating subterms.

In [START_REF] Miller | A logic programming language with lambda-abstraction, function variables, and simple unification[END_REF], Section 9.1, Miller remarks that, if t = βη lσ, l is a pattern à la Miller, t and σ are in β-normal η-long form, then t = β0η lσ, where → β0 is the restriction of → β to redexes of the form (λxt)x (or, by α-equivalence, of the form (λxt)y with y ∈ X and τ (x) = τ (y)). So, when the left-hand sides of rules are patterns, matching modulo βη reduces to matching modulo β 0 η. We now check that → β0η terminates and is strongly confluent:

Lemma 12 → η terminates and is strongly confluent.

Proof. The relation → η terminates for it makes the size of terms decrease. Assume that t p ← η u q → η v.

• p#q. Then, t → η ← η v.

• p = q. Then, t = v.

• p > q. Then, there are a and a ′ such that u| q = λxax, x / ∈ FV(a), v = u[a] q , a → η a ′ and t = u[λxa ′ x] q . Since FV(a ′ ) ⊆ FV(a), x / ∈ FV(a ′ ) and t → η u[a ′ ] q ← η v.

• p < q. By symmetry, t → η ← η v.

Lemma 13 → β0η terminates and is strongly confluent on well-typed terms.

Proof. The relation → β0η terminates on well-typed terms for it is a sub-relation of → βη which terminates on well-typed terms [START_REF] Pottinger | Proofs of the normalization and Church-Rosser theorems for the typed λ-calculus[END_REF]. Assume that t

p ← β0η u q → β0η v. If p#q, then t → β0η u ← β0η v. • t p ← η u q → η v. Then, t = v or t → η ← η v by Lemma 12. • t p ← η u q → β0 v.
p = q. Not possible.

p > q. There is a such that u| q = (λxa)x and v = u[a] q . * p = q0. There is d such that a = dx, x / ∈ FV(d) and t = u[dx] q . Thus, t = v. * p > q0. There is a ′ such that a → η a ′ and t = u[(λxa ′ )x] q . Thus, t → β0 u[a ′ ] q ← η v. * p > q1. Not possible.

p < q. There is a such that u| p = λxax, x / ∈ FV(a) and t = u[a] p . * p0 = q. 35 There is b such that a = λyb and v = u[a x y ] p . Since u is well-typed, τ (x) = τ (y) and, by α-equivalence, we can assume wlog that y = x. Thus, t = v. * p0 < q. There is a ′ such that a → β0 a ′ and v = u[λxa ′ x] p . Thus, t → β0 u[a ′ ] p ← η v.

• t p ← β0 u q → β0 v.
p = q. Then, v = t.

p < q. There are a and a ′ such that u| p = (λxa)x, t = u[a] p , a → β0 a ′ and v = u[(λxa ′ )x] p . Thus, t → β0 u[a ′ ] p ← β0 v.

p > q. By symmetry, t → β0 ← β0 v.

Hence, if t = β0η lσ, then t → * β0η ← * β0η lσ36 . Therefore, we could try to prove that computability is preserved by β 0 -expansion, all the more so since that, for matching modulo α-equivalence, computability is preserved by head-β 0 -expansion as shown by Lemma 2 (a result that also holds with pattern matching modulo βη under some conditions on R as we will see it in Lemma 17 below). But this does not seem easy to prove in general for two reasons.

First, a proof that u is computable whenever t ← β0 u and t is computable, by induction on the size of t does not seem to go through. Indeed, assume that u = λxs. Then, t = λxr and r ← β0 s. But λxs is computable if, for all e ∈ [[τ (x)]], s e

x is computable. Of course, r e x is computable but we generally do not have r e x ← β0 s e x . We therefore need to consider not β 0 -expansion but a restricted form of β-expansion that is stable by instantiation of the bound variables of a pattern:

Definition 24 (Leaf-β-expansion). The set LPos(t) of the (disjoint) leaf positions of a term t is defined as follows:

• LPos(t) = {0 n-1 1p|p ∈ LPos(t 1 )} ∪ . . . ∪ {1p|p ∈ LPos(t n )} if t = f t 1 . . . t n and f ∈ F ; • LPos(t) = {0p|p ∈ LPos(u)} if t = λxu; • LPos(t) = {ε} otherwise.
Given a term v and a leaf position p ∈ LPos(v), let the relation of β-leaf-expansion wrt v at position p be the relation t ← β,v,p u if there are t, a, x, e, b such that t = v[ t] q [a e

x b] p and u = v[ t] q [(λxa)e b] p , where q are all the leaf positions of v distinct from p.

Second, since we do not consider rewriting on terms in β-normal form, lσ can contain some arbitrary β-redex (λxa)b which, after some β 0 η-reductions, becomes a β 0 -redex because b → * β0η x. However, if l is a pattern then such a β-redex can only occur in σ. Therefore, it is not needed to reduce it for checking that t matches l modulo βη. For the sake of simplicity, we will enforce this property in the definition of rewriting itself by using the notion of valuation used for defining rewriting in CRSs37 [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]:

Definition 25 (Valuation). A substitution σ is valid wrt a term t if, for all p ∈ LPos(t), x and t 1 , . . . , t n such that t| p = xt 1 . . . t n , there are pairwise distinct variables y 1 , . . . , y n and a term a such that xσ = λy 1 . . . λy n a. Let the valuation of a term t by a substitution σ, written σ(t), be the term:

• λxσ(u) if t = λxu and σ is away from {x};

• f σ(t 1 ) . . . σ(t n ) if t = f t 1 . . . t n ;
• a{y 1 → t 1 , . . . , y n → t n } if t = xt 1 . . . t n , xσ = λy 1 . . . λy n a and y 1 , . . . , y n are pairwise distinct variables.

Lemma 14 If l is a pattern and p 1 , . . . , p n are the leaf positions of l then, for all substitutions σ valid wrt l, we have σ(l) ← * β,l,p1 . . . ← * β,l,pn lσ.

Proof. Let p be a leaf position of l. By definition of patterns, there are terms t and pairwise distinct variables x, y such that l| p = x t, x ∈ FV(l) and t → * η y. Since σ is valid wrt l, there is a such that xσ = λ ya and σ(l)| p = a{y 1 → t 1 , . . . , y n → t n } ← * β,l,p (λ ya) t = lσ| p .

Hence, valuation preserves typing: τ ( σ(t)) = τ (t). We now introduce our definition of rewriting with matching modulo βη:

Definition 26 (Rewriting with pattern matching modulo βη). Given a set R of rewrite rules of the form f l → r with f l a pattern, let t → R,βη u if there are p ∈ Pos(t), l → r ∈ R and σ such that τ (t| p ) = τ (l), σ is valid wrt l, t| p = η σ(l) and u = t[rσ] p .

Lemma 15 The relation → R,βη is monotone and stable by substitution.

Proof. Monotony is straightforward. We check that it is stable by substitution. Assume that t → R,βη u and let θ be a substitution. There are p ∈ Pos(t), l → r ∈ R and σ such that τ (t| p ) = τ (l), σ is valid wrt l, t| p = η σ(l) and u = t[rσ] p . We have τ (tθ| p ) = τ (t| p ) = τ (l), σθ valid wrt l and tθ| p = η σ(l)θ. We now prove σ(l)θ = η σθ(l). Let q ∈ LPos(l). Since l is a pattern, l| q = x t where x and t ↓ η are pairwise distinct variables and { t ↓ η } ⊆ BV(l, q). Since σ is valid wrt l, there is a such that xσ = λ ya and σ(l| q ) = η a. Wlog we can assume that θ is away from { y}. Therefore, xσθ = λ yaθ and σ(l| q )θ = η aθ = η σθ(l| q ). Therefore, tθ → R,βη uθ.

Definition of computability

Computability is straightforwardly extended to this new form of rewriting as follows:

Definition 27 (Computability predicates for rewriting with matching modulo βη). Given a set R of rewrite rules of the form f l → r with f l a pattern, a term is neutral if it is of the form x v, (λxt)u v or f v with f ∈ D(R) -M(R) 38 and | v| ≥ α f = sup{| l| | ∃r, f l → r ∈ R}. Given a type T , let Red T R,βη be the set of all the sets P ⊆ L T such that: (R1) P ⊆ SN(→) where → = → β ∪ → R,βη ; (R2) P is stable by →; (R3) if t : T is neutral and → (t) ⊆ P , then t ∈ P .

Lemma 16 For all type T , Red T R,βη is stable by non-empty intersection and admits SN T as greatest element. Moreover, for all T, U ∈ T , P ∈ Red T R,βη and

Q ∈ Red U R,βη , ∝ (P, Q) ∈ Red T ⇒U R,βη .
Proof. The proof is similar to the one of Lemma 1. One can easily check the stability by non-empty intersection and the fact that SN T ∈ Red T R,βη . For the stability by ∝, there is no change for (R1) and (R2). We now detail (R3). Let T, U ∈ T , P ∈ Red T R,βη , Q ∈ Red U R,βη , v : T ⇒ U neutral such that → (v) ⊆ ∝ (P, Q) and t ∈ P . We now show that vt ∈ Q by well-founded induction on t with → as wellfounded relation (t ∈ SN by (R1)). Since vt is neutral, by (R3), it suffices to prove that every reduct w of vt is in Q:

• w = v ′ t with v → v ′ .
By assumption, v ′ ∈ ∝ (P, Q). Therefore, w ∈ Q.

• w = vt ′ with t → t ′ . By the induction hypothesis, w ∈ Q.

• There are f l → r ∈ R and σ such that vt = η σ(f l) = f σ( l) and w = rσ. By confluence of → η , (vt)↓ η is of the form f m with | m| = | l|. Since v is neutral, v is of the form x t, (λxa)b t or g m with α g ≤ | m|. We discuss these cases in turn:

v = x t. Then, v↓ η is of the form x u. So, this case is not possible.

v = (λxa)b t. Then, a = η cx with x / ∈ FV(c) and cb tu = η σ(f l). Hence, v

→ β v ′ = a b x t, v ′ t = η (cx) b x tu = cb tu = η σ(f l) and v ′ t → w. Therefore, w ∈ Q since v ′ ∈ ∝ (P, Q), t ∈ P and Q satisfies (R2). -v = g m with α g ≤ | m|. Then, g = f and | m| < | mu| = | l|. Since v is neutral, α f ≤ | m|. By definition of α f , | l| ≤ α f .
So, this case is not possible.

We now check that Lemma 2 still holds if the following condition is satisfied: Definition 28. A set R of rules is β-complete if, for all rules l → r ∈ R and types T, U such that l : T ⇒ U , there is x ∈ X -FV(l) such that τ (x) = T and:

• lx → s x y ∈ R if r = λys; 39 • lx → rx ∈ R otherwise.
For instance, R is β-complete if, for every rule l → r ∈ R, l is of base type. On the other hand, the set R = {f → λxx} is not β-complete since fx → x / ∈ R.

Lemma 17 Assume that R is β-complete. Given T ∈ T and P ∈ Red T R,βη , (λxt)u v ∈ P iff (λxt)u v : T , t u x v ∈ P and u ∈ SN.

Proof. Assume that (λxt)u v ∈ P . By (R2), t u

x v ∈ P . By (R1), (λxt)u v ∈ SN. Therefore, u ∈ SN. Assume now that t u x v ∈ P and u ∈ SN. By (R1), t u x v ∈ SN. Therefore, v ∈ SN, t u x ∈ SN and t ∈ SN. We now prove that, for all t, u, v ∈ SN, (λxt)u v ∈ P , by induction on → prod . Since (λxt)u v is neutral, by (R3), it suffices to prove that every reduct w of (λxt)u v belongs to P . Since rules are of the form f l → r, there are three possible cases:

• w = t u x v.
Then, w ∈ P by assumption.

• w = (λxt ′ )u ′ v ′ and tu v → prod t ′ u ′ v ′ . Then, w ∈ P by the induction hypothesis.

• There are f l → r ∈ R and σ such that λxt = η σ(f l) and w = rσu v. By confluence of → η , there is a such that t → * η ax, x / ∈ FV(a) and a = η σ(f l). Wlog we can assume that x / ∈ FV(l) and σ is away from {x}. Hence, t = η σ(f lx). Since R is β-complete, there are two cases:

r = λys and f lx → s x y ∈ R. Then, t → R,βη s x y σ. By monotony and stability by substitution, t u x v → R,βη (s x y σ) u x v. Hence, (s x y σ) u x v ∈ P by (R2). Therefore, by the induction hypothesis, (λxs x y σ)u v ∈ P . Wlog we can assume that σ is away from {y}. Hence, (λxs x y σ)u v = α rσu v. -r is not an abstraction and f lx → rx ∈ R. Then, t → R,βη (rx)σ = rσx. By monotony and stability by substitution, t u x v → R,βη rσu v. Hence, rσu v ∈ P by (R2).

Corollary 4 Assume that R is β-complete. Given T, U ∈ T , P ∈ Red T R,βη and Q ∈ Red U R,βη , λxt ∈ ∝ (Q, P ) iff λxt : U ⇒ T and, for all u ∈ Q, t u x ∈ P .
Proof. Assume that λxt ∈∝ (Q, P ) and u ∈ Q. Then, by definition of ∝, (λxt)u ∈ P . Therefore, by (R2), t u x ∈ P . Assume now that, for all u ∈ P , t u x ∈ P . By definition of ∝, λxt ∈∝ (Q, P ) if, for all u ∈ Q, (λxt)u ∈ P . By (R1), u ∈ SN. Therefore, by Lemma 17, (λxt)u ∈ P .

But β-completeness is not a real restriction from the point of view of termination since: 40 We now prove that there is t ′ such that t → + β t ′ → * η v, so that we can conclude by the induction hypothesis:

• t p → η u q → β v.
p#q. In this case, t → β → η v.

p ≤ q. There are a and a ′ such that t| p = λxax, x / ∈ FV(a),

u = t[a] p , a → β a ′ and v = t[a ′ ] p . Thus, t → β t[λxa ′ x] p → η v.
p > q. There are a and b such that u| q = (λxa)b and v

= u[a b x ] q . * p ≥ q1. There is d such that t = u[(λxa)d] q and d → η b. Thus, t → β u[a d x ] → * η v. * p = q0. Then, t = u[(λx(λxa)x)b] q . Thus, t → β0 u → β v. * p > q0. There is d such that t = u[(λxd)b] q and d → η a. Thus, t → β u[d b x ] → η v. • t p → η u q → R,βη v.
We now prove that there is t ′ such that t → R,βη t ′ → = η v, so that we can conclude by the induction hypothesis.

p#q. Then, t → R,βη t ′ → η v.

p ≥ q. Then, t → R,βη v.

p < q. There are a and a ′ such that t|

p = λxax, x / ∈ FV(a), u = t[a] p , a → R,βη a ′ and v = ′ ] p . Thus, t → R,βη t[λxa ′ x] p → η v. • t p ← η u q → R,βη v.
By assumption, there is t ′ such that t → t ′ = η v, so that we can conclude by the induction hypothesis.

• t p ← η u q → β v. We now prove that, either v = t and v is computable for t is computable, or there is t ′ such that t → β t ′ ← * η v and we can conclude by the induction hypothesis:

p#q. Then, t → β t ′ ← η v.

p = q. Not possible.

p > q. There are a and b such that u| q = (λxa)b and v = u[a b x ] q . * p = q0. There is d such that a = dx, x / ∈ FV(d) and t = u[db] q . Thus, t = v. * p > q0. There is a ′ such that a → η a ′ and t = u[(λxa

′ )b] q . Thus, t → β u[a ′ b x ] q ← η v. * p ≥ q1. There is b ′ such that b → η b ′ and t = u[(λxa)b ′ ] q . Thus, t → β u[a b ′ x ] q ← * η v. -p < q.
There is a such that u| p = λxax, x / ∈ FV(a) and t = u[a] p . * p0 = q. There is b such that a = λyb and v = u[λxb x y ] p . As already mentioned in Lemma 13, since u is well-typed, we can assume wlog that y = x. Thus, t = v. * p0 < q. There is a

′ such that a → β a ′ and v = u[λxa ′ x] p . Thus, t → β u[a ′ ] p ← η v.
In the previous proof, we have seen that

→ η → R,βη ⊆ → R,βη → = η . Hence, if we also have ← η → R,βη ⊆ → R,βη = η , then ↔ η → R,βη ⊆ → +
R,βη = η , a property that, after [JM84], we call:

Definition 29. A relation R locally η-commutes if ↔ η R ⊆ R + = η .
We now provide sufficient conditions for this property to hold: Definition 30. A set R of rules is η-complete if, for all l, k, r, x such that lk → r ∈ R, k → * η x and x ∈ X -FV(l), we have:

• l → s ∈ R if r = sk ′ , k ′ → * η x and x / ∈ FV(s); 41 • l → λxr ∈ R otherwise. Lemma 21 If R is η-complete, then ← η → R,βη ⊆ → R,βη = η and → R,βη locally η-commutes. Proof. Assume that t p ← η u q → R,βη v.
• p#q. Then, t → R,βη ← η v.

• p ≥ q. Then, t → R,βη v.

• p < q. There is a such that u| p = λxax, x / ∈ FV(a) and t = u[a] p .

-p01 ≤ q. Not possible since the rules are of the form f l → r.

-p00 ≤ q. There is

a ′ such that v = u[λxa ′ x] p and a → R,βη a ′ . Then, t → R,βη u[a ′ ] p ← η v.
-p0 = q. There are f l → r ∈ R and σ such that ax = η σ(f l) and v = u[λxrσ] p . By confluence of → η , there are m and k such that l = mk, a = η σ(f m) and x = η σ(k). Since k is a pattern, there is y ∈ X such that k → * η y and yσ → * η x. Wlog we can assume that y = x. Let θ be the restriction of σ on FV(f m). Since x / ∈ FV(a) and the set of free variables of a term is invariant by = η , we have x / ∈ FV( m) and θ away from {x}. Now, since R is η-complete, there are two cases:

* r = sk ′ , k ′ → * η x, x / ∈ FV(s) and f m → s ∈ R. Then, a → R,βη sθ and FV(sθ) ⊆ FV(a). Since x / ∈ FV(a), x / ∈ FV(sθ) and sθ ← η λxsθx. Since x ← * η xσ and x ← * η k ′ , we have x ← * η k ′ σ. Therefore, t → R,βη ← * η u[λxsθk ′ σ] = v. * Otherwise, f m → λxr ∈ R. Hence, a → R,βη (λxr)θ. Since θ is away from {x}, (λxr)θ = λxrθ. Since x = xθ ← * η xσ, rθ ← * η rσ. Therefore, t → R,βη ← * η v.
For instance, R = {fx → x} is not η-complete since f → λxx / ∈ R and, indeed, the relation ← η does not commute with → R,βη because of the non-joinable critical pair f ← η λxfx → R λxx. Adding the rule f → λxx allows us to recover commutation.

But η-completeness is not a real restriction from the point of view of termination since:

Lemma 22 For every (finite) set of rules S, there is an η-complete (finite) set of rules R ⊇ S such that, using the rules of Figure 8,

f l → r ∈ CC f ( l) for every f l → r ∈ R if f l → r ∈ CC f ( l) for every f l → r ∈ S.
Proof. Let F η be the function on the powerset of T 2 such that, for all R ⊆ T 2 , F η (R) is the smallest set such that R ⊆ F η (R) and, for all l, k, r, x such that lk

→ r ∈ R, k → * η x and x ∈ X -FV(l), l → s ∈ F η (R) if r = sk ′ , k ′ → * η x and x / ∈ FV(s), and l → λxr ∈ F η (R) otherwise. Since F η is extensive (i.e. R ⊆ F η (R)), by Hessenberg's fixpoint theorem [Hes09], F η has a fixpoint R such that S ⊆ R. Since R = F η (R), R is η-complete. If S = {l 1 → r 1 , . . . , l n → r n } and, for every i ∈ [1, n], l i : T i ⇒ A i with A i ∈ B, then card(R) ≤ n + Σ n i=1 | T i |. Assume now that f l → r ∈ CC f ( l)
for every f l → r ∈ S, and that there are f lk → r ∈ R and x ∈ X -FV( l) such that k → * η x. By assumption, r ∈ CC f ( lk). By (var), x ∈ CC f ( l). Therefore, by (eta), k ∈ CC f ( l). Now, since x ∈ X -FV( l), we can get r ∈ CC f ( l) by replacing, everywhere in the derivation proof of r ∈ CC f ( lk), CC f ( lk) by CC f ( l), and the proofs of k ∈ CC f ( lk) obtained with (arg), by the proof of k ∈ CC f ( l) obtained with (var) and (eta). Therefore, by (abs), λxr ∈ CC f ( l). Now, if r = sk ′ with k ′ → * η x and x / ∈ FV(s), then s ∈ CC f ( l) by (eta).

-

τ (l) = V ⇒ W . By definition of computability, u ∈ S if, for all v ∈ [[V ]], uv ∈ [[W ]]. So, let v ∈ [[V ]].
Then, tv ∈ [[W ]] and tv ← β,lx,0p uv. Moreover, uv is valid wrt (lx, 0p) and ||lx|| = ||l||. Therefore, by the induction hypothesis (2), uv ∈

[[W ]].
τ (l) ∈ B. Since t ← β,l,p u, there are i, q, t, u such that p = 0 | l|-i 1q, t = f t, u = f u and t i ← β,li,q u i , that is, there are a, x, e, b such that t i | q = a e x b and u i | q = (λxa)e b. By Lemma 4, u ∈ S if all its reducts are in S and, if f ∈ M(R) and i ∈ Acc(f), then

u i ∈ [[T i ]]. Assume that f ∈ M(R) and i ∈ Acc(f). By Lemma 4, t i ∈ [[T i ]]. If t i = u i then u i ∈ [[T i ]]
. Otherwise, t i ← β,li,q u i . Therefore, since u i is valid wrt (l i , q), by the induction hypothesis (1), u i ∈ [[T i ]]. We now prove that, if u q → v, then v ∈ S: * p#q. Then, t → t ′ ← β,l,p v. By (R2), t ′ ∈ S. Since t ′ is valid wrt (l, p), by the induction hypothesis (3), v ∈ S. * p > q. Not possible since l contains undefined symbols only. * There are f l → r ∈ R and θ such that τ (λxa) = τ (f l), λxa = η θ(f l) and v = rθe b. Wlog we can assume that x / ∈ FV(f l) and θ is away from {x}. Then, as already seen in the proof of Lemma 17, a = η θ(f lx). Since R is β-complete, there are two cases:

• There is s such that r = λxs. Then, f lx → s ∈ R and a → R,βη sθ. Hence, t → t ′ = u[(sθ) e

x b] p ← β,l,p u[(λxsθ)e b] p = v. By (R2), t ′ ∈ S. Since v is valid wrt (l, p), by the induction hypothesis (3), v ∈ S. Finally, we check that β and η-completion commute when left and right-hand sides are βη-normal. Hence, any (finite) set of rules S whose left-hand and right-hand sides are βη-normal can be completed into a (finite) β and η-complete set of rules R ⊇ S.

• Otherwise, f lx → rx ∈ R and a → R,βη rθx. Hence, t → t ′ = u[(rθx) e x b] p ← β,l,p u ′ = u[(λxrθx)e b] p → η v. By (R2), t ′ ∈ S. Since u ′ is valid wrt (l, p), by the induction hypothesis (3), u ′ ∈ S. Therefore, by Lemma 20, v ∈ S. * There is a ′ such that a → a ′ and v = u[(λxa ′ )e b] p . Then, t → t ′ = u[a ′ e x b] p ← β,l,p v. By (R2), t ′ ∈ S. Since v is valid wrt (l, p), by the induction hypothesis (3), v ∈ S. * There is e ′ such that e → e ′ and v = u[(λxa)e ′ b] p . Then, t → * t ′ = u[a e ′ x b] p ← β,l,p v.
Lemma 24 β-completion (resp. η-completion) preserves η-completeness (resp. β-completeness when lefthand and right-hand sides are βη-normal).

Proof. • We will say that R is βη-normal if, for every rule l → r ∈ R, both l and r are βη-normal.

We first prove that the function F η defined in the proof of Lemma 22 preserves β-completeness and βηnormality. Let R be a βη-normal and β-complete set of rules. We have to prove that F η (R) is βη-normal and β-complete, that is, if there are l → r ∈ F η (R) and T, U ∈ T such that l : T ⇒ U , then there is x ∈ X -FV(l) such that τ (x) = T and, either r = λys and lx → s

x y ∈ F η (R), or lx → rx ∈ F η (R). Let l → r ∈ F η (R) -R and assume that there is gk → d ∈ R such that k → * η x ∈ X -FV(g).
Then, either:

-d = sk ′ , k ′ → * η x ∈ X -FV(s) and l → r = g → s. Since R is βη-normal, k = k ′ =
x and r is not an abstraction. Therefore, lx → rx ∈ F η (R) since lx = gk, rx = sk ′ = d and gk → d ∈ R. Moreover, l is βη-normal since l = g and gk is βη-normal, and r is βη-normal since r = s and d = sk ′ is βη-normal.

l → r = g → λxd. Since R is βη-normal, k = x. Therefore, lx → d ∈ F η (R) since lx = gk and gk → d ∈ R. Moreover, l is βη-normal since l = g and g is βη-normal, and r is βη-normal since r = λxd, d is βη-normal and d is not of the form sk ′ with k ′ → * η x ∈ X -FV(s).

• We now prove that the function F β defined in the proof of Lemma 18 preserves η-completeness. Let R be an η-complete set of rules. We have to prove that F

β (R) is η-complete, that is, if lk → r ∈ F β (R) and k → * η x ∈ X -FV(l) then, either r = tk ′ , k ′ → * η x ∈ X -FV(t) and l → t ∈ F β (R), or l → λxr ∈ F β (R). Let l → r ∈ F β (R) -R
and assume that there are g → d ∈ R and T, U ∈ T such that g : T ⇒ U . Then, there is x ∈ X -FV(g) such that x : T and either:

d = λys and lk → r = gx → s x y . Wlog we can assume that y = x. If r = tk ′ and k ′ → * η x ∈ X -FV(t), then d is not βη-normal. Therefore, l → λxr ∈ F β (R) since l = g, r = s and g → λxs ∈ R.

lk → r = gx → dx. Therefore, l → d ∈ F β (R) since l = g and g → d ∈ R.

Handling the subterms of a pattern

We now show that Theorem 5 extends to rewriting with pattern matching modulo βη: (subterm-abs) if λxt ∈ CC f ( l) and x ∈ X -FV( l), then t ∈ CC f ( l) (subterm-app) if tx ∈ CC f ( l) and x ∈ X -(FV(t) ∪ FV( l)), then t ∈ CC f ( l) (eta) if t ∈ CC f ( l), t = η u and τ (t) = τ (u), then u ∈ CC f ( l)

Theorem 8 Given a set of rules R that is both β and η-complete, the relation → β ∪ → R,βη terminates on well-typed terms if there is an F -quasi-ordering ≥ valid wrt the interpretation of Section 4.7 such that, for every rule f l → r ∈ R, l are patterns containing undefined symbols only and r ∈ CC f ( l), where CC is the smallest computability closure closed by the operations I to VI.

Proof. We proceed as for Theorem 5 by showing that, for all (f, t) ∈ Σ max , every reduct t of f t is computable, by well-founded induction on > ∪ → prod . There are two cases:

• There is u such that t = f u and t → prod u. By (R2), u is computable. Therefore, by the induction hypothesis, f u is computable.

• There are s, w, f l → r ∈ R and σ such that t = s w, s = η σ( l) and t = rσ w. By Lemma 20, σ( l) are computable. Let now i ∈ [1, | l|] and p 1 , . . . , p n be the leaf positions of l i By Lemma 14, we have σ(l i ) ← * β,l,p1 . . . ← * β,l,pn l i σ. Since all the terms between σ(l i ) and l i σ are valid, by Lemma 23, l i σ is computable. Since r ∈ CC f ( l) and CC is stable by substitution (for > is stable by substitution), we have rσ ∈ CC f ( lσ). Now, Lemma 3 is easily extended with the rules of Figure 8 for destructuring patterns [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF]. Therefore, rσ is computable since, for all (g, u) ∈ Σ max , if (f, t) > (g, u), then g u is computable by the induction hypothesis.

For instance, let us check that these conditions are satisfied by the formal derivation rule given at the beginning of the section. Let l = λx sin(F x) and assume that D > F ×. By (arg), l ∈ CC = CC D (l). By (var), x ∈ CC. By (subterm-abs), sin(F x) ∈ CC. By (subterm-acc), F x ∈ CC. By (subterm-app), F ∈ CC. By (undef), cos(F x) ∈ CC. By (rec), DF x ∈ CC for l ⊲ s F . By (rec), (DF x) × (cos(F x)) ∈ CC for D > F ×. Therefore, by (abs), λx(DF x) × (cos(F x)) ∈ CC.

Application to CRSs and HRSs

CRSs [START_REF] Klop | Combinatory reduction systems[END_REF][START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF] can be seen as an extension of the untyped λ-calculus with no object-level application symbol but, instead, symbols of fixed arity defined by rules using a matching mechanism equivalent to matching modulo βη on Miller patterns.

In HRSs [START_REF] Nipkow | Higher-order critical pairs[END_REF][START_REF] Mayr | Higher-order rewrite systems and their confluence[END_REF], one considers simply-typed λ-terms in β-normal η-long form with symbols defined by rules using Miller's pattern-matching mechanism.

Note that, although HRS terms are simply typed, one can easily encode the untyped λ-calculus in it by considering an object-level application symbol. Similarly, in CRSs, one easily recovers the untyped λ-calculus by considering an object-level application symbol. Such a CRS is called β-CRS in [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF].

In HALs [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF], Jouannaud and Okada consider arbitrary typed λ-terms with function symbols of fixed arity defined by rewrite rules, and computation is defined as the combination of β-reduction and rewriting.

These three approaches can be seen as operating on the same term algebra (λ-calculus with symbols of fixed arity, which is a sub-algebra of the one we consider here) with different reduction strategies wrt β-reduction [START_REF] Van Oostrom | Comparing combinatory reduction systems and higher-order rewrite systems[END_REF]: in HALs, there is no restriction; in CRSs, every rewrite step is followed by a βdevelopment of the substituted variables (see the notion of valuation in Definition 25); finally, in HRSs, terms are β-normalized.

More precisely, in a CRS, a term is either a variable x, an abstraction λxt, or the application of a function symbol f to a fixed number of terms. A CRS term is therefore in β-normal form. The set of CRS terms is a subset of the set of terms that is stable by reduction or expansion (if matching substitutions are restricted to CRS terms). Only rewrite rules can contain terms of the form x t, but every rewrite step is followed by a β-development. Hence, the termination of a CRS can be reduced to the termination of the corresponding HAL, because a rewrite step in a CRS is included in the relation → R,βη ∪ → * β . In an HRS, terms are in β-normal η-long form and, after a rewrite step, terms are β-normalized and η-expanded if necessary [START_REF] Mayr | Higher-order rewrite systems and their confluence[END_REF]. Hence, in an HRS, the reduction relation is → R → ! β → ! η , where → η is the relation of η-expansion 42 and R ! denotes normalization wrt R. Hence, our results can directly apply to HRSs if the set of terms in η-long form is stable by rewriting for, in this case, no η-expansion is necessary 43 . This is in particular the case if the right-hand side of every rule is in η-long form [START_REF] Huet | Résolution d'équations dans les langages d[END_REF]. Otherwise, one needs to extend our results by proving the termination of → ∪ → η instead (see [START_REF] Cosmo | Combining algebraic rewriting, extensional lambda calculi, and fixpoints[END_REF] for the case where → = → β ∪ → R and R is a set of algebraic rewrite rules).

Conclusion

We have provided a new, more general, presentation of the notion of computability closure [START_REF] Blanqui | Inductive-data-type systems[END_REF] and how it can be extended to deal with different kinds of rewrite relations (rewriting modulo some equational theory and rewriting with matching modulo βη) and applied to other frameworks for higher-order rewriting (Section 6.5). In particular, for dealing with recursive function definitions, we introduced a new more general rule (Figure 4) based on the notion of F -quasi-ordering compatible with application (Definition 6).

Parts of this work have been formalized in the proof assistant Coq [START_REF] Inria | The Coq reference manual[END_REF]: pure λ-terms 44 , computability predicates on (untyped) λ-terms, simply-typed λ-terms using typing environments, the interpretation of types using accessible arguments as in Section 4.7, and the smallest computability closure closed by the operations I, II, IV and V [START_REF] Blanqui | A formalization in Coq of the notion of computability closure for proving the termination of rewrite relations on λ-term[END_REF]. 45 Therefore, the complete formalization of the results presented in this paper is not out of reach. In particular, the operations III and VI, and the computability closure for rewriting modulo some equational theory. On the other hand, the computability closure for rewriting with matching modulo βη seems more difficult.

For the sake of simplicity, we have presented this work in Church simply-typed λ-calculus [Chu40] but, at the price of heavier notations, a special care for type variables, and assuming that α f = sup{| l| | f l → r ∈ R} 42 That is, the relation ←η restricted to terms not of the form λxt and to contexts not of the form C[[]u] [CK96]. 43 The set of terms in η-long form is stable by β-reduction [START_REF] Huet | Résolution d'équations dans les langages d[END_REF]. 44 Using named variables and explicit α-equivalence [START_REF] Curry | Combinatory logic[END_REF] which is closer to informal practice than de Bruijn indices [dB72]. 45 The definitions and theorems without their proofs are available on http://color.inria.fr/doc/main.html. In particular, λ-calculus is formalized in the files LTerm.v, LSubs.v, LAlpha.v, LBeta.v and LSimple.v; computability is formalized in LComp.v, LCompRewrite.v and LCompSimple.v; the interpretation of type constants as in Section 4.7 is formalized in LCompInt.v; the notion of F -quasi-ordering is formalized in LCall.v; and the notion of computability closure is formalized in LCompClos.v. As an example, Gödel system T is proved terminating in LSystemT.v by using the lexicographic status F -quasi-ordering ( s)lex.

is finite,46 these results can be extended to polymorphic and dependent types, and type-level rewriting (e.g. strong elimination), following the techniques developed in [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF].

But the notion of computability closure has other interesting properties or applications:

• As shown in [START_REF] Blanqui | Higher-order dependency pairs[END_REF], it has some important relationship with the notion of dependency pair [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] and can indeed be used to improve the static approach to higher-order dependency pairs [START_REF] Kusakari | Static dependency pair method based on strong computability for higher-order rew[END_REF].

• The notion of computability closure and Jouannaud and Rubio's higher-order recursive path ordering (HORPO) [JR99, JR07] share many similarities. The notion of computability closure is even used in HORPO for strengthening it. HORPO is potentially more powerful than CC because, when comparing the left-hand side of a rule f l with its corresponding right-hand side r, in CC, the subterms of r must be compared with f l itself while, in HORPO, the subterms of r may be compared with subterms of f l. However, in [START_REF] Blanqui | RPO revisited[END_REF], I showed that HORPO is included in the monotone closure of the least fixpoint of the monotone function R → {(f l, r) | r ∈ CC f ( l), τ (f l) = τ (r), FV(r) ⊆ FV(l)} (where CC is the smallest computability closure defined by the rules I to IV), and that Dershowitz' first-order recursive path ordering [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF] is equal to this fixpoint (when CC is restricted to first-order terms). This and the fact that HORPO could not handle the examples of Section 4.6 motivated a series of papers culminating in the definition of the computability path ordering (CPO) subsuming both HORPO and CC, but currently limited to matching modulo α-equivalence [BJR08, BJR15].

• In Section 4.6, we have seen that, on non-strictly positive inductive types, the computability closure can handle recursors (by using an elimination-based interpretation of types), but cannot handle arbitrary function definitions (e.g. the function ex). This can however be achieved by extending the type system with size annotations (interpreted as ranks) and using an F -quasi-ordering comparing size annotations. This line of research was initiated independently by Giménez [START_REF] Giménez | Un calcul de constructions infinies et son application à la vérification de systèmes communiquants[END_REF] and Hughes, Pareto and Sabry [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF], and further developed by Xi [START_REF] Xi | Dependent types for program termination verification[END_REF], Abel [START_REF] Abel | Termination checking with types[END_REF], Barthe et al [BFG + 04] and myself [START_REF] Blanqui | A type-based termination criterion for dependently-typed higher-order rewrite systems[END_REF]. By considering explicit quantifications and constraints on size annotations, one can even handle conditional rewrite rules [START_REF] Blanqui | Combining typing and size constraints for checking the termination of higher-order conditional rewrite syst[END_REF]. Moreover, in [START_REF] Blanqui | On the relation between sized-types based termination and semantic labelling[END_REF], Roux and I showed that these developments can to some extent be seen as an instance of higher-order semantic labeling [START_REF] Zantema | Termination of term rewriting by semantic labelling[END_REF][START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF], a technique which consists in annotating function symbols with the semantics of theirs arguments in some model of the rewrite system.

• In [JR06], using a complex notion of "neutralization" that requires the introduction of new function symbols, Jouannaud and Rubio provide a general method for building a reduction ordering for rewriting with matching modulo βη on β-normal terms from a reduction ordering for rewriting with matching modulo α-equivalence on arbitrary terms, if the latter satisfies some conditions. Then, they provide a restriction of HORPO satisfying the required conditions. A precise comparison between this approach and the one developed in Section 6 remains to be done. It could perhaps shed some light on this notion of neutralization.

p→

  β u to indicate that t| p = (λxa)b and u = t[a b

Figure 1 :

 1 Figure 1: Computability closure operations I

Figure 2 :

 2 Figure 2: Computability closure operations II

Figure 3 :

 3 Figure 3: Computability closure operations III

Figure 4 :

 4 Figure 4: Computability closure operations IV

Figure 5 :

 5 Figure 5: Computability closure operations V for standard inductive systems (Definition 11)

Figure 6 :

 6 Figure 6: Computability closure operations V

Figure 7 :

 7 Figure 7: Computability closure operations I'

  By (R2), t ′ ∈ S. Since u is valid wrt (l, p), e ∈ [[τ (x)]]. By (R2), e ′ ∈ [[τ (x)]]. Therefore, v is valid wrt (l, p) and, by the induction hypothesis (4), v ∈ S. * There is b ′ such that b → prod b ′ and v = u[(λxa)e b ′ ] p . Then, t → t ′ = u[a e x b ′ ] p ← β,l,p v. Since u is valid wrt (l, p), b are computable. Thus, by (R2), b ′ are computable and v is valid. Therefore, by the induction hypothesis (3), v is computable.

Figure 8 :

 8 Figure 8: Computability closure operations VI

  P is stable by reduction: if t ∈ P and t → β u, then u ∈ P ; (R3) if t is a neutral 10 term and → β (t) ⊆ P , then t ∈ P .

	. A set P belongs to Red if the following
	conditions are satisfied:
	(R1) P ⊆ SN(→ β );
	(R2)

  that is, the application of t cannot create new redexes.

	• Sat: Tait' set of saturated 11 sets [Tai75]. A set P belongs to Sat if the following conditions are satisfied:
	(S1) P ⊆ SN(→ β );
	(S2) P contains all the strongly normalizable terms of the form x t;
	(S3) if t u x v ∈ P and u ∈ SN(→ β ), then (λxt)u v ∈ P .
	• SatInd: Parigot' smallest subset of Sat containing SN(→ β ) and stable by ∝ and [Par97]. As Parigot
	remarked, for β-reduction, it is not necessary to consider all saturated sets but only those that can be
	obtained from SN(→ β ) by ∝ and intersection.
	• Bi: Parigot' set of bi-orthogonals 12 [Par93, Par97] is the set {∝ * (E, SN(→ β )) | ∅ = E ⊆ SN(→ β ) * } where SN(→ β ) * is the set of finite sequences of elements of SN(→ β ) and ∝ * : P(L * ) × P(L) → P(L) extends ∝
	as follows:

In fact, Tait speaks of "convertibility" and Girard of "reducibility". To the best of my knowledge, the expression "computability" is due to Troelstra[START_REF] Troelstra | Models and Computability[END_REF] although Troelstra himself invokes Tait. This notion of computability has to be distinguished from the one of Turing and Church[START_REF] Turing | Computability and λ-definability[END_REF]. However, given a Tait-computable λ-term t : U ⇒ V , the function that maps every Tait-computable λ-term u : U to the normal form of tu is indeedTuring-computable.

However, with polymorphic types, or dependent types together with type-level rewriting (e.g. strong elimination), α f may be infinite if R is infinite.

In contrast with the mathematical tradition where a relation R is said well-founded if there is no infinite descending chain a 0 R -1 a 1 R -1 . . .

Here, A + B is the multiset union of the multisets A and B, and {|y 1 , . . . , yn|} the multiset made of y 1 , . . . , yn.

This expression seems due to Gallier[START_REF] Gallier | On Girard's "candidats de réductibilité[END_REF].

Parigot did not use the expression "bi-orthogonal". To my knowledge, this expression first appears in[START_REF] Vouillon | Semantic types: a fresh look at the ideal model for types[END_REF]. See[START_REF] Abel | A polymorphic lambda-calculus with sized higher-order types[END_REF], p. 67, for a discussion about the origin of this expression. Anyway, Parigot computability predicates are indeed bi-orthogonals wrt the orthogonality relation ⊥ between P(SN(→ β )) and P(SN(→ β ) * ) such thatP ⊥E if ∀v ∈ P, ∀ t ∈ E, v t ∈ SN(→ β ). The (right) orthogonal of P ⊆ SN(→ β ) is P ⊥ = { t ∈ SN(→ β ) * | ∀v ∈ P, v t ∈ SN(→ β )}, while the (left) orthogonal of E ⊆ SN(→ β ) * is ⊥ E = ∝ * (E, SN(→ β )).One can then see that Bi = {P ⊆ SN(→ β ) | P = ∅ ∧ ⊥ (P ⊥ ) = P }.

We will give a more general definition in Definition 16.

We give a more general definition in Definition 5.

This definition replaces the one given in Definition 4.

Note that the rule f (c x) → x means that c is injective and thus that, in a set-theoretical interpretation of types, the cardinality of the function space A → B is smaller than or equal to the cardinality of A, which is hardly possible if B is of cardinality greater than or equal to 2.

→ * s is the smallest quasi-ordering containing both → and ⊲s. Its strict part on SN is → + ∪ → * ⊲s.

These definitions can be generalized to any positive inductive type (see Definition 10 just after)[START_REF] Mendler | Inductive definition in type theory[END_REF][START_REF] Blanqui | Inductive-data-type systems[END_REF].

We assume that B is infinite. Alternatively, we could consider type variables.

In fact, in CIC, inductive types are even restricted to strictly-positive inductive types (see Definition 13) for termination may be lost when considering some polymorphic non-strictly positive types[START_REF] Coquand | Inductively defined types[END_REF].

We could improve this definition by taking x ∈ CC f ( l) instead of x ∈ X -FV( l) only[START_REF] Blanqui | Inductive-data-type systems[END_REF][START_REF] Blanqui | RPO revisited[END_REF].

Here, we in fact consider a family of F -quasi-orderings indexed by f l.

In a standard inductive system, all the arguments of a constructor are accessible (Acc(f) = [1, | T |] for every f ∈ F -D(R)).In this case, this new definition of F O is equivalent to the introduction-based definition given in the previous section if one takes Acc(f) = ∅ for every f ∈ D(R), and assumes that M(R) = F -D(R).

This definition generalizes and replaces the one given in Definition 2.

We use the relation and notation of[START_REF] Huet | Confluent reductions: abstract properties and applications to term-rewriting systems[END_REF] and not the relation→ R/E = = E → R = E used in[START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF] for it makes proofs simpler, but the two relations are equivalent from the point of view of termination.

Indeed, the order of molecules in a chemical formula is irrelevant, and the order in which messages are received may be different from the order messages are sent.

l = r is regular if FV(l) = FV(r).

l = r is linear is both l and r are linear.

l = r is collapsing if l ∈ X or r ∈ X

See Definition 15.

This is exactly the situation of Nederpelt's counter-example to the confluence of → βη on untyped Church-style λ-terms[START_REF] Nederpelt | Strong normalization in a typed lambda calculus with lambda structured types[END_REF], which is in fact a counter-example to the confluence of → β 0 η on untyped Church-style λ-terms.

Note that →η cannot be postponed after → β 0 as shown by the following example: (λxa)(λyxy) →η (λxa)x → β 0 a.

In CRSs, → R is defined as the closure of R by context and valuation (extended to all terms).

See Definition 15.

This case is not necessary for Lemma 17 to hold but avoids adding rules whose right-hand sides are β-redexes.

This case could be simplified and dealt with by (R2) if →η was included in →. But, then, we would have to check Lemma 16 again. The present proof shows that this is not necessary.

This case is not necessary for Lemma 20 to hold but avoids adding rules whose right-hand sides are η-redexes.

Because, in this case, α f may be infinite if R is infinite, which may be the case if one considers the rewrite relation generated by a conditional rewrite system, or applies some semantic labeling to a finite rewrite system[START_REF] Zantema | Termination of term rewriting by semantic labelling[END_REF].

Acknowledgements. The author thanks very much the anonymous referees for their very careful reading and many suggestions, and Ali Assaf and Ronan Saillard for their comments on Section 6.

Lemma 18 For every (finite) set of rules S, there is a (finite) β-complete set of rules R ⊇ S such that f l → r ∈ CC f ( l) for every f l → r ∈ R if f l → r ∈ CC f ( l) for every f l → r ∈ S.

Proof. Let F β be the function on the powerset of T 2 such that, for all R ⊆ T 2 , F β (R) is the smallest set such that R ⊆ F β (R) and, for all l → r ∈ R and T, U such that l : T ⇒ U , there is x ∈ X -FV(l) such that τ (x) = T , lx → s ∈ F β (R) if r = λxs, and lx → rx ∈ F β (R) otherwise. Since F β is extensive (i.e. R ⊆ F β (R)), by Hessenberg's fixpoint theorem [START_REF] Hessenberg | Kettentheorie and Wohlordnung[END_REF], F β has a fixpoint R such that S ⊆ R. Since

for every f l → r ∈ S, and that there are f l → r ∈ R and T, U such that f l : T ⇒ U . By assumption, r ∈ CC f ( l). Let now x ∈ X -FV(l). Wlog, we can assume that x / ∈ BV(r). Hence, r ∈ CC f ( lx). By (arg), x ∈ CC f ( lx). Therefore, by (app), rx ∈ CC f ( lx). Now, if r = λys, then s x y ∈ CC f ( lx) by (red).

Note moreover that S ⊆ R ⊆ → S → = β0 . Therefore, → β ∪ → R,βη and → β ∪ → S,βη have the same normal forms and, if = Rβ (resp. = Sβ ) is the smallest congruence containing → β and R (resp. S), then = Rβ is equal to = Sβ .

Preservation of computability by η-equivalence

In this section, we prove that computability is preserved by η-equivalence if ← η → R,βη ⊆ → R,βη = η . Then, we give sufficient conditions for this commutation property to hold.

Lemma 19 Let > T be the smallest transitive relation on types containing > B and such that T ⇒ U > T T and T ⇒ U > T U . The relation > T is well-founded.

Proof. Wlog we can assume that the symbol ⇒ is not a type constant. Then, let ≻ the smallest transitive relation on B ∪ {⇒} containing > B and such that ⇒ ≻ A for all A ∈ B. The relation ≻ is wellfounded for > B is well-founded. Hence, > T is well-founded for it is included in the recursive path ordering (RPO) built over ≻ [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF].

Lemma 20 Let R be a set of rules such that ← η → R,βη ⊆ → R,βη = η , and assume that types are interpreted as in Section 4.7. If t : T is computable, t = η u and u : T , then u is computable.

Proof. Note that, by Lemma 12, t → * η ← * η u. Since t and u are well-typed and → η preserves typing, all terms between t and u are of type T .

We then proceed by induction on (1) the type of t ordered with > T (well-founded by Lemma 19), (2) the rank of t (see Definition 12) if t is of base type, (3) t ordered by → (t ∈ SN by (R1)), and (4) the number of ↔ η -steps between t and u.

If T = V → T ′ , then u is computable if, for all computable v : V , uv : T ′ computable. By monotony, tv = η uv. Since tv : T ′ and T > T T ′ , uv is computable by the induction hypothesis.

If t = u, then u is computable. Assume now that t = η t ′ ↔ η u. By the induction hypothesis, t ′ is computable. Therefore, we are left to prove the lemma when = η is replaced by ↔ η .

Assume now that T is a type constant A. By Lemma 4, a term a : A is computable iff all its reducts are computable and, for all f ∈ M(R), i ∈ Acc(f) and a such that a = f a, a i is computable.

We first prove that, for all f ∈ M(R), i ∈ Acc(f) and u such that u = f u, u i : V ⇒ B is computable. Since t is of base type and t ↔ η u = f u, there are t such that t = f t and t (↔ η ) prod u. Now, u i is computable if, for all computable v : V , u i v is computable. By monotony, t i v ↔ = η u i v and t i v has a type or a rank smaller than the type or rank of f t (for i ∈ Acc(f)). Therefore, u i v is computable by the induction hypothesis.

We now prove that all the reducts v of u are computable.

The fact that the rules of Figure 8 are valid computability closure operations is proved in [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF]. Note that S ⊆ R ⊆ ← * η S → * η . Hence, if = Rβη (resp. = Sβη ) is the smallest congruence containing → η , → β and R (resp. S), then = Rβη is equal to = Sβη . Moreover, → R,βη and → S,βη have the same normal forms on η-long terms.

We have seen that termination of rewriting with matching modulo βη relies on commutation properties between → R,βη and ↔ βη . Such conditions are well-known in first-order rewriting theory: the notion of compatibility of Peterson and Stickel [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF], the notion of local E-commutation of Jouannaud and Muñoz [START_REF] Jouannaud | Termination of a set of rules modulo a set of equations[END_REF] and, more generally, the notion of local coherence modulo E of Jouannaud and Kirchner [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]. Similarly, the addition of extension rules to make a system compatible, locally commute or locally coherent is also well-known since Lankford and Ballantyne [START_REF] Lankford | Decision procedures for simple equational theories with commutative-associative axioms: complete Technical Report ATP-039[END_REF].

Preservation of computability by leaf-β-expansion

We now prove that computability is preserved by leaf-β-expansion, but for patterns containing undefined symbols only.

Definition 31. Let v be a term, p ∈ LPos(v) and q be the leaf positions of v distinct from p. We say that a term t is valid wrt (v, p) if there are t and u such that t = v[ t] p [u] p and, for all y, a and b such that u = (λ ya) b and

Note that, if l is a pattern and σ is valid wrt l, then every term t such that σ(l) ← * β,l,p1 . . . ← * β,l,p k t, where p 1 , . . . , p k are leaf positions of l, is valid wrt (l, p 1 ), . . . , (l, p k ) (for b j ↓ η ∈ BV(l, p i ) in this case).

Lemma 23 Let R be a β and η-complete set of rules, and assume that types are interpreted as in Section 4.7. Let l be a term containing undefined symbols only, and let p be a leaf position of l.

]. Note that l does not need to be a pattern, a property that cannot be preserved when instantiating bound variables. In fact, the complete structure of l is not relevant. Because we look at leaf-β-expansions, only the top part of l that is above the leaf positions is relevant. Hence, let || || be the measure on terms defined as follows:

We prove the lemma by induction on (1) ||l||, (2) τ (l), (3) t ordered by → (for t ∈ SN by (R1)), and (4) the terms b such that u| p = (λ ya) b (for u is valid wrt (l, p)) ordered by → (for b ∈ SN by (R1)). We proceed by case on l: ∈ FV(b i ) and b i ( g z ) = b i . Therefore, s g z is valid. Wlog we can assume that x = z and x / ∈ FV(g). Hence, (λxa) g z = λxa g z and (a e x ) g z = (a g z )

e g z x . Therefore, r g z ← β,m,q s g z and, by the induction hypothesis (1),

• l = f l with τ (f) = T ⇒ U . We proceed by case on τ (l):