Jean-Pierre Jouannaud

Jianqi Li

Termination of dependently typed rewrite rules

Keywords: 1998 ACM Subject Classification F.4.1 Mathematical Logic, F.4.2 Other Rewriting Systems Keywords and phrases rewriting, dependent types, strong normalization, path orderings Digital Object Identifier 10.4230/LIPIcs.TLCA.2015.x σ ∈ Γ Γ Σ x : σ Abstraction: Γ, x : σ Σ t : τ

Our interest is in automated termination proofs of higher-order rewrite rules in presence of dependent types modulo a theory T on base types. We first describe an original transformation to a type discipline without type dependencies which preserves non-termination. Since the user must reason on expressions of the transformed language, we then introduce an extension of the computability path ordering CPO for comparing dependently typed expressions named DCPO. Using the previous result, we show that DCPO is a well-founded order, behaving well in practice.

Introduction

This paper addresses the problem of (semi-)automating termination proofs for typed higherorder calculi defined by rewrite rules. Since many automated techniques exist for showing termination of simply typed higher-order rewrite rules, our first approach is to reduce the former to the latter.

To this end, we introduce a non-termination preserving transformation from dependently typed algebraic λ-terms to simply typed algebraic λ-terms. Unlike the transformation used for showing strong normalization of LF [START_REF] Harper | A framework for defining logics[END_REF], the present one uses algebraic symbols and type constructors in an essential way. Dependently typed rewrite rules can then be shown terminating via the transformation. The user can therefore benefit from all existing tools allowing to check termination of higher-order rewrite rules. The drawback is that these tools will operate on the transformed rules.

Among all termination proof techniques, we favour the one reducing termination proofs to ordering comparisons between lefthand and righthand sides of rules. These comparisons require well-founded orders on typed algebraic λ-terms which are stable by context application and substitution instance. CPO is such an order on simply typed algebraic λ-terms, defined recursively on the structure of the compared terms [START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF]. CPO is indeed well-founded on weakly polymorphic λ-terms, the familiar ML-discipline for which quantifiers on types can only occur in prefix position. A recent extension of core CPO to appear in LMCS handles inductive types, constructors possibly taking functional arguments, and function symbols smaller than application and abstraction.

We formulate here a new extension DCPO of CPO for dependently typed algebraic λ-terms. DCPO is then viewed as an infinite set of dependently typed rewrite rules which are shown terminating by checking the transformed rules with CPO. It follows that DCPO is a well-founded order of the set of dependently typed λ-terms, whose syntax-directed comparisons require little input from the user, in the form of a precedence on the algebraic symbols used in the rules. DCPO is our answer for practice. Substitutions are type-preserving homomorphisms avoiding captures, see for example [START_REF] Barendregt | Lambda calculus with types[END_REF], written here in postfix form, using the notation {x i → s i } i . The congruence on terms generated by renaming the free variable x in s by the fresh variable z ∈ FV(λx.s) to yield the term λz.s{x → z} is called α-conversion, denoted by = α . We use γ, θ for substitutions.

A higher-order rewrite rule is a quadruple ∆ Σ l → r : σ made of lefthand and righthand side terms l, r, and possibly omitted environment ∆ and type σ. Rules β and η are particular rewrite rule schemas. Reductions are defined as usual, and are a particular case of reductions in presence of dependent types, see Definition 5. A higher-order reduction ordering is a quasi-order on terms satisfying: (i) its strict part is well-founded ; (ii) its equivalence is a congruence ; (iii) monotonicity: s t implies u[s] p u[t] p (assuming typability); (iv) stability: s t implies sγ tγ for all substitutions γ; and (v) functionality: -→ β ∪ -→ η ⊆ .

Given a set E the notation s shall be used for a list, multiset, or set of elements of E. Given a binary relation on E, we use s lex t and s mul t for its lexicographic and multiset extensions respectively. We use s t for (∀t ∈ t) s t, and s t for (∃s ∈ s) s t.

