Mechanical verification of algorithm termination

Kostas Arkoudas

June 24, 1997

1 Introduction

An important problem in many verification logics is proving that a recursively defined algorithm halts for all appropriate inputs. Termination is important for demonstrating total correctness. For instance, proving that QuickSort produces a sorted permutation of any given list of numbers presupposes that the algorithm halts on all input lists. Termination is also important from an operational standpoint—infinite loops are generally undesirable. If we have a formal guarantee that every procedure written by the programmer halts on all inputs, then we can be assured that execution will never diverge. In this paper we present an efficient and fully automatic method for proving that a given algorithm halts on all inputs.

Of course in any Turing-complete formalism the problem of determining whether an arbitrary algorithm computes a total function is mechanically undecidable (more undecidable, in fact, than the halting problem^{1}). Accordingly, the best we can hope for is a conservative approximation. The claimed advantage of the present method is that it is a good approximation, i.e., that it verifies the termination of a wide variety of algorithms that a programmer might wish to express in practice; and furthermore, that it does so efficiently, and without requiring any help from or interaction with the user.

There are other alternatives for ensuring termination. One is to constrain the syntax of the language in such a way that the programmer can only define total functions, in which case termination is guaranteed a priori. This is the approach taken in Martin-Löf’s type theory [10], in which only primitive recursive definitions are possible. Gödel’s T system [5] is another formalism in which only total functions are definable. From a theoretical viewpoint these formalisms are quite powerful, in the sense that any total function a programmer might want to compute “in the real world” will likely be definable in the system. It is known, for example, that any computable function which is provably total in first-order arithmetic is definable in Gödel’s T system. This extensional power, however, derives from the use of high-order functionals and often has little bearing in practice.

1In the arithmetic hierarchy the halting problem is in Σ_{1}, while the totality problem is 1-complete for Π_{2}.

Without resorting to functionals one is limited to first-order primitive recursive definitions (in which a recursive call is of the form f(sel(x)) for some selector sel that decreases the size of the input x by exactly one), which are useful, of course, but not quite adequate. Many well-known algorithms— such as Euclid’s algorithm and most sorting algorithms—are defined in a non-primitive-recursive way. Such algorithms are often defined by some form of course-of-values recursion in which the size of an argument to a recursive call may decrease by an arbitrary quantity, not just by one. In MergeSort, for instance, the algorithm is recursively called on each half of the input list; and in Euclid’s algorithm, too, the arguments to the successive recursive calls decrease by large leaps—the main reason why it is such an excellent method for computing greatest common divisors.

Such algorithms would be rejected by a system that only accepted primitive recursive definitions, even though, extensionally speaking, the functions computed by these algorithms would be definable by some primitive recursive definition, albeit a convoluted and inefficient one. The method presented in this paper does not increase the extensional power of these systems, but it does recognize algorithms such as the above that use course-of-values recursion.

Another alternative is to retain a Turing-complete language but require the users to prove to the system that their algorithms always halt. This is the approach taken in the Boyer-Moore theorem prover [1], in which the user must “help” the system understand why an algorithm terminates by formulating certain inductive lemmata that provide relevant hints. The main advantage of this method is its broad applicability, the fact that it can be used on a large class of algorithms. Its downside is that it places a large share of the burden of proof on the user, who is expected to have a clear idea of why the algorithm terminates and to guide the system to the desired conclusions—an expectation that naive users often cannot meet.

Our method stems from Walther’s work on the subject [13], and is based on the idea of argument-bounded functions. A function g is argumentbounded (a.b. for short) if it does not increase the size of its argument; i.e., if the size of g(x) is ≤ the size of x, for any x.^{2} An example is the tail function on lists. Oftentimes the argument to a recursive call of an algorithm f has the form f(g(x)), where g is an a.b. function such as tail and x is the input of f. Under certain conditions an a.b. function g actually reduces the size of its argument, i.e., we have SZ(g(x)) < SZ(x). The basic idea is to verify that these conditions obtain whenever a recursive call f(g(x)) is made. This, of course, will entail that every time a recursive call is made the size of the argument strictly decreases; and since size cannot go on decreasing indefinitely, the algorithm must terminate.

When g is a selector such as pred or tail then the conditions under which SZ(g(x)) < SZ(x) are simple: x must have positive size. In that case the size of g(x) is exactly one less than the size of x. Thus, to verify the termination of f, we must show that in the context of every recursive call f(g(x)), the argument x has positive size. This is usually easy to do, because recursive calls f(g(x)) almost always occur under explicitly stated assumptions such as x ≠ 0, or x ≠ empty, etc. This is why the termination of primitive recursive definitions is so easy to verify.

Selectors, of course, are known to be a.b. by definition. We do not have to infer that. The challenge in moving from primitive recursion to courseof-values recursion is to mechanically identify a.b. functions g other than selectors; infer conditions under which such functions g actually reduce the size of their arguments; and verify that these conditions hold whenever a recursive call f(g(x)) is made.

Consider, for example, the recursive call Gcd(Minus(n,m),m) made in the body of Euclid’s algorithm for computing Gcd(n,m). The key here is to somehow know that Minus(n,m) never increases the size of n (i.e., that Minus is “1-bounded”), and further, that it actually decreases n whenever both n and m are non-zero. We then simply have to verify that every time the recursive call Gcd(Minus(n,m),m) is made, both n and m are non-zero—a fact which is almost handed to us on a platter by the algorithm’s definition. Or consider the algorithm MinSort(l) which returns empty if l is empty and

add(Min(l),MinSort(RemoveMin(l))) otherwise, where RemoveMin(l) is

a previously defined algorithm that returns a copy of l with its smallest element removed.^{3} Again the key here is to know that RemoveMin is a.b., and that it reduces the size of its input list whenever the latter is non-empty. Then all we have to do is verify that l is non-empty in the context of the recursive call MinSort(RemoveMin(l)), which again is transparent from the algorithm’s definition.

2For the purposes of this introduction we focus on unary functions.

3Assume for simplicity that all the elements of l are distinct.

Walther [13] has a sophisticated system for (a) inferring that a function g is a.b., (b) deriving a disjunction of conditions that is sufficient and necessary for g to reduce its argument, and (c) verifying that one of the disjuncts is true whenever a recursive call f(g(x)) is made. At the heart of this arrangement is a calculus for inferring size inequalities. We modify that calculus in a way that expedites inference without sacrificing expressiveness. We then drastically simplify (b) by considering only one type of condition: whether or not the input x has positive size. I.e., we only try to prove one specific lemma: that SZ(x) > 0 is sufficient for SZ(g(x)) < SZ(x). As a result, step (c) is greatly simplified as well: we only need to check that in the context of a recursive call f(g(x)), we have SZ(x) > 0, so we can “fire” our lemma. As we have already indicated, inferring conditions of the form SZ(x) > 0 is usually very easy.

In contrast, because the conditions inferred in (b) by Walther’s method are generally much more complicated than our simple “SZ(x) > 0” triggers, step (c) becomes much harder in his system. In particular, he assumes that a general-purpose induction theorem prover is available which can be invoked at step (c) to verify the disjunction generated in (b). On the one hand this level of sophistication enables his system to recognize some algorithms which our method does not. On the other hand, even if we assume one is available, calling up a general-purpose theorem prover to inductively verify hypotheses of essentially arbitrary complexity can be quite expensive. By contrast, our method does not require any special theorem-proving capabilities and has a provably low worst-case complexity.^{4} Moreover, empirical tests on a variety of benchmarks have shown the success rate of our method to be nearly identical to that of Walther’s.

The remainder of this paper is organized as follows. In the next section we describe IFL, a simple purely functional language that we will use to illustrate our method. In Sec. 3 we define the central concepts on which our method is based, and in the following section we offer a preview without getting into much detail. Sec. 5 explains the main parts of the method in detail, while the next section discusses some examples. Sec. 7 illustrates some typical scenarios in which the method would not work, Sec. 8 examines the possibility of future extensions, and finally Sec. ?? reviews previous similar work.

4And in fact on average the method has been found to be extremely fast. The termination of 35 functions taken from [13], [1], and elsewhere, was verified by the existing implementation of our method (in C++) in slightly less than a minute.

2 The language

2.1 Syntax

Datatypes

The language offers concrete data types very similar to those of ML. The main difference is that polymorphism is not supported. Another difference is that the user must explicitly specify selectors (destructors) for each constructor, as pattern matching is not available.^{5} In particular, an IFL datatype is defined as follows:

datatype T = ConDec {“|” ConDec};^{6}

where each constructor declaration ConDec is either a plain identifier (representing a constructor of no arguments), or an expression of the form

con(sel_{1} : type_{1}, …, sel_{n} : type_{n})

where con, sel_{i}, and type_{i} are identifiers; sel_{i} will be the selector associated with the i^{th} argument position of con. Some well-known data types are defined below in this notation.

    datatype Boolean = true | false;
    datatype NatNum = zero | succ(pred:NatNum);
    datatype NatList = empty | add(head:NatNum,tail:NatList);
    datatype BTree = null |
                    node(value:NatNum,left:BTree,right:BTree);
    datatype LamTerm = var(index:NatNum) |
                       abs(formal:NatNum,body:LamTerm) |
                       app(rator:LamTerm,rand:LamTerm);

A constructor c(sel_{1}:T_{1}, …, sel_{n}:T_{n}) of a datatype T is viewed as a function c : T_{1}×⋯×T_{n} → T that produces objects of type T. E.g. the signatures

