1 Introduction
Termination, that is, the absence of infinite computations, is an important problem in software verification, as well as in logic. In logic, it is often used to prove cut elimination and consistency. In automated theorem provers and proof assistants, it is often used (together with confluence) to check decidability of equational theories and typechecking algorithms.
This paper introduces a new termination criterion for a large class of programs whose operational semantics can be described by higherorder rewriting rules [33] typable in the calculus modulo rewriting ( for short). is a system of dependent types where types are identified modulo the reduction of calculus and a set of rewriting rules given by the user to define not only functions but also types. It extends Barendregt’s Pure Type System (PTS) [3], the logical framework LF [16] and MartinLöf’s type theory. It can encode any functional PTS like System F or the Calculus of Constructions [10].
Dependent types, introduced by de Bruijn in Automath , subsume generalized algebraic data types (GADT) used in some functional programming languages. They are at the core of many proof assistants and programming languages: Coq, Twelf, Agda, Lean, Idris, …
Our criterion has been implemented in Dedukti, a typechecker for that we will use in our examples. The code is available in [12] and could be easily adapted to a subset of other languages like Agda. As far as we know, this tool is the first one to automatically check termination in , which includes both higherorder rewriting and dependent types.
This criterion is based on dependency pairs, an important concept in the termination of firstorder term rewriting systems. It generalizes the notion of recursive call in firstorder functional programs to rewriting. Namely, the dependency pairs of a rewriting rule are the pairs such that is a subterm of and is a function symbol defined by some rewriting rules. Dependency pairs have been introduced by Arts and Giesl [2] and have evolved into a general framework for termination [13]. It is now at the heart of many stateoftheart automated termination provers for firstorder rewriting systems and Haskell, Java or C programs.
Dependency pairs have been extended to different simplytyped settings for higherorder rewriting: Combinatory Reduction Systems [23] and Higherorder Rewriting Systems [29], with two different approaches: dynamic dependency pairs include variable applications [24], while static dependency pairs exclude them by slightly restricting the class of systems that can be considered [25]. Here, we use the static approach.
In [38], Wahlstedt considered a system slightly less general than for which he provided conditions that imply the weak normalization, that is, the existence of a finite reduction to normal form. In his system, uses matching on constructors only, like in the languages OCaml or Haskell. In this case, is orthogonal: rules are leftlinear (no variable occurs twice in a lefthand side) and have no critical pairs (no two rule lefthand side instances overlap). Wahlstedt’s proof proceeds in two modular steps. First, he proves that typable terms have a normal form if there is no infinite sequence of function calls. Second, he proves that there is no infinite sequence of function calls if satisfies Lee, Jones and BenAmram’s sizechange termination criterion (SCT) [26].
In this paper, we extend Wahlstedt’s results in two directions. First, we prove a stronger normalization property: the absence of infinite reductions. Second, we assume that is locally confluent, a much weaker condition than orthogonality: rules can be nonleftlinear and have joinable critical pairs.
In [5], the first author developed a termination criterion for a calculus slightly more general than , based on the notion of computability closure, assuming that typelevel rules are orthogonal. The computability closure of a term is a set of terms that terminate whenever terminate. It is defined inductively thanks to deduction rules preserving this property, using a precedence and a fixed wellfounded ordering for dealing with function calls. Termination can then be enforced by requiring each rule righthand side to belong to the computability closure of its corresponding lefthand side.
We extend this work as well by replacing that fixed ordering by the dependency pair relation. In [5], there must be a decrease in every function call. Using dependency pairs allows one to have nonstrict decreases. Then, following Wahlstedt, SCT can be used to enforce the absence of infinite sequence of dependency pairs. But other criteria have been developed for this purpose that could be adapted to .
Outline
The main result is Theorem 4 stating that, for a large class of rewriting systems , the combination of and is strongly normalizing on terms typable in if, roughly speaking, there is no infinite sequence of dependency pairs.
The proof involves two steps. First, after recalling the terms and types of in Section 2, we introduce in Section 3 a model of this calculus based on Girard’s reducibility candidates [15], and prove that every typable term is strongly normalizing if every symbol of the signature is in the interpretation of its type (Adequacy lemma). Second, in Section 4, we introduce our notion of dependency pair and prove that every symbol of the signature is in the interpretation of its type if there is no infinite sequence of dependency pairs.
In order to show the usefulness of this result, we give simple criteria for checking the conditions of the theorem. In Section 5, we show that plain function passing systems belong to the class of systems that we consider. And in Section 6, we show how to use sizechange termination to obtain the termination of the dependency pair relation.
Finally, in Section 7 we compare our criterion with other criteria and tools and, in Section 8, we summarize our results and give some hints on possible extensions.
For lack of space, some proofs are given in an appendix at the end of the paper.
2 Terms and types
The set of terms of is the same as those of Barendregt’s [3]:
where is the set of sorts^{1}^{1}1Sorts refer here to the notion of sort in Pure Type Systems, not the one used in some firstorder settings., is an infinite set of variables and is a set of function symbols, so that , and are pairwise disjoint.
Furthermore, we assume given a set of rules such that and is of the form . A symbol is said to be defined if there is a rule of the form . In this paper, we are interested in the termination of
where is the reduction of calculus and is the smallest relation containing and closed by substitution and context: we consider rewriting with syntactic matching only. Following [6], it should however be possible to extend the present results to rewriting with matching modulo or some equational theory. Let be the set of terminating terms and, given a term , let be the set of immediate reducts of .
A typing environment is a (possibly empty) sequence of pairs of variables and terms, where the variables are distinct, written for short. Given an environment and a term , let be . The product arity of a term is the integer such that and is not a product. Let denote a possibly empty sequence of terms of length , and be the set of free variables of .
For each , we assume given a term and a sort , and let be the environment such that and .
The application of a substitution to a term is written . Given a substitution , let , and ( if is the identity) be the substitution . Given another substitution , let if there is such that and, for all , .
The typing rules of , in Figure 1, add to those of the rule (fun) similar to (var). Moreover, (conv) uses instead of , where is the joinability relation and the reflexive and transitive closure of . We say that has type in if is derivable. A substitution is welltyped from to , written , if, for all , holds.
The word “type” is used to denote a term occurring at the righthand side of a colon in a typing judgment (and we usually use capital letters for types). Hence, is the type of , is the type of , and is the type of . Common data types like natural numbers are usually declared in as function symbols of type : and .
The dependent product generalizes the arrow type of simplytyped calculus: it is the type of functions taking an argument of type and returning a term whose type may depend on . If does not depend on , we sometimes simply write .
Typing induces a hierarchy on terms [4, Lemma 47]. At the top, there is the sort that is not typable. Then, comes the class of kinds, whose type is : where . Then, comes the class of predicates, whose types are kinds. Finally, at the bottom lie (proof) objects whose types are predicates.
(ax)  