A rewrite relation generated by a set of rules R ∪ {β, η} can be proved terminating by checking whether l r for all rules in R with some higher-order reduction ordering [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. CPO is such a higher-order reduction ordering based on three ingredients [START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF]:

-an order ≥ → on simple types, whose strict part > → satisfies (i) well-foundedness:

> → ∪{ σ → τ, σ | σ, τ ∈ T → S } is well-founded ; (ii) right arrow subterm: σ → τ > → τ ; (iii) preservation: σ → τ = → ν iff ν = σ → τ , σ = → σ , τ = → τ and (iv) decreasingness: σ → τ > → ν implies τ ≥ → ν or ν = σ → µ and τ > → µ.
-a quasi-order ≥ F on F ∪ {@, λ} ∪ X called precedence s.t.: (i) its strict part > F restricts to F ∪ {@, λ}, is well-founded, and satisfies (∀f

∈ F) f > F @ > F λ; (ii) its equivalence = F contains pairs in F × F and all pairs {(x, x) | x ∈ X }. -(∀f ∈ F ∪ {@,
λ}), a status operator _ f ∈ {lex, mul} in postfix index position such that _ @ = mul. Equivalent symbols have the same status.

The following auxiliary relations are used to define CPO [START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF] : s ≥ X t iff s = α t or s > X t, for a set of variables X disjoint from FV(s), is the main order; s > X t and s > X t defined respectively as (∀v ∈ t) s > X v and (∃u ∈ s) u > X t ; s : σ > X t : τ (resp., s : σ ≥ X t : τ ) for s > X t (resp., s ≥ X t) and σ ≥ → τ ; -we are interested in the typed order s : σ > ∅ t : τ , written s : σ > t : τ . Definition 1. Given Γ F s : σ and Γ F t : τ , s > X t iff either t ∈ X and s ∈ X var s = λx : µ.u and u{x → z} : ν ≥ X t : τ subtλ s = f (s), t = λx : µ.v and s> X∪{z:µ} v{x → z} Fλ s = @(u, w), t = λx : µ.v, x ∈ FV(v) and s > X v @λ s = λx : µ.u, t = λy : µ.v and u{x → z} > X v{y → z} λλ s = @(λx : µ.u, w) and u{x → w} ≥ X t beta

s = λx : µ.@(u, x), x ∈ FV(u) and u ≥ X t eta otherwise s = f (s), t = g(t)
with f, g ∈ F ∪{@, λ} ∪ X , and either subt s :

σ ≥ t : τ prec f > F g and s > X t stat f = F g, s > X t and s : σ > f t : τ
This definition of CPO is organized differently from [START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF] to be more compact. The last three cases originating in Dershowitz' recursive path ordering [START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF] describe the normal behaviour of head symbols, whether or not in F. Note here that > f is the status extension (lexicographic or multiset) of the order >. The first 7 cases describe other behaviours, either specific (var, beta, eta), or using explicit α-conversion for the others. In its recursive call, caseFλ increases the set X of upper variables, while other recursive calls either keep it unchanged or reset it to ∅. Relaxations of these recursive calls are indeed ill-founded.

Theorem 2 ([9]). >

+ is a higher-order reduction ordering.

3

Dependent algebras λ Π

Σ

We move to a calculus with dependent types inspired by Edinburgh's LF [START_REF] Harper | A framework for defining logics[END_REF], an extension of the simply typed λ-calculus which can be seen as a formal basis for dependently typed programming languages and their formal study as done with Elf [START_REF] Pfenning | Elf: A language for logic definition and verified metaprogramming[END_REF]. In higher-order algebras, types are typable by a single, usually omitted constant TYPE. In dependent algebras, as in other type theories, types (called type families) are typed by kinds, TYPE being one of them, which describe their functional structure. Let S, F and V be pairwise disjoint sets of respectively type symbols, algebraic function symbols, and variables. Algebraic function symbols in F may carry an arity upper-indexing their name. Type symbols in S are curried constants which kind may be functional. We use respectively f and a for a typical function or type symbol. Raw terms are given by the following grammar:

Kinds K := TYPE | Πx : A.K T ypes A, B := a | Πx : A.B | λx : A.B | A N Objects M, N := x | λx : A.M | M N | f n (M 1 , ..., M n )
λ and Π are LF's binders. Notation = α stands for similarity. Here, λ and Π are binary operators, whose arguments are a type ((λx : A.u)| 1 = A), and the body of the abstraction or product ((λx : A.u)| 2 = u). Both may originate computations. We write f for f 0 ().

Typing judgements

All LF expressions are typed, objects by types, types by kinds, kinds by a special untyped constant KIND (the universe) asserting their well-formedness, we also call them valid. Five kinds of judgement are recursively defined by the LF type system of Figure 2.

sig Σ Σ is a valid signature Σ C Γ Γ is a valid context assuming sig Σ Σ ; Γ K K : KIND K is a valid kind assuming Σ C Γ Σ ; Γ T A : K type A has kind K assuming Σ ; Γ K K : KIND Σ ; Γ O M : A
object M has type A assuming Σ ; Γ T A : K Σ ; Γ T ∨O C : D and Σ ; Γ T ∨K C : D are self explanatory Environments pair up a signature and a context. Signatures assign kinds to type symbols and product types to function symbols. Contexts assign product types to variables. Env Θ := Σ ; Γ where nil is the empty set,

Sig Σ := nil | Σ, a : K | Σ, f n : Π{x i : A i } n .A Π{x i : A i } n .A is Con Γ := nil | Γ, x : A Πx 1 : A 1 .(. . . (Πx n : A n .A) . . .)
In dependent calculi, the order of constants or variables in the environment is determined by their types. This impacts the expression of the so-called substitution lemma:

Lemma 3. Let Σ ; Γ O M : A and Σ ; Γ, x : A, Γ T ∨O s : σ. Then, Σ ; Γ, Γ {x → M } T ∨O s{x → M } : σ{x → M }.
Applying the substitution lemma several times introduces an order on the application of elementary substitutions. We use the notation M • n {x i → N i } i to denote the sequential application to M of the elementary substitutions {x 1 → N 1 }, ..., {x n → N n } in this order. We use the word dependent substitution to stress this sequential behaviour of substitutions.

Given a valid signature Σ and a context Γ valid in Σ, the set λ Σ of valid expressions, called terms is the (disjoint) union of the sets K Π Σ of valid kinds, T Π Σ of valid types and O Π Σ of valid objects (possibly abbreviated as K, T , O). Our presentation of LF performs classically the necessary sanitary checks when forming the signatures and contexts and only those.

Signatures

[Empty] sig nil [TConst] Σ ; nil K K : KIND sig Σ, a : K a / ∈ dom(Σ) [Const] sig Σ Σ ; {x i : A i } k T A k+1 (k = 0..n) : TYPE sig Σ, f n : Π{x i : A i } n .A n+1 f ∈ dom(Σ) Contexts [Empty] sig Σ Σ C nil [Var] Σ C Γ Σ ; Γ T A : TYPE Σ C Γ, x : A x / ∈ dom(Γ) Kinds [Univ] Σ C Γ Σ ; Γ K TYPE : KIND [Prod] Σ ; Γ, x : A K K : KIND Σ ; Γ K Πx : A.K : KIND Types [Ax] Σ C Γ Σ ; Γ T a : K a : K ∈ Σ [Abs] Σ ; Γ, x : A T B : K Σ ; Γ T λx : A.B : Πx : A.K [App] Σ ; Γ T A : Πx : B.K Σ ; Γ O M : B Σ ; Γ T A M : K{x → M } [Prod] Σ ; Γ, x : A T B : TYPE Σ ; Γ T Πx : A.B : TYPE [Conv] Σ ; Γ T A : K Σ ; Γ K K : KIND Σ ; Γ T A : K K ≡ K Objects [Ax] Σ C Γ x : A ∈ Γ Σ ; Γ O x : A [Fun] Σ ; Γ O M i : A i {x 1 → M 1 , ..., x i-1 → M i-1 } Σ ; Γ O f n (M 1 , ..., M n ) : A • n {x i → M i } i where f n : Π{x i : A i } n .A ∈ Σ [Abs] Σ ; Γ, x : A O M : B Σ ; Γ O λx : A.M : Πx : A.B [App] Σ ; Γ O M : Πx : A.B Σ ; Γ O N : A Σ ; Γ O M N : B{x → N } [Conv] Σ ; Γ T ∨O s : σ Σ ; Γ T ∨K σ : TYPE/KIND Σ ; Γ T ∨O s : σ σ ≡ σ Figure 2
LF Typing rules ≡ denoting the convertibility relation, a congruence discussed next in more details, that is generated by βη-conversion on similar terms on the one hand and on the other hand by an additional arbitrary congruence between object terms stable by substitution (possibly identifying them all [START_REF] Barthe | The relevance of proof-irrelevance[END_REF]). By its definition as a congruence, convertibility respects our syntactic categories, objects, types and kinds.

Our dependently typed calculus is referred to as λ Π Σ to stress the signature Σ, or simply LF. Lexicography: we use K for kinds, A,B,C,D for types, M,N for objects, s,t,u,v,w,l,r for (objects or types), σ, τ, µ, ν for (type or kinds), and γ, θ for substitutions.

Dependent rewriting and convertibility

In LF, the usual rules of the λ-calculus apply at the object and type levels, making four different rules generating a congruence called βη-convertibility: beta: (λx :

A.B) M → β T B{x → M } (λx : A.M ) N → β O M {x → N } eta: λx : A.(B x) → η T B if x ∈ FV(B) λx : A.(M x) → η O M if x ∈ FV(M )
Convertibility plays a key role for typing via Conv. In LF, convertibility is defined as the congruence generated by βη-reductions. In reality, convertibility must be strengthened on object level terms in order to type most examples. This problem has been considered in the framework of the calculus of constructions with the Calculus on Inductive Constructions [START_REF] Paulin-Mohring | Inductive definitions in the system Coq -rules and properties[END_REF], the Calculus of Algebraic Constructions [START_REF] Blanqui | The calculus of algebraic constructions[END_REF] and the Calculus of Constructions Modulo Theory [START_REF] Strub | Coq modulo theory[END_REF][START_REF] Barras | CoqMTU: A higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory[END_REF], for which convertibility includes respectively: primitive recursion at higher type generated by the user's inductive types; the user's higher-order rules; and a decidable object-level first-order theory like Presburger arithmetic. These frameworks can be restricted to the LF type system seen as a particular case of the calculus of constructions. In the context of LF, it relates to the liquid types discipline [START_REF] Rondon | Liquid types[END_REF], which shares similar objectives. We now introduce dependent rewrite rules and rewriting.

Definition 4. Given a valid signature Σ, a plain dependent rewriting system is a set {∆ i l i : σ i → r i : τ i } i of quintuples made, for every index i, of a context ∆ i , lefthand and righthand side terms l i , r i , and terms σ i , τ i , s.t. FV(r i ) ⊆ FV(l i ), Σ ; ∆ i T ∨O l i : σ i and Σ ; ∆ i T ∨O r i : τ i with σ i ≡ τ i . ∆ i , σ i and τ i may be omitted.

Definition 5 (Dependent rewriting). Given a rewriting system R, one step rewriting is a relation over terms, written Σ ; Γ R s -→ p t (in short, s -→ R t) defined as: s and t are both types or objects which are typable under Σ; Γ, ∆ l → r :

A ∈ R, where FV(∆) ∩ FV(Γ) = ∅. s = s[l • γ] p and t = s[r • γ] p ,
where γ is a dependent substitution wrt to ∆.

A major semantic property expected from rewrite rules is that rewriting preserves types. In presence of dependencies, types are usually preserved up to some congruence defined by the rules themselves, as in the Calculus of Inductive Constructions or the Calculus of Algebraic Constructions [START_REF] Blanqui | The calculus of algebraic constructions[END_REF]. Here, preservation of typing by rewriting, up to type erasures, follows from Lemma 14.

Example 3.1. Here is a simple example with dependent lists of elements of a given type A. We allow ourselves with some OBJ-like mixfix syntax, using "_" for arguments' positions: nat, A : TYPE; List : Πm : nat.TYPE; 0 : nat; _ + 1 : Πn : nat.nat; _ + _ : Π{m, n : nat}.nat cons : Π{n : nat, a : A, l : List n}.List (n + 1) ,a,app(m,n,k,l)) Using LF's typing rules given in Figure 2, we get:

app : Π{m, n : nat, k : List m, l : List n }. List (m + n) 0 + n → n app(0, n, nil, l) → l (m + 1) + n → (m + n) + 1 app(m+1, n, cons(m, a, k), l) → cons(m+n
{m, n : nat} n, 0 + n, (m + 1) + n, (m + n) + 1 : nat {n : nat, l : List n} app(0, n, nil, l) : List (0 + n) {m, n : nat, k : List m, l : List n} app(m+1, n, cons(m, a, k), l) : List ((m + 1) + n) {m, n : nat, k : List m, l : List n} cons(m+n, a, app(m, n, k, l)) : List ((m + n) + 1)
Typing these rules requires a conversion relation extending βη-conversion on objects with Presburger arithmetic to identify List (0+n), List n and List ((m +1)+n), List ((m+n)+1).

© Jean-Pierre Jouannaud and Jianqi Li 13th International Conference on Typed Lambda Calculi and Applications (TLCA '15). Editor: Thorsten Altenkirch; pp. [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF][START_REF] Blanqui | The calculus of algebraic constructions[END_REF][START_REF] Blanqui | HORPO with computability closure : A reconstruction[END_REF][START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF][START_REF] Blanqui | The computability path ordering[END_REF][START_REF] Borralleras | A monotonic higher-order semantic path ordering[END_REF][START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF][START_REF] Harper | A framework for defining logics[END_REF][START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF][START_REF] Kusakari | Static dependency pair method based on strong computability for higher-order rewrite systems[END_REF] Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

Encoding LF in higher-order algebras

We define here a transformation from the source language to a target language which preserves non-termination of arbitrary reductions, not just β-reductions as in LF. Our target language is the simply-typed λ-calculus enriched with function symbols and type constants of Section 2, a choice which has three important advantages: the target vocabulary can be as close as possible from the source vocabulary; the transformation preserves termination as well as non-termination; the transformed rules can be checked for termination by CPO. The higher-order algebra encoding λ Π Σ will be λ → Σ flat , where Σ flat = S flat Σ flat is a higher-order (non-dependent) signature whose two pieces are described next. The set of types in λ

→ Σ flat is denoted by T → S flat . Terms in λ → Σ flat ,
F.G) M → β G{x → M } = E. By Corol. 8, |D| = |G| = |G{x → M }| = |E|.
Erasing is extended to environments Σ ; Γ by:

|Γ| = {x : |A| | x : A ∈ Γ} and |Σ| = {a : |K| | a : K ∈ Σ} ∪ {f n : |A 1 | → . . . |A n | → |A| where f n : Π{x i : A i } n .A ∈ Σ}.
Note here that a constructor like cons : Πn : N at, x : N at, l : List(n).List(n + 1) ∈ Σ becomes cons : N at → N at → List → List ∈ |Σ|. Eliminating the first (type) argument from cons would easily allow writing rules for which termination is not preserved by the transformation. This does not mean, however, that writing such rules is actually impossible.

Term flattening

Besides types and function symbols in |Σ|, the signature Σ flat will contain algebraic symbols, called flattening constructors, used to mimic LF's abstraction and product.

Σ flat = |Σ| ∪ {lo 2 σ : * → σ → σ, lf 2 σ : * → σ → σ, pif 2 σ : * → (σ → * ) → * | σ ∈ T → S flat }
We may omit subscripts σ, τ in constructor's names, and use lof 2 for (lo 2 σ /lf 2 σ ). The first argument of the flattening constructors, of type * , is the flattening of some dependent type A. The second argument of lo 2 σ is the interpretation of some object M : A, hence σ = |A|, while that of lf 2 σ is the interpretation of a type A : K, hence σ = |K|. Since signatures are monomorphic and σ is arbitrary, the flattening constructors must be indexed by these types. We now define a flattening transformation for expressions of LF which are typed in some environment left unspecified to expressions of λ → Σ flat : Definition 11. The flattening function _ from λ Σ to λ Σ flat (the context in which the input term is valid is omitted) is defined as

x : A = x : |A| Πx : A.B : TYPE = pif 2 |A| ( A, λx : |A|. B) M N : A = @( M, N ) λx : A.M : Πx : A.B = λx : |A|.lo 2 |B| ( A, M ) A N : K = @( A, N ) λx : A.B : Πx : A.K = λx : |A|.lf 2 |K| ( A, B) a : K = a f n (M 1 , ..., M n ) : A = f n ( M 1 , ..., M n )
Since flattening is not surjective, we denote by λ Σ ⊂ λ Σ flat its target. Note that type symbols in S become both sorts in S flat and function symbols in Σ flat , with the same (overloaded) name. This definition obeys the following principles: (i) flattening is a homomorphism, hence commutes with substitutions; (ii) because types may depend on objects, the type information associated with bound variables must be recorded by the encoding to preserve non-termination; (iii) the types of the flattening constructors are compatible with the erasing transformation, which allows to trace the syntactic categories in the transformed world; (iv) the encoding of abstractions and products preserves their variable's binding, but two different encodings are used. The encoding of abstractions is an abstraction, in order to preserve beta-redexes via the transformation. Nothing like that is needed for product types which cannot be applied, and can therefore be transformed into terms of sort |TYPE| = * . In that case, the abstraction is encapsulated in the flattening constructor. This allows to single out easily products' encodings in the flattened world. Now, an LF object M : A is translated as a term M of type |A|, an LF type A : K is translated as both a type |A| and a term A of type |K|, an LF kind K : KIND is translated as a type |K|. Proof 13. The first three are proved by induction on the typing derivations of A, M and s respectively, using Lemma 9 for the third (translation of products) and for the conversion rule. Stability follows by induction on the typing derivation of s.

Preservation of reductions by flattening

Our goal now is to show that the reductions on objects and types in λ

Π Σ are mimicked in λ → Σ flat .
Since rewriting a term cannot not increase its set of free variables, rewriting commutes with the η-rule. A consequence is that, given a dependent rewrite system R, -→ βηR terminates iff -→ βR terminates: encoding the η-rule will not be necessary. To ease the reading, we use for our rewriting symbol in λ → Σ flat , and decorate subterms in flattened rules by their type. [β O ] @(λx : σ.lo 2 τ (A : * , M : τ ), N : σ) M {x → N } [β T ] @(λx : σ.lf 2 τ (A : * , B : τ ), N : σ) B{x → N } In these rules, A and σ are the term flattening and type erasure of the same dependent type D, a relationship that cannot be expressed in λ → Σ flat , hence is not kept in the transformed rules. For example, assuming A, s, t ∈ λ Σ and | A -1 | = σ, then u = @(λx : σ.lof 2 (A, s), t) is a redex which has no counter-part in λ Π Σ . There are indeed new rewrites in the flattened world, making preservation of non-termination a weaker property.

We use [R], [β], [βR] and β[βR] for

{ l r | l → r ∈ R}, {[β T ], [β O ]}, [β]∪[R],

and {β}∪[βR].

As with A, M, N, σ, τ used in [β], variables of R that denote expressions in λ Π Σ keep their name in [R], denoting now expressions of λ → Σ flat belonging to the same syntactic categories as in the dependent world. Then, an instance of a [β]-rule may not be the encoding of an instance of the β-rule in the dependent world if M/B match flattened terms which are no encoding of dependent expressions. Despite these approximations, reductions are preserved: Lemma 14. Let Σ; Γ T ∨O s : σ, s → βR t and Σ; Γ T ∨O t : τ . Then, |σ| = |τ | and s [βR] t. Proof 15. The proof is by induction on the typing derivation of s. All cases are by induction except those where the βR redex is at the top. We carry out four typical cases:

1.

[App]

Σ ; Γ T A : Πx : This Lemma contains the analog of the type-preservation property of non-dependent rewriting, equivalence by conversion being here equivalence modulo type erasures: subject reduction holds for dependent rewriting modulo type erasures.

B.K Σ ; Γ O M : B Σ ; Γ T s = A M : K{x → M } and M → βR M , hence A M → βR A M = t.
Thus λ Π Σ is terminating for an empty set R, implying strong normalisation of βη-reductions at both object and type level, for any convertibility relation ≡ containing βη-convertibility. In particular, ≡ can contain Presburger arithmetic, an important known extension of LF. ,a,app(m,n,k,l))

0 : nat _ +1 : nat → nat List : nat → * nil : List + : nat → nat → nat cons : nat → A → List → List app : nat → nat → List → List → List 0 + n → n (m + 1) + n → (m + n) + 1 app(0, n, nil, l) → l app(m+1, n, cons(m, a, k), l) → cons(m+n
These dependently typed rewrite rules being algebraic, their encoding is the identity. CPO proves their termination with app > F cons > F nil > F + > F _ + 1 > F 0, and List > → {nat, A}.

Theorem 16. Given a signature Σ, a dependent term rewriting system βηR is terminating in λ Π Σ if its flattening β βR is terminating in λ → Σ flat . Proof 17. By using Lemma 14 and a commutation argument for η.

Inverse encoding

Lemma 14 justifies our method for checking strong normalization by a transformation to a higher-order algebra where we can use standard techniques including CPO. But the flattened world is richer than the dependent world, there are more terms and rewrites. Nonetheless, we can also show that termination is partly preserved by defining an inverse transformation such that composing both is the identity. First, we define the inverse transformation on the subset λ Σ ⊆ λ Σ flat , hence allowing us to show that flattening is injective.

Definition 18. The inverse _ -1 : λ Σ → λ Σ is defined as:

x -1 = x a -1 = a f n (s 1 , ..., s n ) -1 = f n ( s 1 -1 , ..., s n -1 ) @(s, t) -1 = s -1 t -1 pif 2 (s, λx : σ.t) -1 = Πx : s -1 . t -1 λx : σ.lf 2 (s, t) -1 = λx : s -1 . t -1 λx : σ.lo 2 τ (s, t) -1 = λx : s -1 . t -1 Lemma 19 (Reversibility). Assume Σ; Γ s : σ in λ Π Σ . Then Σ; Γ ( s) -1 = s : σ.
Proof. By induction on s. Variables, type constants, applications and pre-algebraic terms are clear. We carry out one remaining case, the others being similar. ( Πx :

A.B) -1 = pif 2 |A| ( A, λx : |A|. B) -1 = Πx : ( A) -1 . ( B) -1
. We conclude by induction.

Corollary 20. Let σ; Γ T ∨O s : σ and s| p ∈ λ Σ for some p. Then s| p = s| q for some q.

Flattening being an injection from λ Σ to λ Σ flat , hence a bijection between λ Σ and its target λ Σ , provides strong evidence that λ Π Σ is faithfully encoded by flattening. It follows that, if s = t for s, t ∈ λ Σ , then s = t since s = s -1 = t -1 = t. We apply to Lemma 12:

Corollary 21 (inverse stability). Assume u{x → v} ∈ λ Σ . Then, u{x → v}

-1 = u -1 {x → v -1 }.
Therefore, rewrites in λ Σ can be mapped back to λ Σ , showing both that λ Σ is closed under rewriting by [βR], and that termination in λ Σ implies termination in λ Σ : Lemma 22. Let Σ ; Γ T ∨O s : σ and s [βR] u. Then u = t for some t st s → βR t.

Proof 23. By assumption s| p = lγ [βR] u| p for some p ∈ Pos( s), where l → r ∈ {β}∪R, γ a substitution in λ Σ and u| p = rγ. By Corollary 20, s| p = s| q for some q. By Lemma 19, s| q = lγ -1 = l -1 γ -1 (by Corollary 21) = lθ with θ = γ by Lemma 19.

Hence

s -→ βR s[rθ] q = t. Now, since flattening is a homomorphism, t = s[ rθ] p (by definition of q) = s[ rγ] p (by definition of θ) = u.
This does not prove, however, that termination in λ Π Σ implies termination in λ → Σ flat . The problem is that flattening is non-surjective, since many terms, like those headed by lof 2 , are no flattening of a dependent term. Further, some seemingly good-looking terms, like pif 2 σ (s, λx:σ.t) may not be either, even assuming that s, t are themselves flattening of dependent terms. This is the case because the flattened signature checks that term s has type * , hence is the encoding of some dependent type A, but cannot check whether |A| = σ as it should. The same happens with applications and pre-algebraic terms: (s, t) may not be typable in λ We now have the following infinite derivation: f (a, la) → f (b, lb) → f (a, lb) → f (a, la) . . .. Restricting rewrites on parameters could be a solution.

5

The Dependent Computability Path Ordering

DCPO is an extension of CPO obtained by adding new cases for products. All notations for DCPO are simply and systematically obtained by replacing the CPO ordering notation > by . For example, the precedence will be denoted by Σ . Type families are compared alternatively as types with Π and as terms with . The basic ingredients of DCPO are:

a precedence Σ on F∪S∪{@, λ, Π} s.t. Σ is well-founded, and (∀f ∈ F)f Σ @ Σ {λ, Π}.

a status f ∈ {Mul, Lex} for every symbol f ∈ F ∪ {@} with @ ∈ Mul.

a quasi-order Π on K ∪ T , whose strict part Π and equivalence = Π satisfy: (i) compatibility: ≡⊆ = Π ; (ii) well-foundedness:

Π ∪{ Πx : A.σ, A | A ∈ T , σ ∈ T ∪ K} is well-founded ; (iii) product body subterm: (∀σ ∈ T ∪ K) Πx : A.σ Π σ ; (iv) product preser- vation: |Πx : A.σ|= Π |τ | implies τ = Πx : B.µ for some B, µ, such that |A|= Π |B|, |σ|= Π |µ| ; (v) decreasingness: Πx : A.σ Π τ implies σ Π τ or else τ = Πx : B.ν, A= Π B and τ Π ν.
Building quasi-orders Π on types and kinds with a non-trivial equivalence = Π is not hard [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF].

We now define a first version of DCPO which can be justified by using CPO [START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF]. We will then discuss briefly an enhanced version justified by a more elaborated version of CPO [START_REF] Blanqui | The computability path ordering[END_REF]. In the following definition, z denotes a fresh variable of type A/B. Definition 24 (DCPO). Given Γ Σ s : σ and Γ Σ t : τ , then s X t iff either: (beta) 8. otherwise s = f (s), t = g(t) with f, g ∈ F ∪ S ∪{@} ∪ X , and either of (rpo)

1. t ∈ X
s : σ t : τ (subt) f > F g and s X t (prec) f = Σ g, s X t and s : σ ( ) f t : τ (stat)
All terms built by DCPO are well-typed under the assumption that both starting terms s, t are well-typed. Note (i) the importance of all our assumptions on Π , see for example Case statλΠ; (ii) the order may recursively compare objects with types, even when the input comparison operates on expressions in T 2 ∪ O 2 ; (iii) compared products cannot be kinds.

Example

We now consider our list example, skipping the rules on natural numbers which do not have dependencies. We shall use the (user defined) precedence app Σ {+, cons, nil}, multiset status for app, and a quasi-order on types in which, for all n : nat, then List n Π A and List m= Π List n for all m, n of type nat. Such a type order is easy to get by using a restricted RPO on type erasures, which equivalence therefore contains Presburger arithmetic.

See [START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF]. The goal app(0, n, nil, l) : List 0 + n l : List n is easy, although already requiring identification of 0 + n in List 0 + n with n in List n. We proceed with the second goal: app(m+1, n, cons(m, a, k), l) : List (m + 1) + n cons(m+n, a, app(m, n, k, l)) : List (m+n)+1 The type comparison List (m + 1) + n Π List (m + n) + 1 succeeds by using our type ordering which indeed equates both types, and we are left with the term comparison:

app(m + 1, n, cons(m, a, k), l) cons(m + n, a, app(m, n, k, l)) Using (prec), we get three subgoals, which are processed in turn, using indentation to identify the dependencies between recursive calls, the used Case being indicated between parentheses:

app(m + 1,

Properties of DCPO

Lemma 25 (Monotonicity, stability). Let s, t ∈ λ Σ st s : σ t : σ, C(x : σ) a context, and γ a substitution. Then C{x → sγ} C{x → tγ}.

Proof 26. By induction on the definition of s t and stability of the type order for monotonicity. By induction on the context, and use of the status rules for stability.

As anticipated, we now reduce the well-foundedness of DCPO to the well-foundedness of CPO by using Theorem 16, termination in the target higher-order algebra being checked by CPO. To this end, we need to show that, whenever s : σ t : τ , then s : |σ| > t : |τ |.

We start showing that an order on types and kinds of LF satisfying the requirements for DCPO becomes naturally an order on types of λ → Σ flat satisfying the requirements for CPO. Transitivity is clear. Of course, different choices of µ, ν may sometimes lead to contradictory orderings for σ, τ , hence the equality = → Σ flat may be strictly larger than the corresponding equality = Π . This has indeed no negative impact since the strict part Π is never used in comparisons. Further, the properties of Π transfer naturally to ≥ → Σ flat . Soundness follows: Lemma 27. Assume Π is a DCPO type order. Then ≥ → Σ flat is a CPO type order. The set Σ flat of function symbols of Σ flat is the union of S, F and the flattening constructors. The precedence > Σ flat is obtained by letting the flattening constructors be equivalent minimal symbols. The strict part of > Σ flat is clearly well-founded, while its equivalence is increased by the equality of the flattening constructors. We take status Mul for lo 2 , lf 2 , pif 2 .

Lemma 28. Let s : σ, t : τ and X ⊆ X such that s X t by any DCPO rule. Then s > X t.

Proof 29 (Sketch). The proof is by induction on the definition of DCPO, assuming by induction hypothesis that the property holds at every recursive call. Note that if s : σ, t : τ , σ Π τ and s > X t, then s : |σ| > X t : |τ | by Definition 5.1.

We then obtain the second main result of the paper as a corollary:

Theorem 30 (Well-foundedness of DCPO). Π is well-founded.

Proof 31. By theorem 16. Note that we use the full strength of that result, including the need for type-level rules instances of the various DCPO rules instances which compare types. This is possible since we only need preservation of non-termination by the flattening transformation, that is, the if direction of Theorem 16.

It follows that Π ∪ η is well-founded. One may wonder why we did not include η-rules in the definition of DCPO, since it is in the definition of CPO. The reason is the comparison of lefthand and righthand sides of [η], λx : |A|.lof 2 ( A, @( B, x)) > B which does not go through: the type comparison of the subgoal lof 2 ( A, @( B, x)) : σ > B : |A| → σ fails.

A realistic example

We consider here a more complex, non-algebraic, higher-order example. Given a list l of natural numbers x 1 , ..., x m , and a natural number y, a higher-order variable g which is meant to be instantiated by +, we define a higher-order function foldr such that (foldr(m, l, y) g) calculates g(x 1 g(x 1 , ...g(x m , y))), while (map(m, l) f ) calculates the list f (x 1 ), ..., f (x m ). succeeds by prec l > {g} @(@(g, z), @(foldr(m, l, y) g)) prec l > {g} @(g, z) prec l > {g} g succeeds by var l = foldr(m + 1, cons(m, z, l), y) > {g} z subt cons(m, z, l) : List(m + 1) > {g} z : nat which succeeds by subt l > {g} @(foldr(m, l, y), g) prec l = foldr(m + 1, cons(m, z, l), y) > {g} foldr(m, l, y) stat {m + 1, cons(m, z, l), y}(> {g} ) mul {m, l, y} which succeeds by repeated subt l > {g} g which succeeds by var, therefore ending the computation successfully.

DCPO comparison.

We now carry out the same computation with DCPO directly:

Conclusion

The amount of research work targeting automatic termination is vast. Among the most popular techniques are dependency pairs, introduced by Aart and Giesl and the size-changing principle, pioneered by Neil Jones, which have been generalized to dependently-typed rules [START_REF] Blanqui | A type-based termination criterion for dependently-typed higher-order rewrite systems[END_REF].

Dependent types can also be used to store annotations useful for proving termination [START_REF] Xi | Dependent ML an approach to practical programming with dependent types[END_REF]. Despite these proposals that recent prototypes try to combine, techniques used in Coq and Agda are still poor, as acknowledged by the authors on their websites. Using our techniques would improve this situation. Our first contribution is a new transformation for eliminating type dependencies using a framework richer than the simply-typed λ-calculus, which provides with a natural encoding, and allows us to consider arbitrary rewrite rules, not only β-and η-reductions. Furthermore, these results hold for a practical dependent type system made richer than LF's via a convertibility relation possibly stronger than βη-convertibility, hence allowing us to type many more terms. This easily implementable transformation allow us using existing implementations targeting termination of rules in presence of simple types. The transformation also allows us to show well-foundedness of DCPO, a version of CPO applying to dependently typed terms directly. This is done by considering pairs ordered by DCPO as dependently typed rewrite rules to which the transformation applies. Note that DCPO will naturally benefit from improvements of CPO, without changing the proof technique. In particular, we could easily accommodate size interpretations by using them as a precedence as in [START_REF] Borralleras | A monotonic higher-order semantic path ordering[END_REF], or type level rules such as s = (A u), t = Πy : B.v, with s X B and s X∪{z} v{y → z} flattened as s = @( A, u), and t = pik |B| ( B, λy : |B|. v), with s > X B and s > X∪{z} v{y → z}, whose justification requires the extension of CPO with small function symbols, here pik |B| , which behave as if they were smaller than application and abstraction [START_REF] Blanqui | The computability path ordering[END_REF]. We can then break the main goal into the above solvable subgoals.

Our main interest is indeed to prove termination directly at the dependent type level. Using DCPO allows the programmer, in case of failure, to get an error message in her/his own dependently typed syntax, rather than in the transformed syntax as would be the case when using CPO on the transformed rules. To our knowledge, this is the very first general -Coq and Agda's techniques are very limited-, purely syntactic method that allows one to show termination of a set of dependently typed rewrite rules via computations taking place on the user's dependently typed rules.

Figure 1

 1 Figure 1Type system for monomorphic higher-order algebras

4. 1 Corollary 8 .

 18 Type erasuresTypes. Types in λ → Σ flat are arrow types built from the set of sorts S flat = { * }∪{a | a : K ∈ Σ}. The new sort * will serve to encode LF product types as terms of sort * in λ → Σ flat . LF objects will be encoded as terms whose types are erasures of LF types, as defined next. Type erasures. The classical erasing transformation from families and kinds in λ Π Σ to types in λ → Σ flat eliminates dependencies from objects by replacing product types by arrow types: Definition 6. The erasing map |.| : T ∪ K → T → S flat is defined as: (1)|a| = a (2)|Πx : A.B| = |A| → |B| (3)|λx : A.B| = |B| (4)|TYPE| = * (5)|Πx : A.K| = |A| → |K| (6)|A N | = |A| Sorts being constants, an induction shows that variables in types are eliminated in rule (6): Lemma 7. Let A ∈ T ∪ K. Then FV(|A|) = ∅. For any E ∈ K ∪ T , y ∈ V, and s ∈ O → Σ flat , |E{y → s}| = |E|{y → |s|} = |E|. Lemma 9 (Conversion equality). Let D, E ∈ T such that D ≡ E. Then, |D| = |E|. Proof 10. Conversion is a congruence generated by βη-rewriting and an equivalence = O on object terms. We show that the property is true of both relations by induction on D. (1) Case D = a : K. Then E = D. (2) Case D = Πx : A.B : TYPE. Then E = Πx : A .B : TYPE with A ≡ A and B ≡ B . By induction hypothesis (and definition of the erasing map). (3) Case D = λx : A.B : Πx : A.K. There are two cases: a. E = λx : A .B : Πx : A .K, with A ≡ A and B ≡ B . By induction hypothesis. b. D = λx : A.(E x) → η E where x / ∈ FV(E). Then |D| = |λx : A.(E x)| = |E x| = |E|. (4) Case D = A M : K, where M is an object. Again two cases: a. E = A M , A ≡ A and M ≡ M . Then, |D| = |A| and |E| = |A |. By induction. b. D = (λx :

Lemma 12 .

 12 The following properties hold: (1) soundness: let Σ ; Γ T A : K. Then Σ flat ; |Γ| A : |K|; (2) soundness: let Σ ; Γ O M : A. Then Σ flat ; |Γ| M : |A|; (3) preservation: let Σ ; Γ T ∨O s : σ. Then FV(s) = FV( s); (4) stability: let Σ ; Γ T ∨O s, t : σ, τ and x : τ ∈ Γ. Then s{x → t} = s{x → t}.

  By induction hypothesis, Σ ; Γ T ∨O M : B , |B | = |B| and M [βR] M . By definition of flattening, A M = @( A, M ) : |K{x → M }| = |K| by Corollary 8. By definition of erasing, |Πx : B.K| = |B| → |K|. By Lemma 12 (soundness) A : |B| → |K| and M : |B |. Finally, t = @( A, M ) : |K|, we are done.

  T ∨O s : σ Σ; Γ T ∨K σ : TYPE/KIND Σ ; Γ O s : σ σ ≡ σ . By induction hypothesis, Σ; Γ T ∨O t : τ , |τ | = |σ | and s [βR] t. By Lemma 12, t : |τ |. Lemma 9 concludes.

  O λx : A.u : Πx : A.B Σ ; Γ O M : A Σ ; Γ O s = λx : A.u M : B{x → M } and t = u{x → M }. By inversion, Σ ; Γ O u : B, thus t : B{x → M } by Lemma 3. λx : A.u M = @(λx : A.lo 2 |B| ( A, u), M ) [β] u{x → M } by definition of [β O ]. Lemma 12 and Corollary 8 conclude. 4. Σ ; Γ T ∨O s : σ, s = l • γ and t = r • γ for some l → r ∈ R such that l, r have convertible types µ, ν in their environment. By Lemma 3 applied repeatedly, s, t have types σ = µ • γ and τ = ν • γ, and since ≡ is a congruence, σ ≡ τ . By Lemma 12(stability), lγ = l γ and rγ = r γ hence s [R] t by definition of [R] .

Example 4 . 1 .

 41 Here are the transformed signature and rules for our example on Lists: nat, A : *

ΠΣ

  when s, t are typable in λ Π Σ and @( s, t) is typable in λ → Σ flat . © Jean-Pierre Jouannaud and Jianqi Li 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Editor: Thorsten Altenkirch; pp. 10-15 Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany Indeed, termination in λ Π Σ does not imply termination in λ → Σ flat as shown by this example: let o : TYPE; List : Πx : o.TYPE; a, b : o; la : List a; lb : List b; f 2 : Πm : o, l : List m . o; and {f (a, la) → f (b, lb); b → a, lb → la}, whose dependent derivations are all finite since b cannot rewrite to a in f (b, lb), a non-typable term. In the flattened signature, o and List are sorts, and a, b : o; la, lb : List; f 2 : o → List → o; and {f (a, la) → f (b, lb); b → a; lb → la}.

  and s ∈ X (var) 2. s = (u N ) and u X t or N : B X t : τ (subt@) 3. s = λ/Πx : A.u and u{x → z} :µ X t : τ (subtλΠ) 4. s = f (s), f ∈ Σ, t = (λ/Πy : B.v) : Πy : B.K, and s X B and s X∪{z} v{y → z} (ΣprecλΠ) 5. s = λx : A.u : Πx : A.C, t = λy : B.v : Πy : B.D, |A| = |B|, A X B and u{x → z} : C X v{y → z} : D (statλ) 6. s = Πx : A.u, t = Πy : B.v, |A| = |B|, A X B and u{x → z} X v{y → z} (statΠ) 7. s = ((λx : A.u) : (Πx : A.C) w : A), and u{x → w} t

Definition 5 . 1 .

 51 Given σ, τ ∈ T → S flat , let σ ≥ → Σ flat τ iff ∃µ, ν ∈ T ∪K, |µ| = σ, |ν| = τ , and µ Π ν.

  whose set is denoted by λ Σ flat , are meant to encode LF objects and types in a way which mimics dependently typed computations. We do not encode LF kinds, since computations in kinds are indeed computations on types or objects. Indeed, dependent types will be encoded in λ

→

Σ flat both as types and as terms.

  nat, n : nat, cons(m, a, k) : List m + 1, l : List n} mul {m : nat, n : nat, k : List m, l : List n} which yields m + 1 : nat m : nat and cons(m, a, k) : List m + 1 k : List m, for the reader.

	n, cons(m, a, k), l) m + n	(prec)
	app(m + 1, n, cons(m, a, k), l) m	(subt)
	m + 1 : nat m : nat which yields
	nat Π nat which succeeds and m + 1 m which succeeds by (subt)
	app(m + 1, n, cons(m, a, k), l) n	which succeeds by (subt)
	app(m + 1, n, cons(m, a, k), l) a	(subt)
	cons(m, a, k) : List (m + 1) a : A which yields
	List (m + 1) Π A which succeeds and cons(m, a, k) a which succeeds by (subt)
	app(m + 1, n, cons(m, a, k), l) app(m, n, k, l)	(stat)
	{m + 1 :

  nat : TYPE | 0 : nat | + 1 : Πx : nat.nat List : Πm : nat.TYPE | nil : List 0 | cons : Π{m : nat, x : nat, l : List m}.List m + 1 map : Π{m : nat, l : List m}.(Πf : (Πx : nat.nat).List m) foldr : Π{m : nat, l : list m, y : nat}.Πg : (Π{x 1 : nat, x 2 : nat}.nat).nat map(0, l) → λf : (Πx : nat.nat).nil | foldr(0, l, y) → λg : Π{x 1 : nat, x 2 : nat}.nat.y map(m + 1, cons(m, x, l)) → λf : Π{x : nat}.nat.cons((f x), map(m, l)) foldr(m + 1, cons(m, z, l), y) → λg : Π{x 1 : nat, x 2 : nat}.nat.(g z (foldr(m, l, y) g)) To carry out the example, we let List > T nat, foldr > map > cons > nil > lf 2 > lo 2 > List > nat and (∀σ > T τ ) lf 2 σ > lf 2 τ and lo 2 σ > lo 2 τ . We consider the last rule only. CPO comparison. It generates the following goals (omitting the type comparisons): l > λg : nat → nat → nat.lo 2

		prec
	l > {g} nat	succeeds by prec
	l > {g} λx 1 : nat.lf 2 nat (nat, λx 2 : nat.nat)	Fλ
	l > {g,x1} lf 2 nat (nat, λx 2 : nat.nat)	prec
	l > {g,x1} nat	succeeds by prec
	l > {g,x1} λx 2 : nat.nat	Fλ
	l > {g,x1,x2} nat

nat

(lf 2 nat (nat, λx 1 : nat.lf 2 nat (nat, λx 2 : nat.nat)), @(@(g, z), @(foldr(m, l, y) g))) Fλ l > {g} lo 2 nat (lf 2 nat (nat, λx 1 : nat.lf 2 nat (nat, λx 2 : nat.nat)), @(@(g, z), @(foldr(m, l, y), g))) l > {g} lf 2 nat (nat, λx 1 : nat.lf 2 nat (nat, λx 2 : nat.nat))

  © Jean-Pierre Jouannaud and Jianqi Li 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Editor: Thorsten Altenkirch; pp.[START_REF] Harper | A framework for defining logics[END_REF]-15 Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany foldr(m + 1, cons(m, z, l), y) λg : Π{x 1 : nat, x 2 : nat}.nat.(g z (foldr(m, l, y) g)) (ΣprecλΠ) l Π{x 1 : nat, x 2 : nat}.nat List(m + 1) {g} z : nat succeeds by (subt) l {g} (foldr(m, l, y) g)} (prec) l {g} foldr(m, l, y) (stat) {m + 1, cons(m, z, l), y} {g} {m, l, y} which succeed by repeated (subt) l {g} g succeeds by (var), therefore ending the computation successfully.

		(ΣprecλΠ)
	l nat	which succeeds by (prec)
	l {x1} Πx 2 : nat.nat	(ΣprecλΠ)
	l {x1} nat	which succeeds by (prec)
	l {x1,x2} nat	which succeeds by (prec)
	l {g} (g z (foldr(m, l, y) g))	-we keep the @ operator implicit this time-(prec)
	l {g} g	(var)
	l {g} z	(subt)
	cons(m, z, l) :

© Jean-Pierre Jouannaud and Jianqi Li 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Editor: Thorsten Altenkirch; pp.[START_REF] Blanqui | A type-based termination criterion for dependently-typed higher-order rewrite systems[END_REF][START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF][START_REF] Blanqui | The calculus of algebraic constructions[END_REF][START_REF] Blanqui | HORPO with computability closure : A reconstruction[END_REF][START_REF] Blanqui | The computability path ordering: The end of a quest[END_REF][START_REF] Blanqui | The computability path ordering[END_REF][START_REF] Borralleras | A monotonic higher-order semantic path ordering[END_REF][START_REF] Dershowitz | Orderings for term-rewriting systems[END_REF][START_REF] Harper | A framework for defining logics[END_REF][START_REF] Jouannaud | Polymorphic higher-order recursive path orderings[END_REF][START_REF] Kusakari | Static dependency pair method based on strong computability for higher-order rewrite systems[END_REF] Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

© Jean-Pierre Jouannaud and Jianqi Li 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Editor: Thorsten Altenkirch; pp. 11-15 Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

Acknowledgements. Work supported by NSFC grants 61272002, 91218302, 973 Program 2010CB328003 and Nat. Key Tech. R&D Program SQ2012BAJY4052 of China. This work was done in part during a visit of the first author supported by Tsinghua University.