of zero and succ are zero: → NatNum and succ:NatNum → NatNum. We call

T_{i} the i^{th} argument type of c. A constructor of zero arguments is called a constant. We define the objects of type T as follows:

1. A constant of T is an object of type T.

5The method itself does not essentially depend on these restrictions and could be adapted to a language with pattern-matching and even polymorphism; see Sec. 8.

6The notation {A} means zero or more occurences of A.

2. If c : T_{1} ×⋯×T_{n} → T is a constructor of T and w_{1}, …, w_{n} are objects of types T_{1}, …, T_{n}, respectively, then c(w_{1}, …, w_{n}) is an object of type T.

Thus, an object is simply a Herbrand term that is built exclusively from constructors. E.g. the objects of type NatNum are zero, succ(zero),

succ(succ(zero)), and so on.

We write sel_{i}^{c} to denote the selector associated with the i^{th} argument position of constructor c; e.g., seladd_{2} = tail. Selectors are the inverses of constructors. A constructor c of arity n > 0 “binds” or “pulls together” n objects w_{1}, …, w_{n} to produce a new complex object w, which, in some sense, contains the w_{i} objects. By contrast, when sel_{i}^{c} is applied to w it retrieves the component object w_{i}—it projects the object w along the i^{th} co-ordinate. In symbols, we have sel_{i}^{c}(c(w_{1}, …, w_{n})) = w_{i}.

If a constructor c of T takes an argument of type T then it is called reflexive. Examples are succ, add, and app. Constructors that are not reflexive are called irreflexive. Examples are zero, empty, and var. Note that a datatype T must have at least one irreflexive constructor so that production of T -objects can get started, so to speak. In a similar vein, a selector is called reflexive if its type is the same as its argument type. Thus, pred and tail are reflexive selectors, while head and formal are irreflexive. We will write RCON_{T} and IRCON_{T} for the reflexive and irreflexive constructors of T, respectively, and CON_{T} for RCON_{T} ∪ IRCON_{T}. The set of all selectors of all constructors of T will be written as SEL_{T}.

Our stipulations so far do not specify what happens if we apply a selector of a constructor c : T_{1} × ⋯ × T_{n} → T, say sel_{i}^{c}, to an object of type T that is not constructed by c, i.e., whose top function symbol is not c. E.g. what is “the value” of pred(zero) or of formal(var(zero))? This is a problem because we wish to regard sel_{i}^{c} as a total function from T to T_{i}; that is, sel_{i}^{c} should return some object of type T_{i} or another regardless of what object of type T it is given as input. We adopt the convention that when sel_{i}^{c} is applied to an object of type T whose top symbol is not c, the result is the minimal object of type T_{i}. In general, the minimal object of a datatype T is defined to be either (i) the leftmost constant of T, if one exists, or else (ii) the object obtained by applying the leftmost irreflexive constructor of T (one must exist) to the minimal objects of its argument types. For instance, the minimal objects of NatList and LamTerm are empty and var(zero), respectively.

Functions

A function definition has the form

function fun-name(par_{1}:T_{1}, …, par_{n}:T_{n}):T = fun-body; where fun-body is either (i) a single term r of type T (we will shortly specify what we mean by “a term of type T ”), or else it is (ii) an if-then-else expression of the form

        if E_{1} then r_{1} else · · · if E_{m} then r_{m} else r_{m+1}

for some m ≥ 1. The expression [(E_{1}, r_{1}), …, (E_{m}, r_{m}), (true, r_{m+1})], for m ≥ 0, will be used as a shorthand for the body of an arbitrary function (case (i) would correspond to m = 0 and case (ii) to m > 0). Each r_{i} must be a term of type T, while each boolean expression E_{i} is either an equality of the form r = s for two terms r and s of the same type, or else it is either a negation or a conjunction or a disjunction built from other boolean expressions. Two simple examples illustrating this syntax are included below.

    function Minus(n,m:NatNum):NatNum =
    if m = zero then n
    else
      Minus(pred(n),pred(m));
    function Member(n:NatNum,l:NatList):Boolean =
    if l = empty then false
    else
      if head(l) = n then true
      else
         Member(n,tail(l));

Note that, owing to the else clauses, each condition E_{i} in the body of a function is (operationally) equivalent to E_{i} ∧ ¬E_{i−1} ∧ ⋯ ∧ ¬E_{1}. Thus our choice of syntax automatically ensures that every function is deterministic and case-complete, so that for any sequence of appropriate inputs exactly one condition in the body of the function will be true.

Scripts

A script S is defined to be a finite sequence of definitions of data types and functions. Scripts are sequences because the idea is that they are developed incrementally, in stages: we usually start from scratch, with the empty script S_{0}; then we obtain a script S_{1} by defining the first data type T_{1}; then we extend S_{1} with a new definition, either of a second datatype T_{2} or of our first function f_{1}, thereby otaining a new script S_{2}; then on with a new definition, and so forth. Thus, a script is like a Scheme or ML environment built through the Read-Eval-Print loop. If S is a non-empty script comprising n datatypes T_{1}, …, T_{n} and m functions f_{1}, …, f_{m}, we will write

• CON_{S} for CON_{T_{1}} ∪⋯∪CON_{T_{n}} (and likewise for RCON_{S} and IRCON_{S}),

• SEL_{S} for SEL_{T_{1}} ∪ ⋯ ∪ SEL_{T_{n}},

• FUN_{S} for {f_{1}, …, f_{m}},

• Σ_{S} for CON_{S} ∪ SEL_{S} ∪ FUN_{S} (this is the signature of S), and

• TYPES_{S} for {T_{1}, …, T_{n}}.

Now suppose we are given a mapping V that assigns to each type T in TYPES_{S} a (possibly empty) set V(T) of “variables of type T ” which can be used to denote arbitrary objects of type T. We then define a term of type T, for any T ∈ TYPES_{S}, to be either a variable in V(T) or an expression of the form g(t_{1}, …, t_{k}), where g : T_{1} × ⋯ × T_{k} → T is a member of Σ_{S} and t_{1}, …, t_{k} are terms of types T_{1}, …, T_{k}, respectively. For example, if S contains NatNum, NatList, Minus and Member,

then Minus(n,succ(zero)) and Member(zero,add(succ(zero),empty))

are terms of types NatNum and NatList, respectively (assuming that n is a variable of type NatNum). A ground term is one that does not contain any variables. From the two foregoing examples only the second term is ground.

We will write T_{T} (Σ_{S}, V) for the set of all terms of type T, and T_{T} (Σ_{S}) for the set of all ground terms of type T. Furthermore, we will write T (Σ_{S}, V) for the set of all terms of type T, for any T ∈ TYPES_{S}; so, assuming that TYPES_{S} = {T_{1}, …, T_{n}}, T (Σ_{S}, V) = T_{T_{1}}(Σ_{S}, V) ∪ ⋯ ∪ T_{T_{n}}(Σ_{S}, V). Likewise, the expression T (Σ_{S}) will denote the set of all ground terms of any type. If we let V_{∅} stand for the mapping that assigns to each type the empty set of variables, then T (Σ_{S}) = T (Σ_{S}, V_{∅}).

Next, we define the syntax of boolean expressions over Σ_{S} and V as follows:

E ::= true | false | (s = t) | ¬E | (E ∧ E) | (E ∨ E)

for any s, t ∈ T_{T} (Σ_{S}, V), T ∈ TYPES_{S}. Expressions of the form ¬(s = t) are written as (s ≠ t). Finally, B(Σ_{S}, V) will designate the set of all boolean expressions over Σ_{S} and V.

When a script S is extended with a new datatype or function definition, we must check that certain syntactic conditions are satisfied. For a definition of a new datatype T we need to make sure that all the constructor and selector names are fresh (do not appear in any previous definitions), that there is at least one irreflexive constructor, and that each argument type of every constructor is either a previously defined datatype or T itself. For a definition of a new function f : T_{1} × ⋯ × T_{n} → T with parameters x_{1} : T_{1}, …, x_{n} : T_{n} and body [(E_{1}, r_{1}), …, (E_{m}, r_{m}), (true, r_{m+1})], we must ensure that (i) all parameters are distinct, (ii) T_{1}, …, T_{n}, T are all in TYPES_{S}, and (iii) for every j = 1, …, m + 1 we have r_{j} ∈ T_{T} (Σ_{S} ∪ {f}, V_{f}) and E_{j} ∈ B(Σ_{S} ∪ {f}, V_{f}), where V_{f} maps each T_{i}, i ∈ {1, …, n}, to the set of those parameters amongst x_{1}, …, x_{n} that are of type T_{i}, and every other type to ∅.

A definition that satisfies these constraints is called well-formed. A script is called well-formed if it is obtainable from the empty script through a series of well-formed definitions. Finally, a script is admissible if (a) it is well-formed, and (b) every user-defined function terminates for all apropriate inputs. Checking (a) is easy; (b) is the undecidable task, and is the subject of this paper.

2.2 Semantics

Let a well-formed script S be given. The interpreter Eval_{S} shown in Fig. 1 maps an arbitrary ground term in T (Σ_{S}) to an object in T (CON_{S}). The interpreter can be seen as an implementation of the operational semantics of IFL: the objects of S are considered to be in normal form, whereas a ground term t that contains function symbols from FUN_{S} specifies a computation and needs to be reduced to normal form. Eval_{S} performs this reduction by rewriting t in accordance with the definitions of the various functions in FUN_{S} and the conventions regarding constructors and selectors.

