Inference of termination conditions for numerical loops in Prolog.
We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these difficulties. Our approach is based on transforming a program in a way that allows integrating and extending techniques originally developed for analysis of numerical computations in the framework of query-mapping pairs with the well-known framework of acceptability. Such an integration not only contributes to the understanding of termination behaviour of numerical computations, but also allows us to perform a correct analysis of such computations automatically, by extending previous work on a constraint-based approach to termination. Finally, we discuss possible extensions of the technique, including incorporating general term orderings.
Introduction
Numerical computations form an essential part of almost any real-world
program. Clearly, in order for a termination analyser to be of practical use
it should contain a mechanism for inferring termination of such compu-
tations. However, this topic attracted less attention of the research com-
munity. In this work we concentrate on automatic termination inference
for logic programs depending on numerical computations. Dershowitz et
al. [8] showed that termination of general numerical computations, for
instance on floating point numbers, may be counter-intuitive, i.e., the
observed behaviour does not necessarily coincide with the theoretically
expected one. Thus, we restrict ourselves to integer computations only.
While discussing termination of integer computations the following
question should be asked: what conditions on the queries should be as-
sumed, such that the queries will terminate. We refer to this question as
the termination inference problem.
Example 1. p(X) / X ! 7; X1 is X+1; p(X1): This program terminates
for queries p(X), for all integer values of X. Thus, the answer for the
termination inference problem is the condition "true". 2
This example also hints at why the traditional approaches to termination
analysis fail to prove termination of this example. These approaches
are mostly based on the notion of level mapping, that is, a function from
the set of all possible atoms to the natural numbers, which should decrease
while traversing the rules. In our case, such a level mapping should
depend on X, but X can be negative as well!
Two approaches for solving this problem are possible. First, one can
change the definition of the level mapping to map atoms to integers. How-
ever, integers are, in general, not well-founded. To prove termination one
? supported by GOA: generation logic programming language".
should prove that the mapping is to some well-founded subset of integers.
In the example above (\Gamma1; 7) forms such a subset with an ordering -,
such that x - y if x ! y, with respect to the usual ordering on integers.
The second approach that we present in the paper does not require
changing the definition of level mapping. Indeed, the level mapping as
required exists. It maps p(X) to 7 and to 0 otherwise. This
level mapping decreases while traversing the rule, i.e., the size of p(X),
greater than the size of p(X1), 6 \Gamma X, thus, proving termination.
We present a transformation that allows us to define such a level mappings
in an automatic way by incorporating techniques of [8], such as level
mapping inference, in the well-known framework of the acceptability with
respect to a set [5, 6]. This integration provides not only a better understanding
of termination behaviour of integer computations, but also the
possibility to perform the analysis automatically as in Decorte et al. [7].
The rest of the paper is organised as follows. After making some preliminary
remarks, we present in Section 3 our transformation-first by
means of an example, then more formally. In Section 4 we discuss more
practical issues and present the algorithm implementing the termination
In Section 5 we discuss further extensions, such as proving termination
of programs depending in numerical computations as well as
ones. Then we review related work and conclude.
Preliminaries
We follow the standard notation for terms and atoms. A query is a finite
sequence of atoms. Given an atom A, rel(A) denotes the predicate
occuring in A. Atom P denotes a set of all atoms that can be constructed
from the language underlying P . The extended base
P is a quotient set
of Atom P modulo the variant relation. An SLD-tree constructed using
the left-to-right selection rule of Prolog is called an LD-tree. A goal G
LD-terminates for a program P , if the LD-tree for (P; G) is finite.
Definition 1. [1] Let P be a program and p, q be predicates occuring in
it. We say that p refers to q in P if there is a clause in P that uses p in
its head and q in its body; that p depends on q in P and write p w q, if
(p; q) is in the transitive, reflexive closure of the relation refers to; and
that p and q are mutually recursive and write p ' q, if p w q and q w p.
We recall some basic notions, related to termination analysis. A level
mapping is a function j
is the set of the naturals.
We study termination of programs with respect to sets of queries. The
following notion is one of the most basic notions in this framework.
Definition 2. [6] Let P be a definite program and S be a set of atomic
queries. The call set, Call(P; S), is the set of all atoms A, such that a
variant of A is a selected atom in some derivation for P [ f/ Qg, for
some Q 2 S and under the left-to-right selection rule.
The following definition [14] generalises the notion of acceptability
with respect to a set [5, 6] by extending it to mutual recursion.
Definition 3. Let S be a set of atomic queries and P a definite program.
P is acceptable with respect to S if there exists a level mapping j \Delta j such
that for any A 2 Call(P; S), for any A 0 in P , such that
c.a.s. oe for / (B holds that j A j
De Schreye et al. [5] characterise LD-termination in terms of acceptability.
Theorem 1. (cf. [5]) Let P be a program. P is acceptable with respect
to a set S if and only if P is LD-terminating for all queries in S.
We also need to introduce the notion of interargument relations.
Definition 4. [7] Let P be a definite program, p=n a predicate in P . An
interargument relation for p=n is R p ' N n . R p is a valid interargument
relation for p=n with respect to a norm k \Delta k if and only if for every
To characterise program transformations Bossi and Cocco [3] introduced
the following notion for a program P and a query Q: M[[P
foe j there is a successful LD-derivation of Q and P with c.a.s. oeg [ f? j
there is an infinite LD-derivation of Q and Pg.
In this section we introduce our methodology using a simple example. In
the subsequent sections, we formalise it and discuss different extensions.
The following example generates an oscillating sequence and stops if
the generated value is greater than 1000 or smaller than \Gamma1000.
Example 2. We are interested in proving termination of the set of queries
z is an integerg with respect to the following program:
The direct attempt to define the level mapping of p(X) as X fails, since X
can be positive as well as negative. Thus, a more complex level mapping
should be defined. We start with some observations.
The first clause is applicable if 1000, the second one, if
\Gamma1. Thus, termination of p(X) for X - \Gamma1000,
1 or X - 1000 is trivial. Moreover, if an infinite sequence is obtained by
applying the first clause at the first step, then for the recursive call p(X1),
it holds that \Gamma1000 ! if the second clause was applied at
the first step of the infinite sequence, then for the recursive call p(X1),
it holds that We use this observation and replace a
predicate p with two new predicates p 1!X!1000 and p \Gamma1000!X!\Gamma1 , such
that p 1!X!1000 is called if p(X) is called holds and
p \Gamma1000!X!\Gamma1 is called if p(X) is called and \Gamma1000 holds. The
following program is obtained:
Now we define two different level mappings, one for atoms of p 1!X!1000
and another one for atoms of p \Gamma1000!X!\Gamma1 . Let j p 1!X!1000 (n)
verify acceptability of the
transformed program with respect to fp 1!X!1000 (n)
\Gamma1g. This implies termination of the
transformed program with respect to these queries, and thus, termination
of the original program with respect to S.
Due to the lack of space we discuss only queries of the form p 1!X!1000 (n)
1000. The only clause that its head can be unified with
this query is the first clause. The only atom of a predicate mutually recursive
with p 1!X!1000 is p
should hold 1 , i.e., 1000 m, that is
which is true for n ? 1. 2
The intuitive presentation above hints at the major issues to be discussed
in the following sections: how the cases such as those above can be extracted
from the program, and how the program should be transformed.
3.1 Basic notions
In this section we formally introduce some notions that further analysis
will be based on. Recall that the aim of our analysis is to find, given
a predicate and a query, a sufficient condition for termination of this
query with respect to this program. Thus, we need to define a notion of
a termination condition. We start with a number of auxiliary definitions.
1 The clause is applicable only if 1
Definition 5. Let p be a predicate of arity n. Then, $1 are
called argument position denominators.
If the predicate is clear from the context the superscripts will be omitted.
Definition 6. Let P be a program, S be a set of queries. An argument
position i of a predicate p is called integer argument position, if for every
is an integer.
Argument position denominators corresponding to integer argument positions
will be called integer argument position denominators.
An integer inequality is an atom of one of the following forms Exp1 ?
are constructed from integers, variables and the four operations
of arithmetics. A symbolic inequality over the arguments of a predicate
p is constructed similarly to an integer inequality. However, instead of
variables, integer argument positions denominators are used.
Example 3. are integer inequalities. Given a
predicate p of arity 3, having only integer argument positions
and are symbolic inequalities over the arguments of p. 2
Disjunctions of conjunctions based on integer inequalities are called
integer conditions. Similarly, propositional calculus formulae based on
inequalities over the arguments of the same predicate are called
conditions over the integer arguments of this predicate.
Definition 7. Let p(t be an atom and let c p be a symbolic condition
over the arguments of p. An instance of the condition with respect to
an atom, c p (p(t obtained by replacing the argument positions
denominators with the corresponding arguments, i.e., $i p with t i .
Example 4. Let p(X; Y; 5) be an atom and let c p be ($1 p ?
Now we are ready to define termination condition formally.
Definition 8. Let P be a program, and Q be an atomic query. A symbolic
condition c rel(Q) is a termination condition for Q if given that c rel(Q) (Q)
holds, Q left-terminates with respect to P .
A termination condition for Example 2 is true, i.e., p(X) terminates for
every integer X. We'll see further that this is not always the case.
We discuss now inferring what values integer arguments can take during
traversal of the rules, i.e., the "case analysis" performed in Example 2.
It provides already the underlying intuition-calls of the predicate p c are
identical to the calls of the predicate p, where c holds for its arguments.
More formally, we define a notion of set of adornments. Later we specify
when it is guard-tuned and we show how such a guard-tuned set of
adornments can be constructed.
Definition 9. Let p be a predicate. The set A of symbolic
conditions over the integer arguments of p is called set of adornments for
if for all
Example 5. Example 2, continued. The following are examples of sets of
adornments:
3.2 Program transformation
The next question that should be answered is how the program should
be transformed given a set of adornments. After this transformation
behave with respect to the transformed program exactly
as does, for all calls that satisfy the condition c. To
define a transformation formally we introduce the following definition:
be a rule. called prefix of the rule, if
for all is an integer inequality and the only variables
in its arguments are variables of H. is called the maximal prefix
of the rule, if it is a prefix and is not a prefix.
Since a prefix constrains only variables appearing in the head of a
clause there exists a symbolic condition over the arguments of the predicate
of the head, such that the prefix is its instance with respect to the
head. In general, this symbolic condition is not necessarily unique. The
following notion guarantees uniqueness of such symbolic conditions. In
this case we say that the symbolic condition corresponds to the prefix.
Definition 10. [8] A rule H is called partially normalised
if all integer argument positions in H are occupied by distinct variables 2 .
We will also say that a program P is partially normalised if all the
rules in P are partially normalised. After integer argument positions are
identified a program can be easily rewritten to partially normalised form.
Now we are ready to present the transformation formally.
2 If such a rule has only integer arguments Apt et al. [2] call it homogeneous.
Definition 11. Let P be a program and let p be a predicate in it. Let
A q be a set of possible adornments for P . Then, the program
P a , called adorned with respect to p, is obtained in two steps as following:
1. For every rule r in P , for every subgoal q(t in the body of r,
and for every A 2 A q replace q(t
2. For every rule r
Are adornments and inequalities in the body of r consistent?
If not-reject the rule.
If r defines some q, such that q ' p
Get as adornments of the head of r all A 2 A q , that are consistent
with comparisons of the maximal prefix of r and adornments
of the body of r.
Example 6. Example 2, continued. The sets of adornments presented in
Example 5 are used. With the first set of adornments we obtain P a
If the second set of adornments is used, the program P a 2 is obtained:
Correctness of the transformation should be proved. Finiteness of the
number of clauses, the number of subgoals in a clause and the number
of elements in an adornment ensure that the transformation terminates.
Next we need to prove that the transformation preserves termination.
Adorning clauses introduces new predicates. This means that the
query Q gives rise to a number of different queries. Clearly, termination
of all of these queries with respect to P a is equivalent to termination
of Q with respect to P a augmented by a set of the clauses, such that
for every p ' rel(Q) and for every A 2 A p the clause p(X
We call this extended program P ag .
Lemma 1. Let P be a program, and let Q be a query. Let P ag be a
program obtained as described above. Then, M[[P ag ]](Q) ' M[[P ]](Q).
Proof. For all proofs we refer to [13]. \Xi
The second direction of the containment depends on the consistency
check strategy applied at the point marked by   in the definition of P a .
Example 7. Let Q be p(X) and let P be the following program:
Predicates p and q are mutually recursive. Thus, both of them should be
adorned. Let A p be f$1 ? 0; $1 - 0g and A q be f$1 ? 0; $1 - 0g. The
following program is obtained after the first step of the adorning process.
The second step of the adorning process infers adornments for the heads
of the clauses, possibly rejecting the inconsistent ones. If the inference
technique tries to use all the information it has in the body constraints and
adornments of body subgoals, a program fq $1?0 (X)
is obtained. Other clauses are rejected because of the inconsistency. The
query p(X) terminates with respect to the extended program while it does
not terminate with respect to the original one. Thus, such an inference
technique can actually improve termination.
In order for termination to be preserved a weaker inference engine
should be used, for example, considering inequalities only of the maximal
prefix. Then the following is obtained: p $1?0 (X)
0: q $1?0 (X) The query p(X) does not terminate
with respect to the extended program as expected. The following lemma
shows that if this weaker inference is used, termination is preserved. 2
Lemma 2. Let P be a program, and let Q be a query. Let P ag be a
program obtained as described above. Then, M[[P ]](Q) ' M[[P ag ]](Q).
For the case of maximal prefixes the following summarises the results.
Theorem 2. Let P be a program, let Q be a query and let A be a set
of adornments. Let P ag be a program obtained as described above with
respect to A. Then, M[[P ag ]](Q).
This theorem has two important corollaries.
Corollary 1. Let P be a program, let Q be a query and let A be a set
of adornments. Let A = fa j a 2 A; for all q such that rel(Q) a w
q is not recursive in P a g. Then
a2A is a termination condition for P .
Example 8. Example 6, continued. In P a 2 p ($1-\Gamma1000)-(\Gamma1-$1-1)-($1-1000)
does not depend on recursive predicates. By the corollary, ($1 - \Gamma1000)-
is a termination condition for p(X). 2
Theorem 2 implies that a program P is LD-terminating with respect to all
queries in a set of atomic queries S if and only if P ag , constructed as above,
is acceptable with respect to S. The latter is equivalent to acceptability
of P a with respect to fq A (t g.
Corollary 2. Let P be a program, S be a set of atomic queries and
A q be a set of adornments. Let P a be obtained with respect
to A. P is LD-terminating with respect to all queries in S if and only if P a
is acceptable with respect to fq A (t g.
This corollary allows us to complete the termination proof for Example 2.
Example 9. We show that P a 2 is acceptable with respect to the set
(X)g.
defined as: j p
1000+X, if \Gamma1000
We do not prove completely that P a 2 is acceptable with respect to
analyse only one call, p 1!$1!1000 (X). There are two
clauses, (1) and (2), such that their heads can be unified with it. (2)
is not recursive and the condition holds vacuously. (1) is recursive and
acceptability requires
descent is clear. Otherwise,
As before, there is descent in
the level mapping. The other calls are proved similarly. 2
4 Practical issues
In the previous section we have shown the transformation that allows
reasoning on termination of the numerical computations. In this section
we discuss a number of practical issues to be considered for automation.
4.1 Guard-tuned sets of adornments
In Example 5 we have seen two different sets of adornments. Both of them
are valid according to Definition 9. However, f\Gamma1000
1000)g is in some
sense preferable to f$1 - 100; $1 ? 100g. First of all, it has a declarative
reading: the sets that are constructed express conditions that, when
allow traversing the rule. Second, observe that P a 1 has not only
two mutually recursive predicates, as P a 2 does, but also self-loop on one
of the predicates. To distinguish between "better" and "worse" sets of
adornments we define guard-tuned sets of adornments.
Definition 12. Let P be a partially normalised program, let p be a predicate
in P . A set of adornments A p is called guard-tuned if for every
and for every rule r 2 P with the symbolic condition c corresponding
to its maximal prefix, either c - holds.
Example 10. The first set of adornments, presented in Example 5, is not
guard-tuned while the second one is guard-tuned. 2
Examples suggest two ways of constructing a guard-tuned
set of adornments. Given a program P one might collect the symbolic
conditions, corresponding to the maximal prefixes of the rules defining
a predicate p (we denote this set C p ) and add the completion of the
constructed disjunction. Unfortunately, this set is not necessarily a set of
adornments and if so, it is not necessary guard-tuned.
Example 11. r(X) Two sets of symbolic
conditions can be constructed: fr which is not a
set of adornments and fr $1-5 ; r $1?5 g which is not guard-tuned. 2
We use a different approach. First, we find C g. Then we
define A p to be the set of conjunctions of c i 's and their negations. We
claim that the constructed set is always a guard-tuned set of adornments.
Example 12. As above, C 10g. After simplifying and
removing inconsistencies A
Lemma 3. Let P be a program, p be a predicate in P and A p be constructed
as described. Then A p is a guard-tuned set of adornments.
4.2 How to define a level mapping?
The problem with defining level mappings is that they should reflect
changes on possibly negative arguments and remain non-negative at the
same time. We also like to remain in the framework of level mappings on
atoms defined as linear combinations of sizes of their arguments.
Definition 13. Let be an adorned predicate, where
are expressions and ae 2 f?; -g. The primitive level mapping is defined
as:
If more than one conjunct appears in the adornment, the level mapping
is defined as a linear combination of primitive level mappings corresponding
to the conjuncts. If a conjunct is a disjunction, it is ignored, since
disjunctions are introduced only if some rule cannot be applied.
Definition 14. Let p c be an adorned predicate, The natural level mapping
is:
where the c's are natural number coefficients, are as above.
Example 13. The level mappings used in Example 9 are natural level
mappings such that c 1. For
p ($1-\Gamma1000)-(\Gamma1-$1-1)-($1-1000) the definition holds trivially. 2
The approach of [7] defines symbolic counterparts of the level mappings
and infers the values of the coefficients by solving a system of constraints.
4.3 Inferring termination constraints
In this section, we combine the steps studied so far to an algorithm that
infers termination conditions. The termination condition is constructed as
a disjunction of two: c 1 for non-recursive cases, according to Corollary 1,
and c 2 , for recursive cases, incrementally refined by adding to conjunction
constraints on the integer variables, obtained from the acceptability
condition, as in [7] 3 . The algorithm is presented in Figure 1.
Example 14. q(X; Y )
We look for values of X and Y such that q(X; Y ) terminates. First, the
algorithm infers adornments. In our case f$1 ? $2; $1 - $2g are inferred.
The adorned version of this program is
There is no clause defining q $1-$2 . By Corollary 1, $1 - $2 is a termination
condition. This is the one we denoted c 1 . The termination condition
for q $1?$2 , denoted c 2 is initialised to be $1 ? $2. The level mapping is
otherwise. The acceptability
decrease implies (see
3 Any other technique proving termination and able provide some constraint that, if
implies termination can be used instead of [7].
Let P be a partially normalised program, let Q be a query and let q be rel(Q).
1. For each p ' q construct Ap .
2. Adorn P with respect to q and S
p'q Ap .
3. Let A = fa j a 2 Aq ; for all p such that q a w is not recursive in P a g.
a2A . Let
a2Aq ;a62A .
4. Remove "irrelevant clauses"
Aq be the only consistent with c2 adornments of q.
For every rule r in P a
If for all i, q A i 6w rel(Head(r)) remove r from P a
5. Define a symbolic counterparts of norms,
level mappings and interargument relations.
6. Construct constraints on the symbolic variables. Obtain S.
7. Solve S.
(a) Solution of S doesn't produce extra constraints on variables.
Report termination for c1 - c2 .
(b) Solution of S produces extra constraints involving new integer variables.
Conjunct these constraints to termination condition c2 .
Go back to step 2.
(c) Otherwise report termination for c1 .
Fig. 1. Termination Inference Algorithm
that is c $1?$2 Y ? should hold.
We update c 2 to be ($1 ? $2) - ($2 ? 0). Now we restart the whole process
with respect to Y ? 0. The following adorned program is obtained:
The second and the third clauses are removed, since they are "irrel-
evant" with respect to $2 ? 0. The level mapping is redefined as
ae
ae
Acceptability decreases imply c $1?$2
. The inequality holds, since Y ?
are assumed to hold. This solution does not impose
additional constraints on integer variables. Thus, the analysis terminates
reporting
In order to prove correctness of this algorithm we have to prove its termination
and partial correctness. Termination follows from termination
of its steps and from the finiteness of the number of integer variables, restricting
a number of backwards steps from 7(b) to 2. Partial correctness
follows from the correctness of transformations and [7].
5 Further extensions
In this section we discuss possible extensions of the algorithm presented
above. First of all, we re-consider inference of adornments, then we discuss
integrating termination analysis of numerical and symbolic computations.
5.1 Once more about the inference of adornments
The set of adornments A p , inferred in Subsection 4.1 may sometimes be
too weak for inferring precise termination conditions.
Example 15. p(X; Y )
The maximal prefix of the rule above is
0g. The only termination condition found is $1 - 0,
while the precise termination condition is $1
The problem occured due to the fact that A p restricts only some
subset of integer argument positions, while for the termination proof information
on integer arguments outside of this subset may be needed.
Definition 15. Let P be a program, let p be a predicate in P , let C q be
a set of symbolic conditions over the integer argument positions of q, and
over the integer argument positions
of p is called an extension of C if there exists r 2 P , defining p, such
that some integer argument position denominator appearing in c does not
appear in C p , and c is implied by some c q 2 C q for the recursive subgoals
and some interargument relations for the non-recursive ones.
Let C be a set of symbolic conditions over the integer argument positions
of p and let '(C) be C [ fc j c is an extension of Cg. Define the set of
adornments for p as fc 0- c 0
' \Lambda is a fixpoint of powers of ' and C p is defined as in Subsection 4.1.
Example 16. Example 15, continued. The only extension of C p is
\Gamma1g. Thus, '   (C p
and A
An alternative approach to propagating such an information was suggested
in [8]. It allows one to propagate the existing adornments but not
to infer the new ones and thus, is less precise than our approach.
5.2 Integrating numerical and symbolic computation
In the real-world programs numerical computations are sometimes interleaved
with symbolic ones, as illustrated by the following example [11].
Example 17.
To prove termination of fcollect(tree; variable; [])g three decreases should
be shown: between a call to collect and a call to process between a call to
process and a call to collect and between two calls to process. The first
two can be shown only by a symbolic level mapping, the third one-only
by the numerical approach. 2
Thus, our goal is to combine the existing symbolic approaches with
the numerical one presented so far. One of the possible ways to do so is
to combine two level mappings, j by mapping each atom
P to a pair of natural numbers (j A
by establishing decreases on orderings of such pairs [14].
Example 18. Example 17, continued.
'(collect(t; l0;
a term-size norm. The decreases are satisfied with respect to ?, such that
only if defined as: n - m,
and ?N is the usual order on the naturals. 2
This integrated approach allows one to analyse correctly examples
such as ground, unify, numbervars [15] and Example 6.12 in [8].
6 Conclusion
Termination of numerical computations was studied by a number of authors
[1, 2, 8]. Apt et al. [2] provided a declarative semantics, so called
\Theta-semantics, for Prolog programs with first-order built-in predicates, including
arithmetic operations. In this framework the property of strong
termination, i.e., finiteness of all LD-trees for all possible goals, was completely
characterised based on appropriately tuned notion of acceptabil-
ity. This approach provides important theoretical results, but seems to
be difficult to integrate in automatic tools. In [1] it is claimed that an
unchanged acceptability condition can be applied to programs in pure
Prolog with arithmetic by defining the level mappings on ground atoms
with the arithmetic relation to be zero. This approach ignores the actual
computation, and thus, its applicability is restricted to programs
using some arithmetic but not really relaying on them, such as quick-
sort. Moreover, as Example 14 illustrates, there are many programs that
terminate only for some queries. Alternatively, Dershowitz et al. [8] extended
the query-mapping pairs formalism of [9] to deal with numerical
computations. However, this approach inherited the disadvantages of [9],
such as high computational price.
More research has been done on termination analysis for constraint
logic programs [4, 10, 12]. Since numerical computations in Prolog should
be written in a way that allows a system to verify their satisfiability we
can see numerical computations of Prolog as an ideal constraint system.
Thus, all the results obtained for ideal constraints systems can be ap-
plied. Unfortunately, the research was either oriented towards theoretical
characterisations [12] or restricted to domains isomorphic to N [10].
In a contrast to the approach of [8] that was restricted to verifying
termination, we presented a methodology for inferring termination con-
ditions. It is not clear whether and how [8] can be extended to infer such
conditions. A main contribution of this work to the theoretical understanding
of termination of numerical computations is in situating them
in the well-known framework of acceptability and allowing integration
with the existing approaches to termination of symbolic computations.
The methodology presented can be integrated in automatic termination
analysers, such as [7].
The kernel technique is powerful enough to analyse correctly examples
such as gcd and mod [8] and all examples appearing in Chapter 8 of [15],
which is dedicated to arithmetic. These examples include the examples
appearing in [1]. Moreover, our approach gains its power from the underlying
framework of [7] and thus, allows one to prove termination of some
examples that cannot be analysed correctly by [8], similar to confused
delete [7]. The extended technique, presented in Section 5, allows one to
analyse correctly examples such as Ackermann's function, ground, unify,
numbervars [15] and Example 6.12 in [8].
As future work we consider a complete implementation of the al-
gorithm. Due to the use of the constraint solving techniques we expect it
both to be powerful and highly efficient.



--R

From Logic Programming to Prolog.
A declarative approach for first-order built-in's in prolog
Preserving universal temination through unfold/fold.
On termination of constraint logic programs.
A framework for analyzing the termination of definite logic programs with respect to call patterns.
Termination analysis: some practical properties of the norm and level mapping space.

A general frame-work for automatic termination analysis of logic programs
Automatic termination analysis of logic programs.
Inferring left-terminating classes of queries for constraint logic pro- grams

Verification and validation of logic programs.
Inference of termination conditions for numerical loops.

The Art of Prolog.
--TR

--CTR
Alexander Serebrenik , Danny Schreye, Termination of Floating-Point Computations, Journal of Automated Reasoning, v.34 n.2, p.141-177, December  2005
numerical computation;termination analysis