Frédéric Blanqui

Jean-Pierre Jouannaud

Albert Rubio

THE COMPUTABILITY PATH ORDERING

come

Introduction

This paper addresses the problem of automating termination proofs for typed higher-order calculi by reducing them to ordering comparisons between lefthand and righthand sides of rules.

It also addresses another, more fundamental problem of mathematical importance. Consider the set of terms generated by a denumerable set of variables, application, abstraction and some set of function symbols with arities, our version of the pure λ-calculus. We shall use a (possibly infinite) set R of pairs of λ-terms called rewrite rules used as our computing device. Given a term as input, whether our computing device will eventually terminate and return an answer is in general undecidable, even if R is a singleton set [START_REF] Dauchet | Termination of rewriting is undecidable in the one-rule case[END_REF]. It may even be undecidable for specific rewrite systems, such as the well-known β-reduction rule (formally defined here as the infinite set of its instances). A major question is the following: can we approximate the set of β-terminating terms by some meaningful subset? An important partial answer was given by Turing: the set of simply-typed λ-terms, where the word simply refers to a specific typing discipline introduced by Church in the λ-calculus [START_REF] Church | A formulation of the simple theory of types[END_REF], is terminating when a specific strategy is employed [START_REF] Turing | Some theorems about Church's system[END_REF]. The complete answer, the fact that the very same set is indeed terminatin under any strategy, is due to Sanchis [START_REF] Sanchis | Functionals defined by recursion[END_REF]. Tait and Girard gave later proofs [START_REF] Tait | A realizability interpretation of the theory of species[END_REF][START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF] which have been the basis of many further generalizations, by considering more rules (η-reduction, recursors, general schema), and more terms characterized by more elaborate type disciplines (polymorphic, dependent, inductive type systems). When considering β-reduction alone, the obtained approximations of the set of terminating λ-terms are quite satisfactory. But proving the corresponding statement that computations terminate when given a typed λ-term as input, requires using an extremely powerful technique called reducibility 1 , introduced by Tait for simply typed terms, and further developed by Girard for the richer type disciplines. Given a set of terms and a set of rewrite rules R, a reducibility predicate is defined by axioms that it should satisfy, mainly closure under term constructions, closure under rewriting with R, and containment in the set of terminating terms. Girard exhibited a particular predicate for β-reduction which can be easily adapted for other sets of rules, but there are sets of rules for which some typable terms originate an infinite computation. We therefore turn to a new undecidable question: which sets of rules admit a computability predicate?

The question we answer in this paper is whether this set S (of sets R of rules) admits some non-trivial decidable subset: our approximation of S is the set of sets R of rules such that pairs in R are ordered by (some instance of) the computability path ordering CPO.

The work itself takes its roots in early attempts by Breazu-Tannen and Gallier [START_REF] Breazu-Tannen | Polymorphic rewriting conserves algebraic strong normalization[END_REF] and independently Okada [START_REF] Okada | Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term re[END_REF] to consider mixed typed λ-calculi with algebraic rewriting. Both works used Girard's computability predicates method to show that the strong normalization property of algebraic rewriting was preserved in the union. These results grew into a whole new area, by extending the type discipline on the one hand, and the kind of rules that could be taken care of on the other hand. The type discipline was extended independently by Barbanera and Dougherty in order to cover the whole calculus of constructions [START_REF] Barbanera | Adding algebraic rewriting to the calculus of constructions: strong normalization preserved[END_REF][START_REF] Dougherty | Adding algebraic rewriting to the untyped lambda calculus[END_REF], while the rule format was extended as described next.

Higher-order rewrite rules satisfying the general schema, a generalization of Gödel's primitive recursion rules for higher types, were introduced by Jouannaud and Okada in the case of a polymorphic type discipline [START_REF] Jouannaud | A computation model for executable higher-order algebraic specification languages[END_REF][START_REF] Jouannaud | Abstract data type systems[END_REF]. The latter work was then extended first by Barbanera and Fernández [5,[START_REF] Barbanera | Modularity of termination and confluence in combinations of rewrite systems with λω[END_REF] and finally by Barbanera, Fernández and Geuvers to cover the whole calculus of constructions [START_REF] Barbanera | Modularity of strong normalization and confluence in the algebraic-λ-cube[END_REF]. Recursors for basic inductive types, which constructors admit arguments of a non-functional type only, could be taken care of by the general schema, but arbitrary strictly positive inductive types could not, prompting for an extension of the schema, which was reformulated for that purpose by Blanqui, Jouannaud and Okada [START_REF] Blanqui | Inductive-data-type systems[END_REF]. This new formulation was based on the notion of computability closure of a term f( ⃗ t), defined as a set of terms containing ⃗ t and closed under computability preserving operations in the sense of Tait and Girard. Membership to the general schema was then defined for an arbitrary rewrite rule as membership of its righthand side to the computability closure of its lefthand side. This elegant, flexible and powerful definition of the general schema was finally extended by Blanqui in a series of papers, until it covered the entire calculus of inductive constructions including strong elimination rules [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF][START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF], rewriting modulo some equational theories and rewriting with higher-order pattern-matching [START_REF] Blanqui | Termination of rewrite relations on λ-terms based on Girard's notion of reducibility[END_REF].

Introduced by Jouannaud and Rubio, HORPO was the next step, the very first order on simply typed λ-terms defined by induction on the term structure, as does Dershowitz recursive path ordering for first-order terms [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF]. Comparing two terms with HORPO starts by comparing their types in a given well-founded ordering on types before to proceed recursively on the structure of the compared terms, in a way which depends on a comparison of the roots of both terms in a given well-founded order on the algebraic signature called the precedence [START_REF] Jouannaud | The higher-order recursive path ordering[END_REF]. HORPO was extended to the calculus of constructions by Walukiewicz [START_REF] Walukiewicz-Chrząszcz | Termination of rewriting in the calculus of constructions[END_REF], and to use semantic interpretations of terms instead of a precedence on function symbols by Borralleras and Rubio [START_REF] Borralleras | A monotonic higher-order semantic path ordering[END_REF]. An axiomatic presentation of the rules underlying HORPO can be found in [START_REF] Goubault-Larrecq | Well-founded recursive relations[END_REF]. A more recent work in the same direction is [START_REF] Dershowitz | Jumping and escaping: modular termination and the abstract path ordering[END_REF]. A more general version of HORPO appears in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], which uses the computability closure to strengthen its expressivity. Blanqui proved that the first version of HORPO is contained in an order defined as a fixpoint of the computability closure definition [START_REF] Blanqui | RPO revisited[END_REF]. Indeed, HORPO and the computability closure share many similar constructs, raising expectations for a simpler and yet more expressive definition, instead of a pair of mutually inductive definitions for the computability closure and the ordering itself. On the positive side, the computability closure makes little use of type comparisons, hence may succeed when HORPO fails for type reason. Unfortunately, its fixpoint is not a syntax-oriented definition, hence has a more limited practical usage.

Originally formulated in [START_REF] Blanqui | Higher-order termination: from Kruskal to computability[END_REF], the question of finding a syntax oriented recursive definition of HORPO that would inherit the advantages of the computability closure paved the way to CPO, the computability path ordering. The first definition was given in [START_REF] Blanqui | HORPO with computability closure: a reconstruction[END_REF], later improved as CPO in [START_REF] Blanqui | The computability path ordering: the end of a quest[END_REF]. A major improvement of CPO is that type comparisons are no more systematic, but occur in very specific cases. This does not only speed up computations, but also boosts the ordering capabilities in an essential way. Further, bound variables are handled explicitly by CPO, allowing for arbitrary abstractions in the righthand sides together with a more uniform definition.

In this paper, we present an in-depth study of an improved version of CPO for a simple extension of Church's simple type discipline [START_REF] Church | A formulation of the simple theory of types[END_REF], before we extend it to inductive types along the lines suggested in [START_REF] Blanqui | The computability path ordering: the end of a quest[END_REF] following a technique dating back to Mendler [START_REF] Mendler | Inductive definition in type theory[END_REF][START_REF] Mendler | Inductive types and type constraints in the second-order lambda calculus[END_REF] and extended to rewriting by Blanqui [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF]. In particular, we first show that many improvements of CPO cannot be well-founded: type comparisons are necessary when recursive calls deconstruct the lefthand side, but are not otherwise. While this all came out of the well-foundedness proof, it indeed shows a strong relationship between the recursive structure of CPO and the computability predicates method of Tait and Girard that is used to carry out the proof, which explains the name CPO. It further shows that CPO is indeed a sharp approximation of the set of sets of rules which admit a computability predicate. We then address the treatment of inductive types which remained ad hoc so far, thanks to the use of accessibility, a relationship introduced by Blanqui which generalizes the notion of inductive type [START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF]. We finally introduce another novelty: small symbols. In all previous definitions, function symbols were bigger in the precedence than application and abstraction. Such symbols are now called big, while small symbols behave differently, being possibly smaller than both. Small symbols were suggested by Li to carry out a generalization of CPO to dependent types [START_REF] Jouannaud | Termination of Dependently Typed Rewrite Rules[END_REF].

In the recent years, the success of HORPO has prompted interest in the generalization to higher-order computations of various other methods used for first-order computations, most notably Art and Giesl's dependency pairs [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF][START_REF] Giesl | Mechanizing and improving dependency pairs[END_REF][START_REF] Hirokawa | Tyrolean Termination Tool: techniques and features[END_REF] yielding for instance [START_REF] Sakai | On dependency pair method for proving termination of higher-order rewrite systems[END_REF][START_REF] Kusakari | Static dependency pair method based on strong computability for higher-ord[END_REF][START_REF] Kop | Higher-order dependency pairs with argument filterings[END_REF][START_REF] Suzuki | Argument filterings and usable rules in higher-order rewrite systems[END_REF][START_REF] Kop | Higher order dependency pairs for algebraic functional systems[END_REF][START_REF] Kop | Higher order termination[END_REF], and interpretation methods [START_REF] Manna | On the termination of Markov algorithms[END_REF][START_REF] Lankford | On proving term rewriting systems are Noetherian[END_REF][START_REF] Zantema | Termination of term rewriting by semantic labelling[END_REF][START_REF] Contejean | Mechanically proving termination using polynomial interpretations[END_REF] yielding for instance [START_REF] Van De Pol | Termination of higher-order rewrite systems[END_REF][START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF][START_REF] Roux | Size-based termination: semantics and generalizations[END_REF][START_REF] Fuhs | Polynomial interpretations for higher-order rewriting[END_REF].

The paper is organized as follows. First, we define the sets of types and terms that we consider (simply typed λ-terms with function symbols of fixed arity), and the class of orderings on types that can be used in CPO. We then give a first definition of our ordering (core CPO), and show that it can hardly be improved while keeping the same recursive structure and well-foundedness. We then show how to prove its well-foundedness by extending Tait and Girard's technique of computability predicates. In the following sections, we consider two extensions of core CPO. In the first one, core CPO is extended by using accessible subterms which allows to handle strictly inductive types. In the second, application or abstraction are allowed to be bigger than a function call. Concluding remarks are given in Section 9.

We recommend surveys [START_REF] Dershowitz | Rewrite systems[END_REF][START_REF]Term rewriting systems[END_REF] for rewriting and [START_REF] Barendregt | Lambda calculi with types[END_REF] for typed λ-calculus.

Types and admissible type orderings

CPO is a relation on well typed terms but, instead of allowing the comparison of terms of the same type only, it allows the type to decrease in some well-founded ordering. However, not any type ordering is admissible.

In this section, we first recall the definition of (simple) types and some basic functions on types. Then, we define what are the (strict) orderings on types that can be used in CPO, study some of their properties and give an example based on a well-founded precedence on type constants. Definition 2.1 (Types). Let S be a set of sorts. The set T of types, the arity α(_) and the order o(_) of a type are inductively defined as follows:

• a sort A ∈ S is a type of arity α(A) = 0 and order o(A) = 0.

• if T and U are types, then T → U is a type of arity α(T → U ) = 1 + α(U ) and order

o(T → U ) = max{1 + o(T ), o(U )}.
We use capital letters for types and a different font for sorts (e.g. T and A), and ⃗ T for a (possibly empty) sequence of types T 1 , . . . , T n , of length ⃗ T = n. As usual, → associates to the right so that A → A → A and A → (A → A) are the same. Given a relation R, let R + (resp. R * ) denote the transitive (resp. transitive and reflexive) closure of R. Definition 2.2 (Admissible type orderings). Let ⊳ l and ⊳ r be the relations on types such that T → U ⊳ l T and T → U ⊳ r U respectively, and ⊳ be the transitive closure of their union. A (strict) ordering > on types is admissible if:

• ⊳ r ⊆ > (typ-right-subterm) • ⋗ = (> ∪ ⊳ l ) + is well-founded (typ-sn) • if T → U > V , then U ≥ V or V = T → U ′ with U > U ′
(typ-arrow) where ≥ is the reflexive closure of >. We say that a type T is compatible (resp. strictly compatible) with a sort A, written Sort A (T ) (resp. Sort ⋖A (T )) if B A (resp. B ⋖ A) for every sort B occurring in T .