For any t ∈ T (Σ_{S}), we write Eval_{S}(t)↓ to indicate that Eval_{S} halts when started with t as input. We can now formally define a user-defined function f : T_{1} × ⋯ T_{n} → T to be terminating iff Eval_{S}(f(w_{1}, …, w_{n}))↓ for all objects w_{1} ∈ T_{1}, …, w_{n} ∈ T_{n}. As a convention, when S is implicitly understood or immaterial, we will simply write Eval instead of Eval_{S}.

6The expression E[w_{1}/x_{1}, …, w_{n}/x_{n}] is obtained from E by consistently replacing each occurence of x_{i} by w_{i}. For brevity, we will occasionally write this as E[w_{i}/x_{i}]. Note that the order in which the substitutions are performed is immaterial since the w_{i} are ground.

;; For a constant con ∈ CON_{S} :

Eval_{S} con = con | ;; For a non-constant con ∈ CON_{S} :

Eval_{S} con(t_{1}, …, t_{n}) = con(Eval_{S}(t_{1}), …, Eval_{S}(t_{n})) | ;; For a selector sel_{i}^{c} ∈ SEL_{S}, where Minimal(c,i) returns the ;; minimal object of the i^{th} argument type of c:

Eval_{S} sel_{i}^{c}(t) = case Eval_{S}(t) of

c(t_{1}, …, t_{n}) ==> t_{i} |

==> Minimal(c,i) |

;; For a user-defined function f ∈ FUN_{S} with n parameters x_{1}, …, x_{n} ;; and body [(E_{1}, r_{1}), …, (E_{m}, r_{m}), (true, r_{m+1})]:

Eval_{S} f(t_{1}, …, t_{n}) = let val (w_{1}, …, w_{n}) = (Eval_{S}(t_{1}),...,Eval_{S}(t_{n}))

      fun do if(E::tl bexps,r::tl terms) =

if T Eval_{S}(E[w_{1}/x_{1}, …, w_{n}/x_{n}])^{7} then

Eval_{S}(r[w_{1}/x_{1}, …, w_{n}/x_{n}])

          else
             do if(tl bexps,tl terms)   in

do if([E_{1}, …, E_{m}, true], [r_{1}, …, r_{m+1}]) end

and

T Eval_{S} (s = t) = (Eval_{S}(s) = Eval_{S}(t)) | T Eval_{S} (¬E) = not(T Eval_{S}(E)) | T Eval_{S} (E_{1} ∧ E_{2}) = T Eval_{S}(E_{1}) andalso T Eval_{S}(E_{2}) | T Eval_{S} (E_{1} ∨ E_{2}) = T Eval_{S}(E_{1}) orelse T Eval_{S}(E_{2});

Figure 1: An interpreter for IFL, written in ML-like notation.

3 Theoretical underpinnings

3.1 Object size

Every object has a certain size. How we “measure” that size depends on the type of the object. For example, for objects of type NatList a natural measure of size is the length of the list. Thus we say that the empty list has size 0, the list [3, 1] has size two, and so on. Or, if we agree to let SZ_{T} (w) denote the size of an object w of type T, we can write SZ_{NatList}(empty) = 0, SZ_{NatList}(add(zero, add(succ(zero), empty))) = 2, etc. More formally, we have