(var) 

(weak) 

(prod) 
(abs)  

(app) 

(conv) 

(fun) 
[Filter function on dependent lists] To illustrate the kind of systems we consider, we give an extensive example in the new Dedukti syntax combining typelevel rewriting rules (El converts datatype codes into Dedukti types), dependent types ( is the polymorphic type of lists parameterized with their length), higherorder variables (fil is a function filtering elements out of a list along a boolean function f), and matching on defined function symbols (fil can match a list defined by concatenation). Note that this example cannot be represented in Coq or Agda because of the rules using matching on app. And its termination can be handled neither by [38] nor by [5] because the system is not orthogonal and has no strict decrease in every recursive call. It can however be handled by our new termination criterion and its implementation [12]. For readability, we removed the & which are used to identify pattern variables in the rewriting rules.
Assumptions: Throughout the paper, we assume that is locally confluent () and preserves typing (for all , , and , if and , then ).
Note that local confluence implies that every has a unique normal form .
These assumptions are used in the interpretation of types (Definition 3) and the adequacy lemma (Lemma 3). Both properties are undecidable in general. For confluence, Dedukti can call confluence checkers that understand the HRS format of the confluence competition
. For preservation of typing by reduction, it implements an heuristic
[31].3 Interpretation of types as reducibility candidates
We aim to prove the termination of the union of two relations, and , on the set of welltyped terms (which depends on since includes ). As is well known, termination is not modular in general. As a step can generate an step, and vice versa, we cannot expect to prove the termination of from the termination of and . The termination of cannot be reduced to the termination of the simplytyped calculus either (as done for alone in [16]) because of typelevel rewriting rules like the ones defining El in Example 1. Indeed, typelevel rules enable the encoding of functional PTS like Girard’s System F, whose termination cannot be reduced to the termination of the simplytyped calculus [10].
So, following Girard [15], to prove the termination of , we build a model of our calculus by interpreting types into sets of terminating terms. To this end, we need to find an interpretation having the following properties:

Because types are identified modulo conversion, we need to be invariant by reduction: if is typable and , then we must have .

As usual, to handle reduction, we need a product type to be interpreted by the set of terms such that, for all in the interpretation of , is in the interpretation of , that is, we must have where .
First, we define the interpretation of predicates (and ) as the least fixpoint of a monotone function in a directedcomplete (= chaincomplete) partial order [28]. Second, we define the interpretation of kinds by induction on their size.
[Interpretation of types] Let be the set of partial functions from to the powerset of . It is directedcomplete wrt inclusion, allowing us to define as the least fixpoint of the monotone function such that, if , then:

The domain of is the set of all the terminating terms such that, if reduces to some product term (not necessarily in normal form), then and, for all , .

If and the normal form^{2}^{2}2Because we assume local confluence, every terminating term has a unique normal form . of is not a product, then .

If and , then .
We now introduce and define the interpretation of a term wrt to a substitution , (and simply if is the identity), as follows:

if ,

if and ,

if and ,

otherwise.
A substitution is adequate wrt an environment , , if, for all , . A typing map is adequate if, for all , whenever and .
Let be the set of terms of the form such that , , and, if and , then . (Informally, is the set of terms obtained by fully applying some function symbol to computable arguments.)
We can then prove that, for all terms , satisfies Girard’s conditions of reducibility candidates, called computability predicates here, adapted to rewriting by including in neutral terms every term of the form when is applied to enough arguments wrt [5]:
[Computability predicates] A term is neutral if it is of the form , or with, for every rule , .
Let be the set of all the sets of terms (computability predicates) such that (a) , (b) , and (c) if is neutral and .
Note that neutral terms satisfy the following key property: if is neutral then, for all , is neutral and every reduct of is either of the form with a reduct of , or of the form with a reduct of .
One can easily check that is a computability predicate.
Note also that a computability predicate is never empty: it contains every neutral term in normal form. In particular, it contains every variable.
We then get the following results (the proofs are given in Appendix A):

For all terms and substitutions , .

If is typable, and , then .

If is typable, and , then .

If is typable and ,
then . 
If , and , then .

Given and, for all , such that if . Then, if and, for all , .
We can finally prove that our model is adequate, that is, every term of type belongs to , if the typing map itself is adequate. This reduces the termination of welltyped terms to the computability of function symbols.
[Adequacy] If is adequate, and , then .
Proof.
First note that, if , then either or [4, Lemma 28]. Moreover, if , and (the premises of the (conv) rule), then [4, Lemma 42] (because preserves typing). Hence, the relation is unchanged if one adds the premise in (conv), giving the rule (conv’). Similarly, we add the premise in (app), giving the rule (app’). We now prove the lemma by induction on using (app’) and (conv’):
 (ax)

It is immediate that .
 (var)

By assumption on .
 (weak)

If , then . So, the result follows by induction hypothesis.
 (prod)

Is in ? Wlog we can assume . So, . By induction hypothesis, . Let now and . Note that . So, and, by induction hypothesis, . Since , we have . Therefore, .
 (abs)
 (app’)
 (conv’)
 (fun)

By induction hypothesis, . Therefore, since is adequate.∎
4 Dependency pairs theorem
Now, we prove that the adequacy of can be reduced to the absence of infinite sequences of dependency pairs, as shown by Arts and Giesl for firstorder rewriting [2].
[Dependency pairs] Let > iff there is a rule , is defined and is a subterm of such that are all the arguments to which is applied. The relation is the set of dependency pairs.
Let be the relation on the set (Def. 3), where iff (reduction in one argument), and is the closure by substitution and leftapplication of : iff there are a dependency pair with and and a substitution such that, for all , and, for all , .
In our setting, we have to close by leftapplication because function symbols are curried. When a function symbol is not fully applied wrt , the missing arguments must be considered as potentially being anything. Indeed, the following rewriting system:
whose dependency pairs are f x y > app (f x) y and f x y > f x, does not terminate, but there is no way to construct an infinite sequence of dependency pairs without adding an argument to the righthand side of the second dependency pair.
The rules of Example 1 have the following dependency pairs (the pairs whose lefthand side is headed by fil or fil_aux can be found in Appendix B):
In [2], a sequence of dependency pairs interleaved with steps is called a chain. Arts and Giesl proved that, in a firstorder term algebra, terminates if and only if there are no infinite chains, that is, if and only if terminates. Moreover, in a firstorder term algebra, terminates if and only if, for all and , terminates wrt whenever terminates wrt . In our framework, this last condition is similar to saying that is adequate.
We now introduce the class of systems to which we will extend Arts and Giesl’s theorem.
[Wellstructured system] Let be the smallest quasiorder on such that if occurs in or if there is a rule with (defined or undefined) occurring in . Then, let be the strict part of . A rewriting system is wellstructured if:

is wellfounded;

for every rule , ;

for every dependency pair , ;

every rule is equipped with an environment such that, if and , then , where is the restriction of defined in Fig. 2.
(ax)  
(var) 
(weak)  
(prod) 
(abs)  

(app’) 

(conv’) 
(dp) 
()  
(const) 
( undefined) 
and
Comments
There are no comments yet.