Admissible type orderings originate from [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. Note that a sort can be bigger than an arrow type. If A is a sort occurring in T , then T A. Finally, note that the relation ⋗ is a simplification ordering [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF]. We now give an example of admissible ordering based on a well-founded precedence on sorts. For a concrete use case, see Example 5.2 below. Lemma 2.3. Given a well-founded ordering > S on sorts, let > be the smallest ordering > on types containing > S and ⊳ r and such that, for all U, V, V ′ , it holds that

V > V ′ implies U → V > U → V ′ . Then, > is admissible.
Proof.

• (typ-sn) ⋗ is included in the RPO extending > S [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF], hence is well-founded.

• (typ-right-subterm) By definition.

• (typ-arrow) Let T → U > V .
The proof is by induction on the definition of >.

(

) > is > S . Impossible since T → U is not a sort. (2) > is ⊳ r . Then U = V , hence U ≥ V . ( 1
) V = T → W and U > W . Immediate. ( 3
) T → U > W > V . 4
By induction hypothesis applied to T → U > W , there are two cases:

-U ≥ W . Then, by transitivity, U > V .

-W = T → U ′ for some U ′ < U . By induction hypothesis on T → U ′ > V , there are two cases:

* U ′ ≥ V . By transitivity, U > V . * V = T → V ′ for some V ′ < U ′ .
By transitivity, U > V ′ and we are done.

In the following, we prove some properties of admissible type orderings:

Lemma 2.4. Let > be an admissible type ordering. If T → U > T ′ → U ′ , then U > U ′ .
Proof. By (typ-arrow), either T = T ′ and U > U ′ or U ≥ T ′ → U ′ , in which case we conclude by (typ-right-subterm) and transitivity.

Lemma 2.5. Let > be an admissible type ordering. If A > U , then Sort ⋖A (U ).

Proof. Let B be a sort occurring in U . Then, U B. Hence, by transitivity, A ⋗ B.

Lemma 2.6. Let > be an admissible type ordering. If T > U and Sort A (T ), then Sort A (U ).

Proof. Let C be a sort occurring in U . We proceed by induction on T .

• T = B. Since Sort A (T ), B A. By Lemma 2.5, Sort ⋖B (U ) and C ⋖ B. Therefore, by transitivity, C A. • T = S → T ′ . Then, Sort A (S) and Sort A (T ′ ). By (typ-arrow), there are two cases:

-T ′ ≥ U . Then, by induction hypothesis, Sort A (U ).

-U = S → U ′ and T ′ > U ′ . By induction hypothesis, Sort A (U ′ ). Hence Sort A (U ).

Terms

In this section, we define the set of terms on which CPO operates. We consider simply-typed λ-terms [START_REF] Church | A formulation of the simple theory of types[END_REF][START_REF] Barendregt | Lambda calculi with types[END_REF] with function symbols of fixed arity, that is, a function symbol of arity n always comes with n arguments. We assume that every variable or function symbol comes equipped with a fixed type and that α-equivalence replaces a variable by another variable of the same type.

Definition 3.1 (Terms). Let X be an infinite set of variables, each variable x being equipped with a type τ (x) ∈ T so that there is an infinite number of variables of each type. Let also F be a (finite or infinite) set of function symbols disjoint from X , each function symbol f being equipped with a type τ (f) ∈ T and an arity α(f) ≤ α(τ (f)). The declaration f n ∶ T indicates the arity n and type T of f. The set L of terms is defined inductively as follows:

• a variable x is a term of type τ (x); • if x is a variable and t is a term of type T , then λxt is a term of type τ (x) → T . We denote by τ (t) the type of a term t, and write t ∶ T when τ (t) = T .

• if f n ∶ T 1 → . . . → T n → U
We usually write f ∶ T for the declaration f 0 ∶ T , omitting the arity n = 0, and f for f(). Note that a term f( ⃗ t) may have a functional type, hence can be applied. Application associates to the left so that tuv is the same as (tu)v.

We use the letters x, y, z, . . . for variables, f, g, . . . for function symbols, and a, b, . . ., s, t, u, v, . . ., t ′ , u ′ , . . . for terms.

We denote by FV(t) the set of free variables in t, by ⊲ the strict subterm relationship on terms, and by ⊴ its reflexive closure. The height of a term t, written t , is the height of its tree representation:

x = 0, f = 0 if α(f) = 0, f( ⃗ t) = 1 + max{ t i 1 ≤ i ≤ α(f)} if α(f) > 0, tu = 1 + max{ t , u } and λxt = 1 + t .

Definition 3.2 (Substitution).

• A substitution is a function σ ∶ X → L such that dom(σ) = {x ∈ X σ(x) ≠ x} is finite and, for every x, τ (σ(x)) = τ (x). As usual, the application of a substitution σ to a term t, written tσ, is defined so as to avoid free-variable captures when renaming some bound variables of t by new variables of the same type [START_REF] Curry | Combinatory logic[END_REF].

• A substitution σ is away from a finite set of variables X if (dom(σ)∪FV(σ))∩X = ∅,
where FV(σ) = ⋃ {FV(σ(x)) x ∈ dom(σ)}. • A relation > on terms (or sequences of terms) is stable by substitution away from X if aσ > bσ whenever a > b and σ is away from X. A relation is stable by substitution if it is stable by substitution away from ∅.

We will use the letters σ, θ, . . . for substitutions, and denote the substitution mapping the variables ⃗

x of its domain to the terms in ⃗ t

(hence ⃗ x = ⃗ t ) by ( ⃗ t ⃗
x ). Note that stability by substitution reduces to the standard definition: > is stable by substitution if aσ > bσ whenever a > b (because any substitution is away from ∅).

The equivalence relation identifying terms up to type-preserving renaming of their bound variables is called α-equivalence and written = α as usual [START_REF] Curry | Combinatory logic[END_REF].

Given a relation R, let SN T (R) be the set of terms of type T from which there is no infinite sequence of R-steps, and SN(R) = ⋃{SNT (R) T ∈ T }.

Relations

One ingredient of CPO is a well-founded quasi-ordering on function symbols and, for each equivalence class generated by the corresponding equivalence relation, a status stat ∈ {mul}∪ {lex(n) n > 2} prescribing how to compare the arguments of two equivalent symbols, by either its multiset [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF] or lexicographic extension. We hereafter recall the necessary definitions and state some simple but important properties of these operations. The product extension is introduced here for technical reasons.

Given a relation ≻ on terms, let:

• ⃗ t ≻ prod ⃗ u if ⃗ t = ⃗ u and there is j ∈ {1, . . . , ⃗ u } s.t. t j ≻ u j and, for all i ≠ j, t i = u i . • ⃗ t ≻ mul ⃗ u if { ⃗ t } (≻ 1 M ) + { ⃗ u } where { ⃗ t } is the multiset made of the elements in ⃗ t and M + { x } ≻ 1 M M + { y 1 , . . . , y n } (n ≥ 0)
if, for all i, x ≻ y i (+ being the multiset union);

• ⃗ t ≻ lex(n) ⃗ u if there is j ∈ {1, .
. . , n} such that t j ≻ u j and, for all i < j, t i = u i . Note that both ≻ mul and ≻ lex(n) may compare all the arguments whatever their types are (from left to right for ≻ lex(n) ). In [START_REF] Blanqui | Termination of rewrite relations on λ-terms based on Girard's notion of reducibility[END_REF], the first author describes a more general version of these statuses that take types into account and allow reordering and filtering of the arguments [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]. We could also consider statuses combining both lexicographic and multiset comparisons [START_REF] Fernández | Modular termination of term rewriting systems revisited[END_REF].

In the following, we will omit n in ≻ lex(n) and simply write ≻ lex .

Here are the properties of statuses we will rely on:

Proposition 4.1. Given a relation ≻ on terms:

• ≻ stat preserves termination: if ≻ is well-founded, then ≻ stat is well-founded.

• ≻ stat contains ≻ prod .

• ≻ stat preserves stability: if ≻ is stable by substitution away from X, then so is ≻ stat .

Computability path ordering

In this section, we give the core definition of the computability path ordering (CPO) before to explore its limits by means of examples and compare it with its father definition, HORPO.

5.1. Definition of core CPO. We assume given:

• an admissible ordering on types >;

• a quasi-ordering ≥ F on F, called precedence, whose equivalence

≥ F ∩ ≥ -1 F is written ≃ F and strict part ≥ F ∖ ≥ -1
F is written > F and assumed well-founded; • for every f ∈ F, a status stat(f) ∈ {mul} ∪ {lex(n) n ≥ 2} such that symbols equivalent in ≃ F have the same status.

Definition 5.1 (Core computability path relation). The core computability path relation is the relation ≻ ∅ τ (≻ τ for short) where:

• the set F b of big symbols is identical to F, 2
• for any given finite set X of variables, ≻ X is inductively defined in Figure 1

, • t ≻ X τ u if t ≻ X u and τ (t) ≥ τ (u), • ⪰ X (resp. ⪰ X τ )
is the reflexive closure of ≻ X (resp. ≻ X τ ). The parameter X serves as a meta-level binder to keep track of the variables that were previously bound in the righthand side but have become free when destructuring a righthand side abstraction. We shall say that a variable x is fresh with respect to a comparison u ≻

X v if x ∈ FV(u) ∪ X ∪ FV(v).
1: Core CPO (F b ⊳) f( ⃗ t) ≻ X v if f ∈ F b and (∃i) t i ⪰ τ v (F b =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f ≃ F g, (∀i) f( ⃗ t) ≻ X u i and ⃗ t (≻ τ ) stat(f) ⃗ u (F b >) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f > F g and (∀i) f( ⃗ t) ≻ X u i (F b @) f( ⃗ t) ≻ X uv if f ∈ F b , f( ⃗ t) ≻ X u and f( ⃗ t) ≻ X v (F b λ) f( ⃗ t) ≻ X λyv if f ∈ F b , f( ⃗ t) ≻ X∪{z} v z y , τ (y) = τ (z) and z fresh (F b X ) f( ⃗ t) ≻ X y if f ∈ F b and y ∈ X (@⊳) tu ≻ X v if t ⪰ X v or u ⪰ X τ v (@=) tu ≻ X t ′ u ′ if t = t ′ and u ≻ X u ′ , or tu ≻ X @ t ′ and tu ≻ X @ u ′ where tu ≻ X @ v if t ≻ X τ v or u ⪰ X τ v or tu ≻ X τ v (@λ) tu ≻ X λyv if tu ≻ X v z y and z fresh (@X ) tu ≻ X y if y ∈ X (@β) (λxt)u ≻ X v if t u x ⪰ X v (λ⊳) λxt ≻ X v if t z x ⪰ X τ v, τ (x) = τ (z) and z fresh (λ=) λxt ≻ X λyv if t z x ≻ X v z y , τ (x) = τ (y) = τ (z) and z fresh (λ≠) λxt ≻ X λyv if λxt ≻ X v z y , τ (x) ≠ τ (y), τ (y) = τ (z) and z fresh (λX ) λxt ≻ X y if y ∈ X (λη) λx(tx) ≻ X v if t ⪰ X v and x ∉ FV(t)
Note that the parameter X is carried along computations without change, except in rule (F b λ). Hence, any comparison u ≻ X v generated from an initial comparison s ≻ ∅ t implies X ∩ FV(u) = ∅.

Explicit variable renamings and the associated freshness conditions are used to make the relation invariant by α-equivalence, the smallest congruence generated by the equation λxt = λyt y x if τ (x) = τ (y) and y ∉ FV(λxt) [START_REF] Curry | Combinatory logic[END_REF], and by appropriate renaming of the variables in X, as we shall prove later.

Note the seemingly complex behaviour of application in rule (@=), which allows to search the lefthand side for appropriate arguments bigger than those of the righthand side. This enhancement of CPO intends to mimic the corresponding rule of HORPO without flattening lefthand sides.

Having function symbols equipped with an arity is more general than having uncurried function symbols (i.e. of null arity) only: any uncurried system can be dealt with as it is. However, in this case, the (F b _) rules are very limited: (F b ⊳) is not applicable, (F b =) and (F b >) reduce to the precedence itself. Moreover, applications of the form f ⃗ t with ⃗ t > 0 can only be compared by using the (@_) rules which are more constrained than the corresponding (F b _) rules, especially (@λ) and (@=). Considering function symbols with non-null arities provides more structure to the terms, and this structure can be used for proving termination [START_REF] Hirokawa | Uncurrying for termination[END_REF]. Lemma 6.4 below will show that FV(v) ⊆ FV(u) ∪ X whenever u ≻ X v. Hence, an alternative formulation of rules (@λ) and (λ≠) could therefore be given by replacing the condition "z fresh" by y ∉ FV(v).

Another, perhaps surprising fact is that the definition of core CPO can be simplified by replacing ≻ X by ≻ everywhere but in (F b λ). This is true at the start since we are interested in ≻ τ . This is then an invariant of the computation, for two reasons: X is never increased, except in (F b λ); X is reset to the empty set by (F b ⊳) and (F b =), which are the only rules which may move from a (F b ) comparison to a (@) or (λ) comparison. We could therefore simplify our definition by removing the superfluous X subscripts. This will however no more be true of the extension of core CPO to inductive types, and we prefer to have a uniform definition over the various sections. Further, the present definition will allow us to study a relaxation of (@λ) in the next section.

Surprisingly, core CPO is powerful enough already to prove termination of examples that usually require techniques like the ones developed in Section 7.

Example 5.2. Consider the breadth-first search of labeled trees using continuations [START_REF] Hofmann | Approaches to recursive data types -a case study[END_REF], using the sorts L for lists of labels and C for continuations, the abbreviation ¬T = T → L, and the symbols d ∶ C and c 1 ∶ ¬¬C → C for building continuations. Let now e ∶ ¬C defined by the rule: e c(x) → x e

Its termination can be checked by core CPO by taking C ≥ L and c > F e. Indeed, e c(x) ≻ τ x e holds by (@⊳) since c(x) ≻ τ x e for τ (c(x)) = C ≥ τ (x e) = L and, by (F b @), c(x) ≻ x by (F b ⊳), and c(x) ≻ e by (F b >). 5.2. Transitivity. As HORPO, core CPO is not transitive (both include β-reduction which is not transitive). Adding transitivity as a rule yields non-termination as shown by the following counter-example: Example 5.3. In the premises of (F b @), replace ≻ X by (≻ X ) + . Then, in the system S1 described at the beginning of next section, we have: Similar counter-examples can be built as well for (F b >) and (F b =), since the key point is that, by using (≻ X ) + , we can apply case (F b ⊳) without requiring type decreasingness.

Useful implemented heuristics for under-approximating ≻ + τ are discussed in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. The introduction of small symbols in Section 8 will reduce the need for such heuristics, although not completely. On the other hand, we will show soon that core CPO is a well-founded relation on terms. So is therefore its transitive closure. 5.3. Tightness of core CPO. In this section, we show that almost all possible relaxations (by replacing ≻ τ by ≻, and ≻ by ≻ X ) of the above definition lead to non-termination by providing appropriate examples that are also meant to help understanding how CPO works. To this end, we will consider three different systems, using o ∶ * to declare a sort o:

S1: o ∶ * ; a ∶ o, f 1 ∶ o → o, g ∶ o → o → o; a > F f > F g. S2: o, o ′ ∶ * ; a ∶o, f 1 ∶o → o, j 1 ∶(o ′ → o → o) → o; a > F f > F j. S3: o ∶ * ; a ∶ o, h 2 ∶ o → o → o, k 2 ∶ (o → o) → o → o; a > F h ≃ F k; stat(h)= stat(k)= mul.
For each rule, we now consider all its natural relaxations.

• (F b ⊳) f( ⃗ t) ≻ X v if (∃i)t i ⪰ τ v -Replace ⪰ τ by ⪰ X τ .
Then, in S1, we have:

a ⪰ {x} τ f(x) since τ (a) = o ≥ τ (f(x)) = o and, by (F b >), a ≻ {x} x by (F b X ), (b) f(a) ≻ a by (F b ⊳). (2) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β).
-Replace ⪰ τ by ⪰. Then, in S1, we have:

F b >), a ≻ {x} x by (F b X ) (b) f(a) ≻ a by (F b ⊳). (2) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β). • (F b =) f( ⃗ t) ≻ X g(⃗ u) if f ≃ F g, f( ⃗ t) ≻ X ⃗ u and ⃗ t (≻ τ ) stat(f) ⃗ u -Replace ≻ τ by ≻ X τ . Then, in S1, we have: (1) f(a) ≻ τ (λxf(x))a since τ (f(a)) = o ≥ τ ((λxf(x))a) = o and, by (F b @): (a) f(a) ≻ λxf(x) since, by (F b λ), x ∉ FV(f(a)) and: (i) f(a) ≻ {x} f(x) since, by relaxing (F b =): f(a) ≻ {x} x by (F b X ), a ≻ {x} τ x since τ (a) = o ≥ τ (x) = o and by (F b X ), (b) f(a) ≻ a by (F b ⊳), (2) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β).
-Replace ≻ τ by ≻. We found no counter-example for this case, but this is due to the condition f( ⃗ t) ≻ X ⃗ u. If we consider (F b =mul) and (F b =lex) instead, then simple counter-examples like the following one in S3 come up.

(1) h(a, a)

≻ τ k(λxh(x, x))a since τ (h(a, a)) = o ≥ τ (k(λxh(x, x))a) = o and, by relaxing (F b =mul), {a, a} (≻) mul {λxh(x, x), a}, since a ≻ λxh(x, x), by case (F b λ) because a ≻ {x} x by case (F b X ). (2) k(λxh(x, x))a ≻ τ (λxh(x, x))a since τ (k(λxh(x, x))a) = o ≥ τ ((λxh(x, x))a) = o and by case (F b @), since (a) k(λxh(x, x))a ≻ λxh(x, x) by (F b ⊳). (b) k(λxh(x, x))a ≻ a by (F b ⊳). (3) (λxh(x, x))a ≻ τ h(a, a) since τ ((λxh(x, x))a) = o ≥ τ (h(a, a)) = o
and by (@β). Note that this counter-example can be also applied on case (F b =lex) if we take stat(h) = stat(k) = lex. Unfortunately it does not work on (F b =) since we cannot prove h(a, a) ≻ λxh(x, x).

• (@⊳) tu ≻ X v if t ⪰ X v or u ⪰ X τ v -Replace ⪰ X τ by ⪰ X . Then, in S1, we have: (1) f(a) ≻ τ gaa since τ (f(a)) = o ≥ τ (gaa) = o and, by (F b @): (a) f(a) ≻ ga since, by (F b @): (i) f(a) ≻ g by (F b >), (ii) f(a) ≻ a by (F b ⊳), (b) f(a) ≻ a by 1(a)ii, (2) gaa ≻ τ (λxf(x))a since τ (gaa) = o ≥ τ ((λxf(x))a) = o and, by (@=): (a) ga ≻ τ λxf(x) since τ (ga) = o → o ≥ τ (λxf(x)) = o → o and, by relaxing (@⊳): (i) a ≻ λxf(x) since, by (F b λ): a ≻ {x} f(x) since, by (F b >), a ≻ {x} x by (F b X ), (3) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β). • (@=) tu ≻ X t ′ u ′ if if t = t ′ and u ≻ X u ′ , or tu ≻ X @ t ′ and tu ≻ X @ u ′ , where tu ≻ X @ v if t ≻ X τ v or u ⪰ X τ v or tu ≻ X τ v tu (≻ τ ) mul t ′ u ′ . -Replace tu ≻ X τ t ′ by tu ≻ X t ′ .
Then, taking t ∶ o → o, we get tu ≻ τ tu since, by relaxing (@=), we have tu ≻ t by (@⊳).

-Replace tu ≻ X τ t ′ by tu ≻ X t ′ . Then, taking t ∶ (o → o) → o, we get tu ≻ τ tu since, by relaxing (@=), we have tu ≻ u by (@⊳).

-We found no counter-example yet for the other cases.

• (@λ) tu ≻ X λyv if tu ≻ X v z y , τ (y) = τ (z) and z fresh -Replace ≻ X by ≻ X∪{z} . Then, in S1, we have: (1) f(a) ≻ τ gaa since τ (f(a)) = o ≥ τ (gaa) = o and, by (F b @): (a) f(a) ≻ ga since, by (F b @): (i) f(a) ≻ g by (F b >), (ii) f(a) ≻ a by (F b ⊳), (b) f(a) ≻ a by 1(a)ii, (2) gaa ≻ τ (λxf(x))a since τ (gaa) = o ≥ τ ((λxf(x))a) = o and, by (@=): (a) ga ≻ τ λxf(x) since τ (ga) = o → o ≥ τ (λxf(x)) = o → o and, by relaxing (@λ): (i) ga ≻ {x} f(x) since, by (@⊳): a ≻ {x} f(x) since, by (F b >), a ≻ {x} x by (F b X ), (3) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β). • (λ⊳) λxt ≻ X v if t y x ⪰ X τ v, τ (x) = τ (y) and y fresh -Replace ⪰ X τ by ⪰ X . Then, in S2, we have: (1) f(a) ≻ τ j(λxλya) since τ (f(a)) = o ≥ τ (j(λxλya)) = o and, by (F b >): (a) f(a) ≻ λxλya since, by (F b λ) twice: (i) f(a) ≻ {x,y} a by (F b ⊳), (2) j(λxλya) ≻ τ (λzf(z))a since τ (j(λxλya)) = o ≥ τ ((λzf(z))a) = o and, by (F b @): (a) j(λxλya) ≻ λzf(z) since, by (F b ⊳): (i) λxλya ≻ τ λzf(z) since τ (λxλya) = o ′ → o → o ≥ τ (λzf(z)) = o → o
and, by relaxed (λ⊳), x ∉ FV(λzf(z)) and: λya ≻ λzf(z) since, by relaxed (λ⊳), y ∉ FV(λzf(z)) and a ≻ λzf(z) since, by (

F b λ), a ≻ {z} f(z) since, by (F b >), a ≻ {z} z by (F b X ), (b) j(λxλya) ≻ a since, by (F b ⊳): (i) λxλya ≻ τ a since τ (λxλya) = o ′ → o → o ≥ τ (a) = o and, by (λ⊳),
x ∉ FV(a) and:

λya ≻ τ a since τ (λya) = o → o ≥ τ (a) = o and, by (λ⊳)again. (3) (λzf(z))a ≻ τ f(a) since τ ((λzfz)a) = o ≥ τ (f(a)) = o and, by (@β). • (λ≠) λxt ≻ X λyv if λxt ≻ X v z y , τ (y) ≠ τ (z) and z fresh -Replace ≻ X by ≻ X∪{z} . Then, in S2, we have: (1) f(a) ≻ τ j(λxλya) since τ (f(a)) = o ≥ τ (j(λxλya)) = o, by (F b >): (a) f(a) ≻ λxλya since, by (F b λ) twice: (i) f(a) ≻ a by (F b ⊳), (2) j(λxλya) ≻ τ (λzf(z))a since, by (F b @): (a) j(λxλya) ≻ λzf(z) since, by (F b ⊳): (i) λxλya ≻ τ λzf(z) since τ (λxλya) = o ′ → o → o ≥ τ (λzf(z)) = o → o and, by relaxing (λ≠): λxλya ≻ {z} f(z) since, by (λ⊳), λya ≻ {z} τ f(z) since τ (λya) = o → o ≥ τ (f(z)) = o and by (λ⊳) again, a ≻ {z} τ f(z) since τ (a) = o ≥ τ (f(z)) = o and, by (F b >), a ≻ {z} z by (F b X ), (b) j(λxλya) ≻ a since, by (F b ⊳): (i) λxλya ≻ τ a since τ (λxλya) = o ′ → o → o ≥ τ (a) = o and, by (λ⊳): λya ≻ τ a since τ (λya) = o → o ≥ τ (a) = o and, by (λ⊳) again. (3) (λzf(z))a ≻ τ f(a) by (@β).
-Remove the condition τ (x) ≠ τ (y).

Then, in S1, we have τ (λxa) ≥ τ (λxb) and λxa ≻ τ λxa by the relaxed (λ≠) since λxa ≻ a by (λ⊳).

Comparison with HORPO.

In [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], the last two authors define a relation on simplytyped polymorphic λ-terms, > horpo , and its extension > chorpo using the notion of computability closure introduced in [START_REF] Blanqui | Inductive-data-type systems[END_REF]. In this section, we explain the differences between CPO and > horpo . We will compare CPO with > chorpo in Section 7.3.

• Type discipline. > horpo and > chorpo are relations on simply-typed polymorphic λterms, where types may contain type variables that have to be instantiated when forming function calls, while CPO is a relation on simply-typed monomorphic λterms. In the following, we will therefore compare CPO with the monomorphic versions of > horpo and > chorpo . Extending CPO to polymorphic types along the lines of [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF] is routine. • Relation on types. In [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], the relation ≥ on types must be a quasi-ordering satisfying the following conditions 3 , where > = ≥ ∖ ≥ -1 is its strict part and ≃ = ≥ ∩ ≥ -1 its associated equivalence relation:

(

1) > is well-founded; (2) T → U ≃ V implies V = T ′ → U ′ with T ≃ T ′ and U ≃ U ′ ; (3) T → U > V implies U ≥ V or V = T ′ → U ′ with T ≃ T ′ and U > U ′ ; (4) T ≥ T ′ implies T → U ≥ T ′ → U and U → T ≥ U → T ′ .
It turns out that these conditions are inconsistent: if T > U then, by (4), T → V > U → V and, by (3), V ≥ U → V , which is impossible by (1) [START_REF] Kop | [END_REF]. However, the results of [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF] are still true since property ( 4) is only used to build the simplification ordering ⋗4 used for defining the interpretation of types. Instead, now, we distinguish between > which must contain ⊳ r and satisfy (3)/(typ-arrow) (( 2) is always satisfied when ≤ is an ordering instead of a quasi-ordering), and ⋗ which must contain > ∪ ⊳ l and be well-founded. The monotony property (4) is not required anymore.

In [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], > horpo and > chorpo are proved well-founded not only on well-typed terms but on a larger set of terms called candidate terms, obtained by identifying equivalent types. Since, by ( 2), the arrow structure of equivalent types is invariant, the quotient of the set of types by ≃ can be obtained by simply identifying sorts equivalent in ≃, and the quasi-order becomes then an order in the quotient structure. Since rewriting on candidate terms coincides with rewriting in the quotient, an order on types suffices, which removes the need for candidate terms and their technicalities.

• Relation on terms. One important difference between HORPO and CPO is that, in all sub-derivations of > horpo , types must decrease (t

> horpo u only if τ (t) ≥ τ (u))
while, in CPO, this is not the case: types must be checked only in case the recursive call takes a subterm of the lefthand side term (except in (@⊳) for the left argument of an application). Indeed, CPO is an optimized version of > horpo in this respect. > horpo is defined by a set of 12 rules and each rule but ( 9) is implied by a rule of CPO: 5) by (@⊳), ( 6) by (λ⊳), ( 7) by (F b @), ( 8) by (F b λ) (HORPO requires the strong condition x ∉ FV(v) since it does not manage bound variables; this is however done by the computability closure in CHORPO), ( 10) by (λ=), ( 11) by (@β) and ( 12) by (λη).

