Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui Guillaume Genestier Olivier Hermant




 

 




arrows,shapes,decorations.pathmorphing,backgrounds,positioning,fit,calc

 






ded
   

   





























































































































































































































































































































































































































rul
  [ rulc
rew[1][    ]
  [ rewc[1][    ]
  
[#1]typ[1][ : ][#1]typc[1][ : ][#1]Dedukti
  alsoletter==->:#,
  keywords=symbol,rule,infix,TYPE,set,
  delim=[s][]
    ,
      comment=[n](;;),
      string=[b]",
      commentstyle=,
      showstringspaces=false
    basicstyle=,keywordstyle=backgroundcolor=,language=Dedukti^1 INRIA ^2 LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay ^3 MINES ParisTech, PSL UniversityF. Blanqui, G. Genestier and O. HermantFrédéric Blanqui, Guillaume Genestier and Olivier HermantTheory of computation Equational logic and rewritingTheory of computation Type theoryDependency Pairs Termination in Dependent Type Theory Modulo Rewriting
        Frédéric Blanqui^1,2 Guillaume Genestier^2,3 Olivier Hermant^3
        December 30, 2023
    ======================================================================
    
    
      Dependency pairs are a key concept at the core of modern automated
      termination provers for first-order term rewriting systems. In this
      paper, we introduce an extension of this technique for a large class
      of dependently-typed higher-order rewriting systems. This
      extends previous results by Wahlstedt on the one hand and the first
      author on the other hand to strong normalization and non-orthogonal
      rewriting systems. This new criterion is implemented in the
      type-checker Dedukti.
    
    
    § 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 type-checking algorithms.
    
    This paper introduces a new termination criterion for a large class of
    programs whose operational semantics can be described by higher-order
    rewriting rules <cit.> 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 setof rewriting rules given by the user to
    define not only functions but also types. It extends
    Barendregt's Pure Type System (PTS)ł P<cit.>,
    the logical framework LF <cit.> and Martin-Löf's type
    theory<cit.>. It can encode any
    functional PTS like System F or the Calculus of Constructions
    <cit.>.assaf15phdThis makes łΠ/ a good
      candidate for a logical framework and a platform for proof
      translation and interoperability <cit.>.
    
    Dependent types, introduced by de Bruijn in Automath<cit.>, subsume
    generalized algebraic data types (GADT)<cit.> 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 https://deducteam.github.io/Dedukti<cit.>, a
    type-checker forłΠ/that we will use in our examples. The
    code is available in <cit.> 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 higher-order rewriting and dependent
    types.
    
    This criterion is based on dependency pairs,
    an important concept in the termination of first-order term rewriting
    systems. It generalizes the
    notion of recursive call in first-order functional
    programs to rewriting. Namely, the dependency pairs of a rewriting rulef(l_1,…,l_p) rare the pairs(f(l_1,…,l_p),g(m_1,…,m_q))such thatg(m_1,…,m_q)is a subterm ofrandgis a function symbol defined by some
    rewriting rules. Dependency pairs have been introduced by Arts and Giesl
    <cit.> and have evolved into a general framework for
    termination <cit.>. It is now at the heart of many
    state-of-the-art automated termination provers for first-order rewriting systems and Haskell, Java or C programs.
    
    Indeed, Arts and Giesl
    proved that a rewriting relation terminates if and only if there is no
    infinite sequence of dependency pairs interleaved with reductions in
    the arguments. In a first-order functional setting, it amounts to saying
    that there is no infinite sequence of function calls.
    
    Dependency pairs have been extended to different simply-typed settings for
    higher-order rewriting: Combinatory Reduction Systems
    <cit.>kop12phd and Higher-order Rewriting Systems
    <cit.>, with two different approaches: dynamic
    dependency pairs include variable applications <cit.>, while static
    dependency pairs exclude them by slightly restricting the class of
    systems that can be considered <cit.>suzuki11pro. Here, we use the static approach.
    
    In <cit.>, 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 left-linear (no variable occurs twice in a left-hand side) and
    have no critical pairs (no two rule left-hand 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 ifsatisfies Lee, Jones and Ben-Amram's
    size-change termination criterion (SCT) <cit.>.
    
    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 thatis locally confluent,
    a much weaker condition than orthogonality: rules can
    be non-left-linear and have joinable critical pairs.
    
    In <cit.>, the first author developed a termination
    criterion for a calculus slightly more general thanłΠ/, based
    on the notion of computability closure, assuming that type-level
    rules are orthogonal. The computability closure of a termf(l_1,…,l_p)is a set of terms that terminate wheneverl_1,…,l_pterminate. It is defined inductively thanks to
    deduction rules preserving this property, using a precedence and a fixed well-founded ordering for dealing with function calls. Termination can then be
    enforced by requiring each rule right-hand side to belong to the
    computability closure of its corresponding left-hand side.
    
    Function
    calls are added in the computability closure by using a fixed
    well-founded quasi-ordering. In a way similar to the recursive path
    ordering <cit.>, a function call g(m_1,…,m_q)
    is added in the computability closure of f(l_1,…,l_p) if
    m_1,…,m_q are in the computability closure and, either g is
    smaller than f in a well-founded precedence, or g is equivalent to
    f but m_1,…,m_q is smaller than l_1,…,l_p in the
    multiset or lexicographic extension of some fixed well-founded ordering.
    
    
    We extend this work as well by replacing that fixed ordering by the
    dependency pair relation. In <cit.>, there must be a
    decrease in every function call.
    Using dependency pairs
    allows one to have non-strict 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łΠ/.
    
    
    However, because in our setting typing depends on rewriting,
    some dependency pairs may arise from
    typing. For instance, if f takes an argument of type Ft, then we will have dependency pairs between f and F, even though the rules
    of f do not use F itself. Our extended notion of dependency pair
    boils down to the usual one when one restricts himself to simply-typed
    rewriting rules though.
    
    
      §.§.§ Outline
    
    The main result is Theorem <ref> 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 <ref>,
    we introduce in Section
    <ref> a model of this calculus based on
    Girard's reducibility candidates <cit.>, 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 <ref>, 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 <ref>, we show that plain function passing systems belong to the class of systems that we consider.
    And in Section <ref>, we show how to use
    size-change termination to obtain the termination of the dependency
    pair relation.
    
    Finally, in Section <ref> we compare our criterion with other criteria
    and tools and, in Section <ref>, 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.
    
    
    The paper is self-contained except for a few meta-theoretical
    properties of łΠ/ taken from <cit.>.
    The proofs of some lemmas are given in an appendix at the end of the paper.
    Section
    <ref> is the most technical part of the paper and can be
    skipped at first. It introduces a new interpretation of types
    (Definition <ref>), much simpler than the one of Wahlstedt
    <cit.>. In particular, it does not
    use transfinite ordinal theory but a powerful fixpoint theorem instead.
    
    
    § TERMS AND TYPES
    
    
    The set  of terms of łΠ/ is the same as those of Barendregt's ł P<cit.>:
    
    t∈ = s∈| x∈| f∈|∏ xtt| tt| xtt
    
    where ={,} is the set of sorts[Sorts refer here to the notion of sort in Pure Type Systems, not the one used in some first-order 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 l r such that
    (r)(l) and
    l is of the form f.
    A symbol f is said to be defined if there is a
    rule of the form f r. In this paper, we are interested in the
    termination of
    
    =∪
    
    where  is the $̱-reduction ofł-calculus andis the smallest
    relation containingand closed by substitution and context:
    we
    consider rewriting with syntactic matching only. Following
    <cit.>, it should however be possible to extend the
    present results to rewriting with matching moduloη̱or some
    equational theory.
    Letbe the set of terminating terms and, given a termt, lett={u∈T| t u}be the set of
    immediate reducts oft.
    
    A typing environmentis a (possibly empty) sequencex_1:T_1,…,x_n:T_nof pairs of variables and terms, where the variables are distinct,
    written:for short. Given an environment=:and a termU, let,Ube∏ U.
    The product arity(T)of a termTis the
    integern∈such thatT=∏x_1T_1…∏x_nT_nUandUis
    not a product. Letdenote a possibly empty sequence of termst_1,…,t_nof length||=n, and(t)be the set of free variables oft.
    
    For eachf∈, we assume given a term_fand a
    sorts_f, and let_fbe the environment such that_f=_f,Uand|_f|=(_f).
    
    The application of a substitutionto a termtis writtent.
    Given a substitution,
    let()={x|x≠ x},()=⋃_x∈()(x)and[x→ a,]([x→ a]ifis the identity) be the substitution{(x,a)}∪{(y,b)∈|
    y≠ x}.
    Given another substitution',
    let'if there isxsuch thatx x'and, for ally≠
    x,y=y'.
    
    The typing rules ofłΠ/, in Figure
    <ref>, add to those ofł Pthe rule
    (fun) similar to (var). Moreover, (conv) usesinstead of_$̱, where =^*^* is the joinability
    relation and ^* the reflexive and transitive closure of . We
    say that t has type T in  if þ t:T is derivable. A
    substitution  is well-typed from  to , written
    þ:, if, for all (x:T)∈, þ x:T holds.
    
    The word “type” is used to denote a term occurring at the right-hand side of a colon in a typing judgment (and we usually use capital letters for types). 
    Hence,  is the type of , _f is the type of f,
    and s_f is the type of _f.
    Common data types like natural numbers  are usually declared in łΠ as function symbols of type : _= and s_=.
    
    The dependent product ∏ xAB generalizes the arrow type A B of simply-typed ł-calculus: it is the type of
    functions taking an argument x of type A and returning a term
    whose type B may depend on x.
    If B does not depend on x, we sometimes simply write A B.
    
    Typing induces a hierarchy on terms <cit.>. At the top, there is the sort
     that is not typable. Then, comes the class  of kinds, whose
    type is : K=|∏ xtK where t∈. Then, comes the class of predicates,
    whose types are kinds. Finally, at the bottom lie
    (proof) objects whose types are predicates.
    
    
    [Filter function on dependent lists]
    To illustrate the kind of systems we consider, we give an extensive
    example in the new Dedukti syntax combining type-level
    rewriting rules ( El converts datatype codes into Dedukti
    types), dependent types ( is the polymorphic type of lists
    parameterized with their length), higher-order 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
    <cit.> nor by <cit.> 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 <cit.>.
    For readability, we removed the & which are used to identify pattern variables in the rewriting rules.
     
     [mathescape=true]
    symbol Set: TYPE     symbol arrow: Set  Set  Set
    
    symbol El: Set  TYPE          rule El (arrow a b)  El a  El b
    
    symbol Bool: TYPE      symbol true: Bool     symbol false: Bool
    symbol Nat: TYPE       symbol zero: Nat      symbol s: Nat  Nat
    
    symbol plus: Nat  Nat Nat        set infix 1 "+"  plus
      rule zero + q  q               rule (s p) + q  s (p + q)
    
    symbol List: Set  Nat  TYPE
      symbol nil: a, List a zero
      symbol cons:a, El a p, List a p  List a (s p)
    
    symbol app: a p, List a p q, List a q  List a (p+q)
      rule app a _ (nil _)        q m  m
      rule app a _ (cons _ x p l) q m  cons a x (p+q) (app a p l q m)
    
    symbol len_fil: a, (El a  Bool) p, List a p  Nat
    symbol len_fil_aux: Bool a, (El a  Bool) p, List a p  Nat
      rule len_fil a f _ (nil _)          zero
      rule len_fil a f _ (cons _ x p l)   len_fil_aux (f x) a f p l
      rule len_fil a f _ (app _ p l q m)
            (len_fil a f p l) + (len_fil a f q m)
      rule len_fil_aux true  a f p l  s (len_fil a f p l)
      rule len_fil_aux false a f p l  len_fil a f p l
    
    symbol fil: a f p l, List a (len_fil a f p l)
    symbol fil_aux: b a f, El a p l, List a (len_fil_aux b a f p l)
      rule fil a f _ (nil _)          nil a
      rule fil a f _ (cons _ x p l)   fil_aux (f x) a f x p l
      rule fil a f _ (app _ p l q m)
            app a (len_fil a f p l) (fil a f p l)
                    (len_fil a f q m) (fil a f q m)
      rule fil_aux false a f x p l  fil a f p l
      rule fil_aux true  a f x p l
            cons a x (len_fil a f p l) (fil a f p l)
    Note that the rules of  + are required for the rules of 
        app to preserves typing. Assumptions: Throughout the paper, we assume that  is
    locally confluent () and preserves typing (for all
    , A, t and u, if þ t:A and t u, then þ u:A).
    
    Note that local confluence implies that every t∈ has a unique
    normal form t<cit.>.
    
    These assumptions are used in the interpretation of types (Definition
    <ref>) and the adequacy lemma (Lemma <ref>). Both
    properties are undecidable in general. For confluence, Dedukti
    can call confluence checkers that understand the HRS format of the http://project-coco.uibk.ac.at/confluence competition. For
    preservation of typing by reduction, it implements an heuristic
    <cit.>.
    
    See <cit.> for
      sufficient conditions.
    Note that, when rules contain no abstraction and no variable
    applications, then =∪ is locally confluent on
     iff  is locally confluent on first-order terms <cit.>.
    þ T: iff T∈ and T is typable.
    
      We first prove that, if þ t:T and T=, then T∈, by
      induction on þ t:T. We only detail important cases:
      
      (var) Then, A=. This case is not possible since þ
        A:s and  is not typable.
      
      (app) If B[x→ a]=, then either B= or else B=x and
        a=. Both cases are impossible since both B and a are
        typable while  is not typable.
      
      (conv) This case is not possible since þ B:s and 
        is not typable.
      
      (fun) Then, _f=. This case is not possible since
        þ_f:s_f and  is not typable.
      
      Hence, T can only be typed by using (ax), (weak) and (prod).
    
    
    § INTERPRETATION OF TYPES AS REDUCIBILITY CANDIDATES
    
    
    We aim to prove the termination of the union of two relations, 
    and ,sharing some symbols, namely the abstraction and the
    application of ł-calculus, on the set of well-typed terms (which
    depends on  since  includes _R). As is well known, termination is not modular in general.even when the two relations share no symbols<cit.> As a $̱ step can generate anstep, and
    vice versa, we cannot expect to prove the termination of∪from the termination ofand., unless  is restricted to some class (e.g. object-level
    first-order rewriting systems <cit.>).
    The termination ofłΠ/cannot be reduced to the termination of the
    simply-typedł-calculus either (as done forłΠalone in
    <cit.>) because of type-level rewriting rules like the ones defining 
      El in Example <ref>. Indeed, type-level rules enable
    the encoding of functional PTS like Girard's System F, whose
    termination cannot be reduced to the termination of the simply-typedł-calculus
    <cit.>.
    
    So, following Girard <cit.>, 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 T is typable and T T', then
      we must have T=T'.
    
      *  As usual, to handle $̱-reduction, we need a product type∏ xABto be interpreted by the set of termstsuch
      that, for allain the interpretation ofA,tais in the
      interpretation ofB[x→ a], that is, we must have∏ xAB=aAB[x→ a]whereaPQ(a)={t| a∈ P,ta∈
      Q(a)}.
    
    
    First, we define the interpretation
    of predicates (and) as the least fixpoint of
    a monotone function in a directed-complete (= chain-complete) partial
    order <cit.>. Second, we define the interpretation of
    kinds by induction on their size.
    
    
    
      Let =_p(,()) be the set of partial functions from
       to the powerset of .
      It is directed-complete wrt
      inclusion, allowing us to define  as the least fixpoint of the monotone
      function F: such that, if I∈, then:
      
      *  The domain of F(I) is the set D(I) of all the terminating
      terms T such that, if T reduces to some product term ∏ xAB
      (not necessarily in normal form), then A∈(I) and, for all
      a∈ I(A), B[x→ a]∈(I).
    
      *  If T∈ D(I) and the normal form[Because we assume
      local confluence, every terminating term T has a unique normal
      form T.] of T is not a product, then F(I)(T)=.
    
      *  If T∈ D(I) and T=∏ xAB, then
      F(I)(T)=aI(A)I(B[x→ a]).
    
      We now introduce =D() and
      define the interpretation of a term T wrt to a
    substitution , T_ (and simply T if  is
    the identity), as follows:
    
      * s_= if s∈,
    
      * ∏ xAK_=aA_K_[x→ a,] if
      K∈ and x∉(),
    
      * T_=(T) if T∉∪{} and T∈,
    
      * T_= otherwise.
    
    A substitution  is adequate wrt an environment ,
    , if, for all x:A∈, x∈A_.
    A typing map  is adequate if, for all f, f∈_f whenever
    þ_f:s_f and _f∈s_f.
    
    Let  be the set of terms of the form f such that
    ||=(_f), þ_f:s_f, _f∈s_f and, if
    _f=: and =[→], then _f.
    (Informally, C is the set of terms obtained by fully applying
    some function symbol to computable arguments.)
    
    
    We can then prove that, for all termsT,Tsatisfies Girard's
    conditions of reducibility candidates, called
    computability predicates here, adapted to rewriting by including in
    neutral terms every term of the formfwhenfis applied to enough
    arguments wrt<cit.>:
    
    
    
    A term is neutral if it is of the form ( xAt)u, x or
    f with, for every rule f r∈, ||≤||.
    
    Let  be the set of all the sets of terms S (computability
    predicates) such that (a) S, (b) S S, and (c)
    t∈ S if t is neutral and t S.
    
    
    Note that neutral terms satisfy the following key property: iftis
    neutral then, for allu,tuis neutral and every reduct oftuis
    either of the formt'uwitht'a reduct oft, or of the formtu'withu'a reduct ofu. tu=tu∪tu
    
    One can easily check thatis 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 <ref>):
    
    
    
      * 
      For all terms T and substitutions , T_∈.
      
      * 
      If T is typable, T∈ and T T', then
      T_=T'_.
      
      * 
      If T is typable, T∈ and ', then
      T_=T_'.
      
      * 
      If ∏ xAB is typable and ∏ xAB∈ and
      x∉()∪(),
    
      then ∏ xAB_=aA_B_[x→ a,].
      
      * 
      If þ U:s, þ: and U∈, then
      U_=U_.
      
      *  Given P∈ and, for all a∈ P,
        Q(a)∈ such that Q(a') Q(a) if a a'. Then, xAb∈aPQ(a) if A∈ and, for all a∈ P,
        b[x→ a]∈ Q(a).
      
    
    We can finally prove that our model is adequate, that is, every term of typeTbelongs toT, if the typing mapitself is adequate. This
    reduces the termination of well-typed terms to the computability of
    function symbols.
    
    
    
      If  is adequate, þ t:T and , then
      t∈T_.
    
      First note that, if þ t:T, then either T= or þ T:s<cit.>. Moreover, if þ a:A, A B
      and þ B:s (the premises of the (conv) rule), then þ A:s<cit.> (because  preserves
      typing). Hence, the relation þ is unchanged if one adds the
      premise þ A:s in (conv), giving the rule (conv'). Similarly,
      we add the premise þ∏ xAB:s in (app), giving the rule
      (app'). We now prove the lemma by induction on þ t:T using
      (app') and (conv'):
      
      (ax)  It is immediate that ∈_=.
    
      
      (var) By assumption on .
    
      
      (weak) If ,x:A, then . So, the
        result follows by induction hypothesis.
    
      
      (prod) Is (∏ xAB) in s_=? Wlog we can assume
        x∉()∪(). So, (∏ xAB)=∏ xAB. By
        induction hypothesis, A∈_=. Let now a∈(A) and '=[x→ a,]. Note that (A)=A_. So,
        ',x:A and, by induction hypothesis,
        B'∈s_=. Since x∉()∪(),
        we have B'=(B)[x→ a]. Therefore, (∏ xAB)∈s_.
    
      
      (abs) Is ( xAb) in ∏ xAB_? Wlog we can assume that
        x∉()∪(). So, ( xAb)= xAb. By
        Lemma <ref><ref>, ∏ xAB_=
        aA_B_[x→ a,]. By Lemma
        <ref><ref>, B_[x→ a,] is an
        A_-indexed family of computability predicates such that
        B_[x→ a',]=B_[x→ a,] whenever a
        a'. Hence, by Lemma <ref><ref>, xAb∈∏ xAB_ if A∈ and, for all
        a∈A_, (b)[x→ a]∈B_' where '=[x→
          a,]. By induction hypothesis,
        (∏ xAB)∈s_=. Since
        x∉()∪(), (∏ xAB)=∏ xAB and
        (b)[x→ a]=b'. Since , we have
        A∈. Moreover, since ',x:A, we have
        b'∈B_' by induction hypothesis.
    
      
      (app') Is (ta)=(t)(a) in B[x→ a]_? By induction
        hypothesis, t∈∏ xAB_, a∈A_ and
        (∏ xAB)∈s=. By Lemma <ref><ref>,
        ∏ xAB_=A_B_[x→,]. Hence,
        (t)(a)∈B_' where '=[x→ a,]. Wlog we can
        assume x∉()∪(). So, '=[x→ a]. Hence,
        by Lemma <ref><ref>, B_'=B[x→ a]_.
    
      
      (conv') By induction hypothesis, a∈A_,
        A∈s_= and B∈s_=. By Lemma
        <ref><ref>, A_=B_. So, a∈B_.
    
      
      (fun) By induction hypothesis,
        _f∈s_f_=. Therefore, f∈_f_=_f
        since  is adequate.As usual, by taking the identity for  (variables are computable),
    we get that  terminates on terms typable in łΠ/ if  is
    adequate and  is locally confluent and preserves typing.
    
    § DEPENDENCY PAIRS THEOREM
    
    
    Now, we prove that the adequacy ofcan be reduced to the absence of infinite sequences of dependency pairs, as
    shown by Arts and Giesl for first-order rewriting <cit.>.
    
    
    Let f > g iff there is a rule f r ∈, g is defined
    and g is a subterm of r such that  are all the arguments to which g is applied.
    The relation > is the set of dependency pairs.
    
    Let =_^*>_s be the relation on the set  (Def. <ref>), where f_ f iff _prod
    (reduction in one argument), and >_s is the closure by substitution
    and left-application of >:
    f t_1… t_p  g u_1… u_q iff there are a dependency pair f l_1… l_i>g m_1… m_j with ip and jq
    and a substitution  such that,
    for all ki, t_k^*l_k and, for all kj, m_k=u_k.
    
    
    In our setting, we have to close>_sby left-application because
    function symbols are curried. When a function symbolfis not
    fully applied wrt(_f), the missing arguments must be
    considered as potentially being anything. Indeed, the following rewriting system:
    [mathescape=true]
           app x y  x y             f x y  app (f x) y
    
    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 right-hand side of the second dependency pair.
    
    
    
     The rules of Example <ref> have the following dependency pairs (the pairs whose left-hand side is headed by  fil or  fil_aux can be found in Appendix <ref>):
    [escapeinside=**]
    * A:*               El (arrow a b) > El a
    * B:*               El (arrow a b) > El b
    * C:*                    (s p) + q > p + q
    * D:*   app a _ (cons _ x p l) q m > p + q
    * E:*   app a _ (cons _ x p l) q m > app a p l q m
    * F:*len_fil a f _ (cons _ x p l)  > len_fil_aux (f x) a f p l
    * G:*len_fil a f _ (app _ p l q m) >
                                    (len_fil a f p l) + (len_fil a f q m)
    * H:*len_fil a f _ (app _ p l q m) > len_fil a f p l
    * I:*len_fil a f _ (app _ p l q m) > len_fil a f q m
    * J:*    len_fil_aux true  a f p l > len_fil a f p l
    * K:*    len_fil_aux false a f p l > len_fil a f p l
    
    
    In <cit.>, a sequence of dependency pairs interleaved with_steps is called a chain. Arts and Giesl proved that, in a
    first-order term algebra,terminates if and only if there are no
    infinite chains, that is, if and only ifterminates.
    Moreover, in a first-order term algebra,terminates if and only if, for allfand,fterminates
    wrtwheneverterminates wrt. In our framework,
    this last condition is similar to saying thatis adequate.
    
    We now introduce the class of systems to which we will extend
    Arts and Giesl's theorem.
    
    
    
      Let ≽ be the smallest quasi-order on  such that
      f≽ g if g occurs in _f or if there is a rule f
      r∈ with g (defined or undefined) occurring in r.
      Then, let ≻=≽≼ be the strict part of ≽.
      A rewriting system  is well-structured if:
      
      * ≻ is well-founded;
      
      *  for every rule f r, ||≤(_f);
      
      *  for every dependency pair f>g, ||≤(_g);
      
      *  every rule f r is equipped with an environment _f
        r such that, if _f=∏ U and π=[→], then
        _f r r:Uπ, where  is the restriction of
        þ defined in Fig. <ref>.
      
    
    Condition (a) is always satisfied whenis finite.
    Condition (b) ensures that a term of the formfis neutral
    whenever||=(_f). Condition (c) ensures that>is included
    in.
    
    The relation corresponds to the notion of computability
    closure in <cit.>, with the ordering on function calls
    replaced by the dependency pair relation. It is similar toþexcept that it uses the variant of (conv) and (app) used in the proof
    of the adequacy lemma; (fun) is split in the rules (const) for
    undefined symbols and (dp) for dependency pairs whose left-hand side
    isf; every type occurring in an object term or every type of a
    function symbol occurring in a term is required to be typable by using
    symbols smaller thanfonly.
    
    The environment_f rcan be inferred by Dedukti when
    one restricts rule left hand-sides to some well-behaved class of terms
    like algebraic terms or Miller patterns<cit.> (inłProlog).
    
    One can check that Example <ref> is
    well-structured (the proof is given in Appendix <ref>).
    
    Finally, we need matching to be compatible with computability, that
    is, iff r∈andare computable, thenis
    computable, a condition called accessibility in <cit.>:
    
    
    
      A well-structured system  is accessible if, for all
      substitutions  and rules f r with _f=∏ U and
      ||=||, we have _f r whenever
      þ_f:s_f, _f∈s_f and
      [↦]:.
    
    
    This property is not always satisfied because the subterm relation
    does not preserve computability in general. Indeed, ifCis an undefined type
    constant, thenC=. However,C C≠since=
    xCxx∈and∉. Hence, ifcis an undefined function symbol
    of type_c=(C C) C, thenc ∈Cbut∉C C.
    
    We can now state the main lemma:
    
    
     is adequate if  terminates and  is well-structured
      and accessible.
    
      Since  is well-structured, ≻ is well-founded by condition
      (a). We prove that, for all f∈, f∈_f, by induction
      on ≻. So, let f∈ with _f=_f,U and
      _f=x_1:T_1,…,x_n:T_n. By induction hypothesis, we have
      that, for all g≺ f, g∈_g.
    
      Since _ and  terminate on  and
      _, we have that _∪
      terminates. We now prove that, for all f∈, we have
      f∈U_ where =[→], by a second induction on
      _∪. By condition (b),
      f is neutral. Hence, by definition of computability, it
      suffices to prove that, for all u∈f,
      u∈U_. There are 2 cases:
      
      * u=f with _prod. Then, we can conclude by
        the first induction hypothesis.
    
      
      *  There are fl_1… l_k r∈ and  such that
        u=(r) t_k+1… t_n and, for all i∈{1,…,k},
        t_i=l_i. Since f∈, we have π_f. Since
         is accessible, we get that _f r. By
        condition (d), we have _f r r:Vπ where
        V=∏x_k+1T_k+1…∏x_nT_nU.
    
        Now, we prove that, for all , t and T, if t:T
        (t:T resp.) and , then t∈T_,
        by a third induction on the structure of the derivation of t:T
        (t:T resp.), as in the proof of Lemma <ref>
        except for (fun) replaced by (fun_≺ f) in one case, and
        (const) and (dp) in the other case.
        
      (fun_≺ f) We have g∈_g by the first induction
           hypothesis on g.
         
      (const) Since g is undefined, it is neutral and normal.
           Therefore, it belongs to every computability predicate and in
           particular to _g_.
         
      (dp) By the third induction hypothesis, y_i∈U_i_. By
           Lemma <ref><ref>,
           U_i_=U_i_. So,  and
           g∈. Now, by condition (c),
           g<̃f since g<f. Therefore, by
           the second induction hypothesis, g∈V_.
       
       So, r∈Vπ_ and, by Lemma <ref><ref>,
       u∈U_[x_n→ t_n,..,x_k+1→ t_k+1,π]=U_.
    
    Note that the proof still works if one replaces the relation≽of Definition <ref> by any well-founded quasi-order such thatf≽ gwheneverf>g.
    The quasi-order of Definition <ref>, defined syntactically, relieves the user of the burden of providing one and is sufficient in every practical case met by the authors.
    However it is possible to construct ad-hoc systems which require a quasi-order richer than the one presented here.
    
    By combining the previous lemma and the Adequacy lemma (the identity
    substitution is computable), we get the main result of the
    paper:
    
    
    
      The relation =∪ terminates on terms typable in
      łΠ/ if  is locally confluent and preserves typing, 
      is well-structured and accessible, and  terminates.
    
    
    For the sake of completeness, we are now going to give sufficient
    conditions for accessibility and termination ofto hold, but
    one could imagine many other criteria.
    
    
    
    
    
    
    
    
    
    
    § CHECKING ACCESSIBILITY
    
    
    In this section, we give a simple condition to ensure accessibility
    and some hints on how to modify the interpretation when this condition is
    not satisfied.
    
    As seen with the definition of accessibility, the main problem is to
    deal with subterms of higher-order type. A simple condition is
    to require higher-order variables to be direct subterms of
    the left-hand side, a condition called plain function-passing (PFP) in
    <cit.>, and satisfied by Example <ref>.
    
    
    A well-structured  is PFP if, for all f r∈ with
    _f=∏ U and ||=||, ∉∪{} and, for
    all y:T∈_f r, there is i such that y=l_i and
    T=T_i[→], or else y∈(l_i) and T=D with D
    undefined and ||=(D).
    
    PFP systems are accessible.
    
      Let f r be a PFP rule with _f=,U, =:,
      π=[→]. Following Definition <ref>, assume
      that þ_f:s_f, _f∈ and π. We have
      to prove that, for all (y:T)∈_f r, y∈T_.
      
      *  Suppose y=l_i and T=T_iπ. Then,
        y=l_i∈T_i_π. Since þ_f:s_f,
        T_i∉∪{}. Since _f∈ and
        π, we have T_iπ∈. So,
        T_i_π=(T_iπ). Since T_i∉∪{} and
        ∉∪{}, T_iπ∉∪{}. Since
        T_iπ∈, T_iπ_=(T_iπ). Thus,
        y∈T_.
      
      *  Suppose y∈(l_i) and T is of the form C with
        ||=(C). Then, T_= and y∈ since
        l_i∈T_i_.
    
    But many accessible systems are not PFP. They can be
    proved accessible by changing the interpretation of type constants (a
    complete development is left for future work).
    
    
    [Recursor on Brouwer ordinals][mathescape=true]
    symbol Ord: TYPE
     symbol zero: Ord  symbol suc: OrdOrd     symbol lim: (NatOrd)Ord
    
    symbol ordrec: A(OrdAA)((NatOrd)(NatA)A)OrdA
      rule ordrec u v w zero     u
      rule ordrec u v w (suc x)  v x (ordrec u v w x)
      rule ordrec u v w (lim f)  w f (λn,ordrec u v w (f n))
    
    
      The above example is not PFP because  f:NatOrd is not
      argument of  ordrec.
    Yet, it is accessible if one takes for Ordthe least fixpoint
    of the monotone functionF(S)={t∈|if t^* lim f then 
    f∈ Nat S, and if  t^* suc u then  u∈ S}<cit.>.
    
    Similarly, the following encoding of the simply-typedł-calculus is
    not PFP but can be proved accessible by taking
    
        T 
          c=if c= arrow a b then {t∈|if t^*
          lam f then f∈ T a T b} else
    [Simply-typed ł-calculus][mathescape=true]
    symbol Sort : TYPE              symbol arrow : Sort  Sort  Sort
    
    symbol T : Sort  TYPE
      symbol lam : ∀ a b, (T a  T b)  T (arrow a b)
      symbol app : ∀ a b, T (arrow a b)  T a  T b
      rule app a b (lam _ _ f) x  f x
    
    Note here, that erasing dependencies in types, would lead to an encoding of
    pureλ-calculus, which is well-known to be non-normalizing.
    
    
    § SIZE-CHANGE TERMINATION
    
    
    In this section, we give a sufficient condition forto terminate.
    For first-order rewriting,
    many techniques have been developed for that purpose. To cite just a
    few, see for instance <cit.>.thiemann07phd
    Many of them can probably be extended tołΠ/,
    either because the structure of terms in which they are expressed can be
    abstracted away, or because they can be extended to deal also with
    variable applications,ł-abstractions and$̱-reductions.
    <cit.>
    
    As an example, following Wahlstedt <cit.>, we are going
    to use Lee, Jones and Ben-Amram's size-change termination criterion
    (SCT) <cit.>. It consists in following arguments along
    function calls and checking that, in every potential loop, one of them
    decreases. First introduced for first-order functional languages, it
    has then been extended to many other settings: untyped ł-calculus
    <cit.>, a subset of OCaml<cit.>,
    Martin-Löf's type theory <cit.>, System F
    <cit.>.
    
    We first recall Hyvernat and Raffalli's matrix-based presentation of
    SCT <cit.>:
    
    
      Let  be the smallest transitive relation such that ft_1…
      t_n t_i when f∈. The call graph () associated to
       is the directed labeled graph on the defined symbols of 
      such that there is an edge between f and g iff there is a
      dependency pair fl_1… l_p>gm_1… m_q. This edge is labeled
      with the matrix (a_i,j)_i≤f,j≤g where:
      
      *  if l_i m_j, then a_i,j=-1;
        
      *  if l_i=m_j, then a_i,j=0;
        
      *  otherwise a_i,j=∞ (in particular if i>p or j>q).
       is size-change terminating (SCT) if, in the transitive closure
      of () (using the min-plus semi-ring to multiply the matrices
      labeling the edges), all idempotent matrices labeling a loop have
      some -1 on the diagonal.
    
    
    We add lines and columns of ∞'s in matrices associated to
    dependency pairs containing partially applied symbols (cases i>p or
    j>q) because missing arguments cannot be
    compared with any other argument since they are arbitrary.
    
    The matrix associated to the dependency pair  C: (s p) + q > p +
      q and the call graph associated to the dependency pairs of Example
    <ref> are depicted in Figure <ref>.  The full
    list of matrices and the extensive call graph of Example
    <ref> can be found in Appendix <ref>.
    
    
     terminates if  is finite and  is SCT.
    
     Suppose that there is an infinite sequence χ=f_1_1
     f_2_2… Then, there is an infinite path in the call
     graph going through nodes labeled by f_1,f_2,… Since  is
     finite, there is a symbol g occurring infinitely often in this
     path. So, there is an infinite sequence g_1,g_2,…
     extracted from χ. Hence, for every i,j∈^*, there is a
     matrix in the transitive closure of the graph which labels the loops
     of g corresponding to the relation between _i and
     _i+j. By Ramsey's theorem<cit.>, there is an
     infinite sequence (ϕ_i) and a matrix M such that M corresponds
     to all the transitions g_ϕ_i,g_ϕ_j with
     i≠ j. M is idempotent, indeed
     g_ϕ_i,g_ϕ_i+2 is labeled by M^2 by
     definition of the transitive closure and by M due to Ramsey's
     theorem, so M=M^2. Since, by hypothesis,  satisfies SCT, there
     is j such that M_j,j is -1. So, for all i,
     u^(j)_ϕ_i(^*)^+ u^(j)_ϕ_i+1.
     Since ⊆ and _ is well-founded on ,
     the existence of an infinite sequence contradicts the fact that  is well-founded.
    
    
    By combining all the previous results, we get:
    
    
    
      The relation =∪ terminates on terms typable in
      łΠ/ if  is locally confluent and preserves typing, 
      is finite and  is well-structured, plain-function passing and
      size-change terminating.
    
    
    The rewriting system of Example <ref> verifies all these conditions (proof in the appendix).
    
    
    
    
    
    
    
    
    
    
    § IMPLEMENTATION AND COMPARISON WITH OTHER CRITERIA AND TOOLS
    
    
    We implemented our criterion in a tool called SizeChangeTool<cit.>. As far as we know, there are no other
    termination checker for łΠ/.
    
    If we restrict ourselves to simply-typed rewriting systems, then we
    can compare it with the termination checkers participating in the
    category “higher-order rewriting union beta” of the http://termination-portal.org/wiki/Termination_Competitiontermination
    competition<cit.>: http://wandahot.sourceforge.net/Wanda<cit.> uses dependency
    pairs, polynomial interpretations, HORPO and many transformation
    techniques <cit.>; SOL uses the General Schema
    <cit.> and other techniques; THOR uses some semantic version of HORPO
      <cit.>. As these tools implement various techniques
    and SizeChangeTool only one, it is difficult to compete with
    them. Still, there are examples that are solved by
    SizeChangeTool and not by one of the other tools, demonstrating
    that these tools would benefit from implementing our new technique. For
    instance, the problem  Hamana_Kikuchi_18/h17<cit.> is
    proved terminating by SizeChangeTool but not by Wanda
    because of the rule:
    [mathescape=true]
     rule map f (map g l)  map (comp f g) l
    
    And the problem  Kop13/kop12thesis_ex7.23 is proved terminating
    by SizeChangeTool but not by Sol because of the
    rules:[We renamed the function symbols for the sake of
      readability.][mathescape=true]
     rule f h x (s y)  g (c x (h y)) y     rule g x y  f (λ_,s 0) x y
    
    
    One could also imagine to translate a termination problem in
    łΠ/ into a simply-typed termination problem. Indeed, the
    termination of łΠ alone (without rewriting) can be reduced to the
    termination of the simply-typed ł-calculus
    <cit.>. This has been extended to łΠ/ when there
    are no type-level rewrite rules like the ones defining  El in
    Example <ref><cit.>.  However,
    this translation does not preserve termination as shown by
    the Example <ref> which is not terminating if all the
    types x are mapped to the same type constant.
    
    In <cit.>, Roux also uses dependency pairs for the
    termination of simply-typed higher-order rewriting systems, as well as a
    restricted form of dependent types where a type constant C is
    annotated by a pattern l representing the set of terms matching
    l. This extends to patterns the notion of indexed or sized types
    <cit.>. Then, for proving the absence of infinite chains,
    he uses simple projections <cit.>, which can be seen as a
    particular case of SCT where strictly decreasing arguments are fixed
    (SCT can also handle permutations in arguments).
    
    Finally, if we restrict ourselves to orthogonal systems, it is also
    possible to compare our technique to the ones implemented in the proof
    assistants Coq and Agda. Coq essentially
    implements a higher-order version of primitive recursion. Agda
    on the other hand uses SCT.
    
    Because Example <ref> uses matching on defined symbols,
    it is not orthogonal and can be written neither in Coq nor in
    Agda. Agda recently added the possibility of adding
    rewrite rules but this feature is highly experimental and comes with
    no guaranty. In particular, Agda termination checker does not
    handle rewriting rules.
    
    Coq cannot handle inductive-recursive definitions
    <cit.> nor function definitions with permuted arguments in
    function calls while it is no problem for Agda and us.
    
    
    
    
    
    
    
    
    
    
    § CONCLUSION AND FUTURE WORK
    
    
    We proved a general modularity result extending Arts and
    Giesl's theorem that a rewriting relation terminates if there are
    no infinite sequences of dependency pairs <cit.> from first-order
    rewriting to dependently-typed higher-order rewriting. Then,
    following <cit.>, we showed how to use Lee, Jones and
    Ben-Amram's size-change termination criterion to prove the absence of
    such infinite sequences <cit.>.
    
    This extends Wahlstedt's work <cit.> from weak to
    strong normalization, and from orthogonal to locally confluent rewriting
    systems. This extends the first author's work <cit.>
    from orthogonal to locally confluent systems, and from systems having
    a decreasing argument in each recursive call to systems with
    non-increasing arguments in recursive calls. Finally, this also
    extends previous works on static dependency pairs
    <cit.>suzuki11prokop11rta from simply-typed ł-calculus to
    dependent types modulo rewriting.
    
    To get this result, we assumed local confluence. However, one often
    uses termination to check (local) confluence. Fortunately, there are
    confluence criteria not based on termination. The most famous one is
    (weak) orthogonality, that is, when the system is left-linear and has
    no critical pairs (or only trivial ones) <cit.>, as it is
    the case in functional programming languages. A more general one is
    when critical pairs are “development-closed”<cit.>.
    
    This work can be extended in various directions.
    
    First, our tool is currently limited to PFP rules,
    that is, to rules where higher-order variables are direct subterms of
    the left-hand side. To have higher-order variables in deeper subterms
    like in Example <ref>,
    we need to define a more complex interpretation of types, following
    <cit.>.
    
    Second, to handle recursive calls in such systems, we also
    need to use an ordering more complex than the subterm ordering
    when computing the matrices labeling the SCT call graph.
    The ordering needed for handling Example <ref> is the
    “structural ordering” of Coq and Agda<cit.>. Relations other than subterm have
    already been considered in SCT but in a first-order setting only
    <cit.>.
    
    But we may want to go further because the structural ordering is not
    enough to handle the following system which is not accepted by
    Agda:
    
    [Division]m/n computes ⌈m/n⌉.
    [mathescape=true]
    symbol minus: NatNatNat             set infix 1 "-"  minus
      rule 0 - n  0       rule m - 0  m       rule (s m) - (s n)  m - n
    symbol div: NatNatNat               set infix 1 "/"  div
      rule 0 / (s n)  0    rule (s m) / (s n)  s ((m - n) / (s n))
    [For the sake of simplicity, we do not use the lists annotated with type and lengths of Example <ref>.][Map function on Rose trees][mathescape=true]
    symbol tree : TYPE    symbol list_tree : TYPE
      symbol node : list_tree  tree
      symbol nil : list_tree
      symbol cons : tree  list_tree  list_tree
    symbol map_list : (tree  tree)  list_tree  list_tree
      map_list f nil  nil
      map_list f (cons x l)  cons (f x) (map_list f l)
    symbol map : (tree  tree)  tree  tree
      map f (node(cons x l))  node(cons (map f x) (map_list (map f) l))
    Cet exemple est très différent de celui avec div et moins,
    puisque cette fois-ci on a un appel récursif partiellement appliqué,
    donc il ne suffit pas de modifier SCT,
    il faut modifier même notre définition des DP pour faire passer cet exemple.
    Je ne suis pas sûr qu'on veuille raconter ça ici.
    
    A solution to handle this system is to use arguments filterings
    (remove the second argument of  -) or simple projections
    <cit.>. Another one is to extend the type system with
    size annotations as in Agda and compute the SCT matrices by
    comparing the size of terms instead of their structure
    <cit.>. In our example, the size of  m - n
    is smaller than or equal to the size of  m. One can deduce this
    by using user annotations like in Agda, or by using heuristics
    <cit.>.
    
    Another interesting extension would be to handle function calls with locally
    size-increasing arguments like in the following example:
    [mathescape=true]
         rule f x  g (s x)           rule g (s (s x))  f x
    
    where the number of  s's strictly decreases between two calls to
     f although the first rule makes the number of  s's
    increase. Hyvernat enriched SCT to handle such systems <cit.>.
    
     Acknowledgments. The authors thank the anonymous referees for their comments, which have improved the quality of this article.
    
    
    
    
    
    
    
    
    plainurl10abel10par
    A. Abel.
    http://doi.org/10.4204/EPTCS.43.2MiniAgda: integrating
      sized and dependent types.
     PAR'10.EPTCS 43.arts00tcs
    T. Arts, J. Giesl.
    http://doi.org/10.1016/S0304-3975(99)00207-8Termination of
      term rewriting using dependency pairs.
     TCS 236:133–178, 2000.
    
    barendregt92chapter
    H. Barendregt.
     Lambda calculi with types.
     In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, 
      Handbook of logic in computer science. Volume 2. Background:
      computational structures, p. 117–309. Oxford University Press, 1992.
    
    blanqui00rta
    F. Blanqui.
    http://doi.org/10.1007/10721975_4Termination and confluence
      of higher-order rewrite systems.
     RTA'00.LNCS 1833.blanqui01phd
    F. Blanqui.
    http://tel.archives-ouvertes.fr/tel-00105522Théorie
      des types et récriture.
     PhD thesis, Université Paris-Sud, France, 2001.
    
    blanqui05mscs
    F. Blanqui.
    http://doi.org/10.1017/S0960129504004426Definitions by
      rewriting in the calculus of constructions.
     MSCS 15(1):37–92, 2005.
    
    blanqui16tcs
    F. Blanqui.
    http://doi.org/10.1016/j.tcs.2015.07.045Termination of
      rewrite relations on λ-terms based on Girard's notion of
      reducibility.
     TCS 611:50–86, 2016.
    
    blanqui18jfp
    F. Blanqui.
    http://doi.org/10.1017/S0956796818000072Size-based
      termination of higher-order rewriting.
     JFP 28(e11), 2018.
     75 pages.
    
    chin01hosc
    W. N. Chin, S. C. Khoo.
    http://doi.org/10.1023/A:1012996816178Calculating sized
      types.
     Higher-Order and Symbolic Computation, 14(2-3):261–300,
      2001.
    
    coquand92types
    T. Coquand.
    http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gzPattern
      matching with dependent types.
     TYPES'92.
    
    cousineau07tlca
    D. Cousineau, G. Dowek.
    http://doi.org/10.1007/978-3-540-73228-0_9Embedding pure type
      systems in the łΠ-calculus modulo.
     TLCA'07.LNCS 4583.dedukti
    Dedukti.
    <https://deducteam.github.io/>, 2018.
    dybjer00jsl
    P. Dybjer.
    http://www.jstor.org/stable/2586554A general formulation of
      simultaneous inductive-recursive definitions in type theory.
     JSL 65(2):525–549, 2000.
    
    sizechangetool
    G. Genestier.
    SizeChangeTool.
    <https://github.com/Deducteam/SizeChangeTool>, 2018.
    
    giesl04lpar
    J. Giesl, R. Thiemann, P. Schneider-Kamp.
    http://doi.org/10.1007/978-3-540-32275-7_21The dependency
      pair framework: combining techniques for automated termination proofs.
     LPAR'04.LNCS 3452.giesl06jar
    J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke.
    http://doi.org/10.1007/s10817-006-9057-7Mechanizing and
      improving dependency pairs.
     JAR 37(3):155–203, 2006.
    
    girard88book
    J.-Y. Girard, Y. Lafont, P. Taylor.
    http://www.paultaylor.eu/stable/prot.pdfProofs and
      types.
     Cambridge University Press, 1988.
    
    harper93jacm
    R. Harper, F. Honsell, G. Plotkin.
    http://doi.org/10.1145/138027.138060A framework for defining
      logics.
     JACM 40(1):143–184, 1993.
    
    hirokawa05ic
    N. Hirokawa, A. Middeldorp.
    http://doi.org/10.1016/j.ic.2004.10.004Automating the
      dependency pair method.
     IC 199(1-2):172–199, 2005.
    hirokawa07ic
    N. Hirokawa, A. Middeldorp.
    http://doi.org/10.1016/j.ic.2006.08.010Tyrolean TerminationTool: techniques and features.
     IC 205(4):474–511, 2007.
    
    hughes96popl
    J. Hughes, L. Pareto, A. Sabry.
    http://doi.org/10.1145/237721.240882Proving the correctness
      of reactive systems using sized types.
     POPL'96.
    
    hyvernat14lmcs
    P. Hyvernat.
    http://doi.org/10.2168/LMCS-10(1:11)2014The size-change
      termination principle for constructor based languages.
     LMCS 10(1):1–30, 2014.
    
    hyvernat10wst
    P. Hyvernat, C. Raffalli.
    https://lama.univ-savoie.fr/ raffalli/pdfs/wst.pdfImprovements on the
      "size change termination principle" in a functional language.
     WST'10.
    
    jones04rta
    N. D. Jones, N. Bohr.
    http://doi.org/10.1007/978-3-540-25979-4_1Termination
      analysis of the untyped lambda-calculus.
     RTA'04.LNCS 3091.jouannaud15tlca
    J.-P. Jouannaud, J. Li.
    http://doi.org/10.4230/LIPIcs.TLCA.2015.257Termination of
      Dependently Typed Rewrite Rules.
     TLCA'15.LIPIcs 38.klop93tcs
    J. W. Klop, V. van Oostrom, F. van Raamsdonk.
    http://doi.org/10.1016/0304-3975(93)90091-7Combinatory
      reduction systems: introduction and survey.
     TCS 121:279–308, 1993.
    
    kop11rta
    C. Kop.
    http://doi.org/10.4230/LIPIcs.RTA.2011.203Higher order
      dependency pairs for algebraic functional systems.
     RTA'11.LIPIcs 10.kop12phd
    C. Kop.
    http://hdl.handle.net/1871/39346Higher order
      termination.
     PhD thesis, VU University Amsterdam, 2012.
    
    kop12lmcs
    C. Kop, F. Van Raamsdonk.
    http://doi.org/10.2168/LMCS-8(2:10)2012Dynamic dependency
      pairs for algebraic functional systems.
     LMCS 8(2):1–51, 2012.
    kusakari07aaecc
    K. Kusakari, M. Sakai.
    http://doi.org/10.1007/s00200-007-0046-9Enhancing dependency
      pair method using strong computability in simply-typed term rewriting
      systems.
     AAECC 18(5):407–431, 2007.
    
    lee01popl
    C. S. Lee, N. D. Jones, A. M. Ben-Amram.
    http://doi.org/10.1145/360204.360210The size-change principle
      for program termination.
     POPL'01.
    
    lepigre17draft
    R. Lepigre, C. Raffalli.
    https://arxiv.org/abs/1604.01990Practical subtyping for
      System F with sized (co-)induction.
     2017.
    
    markowsky76au
    G. Markowsky.
     Chain-complete posets and directed sets with applications.
     Algebra Universalis, 6:53–68, 1976.
    
    mayr98tcs
    R. Mayr, T. Nipkow.
    http://doi.org/10.1016/S0304-3975(97)00143-6Higher-order
      rewrite systems and their confluence.
     TCS 192(2):3–29, 1998.
    
    roux11rta
    C. Roux.
    http://doi.org/10.4230/LIPIcs.RTA.2011.299Refinement Types as
      Higher-Order Dependency Pairs.
     RTA'11.LIPIcs 10.saillard15phd
    R. Saillard.
    https://pastel.archives-ouvertes.fr/tel-01299180Type
      checking in the Lambda-Pi-calculus modulo: theory and practice.
     PhD thesis, Mines ParisTech, France, 2015.
    
    sereni05aplas
    D. Sereni, N. D. Jones.
    http://doi.org/10.1007/11575467_19Termination analysis of
      higher-order functional programs.
     APLAS'05.LNCS 3780.suzuki11pro
    S. Suzuki, K. Kusakari, F. Blanqui.
    https://hal.inria.fr/inria-00555008Argument filterings and
      usable rules in higher-order rewrite systems.
     IPSJ Transactions on Programming 4(2):1–12, 2011.
    terese03bookTeReSe.
     Term rewriting systems, volume 55 of  Cambridge Tracts in
      Theoretical Computer Science.
     Cambridge University Press, 2003.
    
    tc<http://termination-portal.org/wiki/Termination_Competition>, 2018.
    thiemann07phd
    R. Thiemann.
    http://aib.informatik.rwth-aachen.de/2007/2007-17.pdfThe
      DP framework for proving termination of term rewriting.
     PhD thesis, RWTH Aachen University, 2007.
     Technical Report AIB-2007-17.
    
    thiemann05aaecc
    R. Thiemann, J. Giesl.
    http://doi.org/10.1007/s00200-005-0179-7The size-change
      principle and dependency pairs for termination of term rewriting.
     AAECC 16(4):229–270, 2005.
    
    toyama87ipl
    Y. Toyama.
    http://doi.org/10.1016/0020-0190(87)90122-0Counterexamples to
      termination for the direct sum of term rewriting systems.
     IPL 25(3):141–143, 1987.
    tpdbhttp://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDBTermination problem
      data base (TPDB), 2018.
    oostrom94phd
    V. van Oostrom.
    http://www.phil.uu.nl/ oostrom/publication/ps/phdthesis.psConfluence
      for abstract and higher-order rewriting.
     PhD thesis, Vrije Universiteit Amsterdam, 1994.
    
    oostrom97tcs
    V. van Oostrom.
    http://doi.org/10.1016/S0304-3975(96)00173-9Developing
      developments.
     TCS 175(1):159–181, 1997.
    
    wahlstedt07phd
    D. Wahlstedt.
    http://www.cse.chalmers.se/alumni/davidw/wdt_phd_printed_version.pdfDependent
      type theory with first-order parameterized data types and well-founded
      recursion.
     PhD thesis, Chalmers University of Technology, 2007.
    
    wanda
    Wanda.
    <http://wandahot.sourceforge.net/>.
    
    
    § PROOFS OF LEMMAS ON THE INTERPRETATION
    
    
     §.§ Definition of the interpretation
    F is monotone wrt inclusion.
    
      We first prove that D is monotone. Let I J and T∈ D(I).
      We have to show that T∈
      D(J). To this end, we have to prove (1) T∈ and (2) if
      T^*(x:A)B then A∈(J) and, for all a∈ J(A),
      B[x→ a]∈(J):
      
      *  Since T∈ D(I), we have T∈.
      
      *  Since T∈ D(I) and T^*(x:A)B, we have A∈(I)
        and, for all a∈ I(A), B[x→ a]∈(I). Since I J, we
        have (I)(J) and J(A)=I(A) since I and J are
        functional relations. Therefore, A∈(J) and, for all a∈
        I(A), B[x→ a]∈(J).
      
    
      We now prove that F is monotone. Let I J and T∈ D(I).
      We have to show that
      F(I)(T)=F(J)(T). First, T∈ D(J) since D is
      monotone.
    
      If T=(x:A)B, then F(I)(T)=aI(A)I(B[x→ a]) and
      F(J)(T)=aJ(A)J(B[x→ a]). Since T∈ D(I), we have
      A∈(I) and, for all a∈ I(A), B[x→ a]∈(I). Since
      (I)(J), we have J(A)=I(A) and, for all a∈ I(A),
      J(B[x→ a])=I(B[x→ a]). Therefore, F(I)(T)=F(J)(T).
    
      Now, if T is not a product, then
      F(I)(T)=F(J)(T)=.
    
    
     §.§ Computability predicates
     is a computability predicate.
    
    Note that =D().
    
      *  by definition of D.
    
      *  Let T∈ and T' such that T T'. We have
      T'∈ since T∈. Assume now that T'^*(x:A)B. Then,
      T^*(x:A)B, A∈ and, for all a∈(A),
      B[x→ a]∈. Therefore, T'∈.
    
      *  Let T be a neutral term such that T. Since
      , T∈. Assume now that T^*(x:A)B. Since
      T is neutral, there is U∈T such that
      U^*(x:A)B. Therefore, A∈ and, for all a∈(A),
      B[x→ a]∈.
      If P∈ and, for all a∈ P, Q(a)∈, then aPQ(a)∈.
    
    Let R=aPQ(a).
    
      *  Let t∈ R. We have to prove that t∈. Let
      x∈. Since P∈, x∈ P. So, tx∈ Q(x). Since
      Q(x)∈, Q(x). Therefore, tx∈, and t∈.
    
      *  Let t∈ R and t' such that t t'. We have to prove that
      t'∈ R. Let a∈ P. We have to prove that t'a∈ Q(a). By
      definition, ta∈ Q(a) and ta t'a. Since Q(a)∈, t'a∈
      Q(a).
    
      *  Let t be a neutral term such that t R. We have to
      prove that t∈ R. Hence, we take a∈ P and prove that ta∈
      Q(a). Since P∈, we have a∈ and ^*(a)P. We
      now prove that, for all b∈^*(a), tb∈ Q(a), by induction on
      . Since t is neutral, tb is neutral too and it suffices to
      prove that tb Q(a). Since t is neutral,
      tb=tb∪ tb. By induction hypothesis,
      tb Q(a). By assumption, t R. So,
      ta Q(a). Since Q(a)∈, tb Q(a)
      too. Therefore, ta∈ Q(a) and t∈ R.
      For all T∈, (T) is a computability predicate.
    
      Since _p(,) is a chain-complete poset, it suffices to
      prove that _p(,) is closed by F. Assume that
      I∈_p(,). We have to prove that F(I)∈_p(,),
      that is, for all T∈ D(I), F(I)(T)∈. There are two
      cases:
      
      *  If T=(x:A)B,
        then F(I)(T)=aI(A)I(B[x→ a]).
        By assumption, I(A)∈ and, for a∈ I(A),
        I(B[x→ a])∈. Hence, by Lemma <ref>,
        F(I)(T)∈.
      
      *  Otherwise, F(I)(T)=∈.▸ Lemma <ref><ref>. For all terms T and substitutions , T_∈.
      By induction on T. If T=s, then T_=∈ by
      Lemma <ref>. If T=(x:A)K∈, then
      T_=aA_K_[x→ a,]. By induction
      hypothesis, A_∈ and, for all a∈A_,
      K_[x→ a,]∈. Hence, by Lemma
      <ref>, T_∈. If
      T∉∪{} and T∈, then
      T_=(T)∈ by Lemma
      <ref>. Otherwise, T_=∈.
    
    
     §.§ Invariance by reduction
    
    
    We now prove that the interpretation is invariant by reduction.
    
    
      If T∈ and T T', then (T)=(T').
    
      First note that T'∈ since ∈. Hence, (T') is well defined. Now, we have T∈
      since . So, T'∈ and, by local confluence and Newman's lemma,
      T=T'. If T=(x:A)B
      then (T)=a(A)(B[x→ a])=(T').
      Otherwise, (T)==(T').
    ▸ Lemma <ref><ref>. If T is typable, T∈ and T T', then T_=T'_.
      By assumption, there are  and U such that þ T:U. Since
       preserves typing, we also have þ T':U. So, T≠, and
      T'≠. Moreover, T∈ iff T'∈ since þ T: iff
      T∈ and T is typable. In addition, we have T'∈
      since T∈ and ∈.
    
      We now prove the result, with T^=T' instead of T T', by
      induction on T. If T∉, then T'∉ and, since
      T,T'∈, T_=(T)=(T')=T'_ by Lemma
      <ref>. If T=, then
      T_==T'_. Otherwise, T=(x:A)K and
      T'=(x:A')K' with A^=A' and K^=K'. By inversion, we have
      þ A:, þ A':, ,x:Aþ K: and ,x:A'þ
      K':. So, by induction hypothesis, A_=A'_ and, for
      all a∈A_, K_'=K'_', where '=[x→
        a,]. Therefore, T_=T'_.
    ▸ Lemma <ref><ref>. If T is typable, T∈ and ', then T_=T_'.
      By induction on T.
      
      *  If T∈S, then T_==T_'.
      
      *  If T=(x:A)K and K∈,
        then T_=aA_K_[x→ a,]
        and T_'=aA_'K_[x→ a,'].
        By induction hypothesis,
        A_=A_' and, for all a∈A_, K_[x→
            a,]=K_[x→ a,']. Therefore,
        T_=T_'.
      
      *  If T∈, then T_=(T) and
        T_'=(T'). Since T^*T', by Lemma
        <ref><ref>, (T)=(T').
      
      *  Otherwise, T_==T_'.
    
     §.§ Adequacy of the interpretation
    ▸ Lemma <ref><ref>. If (x:A)B is typable, ((x:A)B)∈ and
      x∉()∪(),
      then (x:A)B_=aA_B_[x→ a,].
      If B is a kind, this is immediate. Otherwise, since
      ((x:A)B)∈, (x:A)B_=(((x:A)B)). Since
      x∉()∪(), we have ((x:A)B)=(x:A)B. Since
      (x:A)B∈ and , we have
      (x:A)B_=a(A)((B)[x→ a]).
    
      Since (x:A)B is typable, A is of type  and
      A∉∪{}. Hence, A_=(A) and, by Lemma
      <ref>, (A)=(A).
    
      Since (x:A)B is typable and not a kind, B is of type  and
      B∉∪{}. Hence, B_[x→ a,]=(B[x→
        a,]). Since x∉()∪(), B[x→
        a,]=(B)[x→ a]. Hence, B_[x→ a,]=((B)[x→ a]) and,
      by Lemma <ref>,
      ((B)[x→ a])=((B)[x→ a]).
    
      Therefore, (x:A)B_=aA_B_[x→ a,].
    
    
    Note that, by iterating this lemma, we get that v∈∏ U
    iff, for all  such that [→]:,
    v∈U_[→].
    
    ▸ Lemma <ref><ref>. If þ U:s, þ: and U∈, then
      U_=U_.
      We proceed by induction on U. Since þ U:s and þ:,
      we have þ U:s.
      
      *  If s=, then U,U∉∪{}
      and U_=(U)=U_ since
      U∈.
      
      *  Otherwise, s= and U∈.
       
      *  If U=,
         then U_==U_.
        
      *  Otherwise, U=(x:A)K and,
          by Lemma <ref><ref>,
           U_=aA_K_[x→ a,]
           and U_=aA_K_[x→ a,].
           By induction hypothesis,
           A_=A_ and, for all a∈A_,
           K_[x→ a,]=K_[x→ a,]. Wlog we can assume x∉()∪(). So, K_[x→
           a,]=K_[x→ a,].▸ Lemma <ref><ref>. Let P be a computability predicate and Q a P-indexed family of
      computability predicates such that Q(a') Q(a) whenever a
      a'. Then, ł x:A.b∈aPQ(a) whenever A∈ and, for
      all a∈ P, b[x→ a]∈ Q(a).
      Let a_0∈ P. Since P∈, we have a_0∈ and x∈ P. Since
      Q(x)∈ and b=b[x→ x]∈ Q(x), we have b∈.
      Let a∈^*(a_0). We can prove
      that ( xAb)a∈ Q(a_0) by induction on (A,b,a) ordered by
      (,,)_prod. Since Q(a_0)∈ and ( xAb)a is
      neutral, it suffices to prove that ( xAb)a
      Q(a_0). If the reduction takes place in A, b or a, we can
      conclude by induction hypothesis. Otherwise, ( xAb)a b[x→ a]∈
      Q(a) by assumption. Since a_0^*a and Q(a') Q(a) whenever
      a a', we have b[x→ a]∈ Q(a_0).
    
    
    § TERMINATION PROOF OF EXAMPLE <REF>
    
    
    Here is the comprehensive list of dependency pairs in the example:
    [escapeinside=**]
    * A:*               El (arrow a b) > El a
    * B:*               El (arrow a b) > El b
    * C:*                    (s p) + q > p + q
    * D:*   app a _ (cons _ x p l) q m > p + q
    * E:*   app a _ (cons _ x p l) q m > app a p l q m
    * F:*len_fil a f _ (cons _ x p l)  > len_fil_aux (f x) a f p l
    * G:*len_fil a f _ (app _ p l q m) >
                            (len_fil a f p l) + (len_fil a f q m)
    * H:*len_fil a f _ (app _ p l q m) > len_fil a f p l
    * I:*len_fil a f _ (app _ p l q m) > len_fil a f q m
    * J:*    len_fil_aux true  a f p l > len_fil a f p l
    * K:*    len_fil_aux false a f p l > len_fil a f p l
    * L:*    fil a f _ (cons _ x p l)  > fil_aux (f x) a f x p l
    * M:*    fil a f _ (app _ p l q m) >
                            app a (len_fil a f p l) (fil a f p l)
                                  (len_fil a f q m) (fil a f q m)
    * N:*    fil a f _ (app _ p l q m) > len_fil a f p l
    * O:*    fil a f _ (app _ p l q m) > fil a f p l
    * P:*    fil a f _ (app _ p l q m) > len_fil a f q m
    * Q:*    fil a f _ (app _ p l q m) > fil a f q m
    * R:*      fil_aux true  a f x p l > len_fil a f p l
    * S:*      fil_aux true  a f x p l > fil a f p l
    * T:*      fil_aux false a f x p l > fil a f p l
    
    
    The whole callgraph is depicted below.
    The letter associated to each matrix corresponds to the
    dependency pair presented above and in example <ref>, except for TC 's which comes from the computation
    of the transitive closure and labels dotted edges.
    
    
    [draw] (filter) at (2,0) fil;
        [draw] (f_aux) at (-1,0) fil_aux;
        [draw] (l_filter) at (2,-2) len_fil;
        [draw] (l_f_aux) at (-3,-2) len_fil_aux;
        [draw] (el) at (-3.5,0) El;
        [draw] (app) at (5,0) app;
        [draw] (pl) at (5,-2) +;
        [>=latex,->] (el) to[out=135,in=90] (-4.5,0) to[out=-90,in=-135] (el);
        [left] (ell) at (-4.5,0) A,B;
        [>=latex,->] (pl) to[out=45,in=90] (6,-2) to[out=-90,in=-45] (pl);
        [right] (pll) at (6,-2) C;
        [>=latex,->] (app) to[bend left=8] node[midway,right] D (pl);
        [>=latex,->] (app) to[out=45,in=90] (6.2,0) to[out=-90,in=-45] (app);
        [right] (appl) at (6.2,0) E;
        [>=latex,->] (l_filter) to[bend left=8] node[midway,above] F (l_f_aux);
        [>=latex,->] (l_filter) to[bend left=8] node[midway,above] G (pl);
        [>=latex,->] (1.5,-2.27) to[out=-45,in=0] (1.35,-2.8) to[out=180,in=-150] (1.23,-2.21);
        [below] (l_filterl) at (1.35,-2.8) H,I;
        [>=latex,->] (l_f_aux) to[bend left=8] node[midway,above] J,K (l_filter);
        [>=latex,->] (filter) to[bend left=10] node[midway,above] L (f_aux);
        [>=latex,->] (f_aux) to[bend right=10] node[midway,above,right] R (l_filter);
        [>=latex,->] (f_aux) to[bend left=10] node[midway,above] S,T (filter);
        [>=latex,->] (filter) to[bend left=10] node[midway,above] M (app);
        [>=latex,->] (filter) to[bend right=10] node[midway,right] N,P (l_filter);
        [>=latex,->] (1.75,0.23) to[out=45,in=0] (1.6,0.8) to[out=180,in=150] (1.6,0.19);
        [above] (filterl) at (1.6,0.8) O,Q;
        [>=latex,->,densely dashed] (f_aux) to[out=45,in=0] (-1,0.8) to[out=180,in=135] (f_aux);
        [above] (f_auxTC) at (-1,0.8) TC_4;
        [>=latex,->,densely dashed] (2.4,0.19) to[out=30,in=0] (2.4,0.8) to[out=180,in=135] (2.25,0.23);
        [above] (filterTC) at (2.4,0.8) TC_3;
        [>=latex,->,densely dashed] (l_f_aux) to[out=-45,in=0] (-3,-2.8) to[out=180,in=-135] (l_f_aux);
        [below] (l_f_auxTC) at (-3,-2.8) TC_1;
        [>=latex,->,densely dashed] (2.77,-2.21) to[out=-30,in=0] (2.7,-2.8) to[out=180,in=-135] (2.55,-2.27);
        [below] (l_filterTC) at (2.7,-2.8) TC_2;
        
        
        
        
        
        
        
        
      
    
    
    
    
    The argument  a is omitted everywhere on the matrices presented below:
    
    
     A,B=([ -1;    ]),
     C=([ -1  ∞;  ∞  0;    ]),
     D=([  ∞  ∞; -1  ∞;  ∞  0;  ∞  ∞;    ]),
     E=([  ∞  ∞  ∞  ∞; -1 -1  ∞  ∞;  ∞  ∞  0  ∞;  ∞  ∞  ∞  0;    ]),
     F=([  ∞  0  ∞  ∞;  ∞  ∞  ∞  ∞;  ∞  ∞ -1 -1;    ]),
     J= K=([ ∞ ∞ ∞; 0 ∞ ∞; ∞ 0 ∞; ∞ ∞ 0;   ]),
     G=([ ∞ ∞; ∞ ∞; ∞ ∞;   ]),
     H= I= N= O= P= Q=([  0  ∞  ∞;  ∞  ∞  ∞;  ∞ -1 -1;    ]),
     L=([  ∞  0  ∞  ∞  ∞;  ∞  ∞  ∞  ∞  ∞;  ∞  ∞ -1 -1 -1;    ]),
     M=([ ∞ ∞ ∞ ∞; ∞ ∞ ∞ ∞; ∞ ∞ ∞ ∞;   ]),
     R= S= T=([ ∞ ∞ ∞; 0 ∞ ∞; ∞ ∞ ∞; ∞ 0 ∞; ∞ ∞ 0;   ]).
    
    
    Which leads to the matrices labeling a loop in the transitive closure:
    
     TC_1= J× F=([  ∞  ∞  ∞  ∞;  ∞  0  ∞  ∞;  ∞  ∞  ∞  ∞;  ∞  ∞ -1 -1;    ]),
     TC_4= S× L=([  ∞  ∞  ∞  ∞  ∞;  ∞  0  ∞  ∞  ∞;  ∞  ∞  ∞  ∞  ∞;  ∞  ∞  ∞  ∞  ∞;  ∞  ∞ -1 -1 -1;    ]),
     TC_3= L× S= TC_2= F× J=([  0  ∞  ∞;  ∞  ∞  ∞;  ∞ -1 -1;    ])= O= H.
    
    
    It would be useless to compute matrices labeling edges which are not in a strongly connected component of the call-graph (like  S×R),
    but it is necessary to compute all the products which could label a loop,
    especially to verify that all loop-labeling matrices are idempotent,
    which is indeed the case here.
    
    
    As an example, we can detail the calculus performed to compute  TC_3^2:
    
        ([    min(0+0,∞+∞,∞+∞)   min(0+∞,∞+∞,∞+-1)   min(0+∞,∞+∞,∞+-1);    min(∞+0,∞+∞,∞+∞)   min(∞+∞,∞+∞,∞+-1)   min(∞+∞,∞+∞,∞+-1);  min(∞+0,-1+∞,-1+∞) min(∞+∞,-1+∞,-1+-1) min(∞+∞,-1+∞,-1+-1);                     ])
    
    
    We now check that this system is well-structured. For each rule
    f r, we take the environment _f r made of all
    the variables of r with the following types:
     a:Set, b:Set, p:, q:, x:El a, l: a p, m: a q, f:El a.
    
    The precedence infered for this example is the smallest containing:
    
      *  comparisons linked to the typing of symbols:
    
    
    Set    ≼ arrow    
    Set,,0    ≼ nil
    
    Set    ≼ El   
    Set,El,,,s    ≼ cons
       ≼ true    
    Set,,,+    ≼ app
       ≼ false    
    Set,El,,,   ≼ len_fil
       ≼ 0    ,Set,El,,   ≼ len_fil_aux
       ≼ s   
    Set,El,,,,len_fil    ≼ fil
       ≼ +    ,Set,El,,,len_fil_aux    ≼ fil_aux 
    
    Set,   ≼   
    
    
      *  and comparisons related to calls:
    
    
    s    ≼ +    
    s,len_fil    ≼ len_fil_aux 
    
    cons,+    ≼ app    
    nil,fil_aux,app,len_fil    ≼ fil 
    
    0,len_fil_aux,+    ≼ len_fil    
    fil,cons,len_fil    ≼ fil_aux
    
    
    
    This precedence can be sum up in the following diagram, where symbols in the same box are equivalent:
    
    [draw] (filter) at (2,6)fil,fil_aux;
        [draw] (l_filter) at (3,4.5) len_fil,len_fil_aux;
        [draw] (append) at (-1,4.5) app;
        [draw] (true) at (4,1.5) true;
        [draw] (false) at (6,1.5) false;
        [draw] (B) at (5,0) ;
        [draw] (cons) at (-2,3) cons;
        [draw] (nil) at (0,3) nil;
        [draw] (plus) at (3,3) +;
        [draw] (L) at (-1,1.5) ;
        [draw] (arrow) at (-4,1.5) arrow;
        [draw] (El) at (-3,1.5) El;
        [draw] (zero) at (1,1.5) 0;
        [draw] (succ) at (3,1.5) s;
        [draw] (Set) at (-3.5,0) Set;
        [draw] (N) at (2,0) ;
        [>=latex,->] (Set) to (arrow);
        [>=latex,->] (Set) to (El);
        [>=latex,->] (Set) to (L);
        [>=latex,->] (N) to (L);
        [>=latex,->] (N) to (zero);
        [>=latex,->] (N) to (succ);
        [>=latex,->] (B) to (true);
        [>=latex,->] (B) to (false);
        [>=latex,->] (El) to (cons);
        [>=latex,->] (L) to (cons);
        [>=latex,->] (L) to (nil);
        [>=latex,->] (zero) to (nil);
        [>=latex,->] (succ) to (plus);
        [>=latex,->] (cons) to (append);
        [>=latex,->] (plus) to (append);
        [>=latex,->] (plus) to (l_filter);
        [>=latex,->] (append) to (filter);
        [>=latex,->] (l_filter) to (filter);
        [>=latex,->] (zero) to (l_filter);
        [>=latex,->] (L) to[bend right=5] (l_filter);
        [>=latex,->] (B) to[bend right=35] (l_filter);
        [>=latex,->] (nil) to[bend left=15] (filter);
        [>=latex,->] (succ) to (cons);
        [>=latex,->] (El) to[out=15,in=-175] (l_filter); ] ]