SZ_{NatList}(l) = \{ \begin{matrix}0 & if l ≡ empty \\ 1 + SZ_{NatList}(tail(l)) & if l ≡ add(⋯). \end{matrix}  (1)

In a similar spirit, we take the size of a BTree object to be the number of its nodes, so that

                        SZ_{BTree}(null) = 0,
        SZ_{BTree}(tree(s^{7}(0), tree(s^{5}(0), null, null), null)) = 2,

and so on. More precisely:

       SZ_{BTree}(t) = \{ \begin{matrix}0 & if t ≡ null \\ 1 + SZ_{BTree}(left(t)) + \\ SZ_{BTree}(right(t)) & if t ≡ node(· · ·). \end{matrix}  (2)

Each of the two size measures given above applies only to objects of its own particular type, but nevertheless they both use the same essential idea: if an object is built from an irreflexive constructor, let its size be zero (the first clauses of definitions 1—2); if it is built from a reflexive constructor, let its size be one more than the sum of the sizes of its components of the same type (tail clauses of 1—2). This simply reflects the intuition that the irreflexive constructors of a type T produce “simple” objects — primitive building blocks that have no internal structure as far as T is concerned. Hence their size should be zero. By contrast, a reflexive constructor of T takes n > 0 objects s_{1}, …, s_{n} and bundles them into a new “complex” object s. The T -size of s should therefore be one plus the sum of the T -sizes of the s_{i}, the “one plus” signifying that we have gone “one level higher” by applying the reflexive constructor in question, and the summing of the T -sizes of the s_{i} signifying that each s_{i} is now a part of s and thus contributes to the latter’s size. For instance, by joining together two BTrees l and r at a new root node of value v, we produce the more complex object tree(v,l,r), which, intuitively, is one unit larger than the sizes of l and r summed together.

We abstract the preceding observations into a general definition of size for objects of a type T as follows:

SZ_{T} (s) = \{ \begin{matrix}0 & if s ≢ rcons(⋯) \\ 1 + SZ_{T} (t_{i_{1}}) + ⋯ + SZ_{T} (t_{i_{m}}) & if s ≡ rcons(t_{1}, …, t_{n}) \end{matrix} (3)

for any rcons ∈ RCON_{S} with reflexive argument positions i_{1}, …, i_{m}. If the type at hand is implicitly understood or can be easily deduced from the context, we may drop the subscript and simply write SZ(s).

We distinguish between SZ(s) and the size of s as a Herbrand term, which we will denote by |s|. Viewing terms as trees, |s| is simply the number of nodes of s. E.g., for s = add(succ(zero), empty) we have |s| = 4, whereas SZ(s) = 1. In addition, |s| makes sense for any s ∈ T (Σ_{S}, V), including non-ground terms, while SZ is only defined for objects.

3.2 A size ordering and the GTZ predicate

Now let s, t ∈ T (Σ_{S}, V) be two terms of the same type T in some admissible script S, let E_{1}, …, E_{n} ∈ B(Σ_{S}, V), and let v_{1}, …, v_{k} be all and only the variables that occur in s or in t or in one of the E_{j}, where each v_{i} is of some type T_{i}. We will write {E_{1}, …, E_{n}} ⊧ s ⪯ t to indicate that for all objects w_{1} : T_{1}, …, w_{k} : T_{k} for which T Eval_{S}(E_{1}[w_{i}/v_{i}] ∧ ⋯ ∧ E_{n}[w_{i}/v_{i}]) = true, we have

SZ_{T} (Eval_{S}(s[w_{i}/v_{i}])) ≤ SZ_{T} (Eval_{S}(t[w_{i}/v_{i}])).  (4)

When there are no variables to be replaced (i.e. when s, t, and the E_{i} are ground), {E_{1}, …, E_{n}} ⊧ s ⪯ t simply means that if TEval(E_{1} ∧ ⋯ ∧ E_{n}) = true then SZ(Eval(s)) ≤ SZ(Eval(t)). When there are no boolean expressions we simply write s ⪯ t instead of ∅ ⊧ s ⪯ t. Thus the inequality s ⪯ t holds iff every ground instance of it holds. For example, we have Minus(n,m) ⪯ n because no matter what objects we substitute for n and m, the size of Minus(n,m) will always be less than or equal to the size of n.

We use similar notation for strict inequalities: {E_{1}, …, E_{n}} ⊧ s ≺ t iff (4) holds with < in place of ≤, and s ≺ t for ∅ ⊧ s ≺ t; e.g. l ≺ add(n,l). Finally, we write {E_{1}, …, E_{n}} ⊧ GTZ(s) to mean that for all objects w_{1} ∈ T_{1}, …, w_{k} ∈ T_{k}, if TEval(E_{1}[w_{i}/v_{i}] ∧ ⋯ ∧ E_{n}[w_{i}/v_{i}]) = true then SZ(Eval(s[w_{i}/v_{i}])) > 0. We will write GTZ(s) for ∅ ⊧ GTZ(s). Thus GTZ(s) iff the result of evaluating any ground instance of s has positive size. For instance, we have GTZ(succ(n)), but ¬GTZ(Minus(n,m)). For ground s, of course, we have GTZ(s) iff SZ(Eval(s)) > 0; e.g. we have GTZ(succ(zero)) since SZ(Eval(succ(zero))) = 1 > 0.

Note that if the top function symbol of s is a constructor then deciding GTZ(s) is trivial—simply check whether the constructor is reflexive. For we always have GTZ(rc(⋯)) and ¬GTZ(irc(⋯)) for every reflexive (irreflexive) constructor rc (irc). However, in general all three of the relations we have defined in this section (s ⪯ t, s ≺ t, and GTZ(s)) are undecidable because the terms s and t can involve variables, which may range over infinitely many objects. Consequently, in the absence of a fortuitous counter-example any complete procedure for deciding any of these conditions would have to perform infinitely many numerical comparisons, which is not possible in a finite amount of time. But if we restrict these problems to ground terms only, then they become decidable in virtue of the strong normalization guaranteed by the admissibility of S; we could then simply evaluate all the relevant ground terms and decide accordingly.

3.3 Argument-bounded functions

A key role in our method is played by argument-bounded functions. A function f : T_{1} × ⋯ × T_{n} ⟶ T is i-bounded for some i ∈ {1, …, n} if T_{i} = T and f(v_{1}, …, v_{n}) ⪯ v_{i} (for some variables v_{1} : T_{1}, …, v_{n} : T_{n}). Likewise, f is strictly i-bounded if the foregoing condition holds with ≺ in place of ⪯. We call f (strictly) argument-bounded (abbreviated “a.b.”) if it is (strictly) i-bounded in at least one i.^{8}

3.4 The termination theorem

In this paper we will only be concerned with termination of normal algorithms. In IFL, a function f is called normal if every conditional (E_{j}, r_{j}) in its body is such that (i) E_{j} contains no recursive calls f(⋯), and (ii) r_{j} contains no nested recursive calls f(⋯ f(⋯) ⋯). This is not a severe restriction since most function definitions encountered in practice meet these requirements. Non-normal functions such as McCarthy’s 91–function [8] or Takeuchi’s function for reversing a list [11], although mathematically interesting, tend to be of little practical relevance.

Following an idea introduced by Floyd [4], most methods for proving termination, including ours, are based on the concept of well-founded sets. Formally, a well-founded set is an ordered pair (W, R), where W is a set and R is a well-founded binary relation on W. Recall that R is well-founded iff every non-empty subset of W contains at least one R-minimal element; or, equivalently, iff there are no infinite seqences x_{1}, x_{2}, x_{3}, … such that x_{1} R x_{2}, x_{2} R x_{3}, x_{3} R x_{4}, …. If we read x R y as “x is larger than y”, in some abstract sense of “large”, then to say that R is well-founded is to say that no element of W can decrease indefinitely—the descent must eventually stop after finitely many steps. The classic example of a well-founded set is (N, >), the natural numbers under the “greater than” relation.

Our method is based on the following fundamental result:

Theorem 3.1 (Main termination theorem) Let S be an admissible script and let S′ be an extension of S obtained by defining a new normal function f : T_{1} × ⋯ × T_{n} → T with n parameters x_{1} : T_{1}, …, x_{n} : T_{n} and body [(E_{1}, r_{1}), …, (E_{m}, r_{m}), (true, r_{m+1})]. Then f is terminating in S′ iff there is a well-founded set (W, R) and a function Q : T_{1} × ⋯ × T_{n} → W such that for each recursive call f(t_{1}, …, t_{n}) in each r_{j}, j = 1, …, m+1, the following holds for any n objects w_{1} ∈ T_{1}, …, w_{n} ∈ T_{n}: if T Eval_{S}(E_{j}[w_{i}/x_{i}]) = true, then Q(w_{1}, …, w_{n}) R Q(Eval_{S}(t_{1}[w_{i}/x_{i}]), …, Eval_{S}(t_{n}[w_{i}/x_{i}])).

8McAllester and Arkoudas [9] use the (perhaps more suggestive) terms “conserver” and “reducer” for what we call an a.b. and strictly a.b. function, respectively.

A function Q that meets the above requirements is called a termination function for f. Note that the assumptions that f be normal and S be admissible are crucial, otherwise the defining property of Q as stated in the theorem would be nonsensical. As regards normalcy, if some t_{p} contained an additional recursive call f(t′_{1}, …, t′_{n}) then the expression Eval_{S}(t_{p}[w_{i}/x_{i}]) would be undefined because f ∉ Σ_{S} and thus we cannot use Eval_{S} to compute t_{p}[w_{i}/x_{i}]; and we would have the same problem if an E_{j} contained a recursive call to f: the value T Eval_{S}(E_{j}[w_{i}/x_{i}]) would then be ill-defined for the same reasons. But to be sure that these values are well-defined we also need to know that Eval_{S} and T Eval_{S} will halt, and this is the guarantee that the admissibility of S affords us.

The termination function Q should be seen as mapping each n–tuple of objects w_{1} ∈ T_{1}, …, w_{n} ∈ T_{n} to some “quantity” in W. In our method (W, R) will be (N, >), so the values of Q will be numeric. Furthermore, Q will be based on the size function SZ. In particular, we will have

Q(w_{1}, …, w_{n}) = ∑_{i ∈ MS_{f}} SZ(w_{i})  (5)

where MS_{f} is the so-called measured subset of f (in the terminology of Boyer and Moore [1]). This is the set of all argument positions i ∈ {1, …, n} such that for every recursive call f(t_{1}, …, t_{n}) in each r_{j}, j = 1, …, m + 1, we have {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ⪯ x_{i}.

The main idea, as explained in the next section, is to verify that each time a recursive call is made, the size of at least one argument in MS_{f} decreases. It is important to insist that size decrease must occur within the measured subset; merely requiring that the size of some argument should decrease with each recursion is not sufficient (let f(x,y:NatNum) = f(y,x) and consider any call f(a,b) with a ≠ b; every time a recursive call is made the size of at least one argument decreases, yet evaluation clearly diverges). The measured subset provides us with a top fringe of sorts over certain argument positions that can only move lower.

4 Method outline

Our method, in a nutshell, will be to attempt to prove that the function Q, as defined by (5), is indeed a termination function for f. Thus from the outset there are two potential sources of failure, even when we only consider normal functions:

1. Q may not in fact be a termination function for f.

2. Our method may fail to prove that Q is a termination function for f, even if it is. This is to be expected in view of the problem’s undecidability: there is no algorithm which will output “Yes” if and only if Q is a termination function for f.

Nevertheless, it turns out—as a matter of empirical fact—that Q is indeed a termination function for various commonly encountered f, so the first problem is not of dismal proportions. As regards the inevitable incompleteness, we again have to resort to an empirical argument: our method often turns out to be “complete enough” for practical purposes.

Of course if we had an oracle we could easily devise an algorithm for determining whether or not Q is is a termination function for f:

1. Compute MS_{f}: starting with MS_{f} = ∅, repeat for each i = 1, …, n:

2. Check whether {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ⪯ x_{i} for every

3. recursive call f(t_{1}, …, t_{n}) in each r_{j}, j = 1, …, m + 1. If yes,

4. set MS_{f} ← MS_{f} ∪ {i}.

5. If MS_{f} = ∅, halt with answer = “No”.

6. For every recursive call f(t_{1}, …, t_{n}) in each r_{j}, j = 1, …, m + 1, do:

7. If there is no i ∈ MS_{f} such that {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ≺ x_{i},

8. halt with answer = “No”.

9. Output answer = “Yes”.

It is not difficult to see that the above “algorithm” is both sound and complete. The oracle, of course, would be needed at lines 2 and 7, for deciding the two conditions {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ⪯ x_{i} and {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ≺ x_{i}, which are undecidable, as we have already discussed.

In the absence of oracles, we approximate. First, instead of dealing with an arbitrary boolean expression E_{i} in its full generality, we filter from it certain simple syntactic facts called size atoms, which we can put to good use, and ignore everything else. A size atom is either an equality of the form t = rc(⋯), for a reflexive constructor rc, or an inequality t ≠ irc(sel_{1}^{irc}(t), …, sel_{m}^{irc}(t)), for an irreflexive constructor irc of m arguments.

Size atoms can help us prove GTZ(⋯) assertions. E.g., from the atoms n = succ(m) and l ≠ empty we can immediately infer GTZ(n) and GTZ(l), respectively. The following is a simple algorithm that takes an E ∈ B(Σ_{S}, V) and extracts from it a set Ê of size atoms that are logically implied by E (to facilitate exposition, we assume that negation signs in E appear in front of equalities s = t only)^{9}:

ˆ (s = rc(t_{1}, …, t_{n})) = {(s = rc(t_{1}, …, t_{n}))}
ˆ (t ≠ irc(selirc_{1}(t), …, selirc_{m}(t))) = {(t ≠ irc(selirc_{1}(t), …, selirc_{m}(t)))}
ˆ (E_{1} ∧ E_{2}) = Ê_{1} ∪ Ê_{2}
ˆ (E_{1} ∨ E_{2}) = Ê_{1} ∩ Ê_{2}

while Ê = ∅ for every E that does not match any of the four above patterns. Clearly, E ⊧ Ê. Further, for any s, t ∈ T (Σ_{S}, V) and any set of size atoms {A_{1}, …, A_{k}} over Σ_{S} and V, we define a relation s ˆ⪯ t ≡ {A_{1}, …, A_{k}} (to be read “s is less than or equal to t modulo the size atoms A_{1}, …, A_{k}”) in a way that soundly approximates {A_{1}, …, A_{k}} ⊧ s ⪯ t. To wit,

s ˆ⪯ t ≡ {A_{1}, …, A_{k}} implies {A_{1}, …, A_{k}} ⊧ s ⪯ t.

In particular, when {A_{1}, …, A_{k}} = ∅ we have s ˆ⪯ t ⇒ s ⪯ t. The advantage of the ˆ⪯, ≡ relation, of course, is that it is decidable—and easily so. Given arbitrary s, t, and A_{1}, …, A_{k}, we can determine whether or not s ˆ⪯ t ≡ {A_{1}, …, A_{k}} in O(|s|) time. We then develop a similar approximation for the strict inequality problem, and finally we can do away with oracles: we simply use the earlier “algorithm” with s ˆ⪯ t ≡ Ê_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} in place of {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ t_{i} ⪯ x_{i}, and likewise for strict inequalitites.

5 The method

5.1 Proving termination

Recall that scripts are developed incrementally: at each step the user extends the current script by defining a new data type or a new function. An important part of our method consists of proving functions to be a.b., so at any given point let the set B_{i} ⊂ Σ_{S} comprise those functions in the current script S that have been proven to be i-bounded. Note that B_{1} will include

9Clearly, any Boolean expression can be transformed to this form by repeatedly applying DeMorgan’s laws to it.

t ˆ⪯ t [R1]  irc(s_{1}, …, s_{n}) ˆ⪯ t [R2] for every irc ∈ IRCON_{S}  g(s_{1}, …, s_{n}) ˆ⪯ t s_{i} ˆ⪯ t for every g ∈ B_{i} [R3] ĜTZ(t), s_{i_{1}} ˆ⪯ sel_{i_{1}}^{rc}(t), …, s_{i_{m}} ˆ⪯ sel_{i_{m}}^{rc}(t) rc(s_{1}, …, s_{n}) ˆ⪯ t  [R4] for every rc ∈ RCONS_{S} with reflexive argument positions i_{1}, …, i_{m} t = rc(s_{1}, …, s_{n}) ĜTZ(t) for every rc ∈ RCONS_{S}[R5] t ≠ irc_{1}(sel_{1}^{irc_{1}}(t), …, sel_{m_{1}}^{irc_{1}}(t)), …, t ≠ irc_{n}(sel_{1}^{irc_{n}}(t), …, sel_{m_{n}}^{irc_{n}}(t)) [R6] ĜTZ(t) where irc_{1}, …, irc_{n} are all the irreflexive constructors of T, for every T ∈ TYPES_{S}

Figure 2: Definition of the relation ˆ⪯ .

all the reflexive selectors in SEL_{S} by default, since all such selectors are 1bounded. The intended modus operandi is as follows. Immediately after the user has defined a new function f : T_{1} × ⋯ × T_{n} → T, the system tries to prove that f is terminating. If it fails, the definition is rejected and the user must either “try again” by providing an alternative definition (of the same mathematical object), or move on to another task. If f is proven to be terminating, then the next step is to attempt to determine whether it is i-bounded for every i = 1, …, k such that T_{i} = T. If we succeed in proving that f is i-bounded for such an i, we set B_{i} ← B_{i} ∪ {f}. Exactly how we go about deciding whether f is i-bounded is discussed in Sec. 5.2.

The rule schemas in Fig. 5.1 are intended to define two relations ˆ⪯ and ĜTZ on T (Σ_{S}, V), relative to a set of size atoms, that approximate ⪯ and GTZ, respectively. For the remainder of this section, fix a script S, sets B_{i} ⊆ Σ_{S}, and a map V on TYPES_{S}. We will write R_{S} for the logic program comprising all and only the S-specific instances of rules [R1]–[R6]. E.g., assuming that S contains NatNum and LamTerm, and that Minus ∈ B_{1}, R_{S} will contain, amongst others, the rules Minus(s_{1}, s_{2}) ˆ⪯ t ⇐ s_{1} ˆ⪯ t (an instance of [R3]), zero ˆ⪯ t ⇐ (instance of [R2]), and ĜTZ(t) ⇐ t ≠ var(index(t)) (instance of [R6]). The Herbrand universe of the program R_{S}, denoted HU(R_{S}, V) is defined as the set of all Herbrand terms that can be formed from the function symbols in Σ_{S} and the variables in the various V(T), where the latter as treated as constants.^{10} Thus HU(R_{S}, V) contains all the terms in T (Σ_{S}, V) as well as ill-typed but arity-respecting terms such as tail(zero). Note that we define the Herbrand universe of R_{S} not only with respect to the function symbols that appear in “the text” of R_{S}, but with respect to all the function symbols in Σ_{S} and the constants in the various V(T).

Now let {A_{1}, …, A_{n}} be a (possibly empty) set of size atoms over Σ_{S} and V, and let M be the least Herbrand model of the program R_{S} ∪{A_{1}, …, A_{n}}, with respect to HU(R_{S}, V). Then we define s ˆ⪯ t ≡ {A_{1}, …, A_{k}} to hold, for any s, t ∈ T (Σ_{S}, V), iff s ˆ⪯ t is true in M. By virtue of the completeness of SLD resolution, an equivalent, more operational definition, is to say that s ˆ⪯ t ≡ {A_{1}, …, A_{k}} if and only if there is a successful SLD-derivation of s ˆ⪯ t from the program R_{S}∪{A_{1}, …, A_{k}}, a condition which we shall express by writing R_{S} ∪ {A_{1}, …, A_{k}} ⊢ s ˆ⪯ t. The latter notation draws more attention to the particular algorithmic aspects of our method, and for this reason we will hereafter use it instead of s ˆ⪯ t ≡ {A_{1}, …, A_{k}}.

The following result shows that, procedurally, this rule system is very efficient:

Proposition 5.1 Consider the logic program R_{S} ∪ {A_{1}, …, A_{k}} and pick any rule for selecting goals from a query. The SLD-tree of any ground query of the form s ˆ⪯ t has O(|s|) nodes.

The restriction to ground queries is critical, as the presence of variables^{11} can easily lead to infinite derivations. For example, assuming that R_{S} has a clause f(s) ˆ⪯ t ⇐ s ˆ⪯ t for some f ∈ B_{1}, the query s ˆ⪯ t has an infinite SLD-tree. Of course for our purposes this is harmless since we are only interested in posing ground queries. We conclude:

10From the viewpoint of R_{S} the only variables are those that denote arbitrary terms in HU(R_{S}, V). (In a Prolog implementation, these would be represented by identifiers with an upper-case first letter; in our presentation, in Fig. 5.1, they are represented by the letters s and t). At the meta-level of the rules, the “object variables” in the various V(T)

are considered to be constants.

11Again, logic variables, not IFL variables.

Proposition 5.2 For any s, t ∈ T (Σ_{S}, V) and size atoms A_{1}, …, A_{k} over Σ_{S} and V, R_{S} ∪ {A_{1}, …, A_{k}} ⊢ s ˆ⪯ t can be decided in O(|s|) time.^{12}

Soundness is not difficult to show either.

Proposition 5.3 R_{S} ∪ Ê_{1} ∪ ⋯ ∪ Ê_{n} ⊢ s ˆ⪯ t implies {E_{1}, …, E_{n}} ⊧ s ⪯ t.

At this point we have a sound, efficient, and fairly powerful sustem for deducing statements of the form {E_{1}, …, E_{n}} ⊧ s ⪯ t. The following is a sample SLD-derivation proving {n ≠ zero} ⊧ succ(Minus(pred(n),m)) ⪯ n, assuming that Minus ∈ B_{1}:

            succ(Minus(pred(n),m)) ˆ⪯ n ⇐  [R4]
     ĜTZ(n), Minus(pred(n),m) ˆ⪯ pred(n) ⇐  [R6]
   n ≠ zero, Minus(pred(n),m) ˆ⪯ pred(n) ⇐  n ≠ zero
            Minus(pred(n),m) ˆ⪯ pred(n) ⇐  [R3]
                     pred(n) ˆ⪯ pred(n) ⇐  [R1]

□

A few additional rules are needed for inferring strict size inequalities. We single out four such rule schemas in Fig. 5.1. They should be selfexplanatory, with the exception of [R9], which is based on the important notion of a function being strictly i-bounded in a set of argument positions. The basic idea is that, oftentimes, whether or not an i-bounded function f returns an object of strictly smaller size than that of its i^{th} argument depends on whether some of its arguments have positive size. For example, the 1-bounded Minus is also strictly 1-bounded whenever both of its arguments are non-zero. In symbols, GTZ(n, m) ⊧ Minus(n,m) ≺ n, where we write GTZ(t_{1}, …, t_{k}) as an abbreviation for the conjunction GTZ(t_{1}), …, GTZ(t_{k}).

As another example, the selector tail (which is 1-bounded in virtue of being reflexive), is also strictly 1-bounded whenever its argument is a non-empty list, i.e. GTZ(l) ⊧ tail(l) ≺ l. In fact all reflexive selectors strictly reduce arguments of positive size. In general, for any i-bounded g of n arguments and any non-empty subset {a_{1}, …, a_{m}} ⊂ {1, …, n}, we say that g is strictly i-bounded in positions {a_{1}, …, a_{m}} iff g(s_{1}, …, s_{n}) ≺ s_{i} whenever GTZ(s_{a_{1}}, …, s_{a_{m}}). Thus all reflexive selectors are strictly 1bounded in {1}. In section 5.3 we will discuss in detail how we go about

12Counting resolution steps as the fundamental units of computation.

ĜTZ(t) irc(s_{1}, …, s_{n}) ˆ≺ t [R7] for every irc ∈ IRCON_{S}  s_{i} ˆ≺ t g(s_{1}, …, s_{n}) ˆ≺ t [R8] for every g ∈ B_{i} ĜTZ(s_{a_{1}}, …, s_{a_{m}}), s_{i} ˆ⪯ t g(s_{1}, …, s_{n}) ˆ≺ t  [R9] for every g ∈ B_{i} proven to be strictly i-bounded in {a_{1}, …, a_{m}} s_{i_{1}} ˆ≺ selrc_{i_{1}}(t), …, s_{i_{m}} ˆ≺ selrc_{i_{m}}(t) rc(s_{1}, …, s_{n}) ˆ≺ t  [R10] for every rc ∈ RCON_{S} with reflexive argument positions i_{1}, …, i_{m}.

Figure 3: Definition of the relation ˆ≺ .

proving a function to be strictly i–bounded in a set of argument positions; for now the definition alone will suffice. It should be said, however, that for every g ∈ B_{i} there will be at most one instance of [R9], a stipulation we choose to make in the interest of efficiency.^{13}

From now on R_{S} should be understood to comprise all S-specific instances of [R1]–[R10], and our definitions of HU(R_{S}, V) and M should be adjusted accordingly. Similarly to our definition of ˆ⪯, ≡, we define s ˆ≺ t ≡ {A_{1}, …, A_{k}} to mean that s ˆ≺ t is true in M, or equivalently, that

R_{S} ∪ {A_{1}, …, A_{k}} ⊢ s ˆ≺ t.  (6)

As regards complexity, Prop. 5.2 is not affected by the addition of the new rules since [R1]–[R6] are self-contained. By contrast, deciding (6) is slightly more expensive (in the worst case), mainly because both strict and weak goals may be generated in the course of a derivation, on account of [R9]. In particular, it can be proved that the SLD-tree of any ground query s ˆ≺ t with respect to the program R_{S} ∪ {A_{1}, …, A_{k}} has O(|s|^{2}) nodes.

Proposition 5.4 For any s, t ∈ T (Σ_{S}, V) and size atoms A_{1}, …, A_{k} over Σ_{S} and V, R_{S} ∪ {A_{1}, …, A_{k}} ⊢ s ˆ≺ t can be decided in O(|s|^{2}) time.

13In particular, Prop. 5.4 does hot hold without this provision.

With regard to soundness, the readers should have little trouble convincing themselves that an instance of [R7]–[R10] can never lead from a true antecedent to a false conclusion.

At this point most of the pieces of our method have fallen into place: to verify that a new function f is terminating, follow the algorithm given in page 15, with R_{S} ∪ {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊢ t_{i} ˆ⪯ x_{i} in place of {E_{j}, ¬E_{j−1}, …, ¬E_{1}}⊧ t_{i} ⪯ x_{i}, and likewise for the strict inequality test. Two things remain to be explained: how we prove that a function is i-bounded, and how we prove that a function is strictly i-bounded in a certain subset of its argument positions. These are respectively discussed in the next two sections.

We end this section with a simple illustration, a termination proof for the function Member defined in Sec. 2.1. First we need to approximate the measured subset of Member, and we begin by checking i = 1, the first argument position. There is only one recursive call in the body of the function, in r_{3}, and after computing Ê_{3} = ∅, ˆ¬E_{2} = ∅, ˆ¬E_{1} = {l ≠ empty}, we easily determine R_{S} ∪ {l ≠ empty} ⊢ n ˆ⪯ n (through [R1]), thus concluding that 1 ∈ MS_{Member}. Similarly, for i = 2, we readily determine that R_{S} ∪ {l ≠ empty} ⊢ tail(l) ˆ⪯ l (through [R3]). We infer that both argument positions are in the measured subset. Next, we need to verify that each time a recursive call is made, the size of at least one argument in the measured subset decreases. There is only one recursive call to consider. We begin by checking whether the first argument in the measured subset strictly goes down, but we find that R_{S} ∪{l ≠ empty} ⊬ n ˆ≺ n, so our hopes shift to the second (and last) element of the measured subset. Here we successfully find that R_{S} ∪{l ≠ empty} ⊢ tail(l) ˆ≺ l (by [R9] and [R6]), and hence we conclude that Member is terminating. It is easy to see that this derivation is an instance of a more general proof schema, based on combinations of [R9] and [R6], that works for any primitive recursive definition. Such definitions are recognized by the system very efficiently.

5.2 Proving that a function is argument-bounded

Once a newly defined function f : T_{1} × ⋯ × T_{n} → T has been proven terminating, the next order of business is to attempt to prove that f is i-bounded for every i ∈ {1, …, n} for which T_{i} = T. If we succeed in proving this for such an i, we set B_{i} ← B_{i} ∪ {f}.

Our method will take advantage of the fact that we already know f to be terminating. We will essentially try to prove that f(t_{1}, …, t_{n}) ⪯ t_{i} by induction on the running time of the call f(t_{1}, …, t_{n}); since f is total, the said time must be finite. We do this by showing, with the aid of the appropriate inductive hypotheses, that {E_{j}, ¬E_{j−1}, …, ¬E_{1}} ⊧ r_{j} ⪯ x_{i} for each j = 1, …, m + 1. In particular, for each such j, let r_{j} contain a recursive call f(s_{1}, …, s_{n}). By the inductive hypothesis, we know that f(s_{1}, …, s_{n}) ⪯ s_{i}, which can be cast in a way that incorporates transitivity as

f(s_{1}, …, s_{n}) ⪯ t ⇐ s_{i} ⪯ t [Ind].

We then compute R_{S} ∪ Ê_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} ∪ {[Ind]} ⊢ r_{j} ˆ⪯ x_{i} (i). If the verdict is negative we halt with a “No” answer (which is what makes the method incomplete, as f may in fact be i-bounded), otherwise we continue with j + 1. If (i) goes through for every j = 1, …, m + 1, we conclude that f is i-bounded, a clearly sound conclusion. Note that if an r_{j} contains multiple recursive calls f(s_{1}^{1}, …, s_{n}^{1}), …, f(s_{1}^{k}, …, s_{n}^{k}), we postulate an inductive hypothesis f(s_{1}^{p}, …, s_{n}^{p}) ⪯ t ⇐ s_{i}^{p} ⪯ t [Ind_{p}] for each one of them, p = 1, …, k; i.e., we compute

R_{S} ∪ Ê_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} ∪ {[Ind]_{1}, …, [Ind]_{k}} ⊢ r_{j} ˆ⪯ x_{i}.

To illustrate, we show how this algorithm would prove that Minus is 1-bounded. For j = 1 there are no recursive calls in r_{1} ≡ m, and hence no inductive hypotheses to be posited; we simply need to verify that R_{S} ∪ {n = zero} ⊢ m ˆ⪯ m, which is trivial (by [R1]). The next statement, j = 2, contains the recursive call Minus(pred(m),pred(n)), so let [Ind] be the clause representing our inductive hypothesis for this recursive call:

            Minus(pred(m),pred(n)) ˆ⪯ t ⇐ pred(m) ˆ⪯ t.

We now have to check whether

      R_{S} ∪ {n ≠ zero} ∪ {[Ind]} ⊢ Minus(pred(m),pred(n)) ˆ⪯ m.

The goal Minus(pred(m),pred(n)) ˆ⪯ m unifies with the head of [Ind] under the binding t ↦ m, thereby yielding the subgoal pred(m) ˆ⪯ m, which follows easily from [R3]. Thus we conclude that Minus is 1-bounded.

5.3 Deriving strict inequality lemmas

After a function f : T_{1} × ⋯ × T_{n} → T has been proven to be i-bounded for some i, the next step is to try to obtain a strict inequality lemma of the form [R9]. The idea is to iterate through the power-set of {1, …, n}, trying, for each subset {a_{1}, …, a_{m}} ⊂ {1, …, n}, to prove that

GTZ(x_{a_{1}}, …, x_{a_{m}}) ⊧ f(x_{1}, …, x_{n}) ≺ x_{i}.  (7)

The subsets of {1, …, n} are visited in order of increasing cardinality. We stop when we find the first subset {a_{1}, …, a_{m}} that satisfies (7) or when there are no more subsets to consider, whichever occurs first. In the former case we add to R_{S} the following instance of [R9]: f(s_{1}, …, s_{n}) ˆ≺ t ⇐ ĜTZ(s_{a_{1}}, …, s_{a_{m}}), s_{i} ˆ⪯ t, a slightly more general formulation of (7) incorporating transitivity. Thus R_{S} will contain at most one instance of [R9] for every g ∈ B_{i}. The fact that this algorithm is exponential in the number of arguments of f is inconsequential since in practice that number ranges from 1 or 2 in most cases to 5 or 6 in rare instances.

Now (7) would certainly follow if we verified that

R_{S} ∪ ĜTZ(x_{a_{1}}, …, x_{a_{m}}) ∪ Ê_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} ⊢ r_{j} ˆ≺ x_{i}  (8)

for every j = 1, …, m+1. But we would be doing more work than necessary that way. We can cut corners by completely ignoring those branches (E_{j}, r_{j}) that are inconsistent with the antecedent GTZ(x_{a_{1}}, …, x_{a_{m}}), in the sense that if E_{j} holds then GTZ(x_{a_{1}}, …, x_{a_{m}}) could not possibly be true. Thus, we check (8) only for those j for which Con(E_{j} ∧ ¬E_{j−1} ∧ ⋯ ∧ ¬E_{1}, {x_{a_{1}}, …, x_{a_{m}}}) = true, where Con is the algorithm below that takes an E ∈ B(Σ_{S}, V) and a set of terms {t_{1}, …, t_{k}}, t_{i} ∈ T (Σ_{S}, V), and returns false only when E logically implies ¬GTZ(t_{i}) for some i ∈ {1, …, k}:

Con (t_{i} = irc(⋯)) {t_{1}, …, t_{k}} = false |

Con (E_{1} ∧ E_{2}) T = Con(E_{1}, T) andalso Con(E_{2}, T) | Con (E_{1} ∨ E_{2}) T = Con(E_{1}, T) orelse Con(E_{2}, T) | Con = true;

This is a conservative approximation. If Con(E, {t_{1}, …, t_{k}}) returns false then we can be sure that E ⊧ ¬GTZ(t_{i}) for some i ∈ {1, …, k}, but if the result is true then we may still have E ⊧ ¬GTZ(t_{i}). For our purposes this is acceptable; it simply means that we will attempt to verify (8) even though this is not necessary in proving (7).

We can also take advantage of the fact that f is known to terminate and form appropriate inductive hypotheses, as we do when proving i-boundedness. In particular, when trying to prove r_{j} ˆ≺ x_{i} for some r_{j} containing k > 0 recursive calls f(s_{1}^{1}, …, s_{n}^{1}), …, f(s_{1}^{k}, …, s_{n}^{k}), we can assume k inductive hypotheses f(s_{1}^{p}, …, s_{n}^{p}) ˆ≺ t ⇐ ĜTZ(s_{a_{1}}^{p}, …, s_{a_{m}}^{p}), s_{i} ˆ⪯ t [Ind_{p}], one for each recursive call, p = 1, …, k. Accordingly, instead of (8) we attempt to verify the stronger

R_{S} ∪ {ĜTZ(x_{a_{1}}, …, x_{a_{m}}), [Ind_{1}], …, [Ind_{k}]}
∪ Ê_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} ⊢ r_{j} ˆ≺ x_{i}.

If the above goes through for every j for which E_{j} ∧ ¬E_{j−1} ∧ ¬E_{j} ∧ ⋯ ∧ ¬E_{1} is consistent with GTZ(x_{a_{1}}, …, x_{a_{m}}), we conclude that f is strictly i-bounded in positions {a_{1}, …, a_{m}}.

We again illustrate on Minus. Assuming we already have Minus ∈ B_{1}, we begin our traversal of the power-set of {1, 2} by considering {1}, trying to derive the lemma Minus(s_{1}, s_{2}) ˆ≺ t ⇐ ĜTZ(s_{1}), s_{1} ˆ⪯ t. Since this does not in fact hold, it is not derivable. We then consider {2}, which fails for similar reasons. Finally we come to check {1, 2}. We find Con(n = zero, {n, m}) = false, thus we only need to consider the second statement, for which we need to verify that

  R_{S} ∪ {ĜTZ(n, m), [Ind], m ≠ zero} ⊢ Minus(pred(n),pred(m)) ˆ≺ n (9)

where [Ind] is the inductive clause

 Minus(pred(n),pred(m)) ˆ≺ t ⇐ ĜTZ(pred(n), pred(m)), pred(n) ˆ⪯ t.

This does not help us here, but since Minus ∈ B_{1}, R_{S} contains the clause Minus(s_{1}, s_{2}) ˆ≺ t ⇐ s_{1} ˆ≺ t (as an instance of [R8]), whose head unifies with our goal in (9) with the bindings s_{1} ↦ pred(n), s_{2} ↦ pred(m), t ↦ n, backchaining to pred(n) ˆ≺ n, which follows immediately from [R9] via ĜTZ(n) and [R1]. We thus conclude that Minus is strictly 1-bounded in {1, 2} and augment R_{S} with the appropriate instance of [R9].

6 Examples and improvements

We demonstrate the method on some functions that are well-known not to have natural primitive recursive definitions. One of them is Euclid’s algorithm, which in IFL can be expressed as follows:

    function Gcd(n,m:NatNum):NatNum =
    if n = zero ∨ m = zero then Max(n,m)
    else
      if Leq(n,m) = true then Gcd(n,Minus(m,n))
      else
          Gcd(Minus(n,m),m);

Because Minus ∈ B_{1}, we are able to correctly identify the measured subset of Gcd as {1, 2}: For the first position, we have R_{S} ∪ A ⊢ n ˆ⪯ n for the first recursion, and R_{S} ∪A ⊢ Minus(n,m) ˆ⪯ n for the second one, where A is the set of size atoms {n ≠ zero, m ≠ zero}. We then find that in the first recursive call the size of the second argument strictly decreases (specifically, R_{S} ∪ A ⊢ Minus(m,n) ˆ≺ m, by [R9] and [R5]), while in the second recursion it is the first argument that strictly decreases (R_{S} ∪ A ⊢ Minus(n,m) ˆ≺ n, again by [R9] and [R5]).

Next we consider QuickSort, whose implementation uses the auxilliary functions GetSmaller(n,l), which returns a copy of l containing only those numbers that are ≤ n, and GetLarger(n,l), which does the opposite:

    function GetSmaller(n:NatNum,l:NatList):NatList =
    if l = empty then empty
    else
      if Greater(head(l),n) = true then GetSmaller(n,tail(l))
      else
          add(head(l),GetSmaller(n,tail(l)));

This is a primitive recursive definition, so we readily find the measured subset to comprise both argument positions, with the second argument strictly decreasing with each recursive call: R_{S} ∪ {l ≠ empty} ⊢ tail(l) ˆ≺ l (by virtue of [R9] and [R6], as with all primitive recursions). The termination of GetLarger is similarly established. The system will also successfully deduce that the two functions are 2-bounded, augmenting R_{S} with the following instances of [R3] and [R8]:

GetSmaller(s_{1}, s_{2}) ˆ⪯ t ⇐ s_{2} ˆ⪯ t
GetSmaller(s_{1}, s_{2}) ˆ≺ t ⇐ s_{2} ˆ≺ t

With the aid of these lemmas the termination of QuickSort below is easily verified:

  function QuickSort(l:NatList):NatList =
  if l = empty then empty
  else
    Append(QuickSort(GetSmaller(head(l),tail(l))),
         add(head(l),QuickSort(GetLarger(head(l),tail(l)))));

In practice the existing implementation of the method incorporates a few minor enhancements which increase the verification power of the system without significantly affecting its complexity. One of them can be illustrated via the MergeSort function below:

  function MergeSort(l:NatList):NatList =
  if l = empty then empty
  else
    if tail(l) = empty then l
    else
       Merge(MergeSort(RemoveOdd(l)),MergeSort(RemoveEven(l)));

where RemoveOdd(l) returns a copy of l with all elements of l in odd positions removed:

    function RemoveOdd(l:NatList):NatList =
    if l = empty ∨ tail(l) = empty then empty
    else
      add(head(tail(l)),RemoveOdd(tail(tail(l))));

and

    function RemoveEven(l:NatList):NatList =
    if l = empty then empty
    else
      if tail(l) = empty then l
      else
          add(head(l),RemoveEven(tail(tail(l))));

In Sec. 5.3 we pointed out that, oftentimes, whether or not an i-bounded function f decreases the size of its i^{th} argument depends on whether some of its arguments have positive size. A more general version of this claim is in fact true. Consider a unary a.b. function f for simplicity. Whether or not f(w) ≺ w often depends not merely on whether GTZ(w) but rather on whether GTZ(sel(w)) or GTZ(sel(sel(w))), etc., for some selector sel of the appropriate type. This is the case with RemoveEven, for example; RemoveEven(l) ≺ l does not follow from GTZ(l) (all one-element lists are counter-examples), but it does follow from GTZ(tail(l)). As another example, a halving function Half(n) would decrease n only if n > 1; thus Half(n) ≺ n would be entailed by GTZ(pred(n)) but not by GTZ(n).

These cases arise in programming naturally, and to account for them the algorithm given in Sec. 5.3 iterates through the power-set of {x_{1}, …, x_{n}}∪Δ rather than just {x_{1}, …, x_{n}}, where Δ is the set of all terms s such that s ≠ irc(⋯) or s = rc(⋯) is a size atom in the body of f. Thus in the case of RemoveEven we would iterate through {l, tail(l)} rather than just {l}. As before, for every visited subset X, we examine every (E_{j}, r_{j}) for which Con(E_{j}, X) = true, and we try to derive r_{j} ˆ≺ x_{i} from R_{S}, GTZ(X), and the appropriate inductive hypotheses. If we succeed in this for every “consistent” (E_{j}, r_{j}), we augment R_{S} with the appropriate clause. For RemoveEven that would be RemoveEven(s) ˆ≺ t ⇐ ĜTZ(tail(s)), s ˆ⪯ t. This lemma is in fact the key ingredient in the termination proof for MergeSort.

7 Where the method fails

There are three main factors that can prevent the method from recognizing a terminating function f. We discuss each below, in order of increasing importance.

Firstly, f may not be normal. This would not pose a serious problem in practice, as non-normal algorithms are not common.

Secondly, the size measure (5) may not be a termination function for f, either because MS_{f} = ∅ or because it is not the case that the size of some argument in MS_{f} strictly decreases with each recursive call. For instance, the size decrease could be erratic (consider a zig-zag pattern where with each recursion one argument increases by one and the other decreases by two, alternately), or there may be no size decrease at all—the arguments may in fact increase. Consider, for instance, a function f(n) which halts for n ≥ 1000 and recurses on n + 1 for n < 1000. A slightly more realistic example given by Walther [13] is an implementation of Minus(n,m) which returns zero if n ≤ m and succ(Minus(n,succ(m))) otherwise. Here it is the difference between n and m that strictly decreases with each recursion, not the size of any arguments. Such scenarios are not very frequent, however, so this case need not be a serious cause of concern either.

Thirdly, (5) may be a termination function but our method may not be able to prove it. This would be the most frequent cause of failure. There are several places where incompleteness creeps in. To take a simple example, the method relies heavily on scanning boolean expressions in search of size atoms of the form s ≠ irc(⋯) and s = rc(⋯), in order to conclude GTZ(s). If a boolean expression conveys this fact not through a size atom but through some other expression that logically implies it, our method will falter. Consider, for example, an implementation of Plus(n,m) which retuns succ(Plus(n,pred(m))) if m > zero and n otherwise. To verify that the argument pred(m) strictly decreases, our method will be looking verbatim for an atom such as m ≠ zero; it is not smart enough to deduce that m > zero in fact implies m ≠ zero.

Another serious source of incompleteness stems from failing to recognize that a function g is a.b. If that function is later used in a recursive call f(g(x)), we will not be able to verify that f terminates. But even if we prove that g is a.b., we may still fail to derive any strictness lemmas (in the manner of Sec. 5.3) that we might later need for verifying that the size of g(n) is actually smaller than that of n. This is by far the most serious pitfall. In general, proving that g is a.b. is not enough. We must obtain strictness conditions, i.e., conditions which are sufficient to guarantee that g will decrease its argument. Now the only type of strictness conditions our method considers^{14} are GTZ(x) (or GTZ({x_{a_{1}}, …, x_{a_{m}}}) in general, when g has multiple arguments). There are two problems here:

• These strictness conditions are very simple and although they often turn out to be sufficient in practice, there are cases in which they are not, i.e., cases in which it is not true that g(x) will decrease x whenever GTZ(x).

• And even if these conditions are in fact sufficient, our method may not be able to verify this, i.e., the algorithm we give in Sec. 5.3 may fail.

8 Possible future extensions

Extensions are possible in two different directions: in the language and in the method’s power. We briefly discuss each possibility.

8.1 Extending the language

The language in this paper is quite rudimentary. If the method is to have any practical value outside of laconic theorem provers,^{15} it must be made usable in the more realistic context of a modern language with rich features such as polymorphism, high-order functions, mutual recursion, pattern-matching, and state. We briefly speculate on how the method would interact with each of these features:

Polymorphism

This should be a straightforward addition. The method is based on recognizing irreflexive constructors, reflexive selectors, and a.b. functions, and neither of these is affected by the presence of type variables. From the method’s viewpoint the polymorphic datatype

    datatype 'a List = empty | add(head:'a,tail:'a List);

is identical to the monomorphic datatype NatList of Sec. 2.1. All that matters is that the constructor empty is irreflexive while add is reflexive in the second argument position. According to definition (3), whether a list is made of numbers, strings, or other lists is irrelevant to its size. For these reasons, the termination proof for, say, the function Member in Sec. 2.1, would carry over verbatim to a polymorphic version of the function.

14Our method will also automatically instantiate [R8] immediately after g has been proven a.b., which is a type of strictness condition (one that we can take for granted in virtue of the transitivity of ≺), but experience shows that [R8] is not as useful as [R9].

15Perhaps by a compiler that needs a guarantee that certain functions terminate.

High-order functions

Since our method is based on size and there appears to be no natural way of designating any finite quantity as the size of a function, the method could simply ignore those argument positions receiving functions as arguments. This is a perfectly reasonable strategy. In high-order languages such as Scheme or ML, termination usually follows because some finite measure (often the size) of non-functional arguments strictly decreases with each recursive call; functional arguments rarely play a role in this—consider the functionals map and foldr, for instance.

Mutual recursion

Mutual recursion does not pose a serious challenge either. One straightforward way of handling it is to unfold the recursion chain. Suppose, for example, that we extended IFL with a simple and construct like that of ML for defining mutually recursive functions:

    function Even(n:NatNum):Boolean =
    if n = zero then true
    else
       Odd(pred(n))
    and
    function Odd(m:NatNum):Boolean =
    if m = zero then false
    else
       Even(pred(m));

To verify the termination of Even, we replace all calls Odd(s) in its body with B[s/m] where B is the body of Odd and m its parameter.^{16} In this case we would obtain:

    function Even(n:NatNum):Boolean =
    if n = zero then true
    else
      if pred(n) = zero then false
      else

16We may have to rename B first to avoid variable captures.

          Even(pred(pred(n)));

whose termination is easily verified by our method.

Pattern matching

This is also unproblematic. Pattern-matching is merely a convenience for the programmer that (greatly) enhances readability; it is easily desugared into the type of notation we have been using. E.g. a clause such as

Append add(x,xs) y = add(x,Append(xs,y)) becomes
       if l ≠ empty then add(head(l),Append(tail(l),y)),

where l stands for the previously anonymous argument add(x,xs). Alternatively, instead of desugaring we can tailor the method to directly support definitions by pattern matching. This simply requires us to identify those variables in a pattern p that appear in a reflexive constructor position; whenever we subsequently encounter such a variable as an argument to a recursive call inside the scope of p, we treat it as an application of a reflexive selector. Note that extracting size atoms in order to derive GTZ(s) assertions is no longer necessary under pattern-matching, as that information is already handed to us for free.

State

This is by far the most troublesome feature. Suppose we had references (cells), for instance. One may be inclined to regard the “size” of a cell as the size of whatever object is stored therein. This would seem to allow us to prove the termination of functions that recursively call themselves with cells containing smaller and smaller objects. But side effects

rear their ugly head: function f(n:Cell-Of NatNum):NatNum = if !n =
0 then 0 else (n := !n + 1; f(cell(!n - 1))).^{17} A naive extension

of our method will conclude that f terminates, even though it clearly gets into an infinite loop whenever !n is positive. Therefore, it seems wiser to simply ignore reference arguments, just as we suggested for functions. Algorithms that perform course-of-values recursion on cell contents, after all, are not common; algorithms that terminate on account of such recursion are even less common. Of course in the presence of unrestricted destructive assignment (e.g. Scheme’s set!) the above perils are unavoidable and soundness can no longer be guaranteed. Even in those languages, however, the method may be employed beneficially if assignment is used in a disciplined manner.

17Where ! and := are the dereferencing and assignment operators, respectively, and (E_{1}; ⋯; E_{n}) is a sequencing form

8.2 Increasing the deductive power

There are several ways to make the inference engine more sophisticated. The present method could be the starting point for proving termination. In case of failure, we could try another approach from a certain fixed “bag” of techniques. One such technique can be based on the lexicographic extension of ≺ to finite sequences of terms:

[s_{1}, s_{2}, …, s_{n}] ≺ [t_{1}, t_{2}, …, t_{n}] ⇔ (s_{1} ≺ t_{1}) ∨ (s_{1} ⪯ t_{1} ∧ s_{2} ≺ t_{2}) ∨ · · · .

We could then try to verify

R_{S} ∪ E_{j} ∪ ˆ ¬E_{j−1} ∪ ⋯ ∪ ˆ¬E_{1} ⊢ [t_{1}, …, t_{n}] ˆ≺ [x_{1}, …, x_{n}]

for every recursive call f(t_{1}, …, t_{n}), j = 1, …, m + 1. Note that this would allow us to recognize non-normal algorithms. We can easily verify the termination of Ackerman’s function, for example, with this particular method.

Other possibilities include the incorporation of standard techniques for proving termination of rewrite systems [2, 12, 6, 3], working with measures other than size, and enriching the existing rule system with additional clauses. Clearly, however, after a certain point the power of the system becomes inversely proportional to its efficiency.

Acknowldegements

The author gratefully acknowledges David McAllester’s valuable input and contributions to the ideas in this paper, as well as much helpful feedback by Olin Shivers. Any remaining errors, of course, are solely the fault of Dr. Shivers.

References

[1] R. S. Boyer and J. S. Moore, A Computational Logic, Academic Press, New York, 1979.

[2] Nachum Dershowitz and Z. Manna, Proving termination with multiset orderings, Commun. ACM 22, 1979, 465-476.

[3] N. Dershowitz, Termination of Rewriting, J. Symbolic Computation (1987), 3, 69-116.

[4] R. W. Floyd, Assigning meanings to programs, in Mathematical Aspects of Computer Science, Proceedings Symposia in Applied Mathematics 19, (American Mathematical Society, Providence RI, 1967) 19–32.

[5] K. Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12, 1958, 280-287. English translation in: On a hitherto unexplored extension of the finitary standpoint, J. Philos. Logic 9, 1980.

[6] J. V. Guttag, D. Kapur, D. R. Musser, On proving uniform termination and restricted termination of rewriting systems, SIAM J. Comput. 12, 1983, 189-214.

[7] Z. Manna, Termination of Algorithms, Ph.D Thesis, Computer Science Department, Carnegie–Mellon University, Pittsburgh, PA 1968.

[8] Z. Manna, Mathematical Theory of Computation, McGraw Hill, New York, 1974.

[9] D. McAllester and K. Arkoudas, Walther recursion, CADE 13, 1996.

[10] B. Nordström, K. Peterson, and J. Smith, Programming in Martin-Lof’s type theory, International series of monographs on Computer Science, 7, Oxford Science Publications, 1990.

[11] J. S. Moore, A mechanical proof of the termination of Takeuchi’s function, Inf. Process. Let. 9 (4), 1979, 176-181.

[12] A. Pettorossi, Comparing and putting together recursive path orderings, simplification orderings and non-ascending property for termination proofs of term rewriting systems, Proceedings of the Eighth EATCS International Colloquium on Automata, Languages and Programming, Acre, Israel, Springer Lec. Notes Comp. Sc. 115, 1981, 432-447.

[13] C. Walther, On proving the termination of algorithms by machine, Artificial Intelligence, 71, 1994, 101-157.