(1) is implied by (F b ⊳), (2) by (F b >), (3) by (F b =) with stat(f) = mul, (4) by (F b =) with stat(f) = lex, (
Rule (9) compares st and u 1 . . . u n with n ≥ 2 by comparing the multisets { s, t } and { u 1 , . . . , u n }. It is implied by (@=). Indeed, in this case, for all i, either s ⪰ τ u i or t ⪰ τ u i . If there is no i such that s = u i then, for all i, s ≻ τ u i or t ⪰ τ u i , in which case one can prove that st ≻ τ u 1 . . . u k by induction on k. If s = u 1 then, for all i ≥ 2, t ≻ τ u i , in which case one can also prove that st ≻ τ u 1 . . . u k by induction on k. Otherwise, there is i > 1 such that s = u i and t ≻ τ u 1 . But, then, τ (s) ⋗ τ (t) ≥ τ (u 1 ) ⋗ τ (s), which is not possible by (typ-sn).

On the other hand, the CPO rules (λ≠), (@λ), (F b X ), (@X ), (λX ) have no counterpart in HORPO. Therefore, HORPO is strictly included in CPO.

Implementation.

All examples given in the paper have been checked by our implementation, which is available from the web at http://www.lsi.upc.edu/~albert/cpo.zip. In this implementation the precedence and the status should be provided by the user. The implemented prototype includes core CPO as well as the extended versions of the ordering defined in Section 7 and 8. Several more examples are also included together with the implementation showing the power of the developed orderings. However, like RPO, CPO cannot be compared with transformation techniques based on, for instance, the computation of dependency pairs [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF][START_REF] Giesl | Mechanizing and improving dependency pairs[END_REF], but its power shows that it should be the path ordering of choice for solving the (monotonic) ordering comparisons which are generated by these transformation techniques.

Given a precedence and a status for every function symbol, deciding if a term s is smaller than a term t in core CPO can be made in quadratic time (using a dynamic programming algorithm) if (@β) is not used. The proof is basically the same as for RPO [START_REF] Krishnamoorthy | On recursive path ordering[END_REF]. Our prototype implementation written in Prolog does not use dynamic programming. Still, some standard optimizations over the given presentation are made, which mainly affect case (F b =). Let us split this case in two new cases, one for multiset status (F b =mul) and one for lexicographic status (F b =lex), and show that even after removing all or part of the condition f( ⃗ t) ≻ X ⃗ u, the conjunction of both cases is equivalent to the original one.

(F b =mul) f( ⃗ t) ≻ X g(⃗ u) if f ≃ F g, stat(f) = mul and ⃗ t (≻ τ ) mul ⃗ u (F b =lex) f( ⃗ t) ≻ X g(⃗ u) if f ≃ F g, stat(f) = lex and: (∃i) t i ≻ τ u i ∧ (∀j < i) t j = u j ∧ (∀j > i) f( ⃗ t) ≻ X u j In case (F b =mul), ⃗ t (≻ τ ) mul ⃗ u implies that, for every u j , there is t i such that t i ⪰ τ u j , which implies that f( ⃗ t) ≻ X u j by (F b ⊳). Similarly, in case (F b =lex), there is i such that t i ≻ τ u i , (∀j < i) t j = u j and (∀j > i) f( ⃗ t) ≻ X u j , which implies (∀j) f( ⃗ t) ≻ X u j by (F b ⊳). Therefore, we have f( ⃗ t) ≻ X ⃗
u and hence case (F b =) can be applied as well. As said, our implementation assumes that the precedence on function symbols and the status is given. Generating the precedence and the status automatically is a harder problem, and closely relates to the decision problem of solving ordering constraints, which is already NP-complete for RPO [START_REF] Nieuwenhuis | Simple LPO constraint solving methods[END_REF][START_REF] Narendran | RPO constraint solving is in NP[END_REF], but which is nowadays efficiently done in practice by encoding the problem into SAT [START_REF] Codish | SAT solving for termination proofs with recursive path orders and dependency pairs[END_REF]. These kind of encodings can be easily adapted to CPO, as done for HORPO in termination tools like WANDA [START_REF] Kop | Higher order termination[END_REF] and THOR [START_REF] Borralleras | THOR, a tool for proving the termination of higher-order rewrite systems[END_REF].

Well-foundedness of core CPO

We now move to a technical analysis of the most important properties of core CPO.

6.1. Basic properties of core CPO. Lemma 6.1. ≻ X is well-defined.

Proof. a ≻ X b is well-defined by induction on the pair (a, b) with (= α ⊳ ∪ → β ∪ → η , = α ⊳) lex as well-founded relation, where ⊲ is the subterm relation. Definition 6.2 (Monotony). We say that ≻ τ is monotone if the following properties hold:

(1) if f ⃗ T ∶ ⃗ T → U , ⃗ t ∶ ⃗ T , ⃗ t ′ ∶ ⃗ T and ⃗ t (≻ τ ) prod ⃗ t ′ , then f( ⃗ t) ≻ τ f( ⃗ t ′ ); (2) if t ∶ U → V , t ′ ∶ U → V ′ , t ≻ τ t ′ , u ∶ U and V ≥ V ′ , then tu ≻ τ t ′ u; (3) if t ∶ U → V , u, u ′ ∶ U and u ≻ τ u ′ , then tu ≻ τ tu ′ ; (4) if t ∶ T , t ′ ∶ T ′ , t ≻ τ t ′ and τ (x) → T ≥ τ (x) → T ′ , then λxt ≻ τ λxt ′ . Lemma 6.3. ≻ τ is monotone. Proof. (1) Since τ (f( ⃗ t)) = τ (f( ⃗ t ′ )), it suffices to check that f( ⃗ t) ≻ f( ⃗ t ′ ). By Lemma 4.1, ⃗ t (≻ τ ) stat(f) ⃗ t ′ . By (F b ⊳), f( ⃗ t) ≻ ⃗ t ′ since, for each i, t i ⪰ τ t ′ i .
We conclude by (F b =). (2) Since τ (tu) ≥ τ (t ′ u), it suffices to check that tu ≻ t ′ u. This follows by by (@=).

(3) Since τ (tu) = τ (tu ′ ), it suffices to check that tu ≻ tu ′ . This follows by (@=). ( 4) By (λ=).

Note that Lemma 6.3 holds for any relation satisfying (F b ⊳), (F b =), (@=) and (λ=).

Lemma 6.4. If a ≻ X b, then FV(b) ⊆ FV(a) ∪ X.
Proof. By an easy induction on a ≻ X b. We detail a selection of cases:

• (F b λ) By the induction hypothesis, FV(v z y ) ⊆ FV(f( ⃗ t)) ∪ X ∪ {y}. Now, FV(λyv) = FV(v z y ) ∖ {z} since z is fresh. The result follows. • (λ⊳) By the induction hypothesis, FV(v) ⊆ FV(t z x ) ∪ X. Therefore, FV(v) ⊆ FV(λxt) ∪ X since FV(t z x ) ⊆ FV(λxt) ∪ {z} and z ∉ FV(v). • (λ=) By the induction hypothesis, FV(v z y ) ⊆ FV(t z x ) ∪ X. Now, FV(t z x ) ⊆ FV(λxt) ∪ {z} and, either y ∈ FV(v) and FV(v z y ) = FV(λyv) ∪ {z}, or FV(v z y ) = FV(λyv). Therefore, FV(λyv) ⊆ FV(λxt) ∪ X since z ∉ FV(λyv). • (λ≠) By the induction hypothesis, FV(v z y ) ⊆ FV(λxt) ∪ X. Since z is fresh for λxt, X and λyv, y ∉ FV(v). Therefore, FV(λyv) = FV(v) -{y} ⊆ FV(λxt) ∪ X. Lemma 6.5. If a ≻ X b, a = α a ′ and b = α b ′ , then a ′ ≻ X b ′ . Proof. We prove (i) a ≻ X b and a = α a ′ implies a ′ ≻ X b, and (ii) a ≻ X b and b = α b ′ implies a ≻ X b ′ ,
separately by induction on a ≻ X b. We only detail some cases:

• (F b λ) (ii) Assume that λyv = α b ′ . Then, there are y ′ and v ′ such that b ′ = λy ′ v ′ , y ∉ FV(λy ′ v ′ ) and v = α v ′ y y ′ . Hence, v z y = α v ′ y y ′ z y = α v ′ z y ′ and, by the induction hypothesis, f( ⃗ t) ≻ X∪{z} v ′ z y ′ . Now, z ∉ FV(λy ′ v ′ ) ∪ FV(f( ⃗ t)) since FV(λy ′ v ′ ) = FV(λyv) and z ∉ FV(λyv) ∪ FV(f( ⃗ t)). Therefore, by (F b λ), f( ⃗ t) ≻ X λy ′ v ′ . • (λ⊳) (ii) Assume that v = α v ′ . By the induction hypothesis, t z
x ⪰ X τ v ′ . Now, z is fresh for λxt, X and v ′ since FV(v ′ ) = FV(v) and z is fresh for λxt, X and v. Therefore, by (λ⊳), λxt ≻ X v ′ .

(i) Assume now that λxt = α a ′ . Then, there are x ′ and t ′ such that a

′ = λx ′ t ′ , x ∉ FV(λx ′ t ′ ) and t = α t ′ x x ′ . Hence, t z x = α t ′ x x ′ z x = α t ′ z
x ′ and, by the induction hypothesis, t ′ z x ′ ⪰ X τ v. Now, z is fresh for λx ′ t ′ , X and v since FV(λx ′ t ′ ) = FV(λxt) and z is fresh for λxt, X and v. Therefore, by (λ⊳

), λx ′ t ′ ≻ X v. • (λ=) (ii) Assume that λyv = α b ′ . Then, there are y ′ and v ′ such that b ′ = λy ′ v ′ , y ∉ FV(λy ′ v ′ ) and v = α v ′ y y ′ . Hence, v z y = α v ′ z y ′ z y = α v ′ z y ′
and, by the induction hypothesis, t z x ≻ X v ′ z y ′ . Now, z is fresh for λxt, X and λy ′ v ′ since FV(λy ′ v ′ ) = FV(λyv) and z is fresh for λxt, X and λyv. Therefore, by (λ=), λxt

≻ X λy ′ v ′ . • (λ≠) (ii) Assume that λyv = α b ′ . Then, there are y ′ and v ′ such that b ′ = λy ′ v ′ , y ′ ∉ FV(λyv) and v y ′ y = α v ′ . By Lemma 6.4, y ∉ FV(v). Hence, y ′ ∉ FV(v ′ ), v z y = α v ′ z y ′ and, by the induction hypothesis, λxt ≻ X v ′ z y ′ . Moreover, z is fresh for λxt, X and λy ′ v ′ . Therefore, by (λ≠), λxt ≻ X λy ′ v ′ .
Hence, if t ≻ X u and V is a finite set of variables, then one can always assume without lost of generality that the bounding variables of t and u do not belong to V .

Invariance by variable renaming can also be extended to X: Lemma 6.6. Assume that t ≻ X u.

(1) If σ is away from X, then tσ ≻ X uσ.

(2) If e ∈ X, e ′ ∉ FV(λeu) and τ (e) = τ (e ′ ), then t ≻ X-{e}∪{e ′ } u e ′ e .

Proof. Note that substitution preserves typing (τ (tσ) = τ (t)). Let X e ′ e = X -{e} ∪ {e ′ }. Wlog we can assume that e ≠ e ′ . Hence, e ′ ∉ FV(u). We now proceed by induction on the deduction height of t ≻ X u. We only detail some cases:

(1) (F b =) By induction hypothesis and Lemma 4.1, (∀i)

f( ⃗ t)σ ≻ X u i σ and ⃗ tσ (≻ τ ) stat(f) ⃗ uσ. Therefore, by (F b =), f( ⃗ t)σ ≻ X g(⃗ u)σ. (F b λ)
Wlog we can assume σ away from {y}. Hence, (λyv)σ = λy(vσ). Let now z ′ be a variable of the same type as z, fresh for f( ⃗ t)σ, X, λy(vσ) and λzv z y = α λyv, and such that σ is away from

{z ′ }. By induction hypothesis (2), f( ⃗ t) > (X∪{z}) z ′ z (v z y ) z ′ z . Since z ∉ X, (X ∪ {z}) z ′ z = X ∪ {z ′ }. Since ( z ′ z ) is away from {y} and z ∉ FV(v), (v z y ) z ′ z = v z ′ y . By induction hypothesis, f( ⃗ t)σ > X∪{z ′ } (v z ′ y )σ. Since σ is away from {y, z ′ }, (v z ′ y )σ = (vσ) z ′ y . Therefore, by (F b λ), f( ⃗ t)σ ≻ X λy(vσ).
(λ⊳) Wlog we can assume that σ is away from {x}. Hence, (λxt)σ = λx(tσ). After Lemma 6.4 and since σ is away from X, FV(v) ⊆ FV(λxt). Hence, we can also assume wlog that dom(σ) ⊆ FV(λxt). Let now z ′ be a variable of the same type as z, fresh for λx(tσ), X, vσ and x, and such that σ is away from

{z ′ }. Let σ ′ = σ ∪ {(z, z ′ )}. Since σ ′ is away from X, by induction hypothesis, (t z x )σ ′ ≻ X vσ ′ . Since dom(σ) ⊆ FV(λxt) and σ is away from {x, z ′ }, (t z x )σ ′ = (tσ) z ′
x , and since z ∉ FV(v), vσ ′ = vσ. Therefore, by (λ=), λx(tσ) ≻ X vσ.

(λ=) Wlog we can assume that σ is away from {x, y}. Hence, (λxt)σ = λx(tσ) and

(λyv)σ = λy(vσ). After Lemma 6.4 and since σ is away from X, FV(λyv) ⊆ FV(λxt). Hence, we can also assume wlog that dom(σ) ⊆ FV(λxt). Let now z ′ be a variable of the same type as z, fresh for λx(tσ), X, λy(vσ), x and y, and such that σ is away from {z ′ }. Let σ ′ = σ∪{(z, z ′ )}. Since σ ′ is away from X, by induction hypothesis, (t z x )σ ′ ≻ X (v z y )σ ′ . Since dom(s) ⊆ FV(λxt), dom(σ) ⊆ FV(λyv), and σ is away from {x, y, z ′ }, (t z x )σ ′ = (tσ) z ′ x and (v z y )σ ′ = (vσ) z ′ y . Therefore, by (λ=), (λxt)σ ≻ X (λyv)σ.

(λ≠) Wlog we can assume σ away from {x, y}. Hence, (λxt)σ = λx(tσ) and (λyv)σ = λy(vσ). Let z ′ fresh for λxtσ, X and λyvσ. By Lemma 6.4, y ∉ FV(v), hence v z y = v z ′ y . By induction hypothesis, (λxt)σ ≻ X v z ′ y σ. Therefore, by (λ≠), λx(tσ) ≻ X λy(vσ).

(2) (F b λ) Wlog we can assume ( e ′ e ) away from {y}. Hence, (λyv) e ′ e = λy(v e ′ e ). Let now z ′ be a variable of the same type as z, fresh for f( ⃗ t), X e ′ e , λy(v e ′ e ), λzv z y = α λyv and y. By induction hypothesis,

f( ⃗ t) ≻ (X∪{z}) z ′ z (v z y ) z ′ z . Since z ∉ X, (X∪{z}) z ′ z = X∪{z ′ }. Since z ∉ FV(λyv), (v z y ) z ′ z = v z ′ y . By induction hypothesis, f( ⃗ t) ≻ (X∪{z ′ }) e ′ e (v z ′ y ) e ′ e . Since ( e ′ e ) is away from {y, z ′ }, (X ∪ {z ′ }) e ′ e = X e ′ e ∪ {z ′ } and (v z ′ y ) e ′ e = (v e ′ e ) z ′ y . Therefore, by (F b λ), f( ⃗ t) ≻ X e ′
e λyv e ′ e . (λ⊳) Let z ′ be a variable of the same type as z, fresh for λxt, X, X e ′ e , v e ′ e and x. Since ( z ′ z ) is away from X, by induction hypothesis (1),

(t z x ) z ′ z ⪰ X τ v z ′ z . Since z ′ ≠ x and z ∉ FV(t), (t z x ) z ′ z = t z ′ x . Since z ∉ FV(v), v z ′ z = v. So, by induction hypothesis, t z ′ x ⪰ X e ′ e τ v e ′
e . Therefore, by (λ⊳), λxt ≻ X e ′ e v e ′ e . (λ=) Wlog we can assume ( e ′ e ) away from {y}. Hence, (λyv) e ′ e = λy(v e ′ e ). Let now z ′ be a variable of the same type as z, fresh for λxt, X, X e ′ e , λyv e ′ e , x and y. Since ( z ′ z ) is away from X, by induction hypothesis (1),

(t z x ) z ′ z ≻ X (v z y ) z ′ z . Since z ′ ≠ x and z ∉ FV(t), (t z x ) z ′ z = t z ′ x . Since z ′ ≠ y and z ∉ FV(v), (v z y ) z ′ z = v z ′ y . So, by induction hypothesis, t z ′ x ≻ X e ′ e (v z ′ y ) e ′ e .
Since ( e ′ e ) is away from {y, z ′ }, (v z ′ y ) e ′ e = (v e ′ e ) z ′ y . Therefore, by (λ=), λxt ≻ X e ′ e λy(v e ′ e ). (λ≠) Wlog we can assume ( e ′ e ) away from {y}. Hence, (λyv) e ′ e = λy(v e ′ e ). Let z ′ fresh for λxt, X e ′ e and λy(v e ′ e ). By Lemma 6.4, y ∉ FV(v), hence v z y = v z ′ y . By the induction hypothesis, λxt ≻ X e ′ e (v z ′ y ) e ′ e = (v e ′ e ) z ′ y . Therefore, by (λ≠), λxt ≻ X e ′ e λy(v e ′ e ).

6.2. Tait and Girard's computability. We now turn to the proof that ≻ τ is well-founded. This proof is based on the meticulous analysis of the technique of computability predicates of Tait and Girard for proving the termination of β-reduction in typed λ-calculi [START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF][START_REF] Girard | Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur[END_REF][START_REF] Tait | A realizability interpretation of the theory of species[END_REF][START_REF] Girard | Proofs and types[END_REF]. This technique consists in the following three steps:

(1) interpret each type T by a set T of so-called computable terms;

(2) prove that, for every type T , T satisfies some properties among which termination, i.e. T ⊆ SN(≻ τ ); (3) prove that every (well typed) term is computable. For arrow types, we will use the standard interpretation but, for sorts, we a priori have some freedom and we will indeed use this freedom to extend CPO to inductive types later in Section 7. Definition 6.7 (Computability). A base type interpretation is a map I ∶ S → P(L) such that, for all sorts A, I(A) is a set of terms of type A. A base type interpretation naturally extends to types as follows:

•

A I = I(A) • U → V I = {t ∈ L t ∶ U → V ∧ (∀u)u ∈ U I ⇒ tu ∈ V I } Given a base type interpretation I, we say that: • a term t ∶ T is I-computable if t ∈ T I ; • a substitution σ is I-computable on a set X of variables if, for all x ∈ X, xσ is I-computable; it is I-computable if it is I-computable on X ; • a function symbol f ⃗ T ∶ ⃗ T ⇒ U is I-computable if, for all I-computable terms ⃗ t ∶ ⃗ T , f( ⃗ t) is I-computable. Let Σ I be the set of pairs (f, ⃗ t) such that f ∈ F, f( ⃗ t) is a term and ⃗ t are I-computable. Given a relation on terms R, let (> F , R stat ) lex be the relation on Σ I such that (f, ⃗ t) (> F , R stat ) lex (g, ⃗ u) if either f > F g, or f ≃ F g and ⃗ t R stat(f) ⃗ u.
Our first lemma has a straightforward proof: Lemma 6.8. Let I 1 and I 2 be two base type interpretations, and T be a type. Then, T I 1 = T I 2 if I 1 and I 2 agree on every sort occurring in T .

We then consider the following properties: Definition 6.9 (Sets of neutral terms). A set N is a set of neutral terms if it satisfies the following properties:

• X ⊆ N (neutral-var) • for all x, t, u, (λxt)u ∈ N (neutral-beta)

• if t ∈ N then, for all u, tu ∈ N (neutral-app) • for all x and t, λxt ∉ N (neutral-not-lam) Definition 6.10 (Computability properties). Given a base type interpretation I and a set N of neutral terms, a set S of terms of type T is an I-computability predicate if it satisfies the following properties:

• S ⊆ SN(≻ τ ) (comp-sn) • If t ∈ S, then every ≻ τ -reduct of t is I-computable (comp-red) • t ∈ S if t ∶ T , t ∈ N and every ≻ τ -reduct of t is I-computable (comp-neutral) • λxt ∈ S if T = U → V , λxt ∶ T and, for all u ∈ U I , t u
x is I-computable (comp-lam) We can then prove that every term is strongly normalizing if the sets T I satisfy some of these properties and function symbols are I-computable, whatever the base type interpretation I and the set N of neutral terms are: Theorem 6.11. Given a base type interpretation I and a set N of neutral terms, ≻ τ is well-founded if:

• for every type T , T I satisfies (comp-sn), (comp-neutral) and (comp-lam);

• every function symbol f ∈ F is I-computable.

Proof. Because, for every T , T I satisfies (comp-sn), it suffices to prove that every term is I-computable. By (neutral-var), variables belongs to N . Because, for every T , T I satisfies (comp-neutral), variables are computable. Hence, the identity substitution is computable.

We then prove that, for all t ∶ T and computable σ, tσ ∈ T I , by induction on t.

• t = x. Then, tσ = xσ is computable since σ is computable.

• t = uv. By induction hypothesis, uσ and vσ are computable. Therefore, tσ = (uσ)(vσ) is computable. • t = λxu with x ∶ V . By renaming x, we can assume that σ is away from {x}.

Hence, tσ = λx(uσ). By assumption, T I satisfies (comp-lam). Therefore, tσ is computable if, for all computable v ∶ V , (uσ) v x is computable. Since σ is away from {x}, (uσ) v x = u(σ ∪ {(x, v)}) which is computable by induction hypothesis.

• t = f( ⃗ t) with f ⃗ T ∶ ⃗ T → U .
By induction hypothesis, ⃗ tσ are computable. Thus, (f, ⃗ tσ) ∈ Σ and, by assumption, f( ⃗ t)σ is computable.

We are therefore left to find a set of neutral terms N and a base type interpretation I so that type interpretations are computability predicates and function symbols are computable.

First, we are going to study under which conditions the interpretation of an arrow type U → V , U → V I , satisfies the above computability properties, whatever the base type interpretation I and the set of neutral terms N are.

Second, we will define a set of neutral terms N and a base type interpretation I so that, for every type T , T I satisfies all the computability properties. Finally, we will prove that function symbols are computable by induction on (> F , (≻ τ ) stat ) lex , which is well-founded when the following conditions are satisfied: Lemma 6.12. Given a base type interpretation I and a well-founded relation on

I-computable terms R, (> F , R stat ) lex is well-founded if, for all f ⃗ T ∶ ⃗ T → U , ⃗ T I ⊆ SN(R). Proof. If (f, ⃗ t) ∈ Σ I , then ⃗ t ∈ ⃗ T I .
By assumption, ⃗ T I ⊆ SN(R). Hence, by Lemma 4.1, ⃗ t ∈ SN(R stat(g) ) whatever g is. Assume now that there is an infinite (> F , R stat ) lex -decreasing sequence (f i , ⃗ t i ) i≥0 . Then, (f i ) i≥0 is an infinite ≥ F -decreasing sequence. Since > F is wellfounded by assumption, there must be some j such that, for all i ≥ j, f i ≃ F f j . Since symbols equivalent in ≃ F have the same status by assumption, ( ⃗ t i ) i≥j is an infinite R stat(f j ) -decreasing sequence, a contradiction. 6.3. Computability properties of arrow types. In this sub-section, the results hold for any base type interpretation I and any set of neutral terms N . For the sake of simplicity, we drop the index I in T I and simply write T . Lemma 6.13. U → V satisfies (comp-sn) if:

• U ≠ ∅, which is the case if U satisfies (comp-neutral); • V satisfies (comp-sn).
Proof. Assume that there is an infinite reduction sequence

t 0 ≻ τ t 1 ≻ τ . . . with t 0 ∈ U → V and t i ∶ T i . By definition of U → V , T 0 = U → V . By definition of ≻ τ , T 0 ≥ T 1 ≥ . . . By assumption, U ≠ ∅. So, let u ∈ U .
By definition of U → V , we have t 0 u ∈ V . We now prove that there is an infinite reduction sequence starting from t 0 u. Since V is assumed to satisfy (comp-sn), this is not possible. Therefore, U → V satisfies (comp-sn) too. By (typ-arrow) there are only two cases:

• For all i, T i = U → B i for some B i . By monotony (Lemma 6.3),

t 0 u ≻ τ t 1 u ≻ τ . . . • There is i such that T i+1 is a sort or T i+1 = A i+1 → B i+1 with A i+1 ≠ U . Let
Proof. Let t ∈ U → V and t ′ ∶ T ′ such that t ≻ τ t ′ . By definition of U → V , t ∶ U → V . By definition of ≻ τ , U → V ≥ T ′
. By (typ-arrow), there are two cases:

(1) V ≥ T ′ . By assumption, U ≠ ∅. So, let u ∈ U . By definition of U → V , tu ∈ V . By (@⊳), we have tu ≻ τ t ′ . Therefore t ′ ∈ T ′ since V satisfies (comp-red). ( 2)

T ′ = U → V ′ and V ≥ V ′ . Let u ∈ U . By monotony (Lemma 6.3), tu ≻ τ t ′ u. By definition of U → V , tu ∈ V . Since V satisfies (comp-red), t ′ u ∈ V ′ . Therefore, t ′ ∈ T ′ . Lemma 6.15. Let t ∶ U → V and u ∶ U . Then, every ≻ τ -reduct of tu is computable if: • every ≻ τ -reduct of t is computable; • u is computable; • if t = λxv, then v u x is computable; • for all u ′ such that u ≻ τ u ′ , tu ′ is computable; • U satisfies (comp-red); • V satisfies (comp-red); • V ′ satisfies (comp-lam) whenever V ′ ≤ V .
Proof. We prove that every w ∶ W such that tu ≻ τ w is computable, by induction on w . By definition of ≻ τ , we have V ≥ W .

• (@⊳)

t ⪰ w. By (typ-right-subterm), U → V > V . Hence, by transitivity, U → V > W and t ≻ τ w. Therefore, w is computable by assumption. -u ⪰ τ w. Then, w is computable since, by assumption, u is computable and U satisfies (comp-red). • (@=) w = t ′ u ′ and either:

t = t ′ and u ≻ u ′ , in which case t ′ u is computable by assumption since u ≻ τ u ′ ; -or tu ≻ @ t ′ and tu ≻ @ u ′ . We prove that, for v ∈ {t ′ , u ′ }, if tu ≻ @ v then v is computable. There are three cases:

* t ≻ τ v. Then, v is computable by assumption. * u ⪰ τ v.
Then, either u = v and v is computable by assumption, or u ≻ τ v and v is computable since u is computable and U satisfies (comp-red). * tu ≻ τ v. Then, since v ∈ {t ′ , u ′ }, v is computable by induction hypothesis.

• (@λ) w = λyv, tu ≻ v and y ∉ FV(v) by Lemma 6.4. Then, there are A and B such that W = A → B. By (typ-right-subterm), W > B. Hence, by transitivity, V > B and tu ≻ τ v. Thus, by induction hypothesis, v is computable. Since W satisfies (comp-lam), w is computable if, for all computable term a ∶ A, v a y is computable. Since y ∉ FV(v), v a y = v. Therefore, w is computable.

• (@X ) w ∈ ∅. Impossible. • (@β) t = λxv and v u x ≥ ∅ w. Since τ ((λxv)u) = τ (v u x ), we have v u x ⪰ τ w. Thus w is computable since v u
x is computable and V satisfies (comp-red). Lemma 6.16. Let t ∶ U → V and u ∶ U . Then, tu is computable if:

• every ≻ τ -reduct of t is computable; • u is computable;

• if t = λxv, then v u x is computable; • either t is neutral or t = λxv;
• U satisfies (comp-red) and (comp-sn); • V satisfies (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V .
Proof. We prove that tu is computable by induction on u with ≻ τ as well-founded relation ( U satisfies (comp-sn) by assumption). So, by induction hypothesis, for all u ′ such that u ≻ τ u ′ , tu ′ is computable. Hence, by Lemma 6.15, every ≻ τ -reduct of tu is computable. Now, tu is neutral because, either t is neutral and tu is neutral by (neutral-app), or t = λxv and tu is neutral by (neutral-beta). Therefore, tu is computable since V satisfies (compneutral). Corollary 6.17. U → V satisfies (comp-neutral) if:

• U satisfies (comp-red) and (comp-sn);

• V satisfies (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V .
Proof. Let t be a neutral term of type U → V such that every ≻ τ -reduct of t is computable. By definition, t ∈ U → V if, for all computable u ∶ U , tu is computable. Since t is neutral, by (neutral-not-lam), t is not of the form λxv. Therefore, by Lemma 6.16, tu is computable since all the required properties are satisfied.

Lemma 6.18. Let x ∶ U and v ∶ V . Then, λxv is computable if:

• for all computable u ∶ U , v u x is computable;

• U satisfies (comp-sn) and (comp-red) and contains a variable, which is the case if it satisfies (comp-neutral) too; • V satisfies (comp-sn), (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V .
Proof. By definition, λxv is computable if, for all computable u ∶ U , (λxv)u is computable. By Lemma 6.16, (λxv)u is computable if every ≻ τ -reduct of λxv is computable, the other conditions being satisfied. Since U contains a variable, we can wlog assume that this is x. So, v x x = v is computable. Since V satisfies (comp-sn), v ∈ SN(≻ τ ). We now prove that every ≻ τ -reduct w ∶ W of λxv is computable, by induction on (v, w ) with (≻ τ , > N ) lex as well-founded relation. By definition of ≻ τ , we have U → V ≥ W .

• (λ⊳) v ⪰ τ w. Since v is computable and V satisfies (comp-red), we have w computable. u ∶ U computable. We have au = v u x computable by assumption. Therefore, a is computable. By Lemma 6.14, U → V satisfies (comp-red) since U ≠ ∅ and V satisfies (comp-red). Therefore, w is computable too. Corollary 6.19. U → V satisfies (comp-lam) if:

• (λ=) w = λxb and v ≻ b. Then, there is B such that W = U → B. Since U → V ≥ W ,
• U satisfies (comp-sn), (comp-red) and (comp-neutral);

• V satisfies (comp-sn), (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V .
In conclusion, we can see that U → V I is a computability predicate if so are U I and V ′ I for all V ′ ≤ V . Therefore, if we can define a base type interpretation I so that, for every sort A, I(A) is a computability predicate then, for all type T , T I will be a computability predicate.

6.4. Well-foundedness of core CPO. We now define a set of neutral terms N and a base type interpretation I for proving the well-foundedness of core CPO. Definition 6.20 (Neutral terms for core CPO). Let N be the smallest set of terms containing the terms of the form f( ⃗ t) and closed by (neutral-var), (neutral-beta) and (neutral-app).

One can easily check that N satisfies all the properties of Definition 6.10.

In contrast with the usual practice, but as in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], our interpretation of sorts is not the set of strongly normalizing terms of that sort. To define the base type interpretation I, we proceed by induction on ⋗ which is well-founded by (typ-sn). So, let A be a sort and assume that I is defined for all sorts B ⋖ A. Then, let I(A) be the least fixpoint of the monotone function F A defined as follows:

F A (S) = {t ∈ L t ∶ A ∧ (∀u)(∀U ) t ≻ τ u ∧ u ∶ U ⇒ u ∈ U I∪{(A,S)} }
We now prove that F A is indeed well-defined and monotone. Then, by Knaster and Tarski's fixpoint theorem [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF], F A admits a (least) fixpoint. Lemma 6.21. F A is well-defined.

Proof. The recursive call to U I∪{(A,S)} is well-defined because, by definition of ≻ τ , we have A ≥ U . Hence, by Lemma 2.5, Sort A (U ). Lemma 6.22. F A is monotone. 1) and ( 2) with S replaced by S ′ . Indeed, assume that t ≻ τ u and u ∶ U . By [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF]

Proof. Let S ⊆ S ′ , J = I ∪ {(A, S)}, J ′ = I ∪ {(A, S ′ )} and t ∈ F A (S). Then, (1) t ∶ A and (2) (∀u)(∀U ) t ≻ τ u ∧ u ∶ U ⇒ u ∈ U J . Now, we have t ∈ F A (S ′ ) because t satisfies (
, u ∈ U J . By definition of ≻ τ , A ≥ U . If A = U , then u ∈ U J ′ since u ∈ U J = S ⊆ S ′ = U J ′ .
Otherwise, by Lemma 2.5, Sort ⋖A (U ). Therefore, by Lemma 6.8, U J = U J ′ and u ∈ U J ′ . Note that the least fixpoint of F A can be reached by transfinite iteration of F A from ∅ [START_REF] Kuratowski | Une méthode d'élimination des nombres transfinis des raisonnements mathématiques[END_REF][START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF], that is, there is an ordinal a, such that I(A) = F a A (∅) where:

• F 0 A (S) = S • F a+1 A (S) = F A (F a A (S)) • F a A (S) = ⋃ b<a F b A (S)
if a is a limit ordinal We now check that type interpretations are computability predicates. Lemma 6.23. Given a sort A, A satisfies (comp-red), (comp-neutral) and (comp-lam).

Proof. We show each property in turn.

• (comp-red) Let t ∈ A and assume that t ≻ τ u and u ∶ U . Since A = F A ( A ), we have u ∈ U by definition of F A . • (comp-neutral) Let t ∶ A be a neutral term whose ≻ τ -reducts are all computable.

Since A = F A ( A ), we have t ∈ A by definition of F A . • (comp-lam) Trivial for typing reasons. Lemma 6.24. Given a sort A, A satisfies (comp-sn) if, for all type U < A, U satisfies (comp-sn).

Proof. As already mentioned, A = F a

A (∅) for some ordinal a. Since ∅ satisfies (comp-sn), it therefore suffices to check that F A preserves termination: if S ⊆ SN(≻ τ ), then F A (S) ⊆ SN(≻ τ ). So, let S ⊆ SN(≻ τ ) and let t ∈ F A (S). By definition of F A , we have t ∶ A and, if t ≻ τ u and u ∶ U , then u ∈ U J where

J = I ∪ {(A, S)}. By definition of ≻ τ , A ≥ U . If A = U , then U J = S and u ∈ SN(≻ τ ) since S ⊆ SN(≻ τ ). Otherwise, u ∈ SN(≻ τ ) since U ⊆ SN(≻ τ )
by assumption. Theorem 6.25. For all type T , T is a computability predicates, i.e. satisfies (comp-sn), (comp-red), (comp-neutral) and (comp-lam).

Proof. We proceed by induction on ⋗ which is well-founded by assumption (typ-sn). If T is a sort, then we can conclude by Lemma 6.23, Lemma 6.24 and induction hypothesis. Otherwise, T = U → V . Since T ⊳ l U , by induction hypothesis, U is a computability predicate. Let now V ′ be a type such that V ≥ V ′ . By (typ-right-subterm) and transitivity, T > V ′ . Hence, by induction hypothesis, V ′ is a computability predicate. Therefore, U → V satisfies (comp-sn) by Lemma 6.13, (comp-red) by Lemma 6.14, (comp-neutral) by Corollary 6.17 and (comp-lam) by Corollary 6.19. Now, we are left to prove that every function symbol is computable.

Lemma 6.26. Let f ⃗ T ∶ ⃗ T → U and ⃗ t ∈ ⃗ T . Then, f( ⃗ t) ∈ U .
Proof. By Theorem 6.25, ⃗ T satisfies (comp-sn). Hence, by Lemma 6.12, (> F , (≻ τ ) stat ) lex is well-founded. We now prove that, for all (f, ⃗ t) ∈ Σ, f( ⃗ t) is computable, by induction on (> F , (≻ τ ) stat ) lex [START_REF] Abel | Termination checking with types[END_REF].

First, we check that t = f( ⃗ t) is computable if all its ≻ τ -reducts so are. This follows from the facts that, by definition of N , t is neutral and, by Theorem 6.25, U satisfies (comp-neutral).

We now prove that, for all finite sets of variables X, for all substitutions σ such that dom(σ) ∩ FV( ⃗ t) = ∅ and σ is computable on X, and for all terms w such that f( ⃗ t) ≻ X w, we have wσ computable, by induction on the size of w (2). Note that

⃗ tσ = ⃗ t since dom(σ) ∩ FV( ⃗ t) = ∅. • (F b ⊳) (∃i) t i ⪰ τ w.
By stability by substitution of ⪰ τ (Lemma 1), we have t i σ ⪰ τ wσ.

Therefore, wσ is computable since, by Theorem 6.25, V satisfies (comp-red). • (F b =) There are g and ⃗ u such that w = g(⃗ u), f ≃ F g, (∀i) f( ⃗ t) ≻ X u i and ⃗ t (≻ τ ) stat(f) ⃗ u. Since (∀i) f( ⃗ t) ≻ X u i , by induction hypothesis (2), ⃗ uσ are computable. If t i ≻ τ u j then, by stability by substitution (Lemma 1),

t i = t i σ ≻ τ u j σ. Therefore, ⃗ t (≻ τ ) stat(f) ⃗
uσ and, by induction hypothesis (1), g(⃗ u)σ is computable.

• (F b >) Since f( ⃗ t) ≻ X ⃗
u, by induction hypothesis (2), ⃗ uσ are computable. Hence, g(⃗ u)σ is computable by induction hypothesis [START_REF] Abel | Termination checking with types[END_REF].

• (F b @) Since f( ⃗ t) ≻ X u and f( ⃗ t) ≻ X v
, by induction hypothesis (2), uσ and vσ are computable. Therefore, (uv)σ = (uσ)(vσ) is computable.

• (F b λ) Wlog we can assume that σ is away from {y} and y ∉ FV(f( ⃗ t)). Hence, (λyv)σ = λy(vσ). By Theorem 6.25, λy(vσ) is computable if, for all computable u ∶ τ (y), (vσ) u y is computable. Since σ is away from {y}, (vσ Proof. After Theorem 6.11, Theorem 6.25 and Lemma 6.26.

) u y = (v z y )θ where θ = σ ∪ {(z, u)}. Let Z = X ∪ {z}. Since f( ⃗ t) ≻ Z v z y , dom(θ) ∩ FV(f( ⃗ t)) = ∅ and θ is computable on Z, we have v z y θ computable by induction hypothesis (2). • (F b X ) w ∈ X. Then, wσ is computable since σ is computable on X.
We can therefore conclude that ≻ + τ is a monotone, stable, well-founded order. The well-foundedness proof of core CPO is actually similar to that of HORPO, although the proof here is presented in a quite different style from HORPO's monolithic proof [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. This similarity fades away with the two coming extensions, to inductive types and to small symbols. The reason why we have split the proof into small pieces is indeed to factor out its structure and those parts which are common to core CPO and its extensions.

Accessibility

In this section, we introduce an extension of the core definition that will allow us to handle rewrite rules like the ones defining recursors for strictly positive inductive types as used in the Coq proof assistant [START_REF] Coquand | Inductively defined types[END_REF][START_REF] Inria | The Coq reference manual[END_REF]. Given a type A, the recursor (of arity 4) at type A

rec A O ∶ O → A → (O → A → A) → ((N → O) → (N → A) → A) →
A can be defined by the following rewrite rules:

rec A O (zero, u, v, w) → u rec A O (suc(x), u, v, w) → v x (rec A O (x, u, v, w)) rec A O (lim(y), u, v, w) → w y (λn rec A O (y n, u, v, w))
To capture such a relation, we need the following two comparisons to succeed:

rec A
O (lim(y), u, v, w) ≻ y and lim(y) ≻ τ y n. The second comparison cannot succeed unless we allow non empty sets X of variables in (F b =) in order to have lim(y) ≻ {n} τ y n, but we have seen in Section 5.3 that this may lead to non-termination. Instead, we will use a specific ordering: the structural ordering introduced by Coquand for dealing with such kind of definitions in the calculus of constructions [START_REF] Coquand | Pattern matching with dependent types[END_REF].

For the first comparison to succeed, since the type of y is bigger than the type of lim(y), we must not check types in (F b ⊳), but we have seen in Section 5.3 that this may lead to non-termination. To solve this problem, we will compare in (F b ⊳) the right-hand side with possibly deep subterms of the left-hand side.

We cannot take any deep subterm however, as shown by the following example: assuming the signature c 1 ∶ (A → B) → A and f 1 ∶ A → (A → B), the deep subterm comparison f(c(x)) ≻ τ x leads to non-termination, since, taking t = λx f(x) x, we have f(c(t)) c(t) ≻ τ t c(t) ≻ τ f(c(t)) c(t) by monotony and (@β). There are two cases where deep subterms can be used: as for the first, deep subterms whose type is a (sufficiently small) sort [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]; as for the second, Mendler showed that pattern-matching on constructors of a sort A having an argument whose type has a negative occurrence of A wrt the arrow type constructor (see Definition 7.2 just after), leads to non-termination, while, on the contrary, β-reduction combined with recursion combinators for positive inductive types terminates [START_REF] Mendler | Inductive definition in type theory[END_REF][START_REF] Mendler | Inductive types and type constraints in the second-order lambda calculus[END_REF]. 7.1. Accessible subterms. In this sub-section, we first define the sets of positive and negative positions of a type, and the notions of accessible and structurally smaller term, before we prove some properties of these notions. •

Pos(A) = Pos + (A) = Pos(A, A) = {ε} • Pos -(A) = ∅ • Pos(A, B) = ∅ if A ≠ B • Pos(T → U ) = {1p p ∈ Pos(T )} ∪ {2p p ∈ Pos(U )} • Pos(A, T → U ) = {1p p ∈ Pos(A, T )} ∪ {2p p ∈ Pos(A, U )} • Pos + (T → U ) = {1p p ∈ Pos -(T )} ∪ {2p p ∈ Pos + (U )} • Pos -(T → U ) = {1p p ∈ Pos + (T )} ∪ {2p p ∈ Pos -(U )} A sort A occurs only positively (resp. negatively) in T if Pos(A, T ) ⊆ Pos + (T ) (resp. Pos(A, T ) ⊆ Pos -(T )).
f α(f) ∶ ⃗ T → A, we assume given a set Acc(f) of accessible arguments of f such that i ∈ Acc(f) implies Sort A (T i ) and Pos(A, T i ) ⊆ Pos + (T i ).
Note that, if α(f) < ⃗ T , the output type of f is functional. Let us consider Example 7.1 and assume that O > N. Then, O occurs only positively in the type of the first argument of suc, and we can take Acc(suc) = {1}. Similarly, we can take Acc(lim) = {1}.

We can now introduce those sorts A which are not bigger than any arrow type and will be interpreted by SN A (≻ τ ) later: Definition 7.4 (Basic sorts). A sort A is basic if, for all type T < A, T is a basic sort and, for all f α(f) ∶ ⃗ T → A and i ∈ Acc(f), T i = A or T i is a basic sort.

In particular, are basic all first-order data types like unary natural numbers, lists, trees, etc. whose constructors do not take a function as argument.

Accessibility blends accessible arguments and subterms of basic sort: Definition 7.5 (Accessibility). A term u is said to be accessible in a term t if:

• u is a subterm of basic sort of t such that FV(u) ⊆ FV(t), written t ⊳ s b u, or

• there are f α(f) ∶ ⃗ T → A, ⃗ t ∶ ⃗ T and i ∈ Acc(f) such that t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗ T
and t i ⊵ a u, written t ⊳ a u, where ⊵ s b and ⊵ a are the reflexive closures of ⊳ s b and ⊳ a respectively. Coming back to Example 7.1, we have x accessible in suc(x) since suc(x) ⊳ a x, and y accessible in lim(y) since lim(y) ⊳ a y. Lemma 7.6. If t ⊳ a u ∶ U , then there are two sorts A and B such that t ∶ A, B A, Sort B (U ) and Pos(B, U ) ⊆ Pos + (U ).

Proof. By induction on ⊳ a , which is clearly well-founded. Assume that there are Proof. By Lemma 7.6, there is a sort B A such that Sort B (U ) and Pos(B, U ) ⊆ Pos + (U ). Since A occurs in U , A B. Therefore, B = A and we are done. Definition 7.8 ([28]). Given a finite set X of variables, we say that u is structurally smaller than t wrt X, written t ⊳ X @ u, if there are A, v and ⃗

f α(f) ∶ ⃗ T → A, ⃗ t ∶ ⃗ T and i ∈ Acc(f) such that t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗ T and t i ⊵ a u. By definition of Acc, Sort A (T i ) and Pos(A, T i ) ⊆ Pos + (T i ). If t i = u then U = T i
x ∶ ⃗ U such that t ∶ A, u ∶ A, u = v⃗ x, t ⊳ a v, ⃗ x ∈ X and Pos(A, ⃗ U ) = ∅.
One can easily check:

Lemma 7.9. ⊳ s b and ⊳ a (resp. ⊳ X @ ) are stable by substitution (resp. away from X).

(F b ⊳) f( ⃗ t) ≻ X v if f ∈ F b and ⃗ t ⊵ s b ⊵ a ⪰ τ v (F b =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f ≃ F g, f( ⃗ t) ≻ X ⃗ u and ⃗ t (≻ τ ∪ ⊳ X @ ⪰ τ ) stat(f) ⃗ u
The rules of Example 7.1 are now easily oriented by CPO. Take for instance the third rule. It is included in CPO since, by (F b @):

• l = rec A O (lim(y), u, v, w) ≻ w x by (F b @)since:

-l > w by (F b ⊳), -l > y by (F b ⊳) since lim(y) ⊳ a y, • l ≻ λn rec A O (y n, u, v, w) by (F b λ) since l ≻ {n} rec A O (y n, u, v, w) because, by (F b =): -l ≻ {n} y n since by (F b @): * l > y as already seen, * l > n by (F b X ), -l > u, v, w by (F b ⊳), -lim(y) ⊳ {n} @ y n.
Following [START_REF] Blanqui | RPO revisited[END_REF], we could strengthen CPO further by defining ⊳ X @ and ≻ X simultaneously, by replacing in (

F b =), ⊳ X @ by ⊳ f( ⃗ t),X @ and, in the definition of ⊳ X @ , ⃗ x ∈ X by f( ⃗ t) ≻ X ⃗ x.
7.3. Comparison with CHORPO. CHORPO is a variant of HORPO which was also aiming at ordering recursors of inductive types like Brouwer's ordinals. In rules (1), ( 3), ( 4) and ( 7) of the 12 rules of HORPO as recalled in Section 5.4, one has to show recursively that every direct subterm of the left-hand side f( ⃗ t) is bigger than (or equal to) the right-hand side. In CHORPO, one can also use in addition to the direct subterms, any term of the computability closure CC(f( ⃗ t), ∅) of the left-hand side, a set inductively defined by 6 rules (CC1) to (CC6) that, for most of them, correspond to CPO rules as follows.

CC(f( ⃗ t), X) must contain { ⃗ t}, which corresponds to (F b ⊳), and X, which corresponds to (F b X ); (CC1) says that CC(f( ⃗ t), ∅) contains any term u of minimal type such that ⃗ t ⊳ s u, where t ⊳ s u if t ⊳ u and FV(u) ⊆ FV(t), which corresponds to (F b ⊳), (@⊳) and (λ⊳); (CC2) corresponds to (F b >); (CC3) corresponds to (F b =) with ≻ τ replaced by ≻ τ ∪ ⊳ s τ ; (CC4) corresponds to (F b @) and (CC5) to (F b λ).

On the other hand, (CC6) says that CC(f( ⃗ t), ∅) is closed by > horpo . Capturing such a rule in CPO requires to consider the transitive closure of ≻ τ in (F b =) which would most presumably turn CPO into an undecidable relation, as it is probably already the case of CHORPO for the same reason.

In conclusion, while CHORPO and CPO look incomparable, the restriction of CHORPO to (CC1), (CC2), (CC3), (CC4), (CC5) is included in CPO. In fact, CPO can be seen as a decidable reformulation of CHORPO integrating in a simple, uniform and more powerful way both HORPO and the notion of computability closure. Note finally that HORPO and the computability closure are themselves already related, as shown in [START_REF] Blanqui | RPO revisited[END_REF]. More precisely, the first version of HORPO [START_REF] Jouannaud | The higher-order recursive path ordering[END_REF] is included in the fixpoint of the monotone function mapping > to the relation > ∅ CC such that t > X CC u if u ∈ CC(t, X), RPO being equal to this fixpoint when restricted to first-order terms. • ≻ X is well-defined.

• ≻ τ is monotone. • If a ≻ X b, then FV(b) ⊆ FV(a) ∪ X.
• ≻ X is stable by α-equivalence.

• ≻ X is stable by substitution away from X.

• If e, e ′ ∈ X , τ (e) = τ (e ′ ), t ≻ X u and e ′ ∉ FV(λeu), then t ≻ X-{e}∪{e ′ } u e ′ e . Proof. As for the core definition using Lemma 7.9 and the fact that, if a ⊳ a b, then FV(b) ⊆ FV(a).

In order to extend the well-founded proof of core CPO to accessible subterms, we need to define a set of neutral terms and a base type interpretation so that accessible arguments of a computable term f( ⃗ t) are computable. Hence, the following definitions: Definition 7.12 (Neutral terms for CPO with accessible subterms). Let N be the smallest set of terms containing the terms of the form f( ⃗ t) with Acc(f) = ∅, and closed by (neutralvar), (neutral-beta) and (neutral-app).

One can easily check that N satisfies all the properties of Definition 6.10. Note that, now, a term is neutral if and only if it is of the form

x ⃗ v, (λxa) b ⃗ v, or f( ⃗ t) ⃗ v with Acc(f) = ∅.
To define the base type interpretation I, we proceed as for core CPO by well-founded induction on ⋗. So, let A be a sort and assume that I is defined for all sorts B ⋖ A. Then, let I(A) be the least fixpoint of the monotone function F A defined as follows:

F A (S) = {t ∈ L t ∶ A ∧ (∀u)(∀U ) t ≻ τ u ∧ u ∶ U ⇒ u ∈ U I∪{(A,S)} ∧ (∀f)(∀ ⃗ T )(∀ ⃗ t)(∀i) f α(f) ∶ ⃗ T → A ∧ t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗ T ∧ i ∈ Acc(f) ⇒ t i ∈ T i I∪{(A,S)} } • b = c + 1. Then, J b = F A (J c ). If a = c, then J a ⊆ J b by definition of F A . Otherwise,
a < c and, by induction hypothesis, J a ⊆ J c . By Lemma 7.15, J a+1 ⊆ J c+1 . Since J a ⊆ J a+1 by definition of F A , we have J a ⊆ J b . • b is a limit ordinal. Then, J a ⊆ J b by definition of J b .

The functions F a

A provide us with a well-founded relation that is the basis of the wellfoundedness of the structural term ordering when it is instantiated by computable terms: Definition 7.17 (Rank ordering). Let the rank of a term t ∈ A , rk A (t), be the smallest ordinal a such that t ∈ F a A (∅). Then, let t ⊐ u if there is a sort A such that t ∈ A , u ∈ A and rk A (t) > rk A (u).

We now prove that ≻ τ is included in ⊐ and that their union is strongly normalizing on computable terms.

Lemma 7.18. If t ∈ A , u ∈ A and t ≻ τ u, then t ⊐ u.
Proof. By definition, we have t ∈ F a A (∅) where a = rk A (t). We can neither have a = 0 nor a be a limit ordinal. So, there is b such that a

= b + 1. Hence, F a A (∅) = F A (F b A (∅)) and u ∈ F b A (∅) by definition of F A . Therefore, t ⊐ u. Lemma 7.19. T ⊆ SN(≻ τ ∪ ⊐) if, for all T ′ ≤ T , T ′ satisfies (comp-sn).
Proof. Assume that there is an infinite (≻ τ ∪ ⊐)-decreasing sequence (t i ) i≥0 such that t 0 ∈ T and t i ∶ T i . Then, (T i ) i≥0 is an infinite ≥-decreasing sequence. Since > is well-founded by (typ-sn), there must be some j such that, for all i ≥ j, T i = T j . If T j is a sort then, by Lemma 7.18, (t i ) i≥j is an infinite ⊐-decreasing sequence, which is not possible since ⊐ is well-founded. If T j is not a sort, then (t i ) i≥j is an infinite ≻ τ -decreasing sequence since ⊐ only compares terms of base type. But this is not possible since T ≥ T j and, by assumption, T j satisfies (comp-sn).

We now show that ⊳ a preserves computability, and that the structural term ordering ⊳ X @ is stable by computable substitutions of domain X. Lemma 7.20. If t is computable and t ⊵ a u, then u is computable.

Proof. By induction on the definition of ⊵ a . If t = u, this is immediate. Otherwise, there are

f α(f) ∶ ⃗ T → A, ⃗ t ∶ ⃗ T and i ∈ Acc(f) such that t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗ T and t i ⊵ a u. Since t is computable, by definition of A , t i is computable. Therefore, by induction hypothesis, u is computable. Lemma 7.21. If t ∶ A is computable, t ⊳ a u ∶ U and A occurs in U , then there is b such that rk A (t) = b + 1 and u ∈ U J , where J(A) = F b A (∅) and J(B) = I(B) if B ≠ A. Proof.
First note that, by Corollary 7.7, Sort A (U ) and Pos(A, U ) ⊆ Pos + (U ). We now proceed by induction on the definition of ⊳ a . Assume that there are

f α(f) ∶ ⃗ T → A, ⃗ t ∶ ⃗ T and i ∈ Acc(f) such that t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗
T and t i ⊵ a u. By definition, rk A (t) can be neither 0 nor a limit ordinal. Therefore, there must be b such that rk A (t) = b + 1 and t i ∈ T i J . If t i = u, then we are done. Assume now that t i ⊳ a u. Then, there is B such that t i ∶ B. By definition of Acc, B A. By Corollary 7.7, Sort B . Since A occurs in U , we have A B and thus B = A because ⋗ is well-founded by (typ-sn). Hence, by induction hypothesis, there is c such that rk A (t i ) = c + 1 and u ∈ U K , where K(A) = F c A (∅) and K(B) = I(A) if B ≠ A. Therefore, u ∈ U J by Lemma 7.14 since c ≤ b, Sort A (U ) and Pos(A, U ) ⊆ Pos + (U ). Lemma 7.22. If t ⊳ X @ u, σ is computable on X and tσ is computable, then uσ is computable and tσ ⊐ uσ.

Proof. Since t ⊳ X @ u, there are A, v and ⃗ x ∶ ⃗ W such that t ∶ A, u ∶ A, u = v⃗ x, t ⊳ a v, ⃗ x ∈ X and Pos(A, ⃗ W ) = ∅. Therefore, uσ = (vσ)(⃗ xσ) and, since ⊳ a is stable by substitution, tσ ⊳ a vσ. By Lemma 7.21, there is b such that rk A (tσ) = b+1 and vσ ∈ ⃗ W → A J , where J(A) = F b A (∅) and J(B) = I(A) if B ≠ A. Since σ is computable on X, we have ⃗ xσ computable. Since Pos(A, ⃗ W ) = ∅, by Lemma 6.8, we have ⃗ xσ ∈ ⃗ W J . Therefore, uσ ∈ A J and tσ ⊐ uσ.

7.6. Well-foundedness of CPO with accessible subterms. We now check that type interpretations are computability predicates, and that function symbols are computable.

One can easily check that all the lemmas of Section 6.3 are still valid, as well as the lemmas 6.23 and 6.24 (since they do not depend on (F b _) rules). Therefore, following the proof of Theorem 6.25, we get: Theorem 7.23. For all type T , T is a computability predicate, i.e. satisfies (comp-sn), (comp-red), (comp-neutral) and (comp-lam).

Lemma 7.24. If A is a basic sort, then A = SN A (≻ τ ).

Proof. By Lemma 6.24, it suffices to prove that, for all t ∈ SN A (≻ τ ), we have t ∈ A . By (typ-sn), ⋗ is well-founded. By Lemma 7.11, ≻ τ is monotone and thus ≻ τ ∪ ⊳ is well-founded on SN(≻ τ ). We can therefore proceed by induction on (A, t) with (⋗, ≻ τ ∪ ⊳) as well-founded relation.

We first prove that every ≻ τ -reduct u of t is computable. Since t ∈ SN A (≻ τ ), we have u ∈ SN U (≻ τ ). By definition of ≻ τ , A ≥ U . Therefore, U is a basic sort and, by induction hypothesis, u ∈ U since A ⋗ U or else A = U and t ≻ τ u.

Hence, if t is neutral, then t ∈ A since A satisfies (comp-neutral). Otherwise, t = f(t 1 , . . . , t α(f) )t α(f)+1 . . . t ⃗ T with f α(f) ∶ ⃗ T → A and Acc(f) ≠ ∅. Let i ∈ Acc(f). Then, Sort A (T i ). Since A is basic, T i = A or T i is a basic sort. In both cases, T i A and T i is a basic sort. Therefore, t i ∈ T i since t i ∈ SN T i (≻ τ ) and A ⋗ T i or else A = T i and t ⊳ t i .

Lemma 7.25. Let f ⃗ T ∶ ⃗ T → U and ⃗ t ∈ ⃗ T . Then, f( ⃗ t) is computable.
Proof. There are ⃗ U and A such that T ⊆ SN(≻ τ ∪ ⊐). Therefore, by Lemma 6.12, (> F , (≻ τ ∪ ⊐) stat ) lex is wellfounded. We can therefore prove that, for all

U = ⃗ U → A. By definition, f( ⃗ t) is computable if, for every ⃗ u ∈ ⃗ U , f( ⃗ t)⃗ u
((f, ⃗ t), ⃗ u) such that f( ⃗ t)⃗ u is of base type, f( ⃗ t)⃗ u is computable, by induction on ((> F , (≻ τ ∪ ⊐) stat ) lex , (≻ τ ) lex ) lex (0).
Since f( ⃗ t)⃗ u is of base type and all its accessible arguments are computable by assumption, it suffices to prove that all its ≻ τ -reducts are computable. To this end, we prove that, for all k ≤ n = ⃗ u , every ≻ τ -reduct of f( ⃗ t)u 1 . . . u k is computable, by induction on k (1). • k = 0. The proof is the same as for Lemma 6.26 except for the new cases:

-(F b ⊳) There are i, u ∶ U and v ∶ V such that t i ⊵ s b u ⊵ a v ⪰ τ w. By stability by substitution of ⊵ s b , ⊵ a and ⪰ τ (Lemma 7.9 and 7.11), we have t i = t i σ ⊵ s b uσ ⊵ a vσ ⪰ τ wσ. Since ⃗ t are computable and ⃗ T satisfies (comp-sn), we have ⃗ t ∈ SN(≻ τ ). Since ≻ τ is monotone (Lemma 7.11), we have uσ ∈ SN(≻ τ ). Hence, by Lemma 7.24, uσ is computable and, by Lemma 7.20, vσ is computable. Therefore, wσ is computable since, by Theorem 7.23, V satisfies (comp-red).

-(F b =) There are g and ⃗ u such that w

= g(⃗ u), f ≃ F g, ⃗ t (≻ τ ∪ ⊳ X @ ⪰ τ ) stat(f) ⃗ u and f( ⃗ t) ≻ X ⃗ u. Since f( ⃗ t) ≻ X ⃗
u, by induction hypothesis (2), ⃗ uσ are computable. If t i ≻ τ u j then, by stability by substitution (Lemma 7.11), t i = t i σ ≻ τ u j σ. If t i ⊳ X @ v ⪰ τ u j then, by Lemma 7.22, t i σ ⊐ vσ and, by stability by substitution again, vσ ⪰ τ u j σ. Therefore, by Lemma 7.18 and transitivity, t i σ ⊐ u j σ. Thus, in both cases, ⃗ t (≻ τ ∪ ⊐) stat(f) ⃗ uσ and, by induction hypothesis (0), g(⃗ u)σ is computable.

• k > 0. Then, f( ⃗ t)⃗ u = tu k where t = f( ⃗ t)u 1 . . . u k-1 . By induction hypothesis (1), every ≻ τ -reduct of t is computable. Now, if u k ≻ τ u ′ k , then tu ′
k is computable by induction hypothesis (0). Therefore, by Lemma 6.15, every ≻ τ -reduct of tu k is computable.

rec A C (d, u, v) → u rec A C (c(x), u, v) → v x (λy ¬A x (λz C y rec A C (z, u, v)))
The problem is that we do not have c(x) ⊳ {y,z} @ z. Indeed, C is non-strictly positive and the structural term ordering can only handle strictly positive types.

To handle such rules, we know two solutions. The first one is to define the interpretation of C so that rec A C is computable by definition [START_REF] Werner | Une théorie des constructions inductives[END_REF][START_REF] Matthes | Extensions of system F by iteration and primitive recursion on monotone inductive types[END_REF][START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF], which is possible since positivity conditions are satisfied. However, this solution lacks flexibility for the user who is forced to define all other functions on C via the recursor.

The second, flexible solution consists in considering types with size annotations (to be interpreted by ordinals) and, in (F b =), compare terms by their size annotations, an approach initiated independently in [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF][START_REF] Giménez | Un calcul de constructions infinies et son application à la vérification de systèmes communiquants[END_REF] and later developed in various works, e.g. [START_REF] Abel | Termination checking with types[END_REF][START_REF] Barthe | Type-based termination of recursive definitions[END_REF][START_REF] Blanqui | A type-based termination criterion for dependently-typed higher-order rewrite systems[END_REF][START_REF] Blanqui | Combining typing and size constraints for checking the termination of higher-order conditional rewrit[END_REF]. Indeed, assuming that c(x) has type C α+1 , then x has type ¬¬C α and, thus, the bound variable z gets the type C α which size annotation is smaller than the one of c(x).

Including semantics in RPO was pioneered by Kamin and Lévy [START_REF] Kamin | Attempts for generalizing the recursive path orderings[END_REF], and extended to HORPO in [START_REF] Borralleras | A monotonic higher-order semantic path ordering[END_REF]. In both cases, semantics was added by replacing the precedence by a semantic order on terms. The use of size annotations is a different way to include semantics in these orders. These two different ways of including semantics in recursive path orders are however related: both can be seen as an instance of the more general semantic labeling schema [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][START_REF] Blanqui | On the relation between sized-types based termination and semantic labelling[END_REF].

Small symbols

In this section, we consider a further extension of CPO that originated from some draft version of [START_REF] Jouannaud | Termination of Dependently Typed Rewrite Rules[END_REF] and try to answer the following general question: can we relax the constraints on the precedence? More precisely, to which extent can a function symbol be smaller than an application or an abstraction? We are going to show that this is indeed possible if the rules governing these small symbols are more restrictive than the ones for big symbols.

We first define the extension of CPO to small symbols, and then show the computability properties including a specific one for small symbols. Unlike before, this will reveal a circularity among the dependencies between the different computability properties, hence strong normalization does not follow. Breaking this circularity will require assumptions on the types of small symbols that are then investigated for practical purposes. It will appear that, for instance, any constructor of a strictly-positive inductive type can be considered a small symbol.

8.1. CPO with small symbols. Definition 8.1 (CPO with small symbols). We assume that the set of function symbols is partitioned into a set F b of big symbols and a set F s of small symbols so that:

• no small symbol is greater or equivalent to a big symbol (small-lt-big) • small symbols with arrow output type have no accessible argument (small-acc) We then extend ≻ X by adding the rules of Figure 3.

We will add conditions on the types of small symbols after Definition 8.9 (see Figure 4).

(@F s ) tu ≻ X f(⃗ v) if f ∈ F s and (∀i) tu ≻ X τ v i (λF s ) λxt ≻ X f(⃗ v) if f ∈ F s and (∀i) λxt ≻ X τ v i (F s ⊳) f( ⃗ t) ≻ X v if f ∈ F s and (∃i) t i ⪰ τ v (F s =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F s , f ≃ F g, (∀i) f( ⃗ t) ≻ X τ u i and ⃗ t (≻ τ ∪ ⊳ X @ ⪰ τ ) stat(f) ⃗ u (F s >) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F s , f > F g and (∀i) f( ⃗ t) ≻ X τ u i (F s @) f( ⃗ t) ≻ X u v if f ∈ F s , f( ⃗ t) ≻ X τ u and f( ⃗ t) ≻ X τ v (F s X ) f( ⃗ t) ≻ X x if f ∈ F s and x ∈ X
Because of the rules (@F s ) and (F s @), one may think that the relation is not terminating anymore, but this is not the case for typing reasons. Indeed, in contrast with rules for big symbols, rules for small symbols require type checking the recursive calls systematically.

For instance, assume that f ∶ o → o and g 2 ∶ o → o → o. Then, although we have f a ≻ τ g(a, a) by (@F s ) since f a ≻ τ a by (@⊳), we do not hopefully have g(a, a) ≻ τ f a by (F s @) because we do not have g(a, a) ≻ τ f for typing reasons.

On the other hand, there is no rule (F s λ) such that f( ⃗ t) ≻ X λyv if f( ⃗ t) ≻ X v and y ∉ FV(v) because, together with the rule (λF s ), it would lead to non-termination as shown by the following example: given small symbols a ∶ o → o > F b ∶ o, λxb ≻ τ a by (λF s ), and a ≻ τ λxb by (F s λ) since a ≻ τ b by (F s >). It is however possible to have (F s λ) if one removes (λF s ). We choose to present the case of (F s λ) because it seems more useful, but the termination proof can be easily adapted if (F s λ) is replaced by (λF s ). Note however that this does not lead to the same definition for the sets SPos, LPos, . . . (Definition 8.9) studied in Section 8.4.

Two potential improvements are left. First, take a rule (F s ⊳) similar to the rule (F b ⊳) of Figure 2. Second, get rid of the assumption (small-acc), if possible.

• V ′ satisfies (comp-lam) and (comp-small) whenever V ′ ≤ V .

Proof. As for Corollary 6.17 but using Lemma 8.4 instead. Lemma 8.6. Let x ∶ U and v ∶ V . Then, λxv is computable if:

• for all computable u ∶ U , v u x is computable; • U satisfies (comp-sn) and (comp-red) and contains a variable, which is the case if it satisfies (comp-neutral) too; • V satisfies (comp-sn), (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V ; • W satisfies (comp-small) whenever W ≤ U → V .
Proof. The proof is the same as for Lemma 6.18 except for the new case:

• (λF s ) w = f(⃗ v), f ∈ F s and (∀i) λxv ≻ τ v i .
By induction hypothesis, ⃗ v are computable. Thus, w is computable since, by assumption, W satisfies (comp-small).

Corollary 8.7. U → V satisfies (comp-lam) if:

• U satisfies (comp-sn), (comp-red) and (comp-neutral);

• V satisfies (comp-sn), (comp-red) and (comp-neutral);

• V ′ satisfies (comp-lam) whenever V ′ ≤ V ; • W satisfies (comp-small) whenever W ≤ U → V .
We are left with the new computability property for small symbols:

Lemma 8.8. U satisfies (comp-small) if:

• U satisfies (comp-neutral);

• U ′ satisfies (comp-small) whenever U ′ < U ;

• for every small f ⃗ T ∶ ⃗ T → U , ⃗ T satisfies (comp-sn) and (comp-red).

Proof. Assume that f α(f) ∶ ⃗ T → U is small. By assumption, ⃗ T satisfies (comp-sn) and, by Lemma 7.19, ⃗ T ⊆ SN(≻ τ ∪ ⊐). Therefore, by Lemma 6.12, (> F ,(≻ τ ∪ ⊐) stat ) lex is wellfounded when restricted to small symbols. We can therefore prove that, for all (f, ⃗

t) ∈ Σ with f ∈ F s , f( ⃗ t) is computable, by induction on (> F , (≻ τ ∪ ⊐) stat ) lex (1)
. We first prove that f( ⃗ t) is computable if all its ≻ τ -reducts so are. If U is a sort, then the result holds since ⃗ t are computable. Otherwise, by (small-acc), Acc(f) = ∅ and f( ⃗ t) is neutral. Therefore, the result holds since U satisfies (comp-neutral) by assumption.

We now prove that every

≻ τ -reduct w ∶ W of f( ⃗ t) is computable by induction on w (2). By definition of ≻ τ , we have U ≥ W . • (F s ⊳) (∃i) t i ⪰ τ w.
By assumption, ⃗ T satisfies (comp-red). Thus, w is computable.

• (F s =) There are g ∶ ⃗ U → W and ⃗ u ∶ ⃗ U such that w = g(⃗ u), (∀i) f( ⃗ t) ≻ τ u i , f ≃ F g and ⃗ t (≻ τ ∪ ⊳ ∅ @ ⪰ τ ) stat(f) ⃗ u.
By (small-lt-big), g is small. Since f( ⃗ t) ≻ τ ⃗ u, by induction hypothesis (2), ⃗ u are computable. We distinguish two cases: -U > W . Then, g(⃗ u) is computable since W satisfies (comp-small).

-U = W . If t i ⊳ ∅ @ v ⪰ τ u j then, by Lemma 7.22, t i ⊐ v and, by Lemma 7.18, v ⊒ u j . Therefore, by transitivity, t i ⊐ u j . Hence, ⃗ t (≻ τ ∪ ⊐) stat(f) ⃗ u and, by induction hypothesis (1), g(⃗ u) is computable. • (F s >) There are g ∶ ⃗ U → W and ⃗ u ∶ ⃗ U such that w = g(⃗ u), (∀i) f( ⃗ t) ≻ τ u i and f > F g. By (small-lt-big), g is small. Since f( ⃗ t) ≻ τ ⃗ u, by induction hypothesis (2), ⃗ u are computable. We distinguish two cases:

• T satisfies (comp-neutral) if NPos A (T ) = ∅, • T satisfies (comp-lam) if LPos A (T ) = ∅, • T satisfies (comp-small) if CPos A (T ) = ∅.
Proof. We proceed by induction on ⋗ which is well-founded by (typ-sn).

• T = B. Since Sort A (T ), we have B A.

-SPos A (T ) = ∅. T satisfies (comp-red) by Lemma 6.23. By Lemma 6.24, T satisfies (comp-sn) if, for all U < T , U satisfies (comp-sn). So, let U < T . By transitivity, U ⋖ A. Hence, by Lemma 2.5, Sort ⋖A (U ) and, by Lemma 8.10, SPos A (U ) = ∅. Therefore, by induction hypothesis, U satisfies (comp-sn). -NPos A (T ) = ∅. T satisfies (comp-neutral) by Lemma 6.23.

-LPos A (T ) = ∅. T satisfies (comp-lam) by Lemma 6.23.

-CPos A (T ) = ∅. Then, B ⋖ A and, by assumption, T satisfies (comp-small).

• T = U → V . Then, Sort A (U ) and Sort A (V ).

-SPos A (T ) = ∅. Then, NPos A (U ) = ∅ and SPos A (V ) = ∅. By induction hypothesis, U satisfies (comp-neutral) and V satisfies (comp-sn) and (comp-red). Hence, T satisfies (comp-sn) and (comp-red) by Lemmas 6.13 and 6.14.

-NPos A (T ) = ∅. Then, SPos A (U ) = ∅ and SPos A (V ) = NPos A (V ) = LPos A (V ) = CPos A (V ) = ∅. By induction hypothesis, U satisfies (comp-sn) and (comp- red). Let now V ′ ≤ V . By Lemma 2.6, Sort A (V ′ ). By Lemma 8.11, SPos A (V ′ ) = NPos A (V ′ ) = LPos A (V ′ ) = CPos A (V ′ ) = ∅.
(W ) = ∅. ⋅ W = U → V ′ and V > V ′ . Then, by Lemma 8.11, SPos A (V ′ ) = NPos A (V ′ ) = LPos A (V ′ ) = CPos A (V ′ ) = ∅. Thus, CPos A (W ) = ∅. Hence, by induction hypothesis, W satisfies (comp-small). * Let now f ⃗ T ∶ ⃗ T → T be small. There are ⃗ B and B such that V = ⃗ V → B. So, by (small-arrow), (∀i) Sort B (T i ) and T i T . We first prove that, if Sort A ( ⃗ S → B) and CPos A ( ⃗ S → B) = ∅, then B ⋖ A, by induction on ⃗ S. If ⃗ S is empty, then Sort A (B) and CPos A (B) = ∅. Thus, B ⋖ A. If ⃗ S = U ⃗ V , then CPos A ( ⃗ S → B) = ∅ implies that CPos A ( ⃗ V → B) = ∅.
(V ) = NPos A (V ) = LPos A (V ) = CPos A (V ) = ∅.
By induction hypothesis, U satisfies (comp-sn), (comp-red) and (comp-neutral).

Can therefore be declared as small, any symbol whose type is of order less than or equal to 2 since its arguments have then a type of order less than or equal to 1. This is in particular the case of the constructors of first-order data types.

More generally, can be declared as small every constructor of a strictly-positive inductive type, whatever its order is, which is the class of inductive types allowed in the Coq proof assistant [START_REF] Inria | The Coq reference manual[END_REF]:

Lemma 8.16. Given types ⃗ T and a sort A, SPos A ( ⃗ T → A) = ∅ if Sort ⋖A ( ⃗ T ).
Proof. By induction on T .

• T = A. Immediate.

• T = U → V . Then, Sort ⋖A (U ) and V is of the form ⃗ T → A with Sort ⋖A ( ⃗ T ). By Lemma 8.10, NPos A (U ) = ∅. By induction hypothesis, SPos A (V ) = ∅. Therefore, SPos A (T ) = ∅.
Non-strictly positive types are not available in Coq because strong elimination rules may cause non-terminating computations in Coq's richer type system [START_REF] Coquand | Inductively defined types[END_REF]. Nothing such that can happen in our simple type system in which constructors of non-strictly positive inductive types of order ≤ 2 can be declared as small: Lemma 8.17. But positivity is not always sufficient as shown by the following example. Assume that f ∶ T → A with T = (B → N ) → A, N = (B → A) → B and B < A. The sort A occurs negatively in N and positively in T , which is a 3rd order type. We cannot declare f as small since we do not know how to prove that T satisfies (comp-sn) by using our lemmas. Indeed, to prove that T satisfies (comp-sn), we need to prove that B → N satisfies (comp-neutral) (Lemma 6.13). To prove that B → N satisfies (comp-neutral), we need to prove that N satisfies (comp-lam) (Corollary 8.5). To prove that N satisfies (comp-lam), we need to prove that B → A satisfies (comp-neutral) (Corollary 8.7). To prove that B → A satisfies (comp-neutral), we need to prove that A satisfies (comp-small) (Corollary 8.5). But, to prove that A satisfies (comp-small), we need to prove that T satisfies (comp-sn) (Lemma 8.8). The circularity has not been broken here, but we can of course declare f as being big instead of small. 8.5. Examples. In this section, we analyze two examples that show the need for small symbols and their use. We will see that CPO with small symbols contains not only core CPO, but also a subset of its transitive closure. But CPO with small symbols is not transitive either, as shown by the second example which needs the use of both small symbols and the transitive closure.

NPos A (T )= LPos A (T )= CPos A (T )= ∅ if o(T ) ≤ 1, Sort A (T ) and Pos(A, T ) ⊆ Pos -(T ).
Example 8.19. Taken from the Termination Problems Data Base (TPDB) [START_REF]Termination pproblem data base (TPDB)[END_REF] under the name Applicative_05__TreeFlatten. Let a be a sort. Consider the function symbols nil ∶ a, flatten ∶ a → a, concat 1 ∶ a → a, cons 2 ∶ a → a → a, append 2 ∶ a → a → a, node 2 ∶ a → a → a and map 2 ∶ (a → a) → a → a.

The higher-order rewrite system map(F, nil) → nil map(F, cons(x, v)) → cons(F x, map(F, v))

flatten node(x, v) → cons(x, concat(map(flatten, v))) concat(nil) → nil concat(cons(x, v)) → append(x, concat(v)) append(nil, v) → v append(cons(x, u), v) → cons(x, append(u, v)) can be proved terminating with CPO by considering concat, append, map, cons and nil small, while node and flatten can be either small or big (we consider them as big in the following). All symbols can have multiset status. Let the precedence be concat > F append > F cons, node > F map > F nil, node > F flatten and map > F cons.

Let us show the proof of the third rule, which is the most interesting one. Since cons is small, we apply first (@F s ) and then we recursively need flatten node(x, v) ≻ τ x, which holds by (@⊳) and then (F b ⊳), and flatten node(x, v) ≻ τ concat(map(flatten, v)), which needs (@F s ) again. We then recursively need flatten node(x, v) ≻ τ map(flatten, v), which generates the subgoal node(x, v) ≻ τ map(flatten, v) by (@⊳), and then the new subgoals node(x, v) ≻ τ flatten and node(x, v) ≻ τ v by (F b >). We conclude by (F b >) and (F b ⊳).

The above example cannot be shown by core CPO because flatten is curried and the head symbol of the third rule is then an application. There is however a way out with the transitive closure of core CPO if one allows the introduction of new symbols. Let flattenunc 1 ∶ a → a be a new symbol. Assuming for example flatten > F flattenunc and node > F {cons, concat, map, flatten}, we can then show the successive ordering comparisons: flatten node(x, v) ≻ τ (λx flattenunc(x)) node(x, v) (λx flattenunc(x)) node(x, v) ≻ τ flattenunc(node(x, v)) flattenunc(node(x, v)) ≻ τ cons(x, concat(map(flatten, v))) The first reduces to flatten ≻ τ λx flattenunc(x), the second is a β-reduction, and the third is a classical RPO-like computation. Details are left to the reader.

The use of small symbols can therefore help showing termination of examples that would otherwise require the use of the transitive closure of core CPO (as well as a signature extension in the above case). Small symbols, however, do not make CPO transitive. Our second example requires indeed using both small symbols and the transitive closure: The higher-order rewrite system plus(0) x → x plus(s(y)) x → s(plus(y) x) times(0) x → 0 times(s(y)) x → plus(times(y) x) x map(F ) nil → nil map(F ) cons(x, v) → cons(F x, map(F ) v))

inc → map(plus(s(0))) double → map(times(s(s(0)))) can be proved terminating with CPO by taking a = b in the type ordering, cons and s as small symbols, the precedence times > F plus, inc > F {map, plus, 0}, double > F {map, times, 0}, and status multiset for all symbols.

We consider the 4th rule, for which we shall use the transitive closure of CPO, and the 6th rule, for which small symbols are needed (for the second rule too).

For the 4th rule, we exhibit the middle term (λz plus(times(y) z) z) x which is smaller than the lefthand side and β-reduces to the righthand side of the rule.

To prove that times(s(y)) x is greater than this middle term, we apply (@=), and since the second arguments are equal, we have to show that times(s(y)) ≻ τ (λz plus(times(y) z) z). Since, both terms have the same type, by (F b λ) and then (F b @), we are left to show times(s(y)) ≻ {z} plus(times(y) z), since times(s(y)) ≻ {z} z holds by (F b X ). For this last check, we apply first (F b >) and then (F b @), since times(s(y)) ≻ {z} times(y) holds by (F b =) and then (F s ⊳), and times(s(y)) ≻ {z} z holds by (F b X ).

For the 6th rule, we apply first (@F s ), which requires to check map(F ) cons(x, v) ≻ τ F x and map(F ) cons(x, v) ≻ τ map(F ) v. Since the types of both sides are equivalent, the first one holds by applying (@=) and then (F b ⊳) to the first argument and (F s ⊳) to the second one. Finally, for map(F ) cons(x, v) ≻ τ map(F ) v, we apply (@=) and then (F s ⊳) to the second argument.

Conclusion

We have defined in this paper a well-founded relation on algebraic lambda-terms following a type discipline accepting simple types in the sense of Church, and inductive types in the sense of Martin-Löf. Further, we could easily cope with (implicitly) universally quantified type variables as in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], a type discipline called weak polymorphism.

We want to stress that core CPO has reached a point where we cannot expect any major improvement, as indicated by the counter-examples found to our own attempts to improve it. We are in great debt with Cynthia Kop and Femke van Raamsdonk for igniting this quest, by providing us with an example that removing the type check in the rule (F b =) results in losing the well-foundedness property [START_REF] Kop | [END_REF]. The very existence of these counter-examples supports our conviction that CPO defines an extremely sharp decidable approximation of sets of rules for which there exists a computability predicate.

Of course, all these counter-examples still hold when adding inductive types and small symbols. We did our best to exploit the idea of small symbols as much as possible within our proof frame, but cannot argue that the conditions on the signature of small symbols are all necessary and that the corresponding recursive calls cannot be improved: we did not extend our quest for counter-examples to this question. We finally believe that there is also some room left for improving the accessibility relationship, which is restricted so far to terms headed by a function symbol, possibly applied to extra arguments.

A more challenging problem to be investigated now is the generalization of this new definition to the calculus of constructions along the lines of [START_REF] Walukiewicz-Chrząszcz | Termination of rewriting in the calculus of constructions[END_REF] and the suggestions made in [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF], where an RPO-like ordering on types was proposed which allowed to give a single definition for terms and types. Generalizing CPO to dependent types appears to follow the classical route initiated in [START_REF] Harper | A framework for defining logics[END_REF], albeit non-trivial [START_REF] Jouannaud | Termination of Dependently Typed Rewrite Rules[END_REF]. We therefore believe that this work should be applicable to Dedukti [START_REF] Boespflug | The lambda-pi-calculus modulo as a universal proof language[END_REF][START_REF] Saillard | [END_REF] with limited effort. On the other hand, we have failed so far to generalize CPO to truly polymorphic types: its use in the proof assistant Coq [START_REF] Inria | The Coq reference manual[END_REF] will require much more effort.

Finally, note that HORPO [START_REF] Koprowski | Coq formalization of the higher-order recursive path ordering[END_REF] on the one hand, and the notion of computability closure on the other hand [START_REF] Blanqui | A formalization in Coq of the notion of computability closure for proving the termination of rewrite relations on[END_REF], have already been formalized in the proof assistant Coq [START_REF] Inria | The Coq reference manual[END_REF]. These works could serve as a basis for formalizing the results presented in this paper and develop a termination certificate verifier for CPO.

Figure

  Figure 1: Core CPO(F b ⊳) f( ⃗ t) ≻ X v if f ∈ F b and (∃i) t i ⪰ τ v (F b =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f ≃ F g, (∀i) f( ⃗ t) ≻ X u i and ⃗ t (≻ τ ) stat(f) ⃗ u (F b >) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f > F g and (∀i) f( ⃗ t) ≻ X u i (F b @) f( ⃗ t) ≻ X uv if f ∈ F b , f( ⃗ t) ≻ X u and f( ⃗ t) ≻ X v (F b λ) f( ⃗ t) ≻ X λyv if f ∈ F b , f( ⃗ t) ≻ X∪{z} v z y , τ (y) = τ (z) and z fresh (F b X ) f( ⃗ t) ≻ X y if f ∈ F b and y ∈ X

( 1 )

 1 f(a) ≻ τ (λxf(x))a since τ (f(a)) = o ≥ τ ((λxf(x))a) = o and, by relaxing (F b @): (a) f(a) ≻ + λxf(x) since (i) f(a) ≻ a by (F b ⊳), and (ii) a ≻ λxf(x) by (F b λ) since a ≻ {x} f(x) by (F b >) and then (F b X ) (b) f(a) ≻ a by (F b ⊳). (2) (λxf(x))a ≻ τ f(a) since τ ((λxf(x))a) = o ≥ τ (f(a)) = o and by (@β).

( 1 )

 1 f(a) ≻ τ (λxf(x))a since τ (f(a)) = o ≥ τ ((λxf(x))a) = o and, by (F b @): (a) f(a) ≻ λxf(x) since, by (F b λ), x ∉ FV(f(a)) and (i) f(a) ≻ {x} f(x) since, by relaxing (F b ⊳):

( 1 )

 1 f(a) ≻ τ (λxf(x))a since τ (f(a)) = o ≥ τ ((λxf(x))a) = o and, by (F b @): (a) f(a) ≻ λxf(x) since, by relaxing (F b ⊳):(i) a ⪰ λxf(x) since, by (F b λ), x ∉ FV(a) and a ≻ {x} f(x) and, by (

  u x ≻ τ b u x . Therefore, b u x is computable since V satisfies (comp-red) by assumption. • (λ≠) w = λyb, τ (x) ≠ τ (y), λxv ≻ b and y ∉ FV(b) by Lemma 6.4. Then, there are A and B such that W = A → B. Since U ≠ A, by (typ-arrow), V ≥ W . Since, by assumption, W satisfies (comp-lam), it suffices to prove that, for all computable a ∶ A, b a y is computable. Since y ∉ FV(b), b a y = b. By (typ-right-subterm), U → V > V and W > B. Hence, by transitivity, U → V > B and λxv ≻ τ b. Therefore, since w > N b , by induction hypothesis, b is computable. • (λX ) w ∈ ∅. Impossible. • (λη) v = ax, a ⪰ w and x ∉ FV(a). Since τ (λxv) = τ (a), we have a ⪰ τ w. Let

Theorem 6 . 27 .

 627 The relation ≻ τ of Definition 5.1 is well-founded.

Example 7 . 1 .

 71 Consider the inductive type O of "Brouwer ordinals" whose constructors are zero ∶ O for zero, suc 1 ∶ O → O for successor, and lim 1 ∶ (N → O) → O for limit, where N is the inductive type of Peano (unary) natural numbers with constructors 0 ∶ N and s 1 ∶ N → N.

Definition 7 . 2 (

 72 Positive and negative positions in a type). The sets Pos(T ), Pos(A, T ), Pos + (T ) and Pos -(T ) of positions, positions of A, positive positions and negative positions in a type T are inductively defined as follows:

  For instance, for T = (A → B) → B with A ≠ B, we have Pos(T ) = {ε, 1, 2, 11, 12}, Pos + (T ) = {11, 2}, Pos -(T ) = {12}, Pos(A, T ) = {11} and Pos(B, T ) = {12, 2}. Hence, A occurs only positively in T , but B has both positive and negative occurrences in T . Definition 7.3 (Accessible arguments). For every

  and we are done with B = A. Assume now that t i ⊳ a u. Then, by induction hypothesis, there are two sorts B and C such that t i ∶ B, C B, Sort C (U ) and Pos(C, U ) ⊆ Pos + (U ). Since Sort A (T i ) and T i = B, we have B A. By transitivity, we get C A. Corollary 7.7. If t ∶ A, t ⊳ a u ∶ U and A occurs in U , then Sort A (U ) and Pos(A, U ) ⊆ Pos + (U ).

7. 2 .

 2 CPO with accessible subterms. Definition 7.10 (CPO with accessible subterms). The relation ≻ X is extended by replacing the rules (F b ⊳) and (F b =) of Figure 1 by the ones of Figure 2.

Figure 2 :

 2 Figure 2: New CPO rules with accessible subterms(F b ⊳) f( ⃗ t) ≻ X v if f ∈ F b and ⃗ t ⊵ s b ⊵ a ⪰ τ v (F b =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F b , f ≃ F g, f( ⃗ t) ≻ X ⃗ u and ⃗ t (≻ τ ∪ ⊳ X @ ⪰ τ ) stat(f) ⃗ u

7. 4 .

 4 Computability with accessible subterms. Lemma 7.11 (Basic properties).

Theorem 7 . 26 .

 726 The relation ≻ τ of Definition 7.10 is well-founded. Proof. After Theorem 6.11, Theorem 7.23 and Lemma 7.25. 7.7. Using semantic comparisons. The extension of CPO described here is still not able to orient the terminating rules defining the recursor of the type C in Example 5.2: Example 7.27. Given an arbitrary type A, the recursor (of arity 3) at type A of the type C of continuations of Example 5.2 has type rec A C ∶ C → A → (¬¬C → ¬¬A → A) → A. Its rewrite rules are the following:

Figure 3 :

 3 Figure 3: Additional CPO rules for small symbols(@F s ) tu ≻ X f(⃗ v) if f ∈ F s and (∀i) tu ≻ X τ v i (λF s ) λxt ≻ X f(⃗ v) if f ∈ F s and (∀i) λxt ≻ X τ v i (F s ⊳) f( ⃗ t) ≻ X v if f ∈ F s and (∃i) t i ⪰ τ v (F s =) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F s , f ≃ F g, (∀i) f( ⃗ t) ≻ X τ u i and ⃗ t (≻ τ ∪ ⊳ X @ ⪰ τ ) stat(f) ⃗ u (F s >) f( ⃗ t) ≻ X g(⃗ u) if f ∈ F s , f > F g and (∀i) f( ⃗ t) ≻ X τ u i (F s @) f( ⃗ t) ≻ X u v if f ∈ F s , f( ⃗ t) ≻ X τ u and f( ⃗ t) ≻ X τ v (F s X ) f( ⃗ t) ≻ X x if f ∈ F s and x ∈ X

  By (typ-right-subterm) and transitivity, T > V ′ . Hence, by induction hypothesis, V ′ satisfies (comp-red), (comp-neutral), (comp-lam) and (comp-small). Therefore, by Corollary 8.5, T satisfies (comp-neutral).-CPos A (T ) = ∅. Then, NPos A (T ) = ∅, hence SPos A (U ) = ∅ and SPos A (V ) = NPos A (V ) = LPos A (V ) = CPos A (V ) = ∅. We now check the conditions of Lemma 8.8: * T satisfies (comp-neutral) since NPos A (T ) = ∅. * Let W < T . We prove that CPos A (W ) = ∅. By (typ-arrow), there are two cases: ⋅ V ≥ W . Then, by Lemma 8.11, CPos A

  Hence, by induction hypothesis, B ⋖ A. We therefore have B ⋖ A for T = U ⃗ V → B, Sort A (T ) and CPos A (T ) = ∅. Hence, Sort ⋖A ( ⃗ T ) and, by Lemma 8.10, SPos A ( ⃗ T ) = ∅. If T i ⋖ T , then T i satisfies (comp-red) and (comp-sn) by induction hypothesis. Otherwise, T i = T and T i satisfies (comp-red) and (comp-sn) as shown previously. -LPos A (T ) = ∅. Then, SPos A (U ) = NPos A (U ) = ∅ and SPos A

Proof.

  We proceed by induction on T . • T = B. Then, NPos A (T ) = LPos A (T ) = ∅ by definition. Since Sort A (T ), we have B ≤ A. Since Pos(A, T ) ⊆ Pos -(T ) and Pos -(T ) = ∅, we have B ≠ A. Therefore, CPos A (T ) = ∅. • T = U → V . Since o(T ) ≤ 1, we have o(U ) ≤ 0 and o(V ) ≤ 1. Thus, U is a sort and SPos A (U ) = NPos A (U ) = ∅. By Lemma 8.15, SPos A (V ) = ∅. Since Sort A (T ), we have Sort A (V ). Since Pos(A, T ) ⊆ Pos -(T ), we have Pos(A, V ) ⊆ Pos -(V ). Hence, by induction hypothesis, NPos A (V ) = LPos A (V ) = CPos A (V ) = ∅. Therefore, NPos A (T ) = LPos A (T ) = CPos A (T ) = ∅. Lemma 8.18. SPos A (T ) = ∅ if o(T ) ≤ 2, Sort A (T ) and Pos(A, T ) ⊆ Pos + (T ).

Proof.

  We proceed by induction on T .• T = B. Then, SPos A (T ) = ∅ by definition. • T = U → V . Since o(T ) ≤ 2, we have o(U ) ≤ 1 and o(V ) ≤ 2. Since Sort A (T ), we have Sort A (U ) and Sort A (V ). Since Pos(A, T ) ⊆ Pos + (T ), we have Pos(A, U ) ⊆ Pos -(U ) and Pos(A, V ) ⊆ Pos + (V ).Hence, by Lemma 8.17, NPos A (U ) = ∅ and, by induction hypothesis, SPos A (V ) = ∅. Therefore, SPos A (T ) = ∅.

Example 8 . 20 .

 820 Taken from TPDB under the name AotoYamada_05__014. Let a and b be sorts. Consider the function symbols 0∶ b, nil ∶ a, inc ∶ a → a, double ∶ a → a, s 1 ∶ b → b, plus 1 ∶ b → b → b, times 1 ∶ b → b → b, map 1 ∶ (b → b) → a → a,and cons 2 ∶ b → a → a.

  and t 1 , . . . , t n are terms of type T 1 , . . . , T n respectively, then f(t 1 , . . . , t n ) is a term of type U ; • if t and u are terms of types U → V and U respectively, then tu is a term of type V ;

In fact, Tait speaks of "convertibility" in[START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF], "realizability" in[START_REF] Tait | A realizability interpretation of the theory of species[END_REF]; and Girard of "réductibilité" and "reducibility" in[START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'ana[END_REF][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]. Following Gödel, "computability" is used by Troelstra in[START_REF] Troelstra | Models and Computability[END_REF], p. 100.

In core CPO, all symbols are big. Small symbols will show up in Section 8.

Written ≥ → T S in Lemma 3.15 of[START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF].

Acknowledgements. The authors thank the reviewers for their suggestions.

This research was supported by the Spanish MINECO under grant TIN2013-45732-C4-3-P.

Note that, by this definition, a term f(t 1 , . . . , t α(f) )t α(f)+1 . . . t n ∶ A is computable if all its ≻ τ -reducts and all its accessible arguments t i with i ∈ Acc(f) are computable. This makes the terms of this form behave like neutral terms when ⃗ t are computable. We now prove that F A is indeed well-defined and monotone. Lemma 7.13. F A is well-defined.

Proof. The calls to U I∪{(A,S)} and T i I∪{(A,S)} with i ∈ Acc(f) are well-defined because every sort occurring in U or T i is to A. Indeed, by definition of ≻ τ , we have A ≥ U . Hence, by Lemma 2.5, Sort A (U ). As for T i , it follows by definition of Acc(f).

Lemma 7.14. Let T be a type such that Sort A (T ). Then, the function S ↦ T I∪{(A,S)} is monotone (resp. anti-monotone) wrt set inclusion if Pos(A, T ) ⊆ Pos + (T ) (resp. Pos(A, T ) ⊆ Pos -(T )).

Proof. Let S ⊆ S ′ , J = I ∪ {(A, S)} and J ′ = I ∪ {(A, S ′ )}. We proceed by induction on T .

• T = A. Then, T J = S ⊆ S ′ = T J ′ .

• T = B ⋖ A. Then, T J = I(B) = T J ′ .

• T = U → V and Pos(A, T ) ⊆ Pos + (T ). Let t ∈ T J . By definition of T , t ∈ T J ′ if, for all u ∈ U J ′ , tu ∈ V J ′ . By definition, Pos(A,

Hence, Pos(A, U ) ⊆ Pos + (U ) and Pos(A, V ) ⊆ Pos -(V ). Therefore, by induction hypothesis, 2) and (3) with S replaced by S ′ :

(1) t ∶ A by (1).

(

Otherwise, by Lemma 2.5, Sort ⋖A (U ). Therefore, by Lemma 6.8,

. By definition of Acc, Sort A (T i ), Pos(A, T i ) ⊆ Pos + (T i ) and, by Lemma 7.14, T i J ⊆ T i J ′ . Therefore, t i ∈ T i J ′ since t i ∈ T i J by (3). 7.5. Well-foundedness of the structural term ordering. Lemma 7.16. The function a ↦ F a A (∅) is monotone. Proof. Let J a = F a A (∅). We prove by induction on b that, for all a < b, J a ⊆ J b . 8.2. Computability properties.

Lemma 8.2 (Basic properties).

• ≻ X is well-defined.

• ≻ X is stable by α-equivalence.

• ≻ X is stable by substitution away from X.

• If e, e ′ ∈ X , τ (e) = τ (e ′ ), t ≻ X u and e ′ ∉ FV(λeu), then t ≻ X-{e}∪{e ′ } u e ′ e . Keeping the same definitions for neutral terms and the base type interpretation as in Section 6, it is easy to check that Lemma 6.13 and Lemma 6.14 still hold. However, because of the new rules (@F s ) and (λF s ), Corollary 6.17 and Corollary 6.19, hence Lemma 6.16 and Lemma 6.18 reveal new dependencies that require introducing the following new computability property for a set S of terms of type T :

Note that big symbols do not need any computability property because they are bigger than everybody else, and therefore other computability properties do not depend upon the computability of big symbols. It follows that they cannot be implied in any circularity.

Proof. The proof is the same as for Lemma 6.15 except for the new case:

Proof. As for Lemma 6.16 but using Lemma 8.3 instead. Corollary 8.5. U → V satisfies (comp-neutral) if:

• U satisfies (comp-sn) and (comp-red);

• V satisfies (comp-red) and (comp-neutral);

-U > W . Then, g(⃗ u) is computable since W satisfies (comp-small).

-U = W . Then, g(⃗ u) is computable by induction hypothesis (1). • (F s @) There are u and v such that w = uv and f( ⃗ t) ≻ τ uv. By induction hypothesis (2), u and v are computable. Therefore, uv is computable. • (F s X ) Not possible.

8.3.

Well-foundedness of CPO with small symbols. In contrast with the previous cases, we cannot conclude from the above lemmas that, for every type T , T is a computability predicate, because of circularities.

Indeed, for A to satisfy (comp-small), we need, for every small symbol f ∶ T → A, T to satisfy (comp-sn); but for T to satisfy (comp-sn) when T = U → V , we need U to satisfy (comp-neutral); but for U to satisfy (comp-neutral) when U = W → A, we need A to satisfy (comp-small). To break this circularity, we will make these dependencies more precise by introducing sets of positions in types that reflect how these computability properties depend from each other. The idea here is that if there is no problematic occurrence of A in T , then T satisfies (comp-sn), and similarly for the other properties.

Instead of sets of positions, we could have simply considered boolean functions returning true if T contains a problematic occurrence of A. Considering positions allows us to pinpoint precisely which occurrences are problematic, and therefore to obtain sharper conditions on F s ensuring the absence of cycle in the dependency graph of the computability properties. Of course, one may think that there are different ways to carry out these proofs, resulting in different dependency graphs. We believe that these relationship are intrinsic to the computability properties, although we have not been able to substantiate this claim so far. Definition 8.9 (Computability-property positions). For each computability property (S standing for (comp-sn), R for (comp-red), N for (comp-neutral), L for (comp-lam) and C for (comp-small)), we inductively define a set of positions in a type T wrt a sort A as follows:

Note that RPos A (T ) = SPos A (T ) ⊆ LPos A (T ) and NPos A (T ) ⊆ CPos A (T ). Straightforward simplifications then yield:

We can now express in Figure 4 conditions on the types of the small symbols ensuring, as we shall show next, the absence of cycles in the dependency graph.

Consider the (small-sort) case and assume that T i A. Then, either T i = A and SPos A (T i ) = ∅ by definition, or T i ⋖ A and SPos A (T i ) = ∅ by Lemma 8.11. The condition for base types is therefore (strictly) weaker than the one for arrow types. This weaker

form will indeed be important later for deciding if a function symbol of base output type can be declared small.

Lemma 8.11. If T > T ′ and Sort A (T ) then:

Proof. We proceed by induction on T . Note that Sort A (T ′ ) by Lemma 2.6.

• T = B. Since Sort A (T ), we have B ≤ A. By transitivity, T ′ < A. Hence, by Lemma 2.5, Sort ⋖A (T ′ ). Therefore,

-SPos A (T ) = ∅. Then, NPos A (U ) = ∅ and SPos A (V ) = ∅. By (typ-arrow), there are two cases:

By (typ-arrow), there are two cases:

By (typ-arrow), there are two cases:

Lemma 8.12. Assume that the condition (small-arrow) of Figure 4 holds. Let A be a sort such that, for all sort B ⋖ A, B satisfies (comp-small), and let T be a type such that Sort A (T ). Then:

By (typ-right-subterm) and transitivity, T > V ′ . Hence, by induction hypothesis, V ′ satisfies (comp-sn), (compred), (comp-neutral), (comp-lam) and (comp-small).

Let now W ≤ T . By Lemma 2.6, Sort A (W ). Since LPos A (T ) = ∅, we have CPos A (T ) = ∅. Hence CPos A (W ) = ∅ by Lemma 8.11. If W = T , we have already seen that T satisfies (comp-small). Otherwise, W > T and, by induction hypothesis, W satisfies (comp-small). Therefore, by Corollary 8.7, T satisfies (comp-lam).

Theorem 8.13. Assume that the conditions of Figure 4 hold. For all type T , T is a computability predicate, i.e. satisfies (comp-sn), (comp-red), (comp-neutral), (comp-lam) and (comp-small).

Proof. We proceed by induction on ⋗ which is well-founded by assumption (typ-sn). We distinguish two cases:

• T is a sort A. By Lemma 6.23, A satisfies (comp-red), (comp-neutral), (comp-lam). By Lemma 6.24 and induction hypothesis, A satisfies (comp-sn). Let W < A. By Lemma 2.5, Sort ⋖A (W ). By Lemma 8.10, CPos A (W ) = ∅. Therefore, W satisfies (comp-small) by Lemma 8.12.

Let now f α(f) ∶ ⃗ T → A be small. By (small-sort), we have (∀i) Sort A (T i ) and SPos A (T i ) = ∅. Therefore, ⃗ T satisfies (comp-sn) and (comp-red) by Lemma 8.12. Hence, A satisfies (comp-small) by Lemma 8.8.

• Otherwise, T = U → V . Since T ⊳ l U , by induction hypothesis, U is a computability predicate. Let now V ′ be a type such that V ≥ V ′ . By (typ-right-subterm) and transitivity, T > V ′ . By induction hypothesis, V ′ is a computability predicate. Therefore, U → V satisfies (comp-sn) by Lemma 6.13, (comp-red) by Lemma 6. Proof. After Theorem 6.11, Theorem 8.13 and Lemma 7.25.

8.4.

Checking computability assumptions for small symbols. We explore here simple sufficient conditions under which the set SPos A (T ) is empty, and therefore, which symbols whose output type is a sort A can be declared as small. The order of a type plays an important role here. In case these conditions are not met, it is of course always possible to check (small-sort) and (small-arrow), which are both decidable.