1: %\documentstyle[11pt,fullpage]{article}
2: %\documentstyle[11pt,springer1]{article}
3: \documentstyle[entcsmacro]{entcs}
4: % The following is enclosed to allow easy detection of differences in
5: % ascii coding.
6: % Upper-case A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
7: % Lower-case a b c d e f g h i j k l m n o p q r s t u v w x y z
8: % Digits 0 1 2 3 4 5 6 7 8 9
9: % Exclamation ! Double quote " Hash (number) #
10: % Dollar $ Percent % Ampersand &
11: % Acute accent ' Left paren ( Right paren )
12: % Asterisk * Plus + Comma ,
13: % Minus - Point . Solidus /
14: % Colon : Semicolon ; Less than <
15: % Equals = Greater than > Question mark ?
16: % At @ Left bracket [ Backslash \
17: % Right bracket ] Circumflex ^ Underscore _
18: % Grave accent ` Left brace { Vertical bar |
19: % Right brace } Tilde ~
20:
21: \def\lastname{Dershowitz et al.}
22: \input{psfig}
23: %%% with width
24: \newcommand{\wgefig}[4]% get figure
25: {\begin{figure}[htb]
26: \begin{center}%
27: \mbox{}
28: {\psfig{figure=#1,width=#4}}
29: \mbox{}
30: \end{center}
31: \caption{{#2}\label{#3}}
32: \end{figure}}
33:
34: \newcommand{\wrt}{w.r.t.} % with respect to
35: \newcommand{\ie}{i.e.} % i.e.
36: \newcommand{\eg}{e.g.} % e.g.
37: \newcommand{\eat}[1]{}
38: \newcommand{\imp}{{\ :\!\!-\ }}
39: \newcommand{\mc}{{mc\_carthy\_91}}
40:
41: \begin{document}
42:
43: \begin{frontmatter}
44: \title{Automatic Termination Analysis of Programs Containing Arithmetic
45: Predicates}
46: \author[Tel-Aviv]{Nachum Dershowitz}
47: \author[Jerusalem]{Naomi Lindenstrauss}
48: \author[Jerusalem]{Yehoshua Sagiv}
49: \author[Leuven]{Alexander Serebrenik}
50: \address[Tel-Aviv]{School of Mathematical Sciences\\ Tel-Aviv University\\
51: Tel-Aviv 69978, Israel}
52: \address[Jerusalem]{Institute for Computer Science\\The Hebrew University\\
53: Jerusalem 91904, Israel}
54: \address[Leuven]{Department of Computer Science\\Katholieke Universiteit Leuven\\
55: B-3001 Heverlee, Belgium}
56: \begin{abstract}
57: For logic programs with arithmetic predicates, showing termination
58: is not easy, since the usual order for the integers is not well-founded.
59: A new method, easily incorporated in the TermiLog system for automatic
60: termination analysis, is presented for showing termination in this case.
61:
62: The method consists of the following steps:
63: First, a finite abstract domain for representing the range of integers
64: is deduced automatically. Based on this abstraction, abstract
65: interpretation is applied to the program. The result is a finite
66: number of atoms
67: abstracting answers to queries which are used to extend the
68: technique of query-mapping pairs. For each query-mapping
69: pair that is potentially non-terminating,
70: a bounded (integer-valued) termination function is guessed.
71: If traversing the pair decreases the value of the termination function,
72: then termination is established.
73: Simple functions often suffice for each query-mapping
74: pair, and that gives our approach an edge over the classical approach of
75: using
76: a single termination function for all loops, which must inevitably
77: be more complicated
78: and harder to guess automatically.
79: It is worth noting that the termination of McCarthy's
80: 91 function can be shown automatically using our method.
81:
82: In summary, the proposed approach is based on combining
83: a finite abstraction of the integers with the technique
84: of the query-mapping pairs, and is essentially capable of dividing
85: a termination proof into several cases, such that a simple termination
86: function suffices for each case. Consequently, the whole process of
87: proving
88: termination can be done automatically in the framework of TermiLog
89: and similar systems.
90: \end{abstract}
91: \end{frontmatter}
92:
93: %%%\input{intro}
94: \section{Introduction}
95: In studying termination of both pure logic programs and of real Prolog
96: programs, we discovered that in most cases,
97: termination of the programs we encountered
98: depended on the following factors:
99: \begin{enumerate}
100: \item {\em Simple structural recursion.} This case may usually be resolved by
101: the use of term size or list length as a norm~\cite{DeSchreye:Decorte:NeverEndingStory,Plumer:Book}. {\em General linear norms}, defined in~\cite{Lindenstrauss:Sagiv}, are a generalisation of these standard norms.
102: \item {\em Recursion with local variables.}
103: In this case an additional preprocessing step,
104: deriving interargument relations, is necessary~\cite{Benoy:King,Brodsky:Sagiv,Ullman:van:Gelder,Plumer}.
105: \item {\em Pseudo-recursion.} These are calls to recursively defined
106: predicates
107: that can be eliminated by repetitive unfolding~\cite{Apt:Book,Bossi:Cocco,Lindenstrauss:Sagiv:Serebrenik:L,Tamaki:Sato}.
108: \item {\em Non-logical features of Prolog.}
109: Such components of Prolog programs ({\tt assert/1, !/1, ->/2, findall/3}, etc.)
110: have historically attracted
111: less attention. Termination \wrt\ control predicates may be found, for
112: example, in~\cite{Lindenstrauss:Sagiv}. Termination \wrt\ cut was studied
113: in~\cite{Andrews:WST99}.
114: \item {\em Numerical loops.} They are the topic of this paper.
115: \item {\em Non-linear loops.} These are situations in which recursion is not covered
116: by general linear norms,
117: as defined in~\cite{Lindenstrauss:Sagiv}.
118: \end{enumerate}
119:
120: Termination of logic programs in the general case is undecidable (see
121: \cite{Apt:Handbook} for the formal proof). However, the simple semantics
122: of logic programs made the search for sufficient conditions for termination
123: a challenge for the research community.
124:
125: Research on the first two topics of the list above
126: led to completely automated tools for
127: verifying termination~\cite{Codish:Taboch,Lindenstrauss:Sagiv:Serebrenik},
128: based on the use of linear norms (cf.\ ~\cite{Bossi:Cocco:Fabris,DeSchreye:Decorte:NeverEndingStory,Plumer:ICLP,Vershaetse:DeSchreye:Deriving:Linear:Size:Relations}).
129: These systems are powerful enough to deal with a large fraction
130: of the programs that have appeared in the literature~\cite{Apt:Book,Maria:Benchmarks,DeSchreye:Decorte:NeverEndingStory,Lindenstrauss:Sagiv}.
131: Moreover, most of the examples can be proved using term-size or,
132: less often, list-size.
133: When other linear norms are
134: necessary, the user is expected to provide them.
135: For any given program, these tools either provide a termination proof, or else
136: report that there may be cases of non-termination.
137:
138: Automatic linear norm inference was
139: studied in~\cite{Decorte:DeSchreye}. However, there are
140: examples, for which (it can be proved that)
141: no general linear norm can demonstrate
142: termination. These examples are covered by the last two items in the list
143: above.
144:
145: In this paper we concentrate on Case 5. Our approach is suitable for
146: automatization and may be integrated in existing systems. In Case 6
147: more sophisticated orderings (like recursive path ordering~\cite{Dershowitz})
148: or non-numerical sizes should be used.
149: These may be incorporated in the query-mapping pairs technique,
150: as described in Section~\ref{QM}. The difficulty here is in discovering
151: them automatically, though techniques can be borrowed from the term-rewriting
152: literature.
153:
154: The remainder of the paper is organized as follows: In
155: Section~\ref{Motivation} a motivating example is given.
156: In Sections~\ref{Preliminaries}--\ref{QM}
157: the different components of the algorithm are explained and
158: in Section~\ref{Algorithm} the complete algorithm is formulated.
159: In Section~\ref{Conclusion} some conclusions are presented.
160:
161: %%%\input{section2}
162: \section{The 91 function}
163: \label{Motivation}
164: We start by illustrating the use of our algorithm for proving the termination
165: of the 91 function. This deliberately contrived function was invented by John
166: McCarthy for
167: exploring properties of recursive programs, and is considered to be a good
168: test case for automatic verification systems (cf. \cite{Giesl,Knuth,Manna:McCarthy}). The treatment here is on the intuitive level.
169: Formal details will be given in subsequent sections.
170:
171: Consider the clauses:
172:
173: \begin{example}
174: \label{91:function}
175: \begin{eqnarray*}
176: &&\mathtt {\mc(X,Y) \imp X>100, Y\;\;is\;\; X-10.}\\
177: &&\mathtt {\mc(X,Y) \imp X\leq 100, Z\;\;is\;\; X+11,\mc(Z,Z1),} \\
178: &&\hspace{4.1cm}\mathtt {\mc(Z1,Y).}
179: \end{eqnarray*}
180:
181: \noindent
182: and assume that a query of the form {\tt \mc($i$,$f$)} is given,
183: that is, a query in which
184: the first argument is bound to an integer, and the second is free. This
185: program computes the same answers as the following one:
186:
187: \begin{eqnarray*}
188: &&\mathtt {\mc(X,Y) \imp X>100, Y\;\;is\;\;X-10.}\\
189: &&\mathtt {\mc(X,91) \imp X\leq 100.}
190: \end{eqnarray*}
191: \noindent
192: with the same query. Note, however, that while the termination of the latter
193: program is obvious, since there is no recursion in it, the termination of
194: the first one is far from being trivial and a lot of effort was dedicated
195: to find termination proofs for it (\cite{Giesl,Knuth,Manna:McCarthy}).
196: \end{example}
197:
198: Our algorithm starts off by {\bf discovering numerical arguments}. This step
199: is based on abstract interpretation,
200: and as a result both arguments of {\tt \mc} are proven to be numerical.
201: Moreover,
202: they are proven to be of integer type. The importance of knowledge of this
203: kind and
204: techniques for its discovery are discussed in Subsection~\ref{Discovering}.
205:
206: The next step of the algorithm is the inference of the {\bf integer
207: abstraction domain} which will help overcome difficulties caused by the fact
208: that the
209: (positive and negative) integers with the usual (greater-than or less-than) order are not well-founded. Integer abstractions are
210: derived from arithmetic comparisons in the bodies of rules. However,
211: a simplistic approach may be insufficient and the more powerful techniques
212: presented in Section~\ref{IntDomain} are sometimes essential. In our case
213: the domain $\{(-\infty,89], [90,100], [101,\infty)\}$ of intervals is deduced. For the sake of
214: convenience we denote this tripartite domain by $\{${\sl small, med, big}$\}$.
215:
216: In the next step, we {\bf use abstract interpretation to describe answers to
217: queries}. This allows us to infer numerical inter-argument relations of a
218: novel type.
219: In Section~\ref{AbstrInterp} the technique for inference of constraints of this
220: kind is presented. For our running example we get the following abstract atoms.
221:
222: \medskip
223: \begin{tabular}{ll}
224: {\tt \mc({\sl big},{\sl big})}& {\tt \mc({\sl med},{\sl med})}\\
225: {\tt \mc({\sl big},{\sl med})}& {\tt \mc({\sl small},{\sl med})}
226: \end{tabular}
227: \medskip
228:
229: \noindent These abstract atoms characterise the answers of the program.
230:
231: The concluding step creates {\bf query-mapping pairs} in the fashion of~\cite{Lindenstrauss:Sagiv}. This process uses the abstract descriptions
232: of answers to queries and is described in Section~\ref{QM}.
233: In our case, we obtain among others, the query-mapping pair
234: having the query {\tt \mc($i$,$f$)} and the mapping presented in
235: Figure~\ref{qm91a}. The upper nodes correspond to argument positions of the
236: head of the recursive clause,
237: and lower nodes---to argument positions of the second
238: recursive subgoal in the body.
239: Black nodes denote integer argument positions,
240: and white nodes denote positions
241: on which no assumption is made. The
242: arrow denotes an increase of the first argument, in the sense that
243: the first argument in the head is less than
244: the first argument in the second recursive subgoal.
245: Each set of nodes is accompanied by a set of constraints. Some
246: are inter-argument relations of the type considered
247: in~\cite{Lindenstrauss:Sagiv}. In our example this subset is empty. The rest
248: are constraints based on the integer abstraction domain. In this
249: case, that set contains the constraint that the first argument is in
250: {\sl med}.
251: \wgefig{qm91a.eps}{Mapping for McCarthy's 91 function}{qm91a}{0.40\textwidth}
252: The query-mapping pair presented is circular (upper and lower nodes are the same
253: ),
254: but the termination tests of~\cite{Codish:Taboch,Lindenstrauss:Sagiv} fail.
255: Thus, a termination function must be guessed.
256: For this loop we can use the function $100-${\sl arg1}, where
257: {\sl arg1} denotes the first argument of the atom.
258: The value of this function decreases while traversing the given
259: query-mapping pair from the upper to the lower nodes.
260: Since it is also bounded from below ($100\geq ${\sl arg1}),
261: this query-mapping pair may be traversed only finitely many times. The
262: same holds for the other circular query-mapping pair in this case.
263: Thus, termination is proved.
264:
265: %%%%\input{formal}
266: \section{Logic programs containing arithmetic predicates}
267: \label{Preliminaries}
268:
269: The algorithm we describe here would come into play
270: only when the usual termination analysers fail to prove
271: termination using the structural arguments of predicates.
272: As a first step it verifies the presence of an integer loop in
273: the program. If no integer loop is found, the possibility of
274: non-termination is reported, meaning that the termination
275: cannot be proved by this technique. If integer loops are found, each of them
276: is taken into consideration.
277: The algorithm starts by discovering integer positions in the program,
278: proceeds with creating appropriate abstractions, based on the integer loops,
279: and concludes by applying an extension of the query-mapping pairs technique.
280: The formal algorithm is presented in Section~\ref{Algorithm}.
281:
282: \subsection{Numerical and integer loops}
283: Our notion of numerical loop is based on the predicate dependency graph
284: (cf.\ \cite{Plumer:Book}):
285:
286: \begin{definition}
287: Let $P$ be a program and let $\Pi$ be a strongly connected component
288: in its predicate dependency graph. Let $S\subseteq P$ be the set of
289: program clauses, associated with $\Pi$ (i.e. those clauses that have the
290: predicates of $\Pi$ in their head).
291: $S$ is called {\em loop} if there is a cycle through predicates of $\Pi$.
292: \end{definition}
293: \begin{definition}
294: A loop $S$ is called {\em numerical\/} if there
295: exists $H\imp B_1,\ldots,B_n$ in $S$, such that for some $i$,
296: $B_i\equiv \mbox{\sl Var\ }\mbox{\tt is\ }\mbox{\sl Exp}$,
297: and either {\sl Var} is equal to some argument of $H$ or {\sl Exp} is an arithmetic expression involving a variable that is equal to some argument of $H$.
298: \end{definition}
299:
300:
301: However,
302: termination of numerical loops that involve numbers that are not integers
303: often depends on the specifics of
304: implementation and hardware, so
305: we limit ourselves
306: to ``integer loops'', rather than all numerical loops.
307: The following examples illustrate actual behaviour that
308: contradicts intuition of general numerical loops---a loop
309: that should not terminate terminates, while a loop that
310: should terminate does not. We checked the
311: behaviour of these examples on UNIX, with
312: the CLP(Q,R) library~\cite{CLP:Manual} of SICStus Prolog~\cite{SICStus:Manual},
313: CLP(R)~\cite{Jaffar:Maher} and XSB~\cite{XSB:Manual}.
314:
315: \begin{example}
316: \label{ex:real:loops}
317: Consider the following program. The goal {\tt p(1.0)} terminates although we
318: would expect it not to terminate. On the other hand the goal {\tt q(1.0)}
319: does not terminate, although we would expect it to terminate.
320: \begin{eqnarray*}
321: && \mathtt {p(0.0)\imp !.}\\
322: && \mathtt {p(X) \imp X1\;\;is\;\;X/2,\;\;p(X1).}\\
323: &&\\
324: && \mathtt {q(0.0)\imp !.}\\
325: && \mathtt {q(X) \imp X1\;\;is\;\;X\;-\;0.1,\;\;q(X1).}
326: \end{eqnarray*}
327: \end{example}
328:
329: One may suggest that assuming that the program does not contain division
330: and non-integer
331: constants will solve the problem. The following example shows that this
332: is not the case:
333: \begin{example}
334: \label{ex:num:loop}
335: \begin{eqnarray*}
336: && \mathtt {r(0).}\\
337: && \mathtt {r(X) \imp X>0,\;\;X1\;\;is\;\;X-1,\;\;r(X1).}
338: \end{eqnarray*}
339: The predicate {\tt r} may be called with a
340: real, non-integer argument, and then its behaviour is implementation dependent.
341: For example, one would expect that
342: {\tt r(0.000000001)} will fail and {\tt r(0.0)} will succeed.
343: However, in SICStus Prolog both goals
344: fail, while in CLP(R) both of them succeed!
345: \end{example}
346:
347: Therefore, we limit ourselves to integer loops, that is numerical loops
348: involving integer constants and arithmetical calculations over integers:
349: \begin{definition}
350: A program $P$ is {\em integer-based} if, given a query such that all
351: numbers appearing in it are integers, all subqueries that arise have this
352: property as well.
353: \end{definition}
354:
355: Although this definition may seem overly restrictive we use it to avoid
356: unnecessary complications.
357:
358: \begin{definition}
359: A numerical loop $S$ in a program $P$ is called an {\em integer\/} loop if $P$
360: is integer-based.
361: \end{definition}
362:
363: Termination of a query may depend on whether its argument is an integer, as
364: the following example shows:
365:
366: \begin{eqnarray*}
367: && \mathtt {p(0).}\\
368: && \mathtt {p(N) \imp N\;>\;0,\;\;N1\;\;is\;\;N\;-\;1,\;\;p(N1).}\\
369: && \mathtt {p(a) \imp p(a).}
370: \end{eqnarray*}
371:
372: \noindent For this program, {\tt p($n$)} for integer $n$ terminates, while
373: {\tt p(a)} does not.
374:
375: So we extend our notion of query pattern.
376: Till now a query pattern was an atom with the
377: same predicate and arity as the query, and arguments $b$
378: (denoting an argument that is instantiated enough with respect to the norm)
379: or $f$ (denoting an argument on which no
380: assumptions are made). Here, we extend the notion to include
381: arguments of the form $i$,
382: denoting an argument that is an integer (or integer expression). Note that $b$
383: includes the possibility of $i$, in the same way that $f$ includes the
384: possibility $b$. In the diagrams to follow we denote $i$-arguments by
385: black nodes, $b$-arguments by gray nodes and $f$-arguments by white nodes.
386:
387: Our termination analysis is always performed with respect to a given program
388: and a query pattern. A positive response guarantees termination of every query
389: that matches the pattern.
390:
391: \subsection{Discovering numerical arguments}
392: \label{Discovering}
393: Our analysis that will be discussed in the subsequent sections is based
394: on the size relationships between ``numerical arguments''. These are arguments
395: that are numerical for all subqueries generated from the initial query.
396:
397: The inference is done in two phases---bottom-up and top-down.
398: Bottom-up inference is similar to type analysis
399: (cf.\ \cite{Boye:Maluszynski,Codish:Lagoon}),
400: using the abstract domain
401: $\{\mbox{\sl int},\mbox{\sl not\_int}\}$ and the observation that an argument
402: may become {\sl int} only
403: if it is obtained from {\tt is/2} or is bound to an integer expression of
404: arguments
405: already found to be {\sl int} (i.e. the abstraction of $\mbox{\sl int}+\mbox{\sl int}$
406: is {\sl int}).
407: Top-down inference is query driven and is similar to the ``blackening''
408: process,
409: described in~\cite{Lindenstrauss:Sagiv},
410: only in this case the information propagated is being an integer expression
411: instead of ``instantiated enough''.
412:
413: The efficiency of discovering numerical arguments may be improved
414: by a preliminary step of guessing the numerical argument positions. The
415: guessing is based on the knowledge that variables appearing in comparisons
416: or {\tt is/2}-atoms should be numerical. Instead of considering the whole
417: program it is sufficient in this case to consider only clauses of
418: predicates having clauses with the guessed arguments
419: and clauses of predicates on which they depend. The
420: guessing as a preliminary step becomes crucial when considering
421: ``real-world'' programs that are large, while their numerical part is
422: usually small.
423:
424: %%%%\input{formal1}
425: \section{Integer Abstraction Domain}
426: \label{IntDomain}
427: In this subsection we present a technique that allows us to overcome the
428: difficulties caused by the fact that
429: the integers with the usual order are not
430: well-founded. Given a program $P$ we introduce a finite abstraction domain,
431: representing integers. The integer abstractions are derived from the subgoals
432: involving integer arithmetic positions.
433:
434: Let $S$ be a set of clauses in $P$, consisting of an integer loop and
435: all the clauses for predicates on which the predicates of the integer loop
436: depend. As a first step for defining the abstract domain we
437: obtain the set of comparisons ${\cal C}$ for the clauses in $S$.
438:
439: More formally, we consider as a
440: {\em comparison}, an atom of the form $t_1 \rho t_2$, such that
441: $t_1$ and $t_2$ are either variables or constants and
442: $\rho\in \{<,\leq,\geq,>\}$. Observe that we restrict ourselves
443: only to these atoms in order to ensure the
444: finiteness of ${\cal C}$. Note that by excluding $\not =$ and $=$ we
445: do not limit the generality of the analysis. Indeed if $t_1 \not = t_2$
446: appears in a clause it may be replaced by two clauses containing
447: $t_1 > t_2$ and $t_1 < t_2$ instead of $t_1 \not = t_2$,
448: respectively. Similarly, if the clause contains a subgoal $t_1 = t_2$,
449: the subgoal may be replaced by two subgoals $t_1 \geq t_2, t_1 \leq t_2$.
450: Thus, the equalities we use in the examples to follow should be seen as
451: a brief notation as above.
452:
453: In the following subsections we present a number of techniques
454: to infer ${\cal C}$ from the clauses of $S$.
455:
456: We define ${\cal D}_p$ as the set of pairs $(p,c)$, for all satisfiable $c \in 2
457: ^{{\cal C}_p}$. Here we interpret $c \in 2^{{\cal C}_p}$ as a conjunction
458: of the comparisons in $c$ and the negations of the comparisons in
459: ${\cal C}_p \setminus c$.
460: The abstraction domain ${\cal D}$ is taken as the union of the sets
461: ${\cal D}_p$ for the recursive predicates $p$ in $S$.
462: Simplifying the domain may improve the running time of the analysis, however
463: it may make it less precise.
464:
465: \subsection{The simple case---collecting comparisons}
466:
467: The simplest way to obtain ${\cal C}$ from the clauses of $S$ is
468: to consider the comparisons appearing in the bodies of recursive clauses
469: and restricting integer positions in their heads.
470:
471: We would like to view ${\cal C}$ as a set of comparisons of head argument
472: positions. Therefore we assume in the simple case that $S$ is
473: {\em partially normalised}, that is, all head {\em integer\/}
474: argument positions in clauses of $S$ are occupied by distinct variables.
475: Observe that the assumption holds for all the examples considered so far.
476: This assumption will not be necessary with the more powerful technique
477: presented in the next subsection.
478:
479: Consider
480: \begin{example}
481: \label{comparisons}
482: \begin{eqnarray*}
483: &&\mathtt {t(X)\imp X>5, X<8, X<2, X1\;is\;X+1, X1<5, t(X1).}
484: \end{eqnarray*}
485: Let {\tt t($i$)} be a query pattern for the program above.
486: In this case, the first argument of {\tt t} is an integer argument.
487: Since {\tt X1} does not appear in the head of the first clause
488: {\tt X1<5} is not considered and,
489: thus, ${\cal C}= \{X>5,X<8,X<2\}$. We have in this example
490: only one predicate and the union is over the singleton set.
491: So, ${\cal D} = \{X<2,2\leq X\leq 5,5<X<8,X\geq 8\}$.
492: \end{example}
493:
494: The following example evaluates the {\sl mod\/} function.
495: \begin{example}
496: \label{mod}
497: \begin{eqnarray*}
498: && \mathtt {mod(A,B,C) \imp A\geq B, B>0, D\;is\;A-B, mod(D,B,C).}\\
499: && \mathtt {mod(A,B,C) \imp A< B, A \geq 0, A = C.}
500: \end{eqnarray*}
501: Here we ignore the second clause since it is not recursive. Thus, by
502: collecting
503: comparisons from the first clause, ${\cal C} _{\mbox{\tt mod}}= \{
504: arg1\geq arg2, arg2>0\}$ and thus,
505: by taking all the conjunctions of comparisons of ${\cal C}$
506: and their negations, we obtain ${\cal D}_{\mbox{\tt mod}} =
507: \{(\mbox{\tt mod},\mbox{\sl arg1}\geq \mbox{\sl arg2} \;\&\; \mbox{\sl arg2}>0),
508: (\mbox{\tt mod},\mbox{\sl arg1}\geq \mbox{\sl arg2} \;\&\; \mbox{\sl arg2}\leq 0
509: ),
510: (\mbox{\tt mod},\mbox{\sl arg1}< \mbox{\sl arg2} \;\&\; \mbox{\sl arg2}>0),
511: (\mbox{\tt mod},\mbox{\sl arg1}< \mbox{\sl arg2} \;\&\; \mbox{\sl arg2}\leq 0)\}
512: $.
513: \end{example}
514:
515: However, sometimes the abstract domain obtained in this way is insufficient
516: for proving termination, and thus, should be refined. The domain may be
517: refined by enriching the underlying set of comparisons. Possible
518: ways to do this are using inference of comparisons instead of collecting them,
519: or performing an unfolding, and applying the collecting or inference
520: techniques to the unfolded program.
521:
522: \subsection{Inference of Comparisons}
523:
524: As mentioned above, sometimes the abstraction domain obtained from
525: comparisons appearing in $S$ is insufficient. Thus, we would like to refine it.
526: Instead of collecting comparisons, appearing in bodies of clauses,
527: we collect certain comparisons that are {\em implied} by bodies of clauses.
528: For example, {\tt X is Y+Z} implies the constraint
529: {\sl X=Y+Z} and {\tt functor(Term,Name,Arity)} implies {\sl Arity}$\geq 0$.
530:
531: As before, we restrict ourselves to recursive clauses (or clauses
532: recursive predicates depend on) and comparisons that
533: constrain integer argument positions of heads.
534: Since a comparison that is contained in the body is implied by it,
535: we always get
536: a superset of the comparisons obtained by the collecting technique, presented
537: previously. The set of comparisons inferred depends on the power of the
538: inference engine used (e.g. CLP-techniques may be used for this purpose).
539:
540: We define the abstract domain ${\cal D}$ as above. Thus, the
541: granularity of the abstract domain also depends on the power of the inference
542: engine.
543:
544: \subsection{Unfolding}
545:
546: Unfolding (cf.\ \cite{Apt:Book,Bossi:Cocco,Lindenstrauss:Sagiv:Serebrenik:L,Tamaki:Sato}) allows us to generate
547: a sequence of abstract domains, such that each refines the previous.
548:
549: More formally, let $P$ be a program and let
550: $H\imp B_1,\ldots,B_n$ be a recursive rule in $P$.
551: Let $P_1$ be the result of unfolding an atom $B_i$ in
552: $H\imp B_1,\ldots,B_n$ in $P$. Let $S_1$ be a set of clauses in $P_1$,
553: consisting of an integer loop and the clauses
554: of the predicates on which the integer loop predicates depend.
555: More formally, if $S$ is an integer loop, then by using the standard notation
556: of Apt~\cite{Apt:Book} we define $S_1$ to be
557: $S\cup \{H\leftarrow B| (H\leftarrow B)\in P \wedge
558: \exists (H_1\leftarrow B_1)\in S,\; \mbox{\sl s.t. }
559: \mbox{\sl rel($H_1$)}\sqsupseteq \mbox{\sl rel($H$)}\}$.
560:
561: Obtain ${\cal D}$ for the clauses of $S_1$
562: either by collecting comparisons from
563: rule bodies or by inferring them, and use it as a new abstraction domain
564: for the original program.
565: If the algorithm still fails to prove termination, the process of
566: unfolding can be repeated. Note, that for the cases
567: encountered in practice at most one step of unfolding is necessary.
568:
569: \begin{example}
570: Unfolding {\tt \mc(Z1,Z2)} in the recursive clause we obtain a new program
571: for the query {\tt \mc($i$,$f$)}
572: \begin{eqnarray*}
573: && \mathtt {\mc(X,Y) \imp X>100,\;Y\;\;is\;\;X-10.}\\
574: && \mathtt {\mc(X,Y) \imp X\leq 100,\;Z1\;\;is\;\;X+11, Z1>100,}\\
575: && \mathtt {\hspace{1.6in} \;Z2\;\;is\;\;Z1-10,\mc(Z2,Y).}\\
576: && \mathtt {\mc(X,Y) \imp X\leq 100,\;Z1\;\;is\;\;X+11, Z1\leq 100,}\\
577: && \mathtt {\hspace{1.6in}Z3\;\;is\;\;Z1+11,\mc(Z3,Z4),}\\
578: && \mathtt {\hspace{1.6in}\mc(Z4,Z2),\mc(Z2,Y).}
579: \end{eqnarray*}
580: Now if we use an inference engine that is able to discover that {\tt X is Y+Z}
581: implies the constraint {\sl X=Y+Z}, we obtain the
582: following constraints on the bound head integer variable $X$
583: (for convenience we omit redundant ones):
584: From the first clause we obtain $X>100$. From the second clause---%
585: $X\leq 100$, and since $X+11>100$ we get $X>89$. Similarly, from the third
586: clause---$X\leq 89$. Thus, ${\cal C}=\{X\leq 89,X>89 \wedge X\leq 100, X>100\}$
587: Substituting this in the definition of ${\cal D}$, and removing inconsistencies
588: and redundancies, we obtain ${\cal D}=\{X\leq 89,X>89 \wedge X\leq 100, X>100\}$.
589: \end{example}
590:
591: \subsection{Propagating domains}
592: \label{propagating}
593: The comparisons we obtain by the techniques presented
594: above may restrict only {\sl some\/} subset of integer argument
595: positions. However, for the termination proof, information on integer arguments
596: outside of this subset may be needed.
597: For example, as we will see shortly,
598: in order to analyse correctly {\tt \mc} we need to determine the domain for
599: the second argument, while the comparisons we have constrain
600: only the first one. Thus, we need some technique of {\sl propagating\/}
601: abstraction domains that we obtained for one subset of integer argument
602: positions to another subset of integer argument positions. Clearly,
603: this technique may be seen as a heuristic and it is inapplicable if there
604: is no interaction between argument positions.
605:
606: To capture this interaction we draw a graph for each recursive numerical
607: predicate, that has the numerical argument positions as vertices and edges
608: between vertices that can influence each other. In the case of {\tt \mc} we
609: get the graph having an edge between the first argument position and the
610: second one.
611:
612: Let $\pi$ be a permutation of the vertices of a connected component of this
613: graph. Define $\pi {\cal D}$ to be the result of replacing each occurrence
614: of $arg_i$ in ${\cal D}$ by $arg_{\pi (i)}$.
615: Consider the Cartesian product of all abstract domains
616: $\pi {\cal D}$ thus obtained, discarding unsatisfiable conjunctions.
617: We will call this Cartesian product the {\em extended domain\/} and denote
618: it by ${\cal E} {\cal D}$.
619: In the case of {\tt \mc} we get as
620: ${\cal E}{\cal D}$ the set of elements
621: {\tt \mc($A$,$B$)}, such that $A$ and $B$ are in
622: $\{\mbox{\sl small},\mbox{\sl med},\mbox{\sl big}\}$.
623:
624: More generally, when there are arithmetic relations (e.g.\ $Y = X+1$)
625: between argument positions ${\cal E}{\cal D}$ can contain
626: new subdomains that can be inferred from those in ${\cal D}$.
627:
628: %%%%%%%%%%%\input{abstrinterp1}
629: \section{Abstract interpretation}
630: \label{AbstrInterp}
631: In this section we use the integer abstractions obtained earlier to
632: classify, in a finite fashion, all possible answers to queries. This analysis
633: can be skipped in simple cases (just as in TermiLog
634: constraint inference can be skipped when not needed), but is necessary
635: in more complicated cases, like {\tt \mc}. Most examples encountered in
636: practice do not need this analysis.
637:
638: The basic idea is as follows: define an abstraction domain and perform a
639: bottom-up constraints inference.
640:
641: The abstraction domain that should be defined is a refinement of the
642: abstraction domain we defined in Subsection~\ref{IntDomain}.
643: There we considered only recursive clauses, since non-recursive clauses do not
644: affect the query-mapping pairs.
645: On the other hand, when trying to infer constraints that hold for
646: answers of the
647: program we should consider non-recursive clauses as well. In this way
648: using one of the techniques presented in the previous subsection both
649: for the recursive and the non-recursive clauses
650: an abstraction domain $\tilde{\cal D}$ is obtained.
651: Clearly, $\tilde{\cal D}$ is a refinement of ${\cal D}$.
652:
653: \begin{example}
654: For {\tt \mc} we obtain that the elements of $\tilde{\cal D}$ are the intersections of the elements in
655: $ {\cal E}{\cal D}$ (see the end of Subsection~\ref{propagating})with the constraint in the non-recursive clause and its negation.
656: \end{example}
657:
658: \begin{example}
659: \label{Dtilde}
660: Continuing the {\tt mod}-example we considered in Example~\ref{mod} and
661: considering the non-recursive clause for {\tt mod} as well, we
662: obtain by collecting
663: comparisons that $\tilde{\cal C} = \{arg1\geq arg2, arg2>0, arg1< arg2,
664: arg3<arg2,arg1 \geq 0,
665: arg1\leq arg3, arg1\geq arg3\}$ and, thus, $\tilde{\cal D}$ consists of all
666: pairs $(\mbox{\tt mod},c)$ for $c$ a satisfiable
667: element of $2^{\tilde{\cal C}}$.
668: \end{example}
669:
670: Given a program $P$, let $\cal B$ be the corresponding extended Herbrand base,
671: where we assume that arguments in numerical positions are integers.
672: Let $T_{P}$ be the immediate consequence operator.
673: Consider the Galois connection provided by the
674: abstraction function $\alpha: {\cal B} \rightarrow \tilde{\cal D}$
675: and the concretization function $\gamma: \tilde{\cal D} \rightarrow {\cal B}$
676: defined as follows:
677: The abstraction $\alpha$ of an element in ${\cal B}$ is the pair from
678: $\tilde{\cal D}$
679: that characterises it. The concretization $\gamma$ of an element in
680: $\tilde{\cal D}$ is the set of all atoms in ${\cal B}$ that satisfy it.
681: Note that $\alpha$ and $\gamma$ form a Galois connection due to the
682: disjointness of the elements of $\tilde{\cal D}$.
683:
684: Using the Fixpoint Abstraction Theorem (cf.\ \cite{Cousot:Cousot}) we get that
685: \[\alpha \left ( \bigcup _{n=1}^{\infty}T_{P}^{i}(\emptyset ) \right ) \subseteq
686: \bigcup _{n=1}^{\infty} (\alpha \circ T_{P}\circ \gamma )^{i}(\emptyset)\]
687: We will take a map $\mbox{\tt w}: \tilde{\cal D} \rightarrow\tilde{\cal D}$, that is
688: a {\em widening\/}~\cite{Cousot:Cousot} of
689: $\alpha \circ T_{P}\circ \gamma$ and compute its
690: fixpoint. Because of the finiteness of $\tilde{\cal D}$ this fixpoint may be
691: computed bottom-up.
692:
693: The abstraction domain
694: $\tilde{\cal D}$ describes all possible atoms in the extended
695: Herbrand base ${\cal B}$.
696: However, it is sufficient for our analysis to describe only
697: computed answers of the program, i.e., a subset of ${\cal B}$.
698: Thus, in practice, the computation of the fixpoint can sometimes be simplified
699: as follows:
700: We start with the constraints of the non-recursive clauses. Then we repeatedly
701: apply the recursive clauses to the set of the constraints obtained thus far,
702: but abstract the conclusions to elements of ${\cal D}$. In this way we obtain
703: a CLP program that is an abstraction of the original one. This holds in the next example.
704: The abstraction corresponding to the predicate {\tt p} is denoted
705: ${\mathtt {p_w}}$.
706:
707: \begin{example}
708: Consider once more {\tt \mc}. As claimed above we start from the non-recursive
709: clause, and obtain that
710: \begin{eqnarray*}
711: && \mathtt {\mc_w(A, B) \imp \{A>100,B=A-10\}.}
712: \end{eqnarray*}
713: By substituting in the recursive clause of {\tt \mc} we obtain the following
714: \begin{eqnarray*}
715: && \mathtt {\mc(X,Y) \imp X\leq 100,\;Z1\;\;is\;\;X+11, Z1>100,}\\
716: && \mathtt {\hspace{1.5in} \;Z2\;\;is\;\;Z1-10, Z2>100, \;Y\;\;is\;\;Z2-10.}
717: \end{eqnarray*}
718: By simple computation we discover that in this case {\tt X} is 100,
719: and {\tt Y} is 91. However, in order to guarantee the termination of
720: the inference process we do not infer the precise constraint
721: $\{X = 100, Y = 91\}$, but its abstraction, i.e., an atom
722: $\mathtt {\mc_w({med}, {med})}$. Repeatedly applying the
723: procedure described, we obtain an additional answer
724: $\mathtt {\mc_w({small}, {med})}$.
725:
726: More formally, the following SICStus Prolog CLP(R) program performs the
727: bottom-up construction of the abstracted program, as described above.
728: We use the auxiliary predicate {\tt in/2} to denote a membership in ${\cal D}$
729: and the auxiliary predicate {\tt e\_in/2} to denote a membership in
730: the extended domain ${\cal E}{\cal D}$.
731: \begin{eqnarray*}
732: && \mathtt {\imp use\_module(library(clpr)).}\\
733: && \mathtt {\imp use\_module(library(terms)).}\\
734: && \mathtt {\imp dynamic(\mc_w/2).}\\
735: && \\
736: && \mathtt {in(X,big) \imp \{X> 100\}.}\\
737: && \mathtt {in(X,med) \imp \{X>89,X\leq 100\}.}\\
738: && \mathtt {in(X,small) \imp \{X\leq 89\}.}\\
739: && \\
740: && \mathtt {e\_in((X,Y),(XX,YY))\imp in(X,XX), in(Y,YY).}\\
741: && \\
742: && \mathtt {\mc_w(X,Y) \imp \{X>100, Y=X-10\}.}\\
743: && \\
744: && \mathtt {assert\_if\_new((H\imp B)) \imp \backslash\!+ (clause(H1,B1),}\\
745: && \mathtt {\hspace{6.0cm}unify\_with\_occurs\_check((H,B),(H1,B1))),}\\
746: && \mathtt {\hspace{5.2cm}assert((H\imp B)). }\\
747: && \\
748: && \mathtt {deduce \imp \{X\leq 100,Z=X+11\},\mc_w(Z,Z1),}\\
749: && \mathtt {\hspace{2.0cm} \mc_w(Z1,Y),e\_in((X,Y),(XX,YY)),}\\
750: && \mathtt {\hspace{2.0cm} assert\_if\_new((\mc_w(A,B) \imp e\_in((A,B),(XX,YY)))),}\\
751: && \mathtt {\hspace{2.0cm}deduce.}\\
752: && \mathtt {deduce.}
753: \end{eqnarray*}
754: The resulting abstracted program is
755: \begin{eqnarray*}
756: && \mathtt {\mc_w(A, B) \imp \{A>100,B=A-10\}.}\\
757: && \mathtt {\mc_w(A, B) \imp e\_in((A,B), (med, med)).}\\
758: && \mathtt {\mc_w(A, B) \imp e\_in((A,B), (small, med)).}
759: \end{eqnarray*}
760: Since we assumed that the query was of the form {\tt \mc($i$,$f$)} we can view
761: these abstractions as implications of constraints like
762: $\mbox{\sl arg1}\leq 89$ implies $89<\mbox{\sl arg2}\leq 100$. We also point
763: out that the resulting abstracted program coincides with the results obtained
764: by the theoretic reasoning above.
765: \end{example}
766:
767: As an additional example consider
768: the computation of the {\sl gcd} according to Euclid's
769: algorithm. Proving termination is not trivial, even if the successor notation
770: is
771: used. In~\cite{Lindenstrauss:Sagiv:Serebrenik:L} only applying a special
772: technique allowed to do this.
773:
774: \begin{example}
775: Consider the following program and the query {\tt gcd($i$,$i$,$f$)}.
776: \begin{eqnarray*}
777: && \mathtt {gcd(X,0,X) \imp X>0.}\\
778: && \mathtt {gcd(X,Y,Z) \imp Y>0, mod(X,Y,U), gcd(Y,U,Z).}\\
779: && \\
780: && \mathtt {mod(A,B,C) \imp A\geq B, B>0, D\;is\;A-B, mod(D,B,C).}\\
781: && \mathtt {mod(A,B,C) \imp A< B, A \geq 0, A = C.}
782: \end{eqnarray*}
783: In this example we have two nested integer loops represented by the predicates
784: {\tt mod} and {\tt gcd}. We would like to use the information obtained from
785: the abstract interpretation of {\tt mod}
786: to find the relation between the {\tt gcd}-atoms in the recursive clause.
787: Thus, during the bottom-up inference
788: process we abstract the conclusions to elements of
789: ${\tilde{\cal D}_{\mathtt mod}}$, as it was evaluated in Example~\ref{Dtilde}.
790: Using this technique
791: we get that if $mod(X,Y,Z)$ holds then always $Z<Y$ holds, and this is what is needed to prove the
792: termination of $gcd$.
793: \end{example}
794:
795: The approach presented in this subsection is
796: a novel approach compared to the inter-argument relations that were
797: used previously in termination analysis~\cite{Benoy:King,Brodsky:Sagiv:2,Codish:Taboch,DeSchreye:Decorte:NeverEndingStory,Lindenstrauss:Sagiv,Mesnard:Ganascia,Plumer:Book,Ullman:van:Gelder,Vershaetse:DeSchreye,Vershaetse:DeSchreye:Deriving:Linear:Size:Relations}---instead of comparing
798: the sizes of arguments the ``if \ldots then \ldots'' expressions are
799: considered, making the analysis more powerful.
800:
801: %%%%%%%%%%%%%%%%%%\input{qm}
802: \section{Query-mapping pairs}
803: \label{QM}
804: We use the query-mapping pairs technique, presented
805: in~\cite{Lindenstrauss:Sagiv}, for reasoning about termination.
806: The basic idea is to partition query evaluation
807: into ``simple steps'', corresponding to one rule application and then
808: compose them. The ``steps'' are
809: performed over a finite abstract domain. Circular ``steps'' are suspicious.
810: If, for each such circular step, we succeed in showing a decrease of
811: some
812: argument position according to some integer linear norm, termination is proved,
813: due to the
814: well-foundedness of the norm. Since the abstract domain is finite,
815: we have to check only a finite number of
816: objects.
817: Here, we extend the technique to programs having numerical arguments.
818: We also assume that an integer linear norm is defined for all arguments.
819:
820: As presented in~\cite{Lindenstrauss:Sagiv},
821: queries are given as constrained abstract atoms.
822: More formally, let $\leftarrow A_1,\ldots, A_n \leadsto \ldots \leadsto\; \leftarrow B_1,\ldots, B_k$ be a partial branch in the LD-tree~\cite{Apt:Book},
823: and let $\theta$ be the composition of the substitutions along
824: this branch. Assume also that the atom $B_1$ came into being from the
825: resolution on $A_1$. In the query-mapping pair corresponding to this
826: branch, the query is the abstraction of $A_1$ and the
827: mapping is a quadruple---the domain, the range, arcs and edges.
828: The domain is the abstraction of $A_1\theta$,
829: the range is the abstraction of $B_1$ and arcs and edges represent
830: order relations between the nodes of the domain and range. Note that
831: edges are undirected, while arcs are directed.
832:
833: We extend this construction by
834: adding numerical arcs and edges between numerical argument positions.
835: These arcs and edges are added if
836: numerical inequalities and equalities between the arguments can be deduced.
837: Deduction of numerical edges and arcs is usually done by considering the
838: clauses. However, if a subquery $q$ unifies with a head of a clause
839: $A\imp B_1,\ldots,B_k,\ldots,B_n$ and we want to know the relation
840: between $q$ and $B_k$ (under appropriate substitutions), we {\em may} use the
841: results of the abstract interpretation to conclude numerical constraints for
842: $B_1,\ldots,B_{k-1}$. The reason is that if we arrive at $B_k$, this
843: means that we have proved $B_1,\ldots,B_{k-1}$
844: (under appropriate substitutions). All query-mapping pairs deduced in this
845: way are then repeatedly composed. The process terminates because there is
846: a finite number of query-mapping pairs.
847:
848: A query-mapping pair is called {\em circular} if the
849: query coincides with the range. The initial query terminates if for
850: every circular query-mapping pair one of the following conditions
851: holds:
852: \begin{itemize}
853: \item The circular pair meets
854: the requirements of the termination test of~\cite{Lindenstrauss:Sagiv}.
855: \item
856: There is a non-negative termination function for which we can prove a decrease
857: from the domain to the range using the numerical edges and arcs and the
858: constraints of the domain and range.
859: \end{itemize}
860: Two points should be referred to: how does one automate the guessing of the function
861: ? And how does one prove that it decreases?
862: Our heuristic for guessing a termination function is based on the inequalities
863: appearing in the abstract constraints. Each inequality of the form
864: {\sl Exp1}$\;\rho\;${\sl Exp2} where $\rho$ is one of $\{>,\geq\}$ suggests
865: a function {\sl Exp1-Exp2}.
866:
867: The common approach to termination analysis is to find
868: {\em one} termination function that decreases over all possible execution paths.
869: This leads to complicated termination functions. Our approach allows one
870: to guess a number of relatively simple termination functions, each suited
871: to its query-mapping pair. Since termination functions are simple to find, the
872: guessing process can be performed automatically.
873:
874: After the termination function is guessed, its decrease must be proved.
875: Let $V_1,\ldots,V_n$ denote numerical argument positions in the domain and
876: $U_1,\ldots,U_n$ the corresponding numerical argument positions in the range
877: of the query-mapping pair. First, edges of the query-mapping pair
878: are translated to equalities and arcs, to inequalities between these variables.
879: Second, the atom constraints for the $V$'s
880: and for the $U$'s are added.
881: Third, let $\varphi$ be a termination function. We would like to check that
882: $\varphi(V_1,\ldots,V_n) > \varphi(U_1,\ldots,U_n)$ is implied by the constraints. Thus, we add the negation of this claim to the collection of the
883: constraints
884: and check for unsatisfiability. Since termination functions are linear,
885: CLP-techniques,
886: such as CLP(R)~\cite{Jaffar:Maher} and CLP(Q,R)~\cite{CLP:Manual},
887: are robust enough to obtain the desired contradiction. Note however,
888: that if more powerful constraints solvers are used, non-linear termination
889: functions may be considered.
890:
891: To be more concrete:
892: \begin{example}
893: \label{difficult:loops}
894: Consider the following program with query {\tt p($i$,$i$)}.
895: \begin{eqnarray*}
896: && \mathtt {p(0,\_).}\\
897: && \mathtt {p(X,Y)\imp X>0,X<Y,X1\;\;is\;\;X+1, p(X1,Y).}\\
898: && \mathtt {p(X,Y)\imp X>0,X\geq Y,X1\;\;is\;\;X-5, Y1\;\;is\;\;Y-1, p(X1,Y1).}
899: \end{eqnarray*}
900:
901: We get, among others, the circular query-mapping pair having the query
902: ({\tt p($i$,$i$)},$\{\mbox{\sl arg1}>0,\mbox{\sl arg1}<\mbox{\sl arg2}\}$)
903: and the mapping given in Figure~\ref{qmdl}. The termination function
904: derived for the circular
905: query-mapping pair is {\sl arg2}$-${\sl arg1}. In this case,
906: we get from the arc and the edge
907: the constraints: $V_1<U_1, V_2=U_2$.
908: We also have that $V_1>0, U_1>0, V_1<V_2, U_1<U_2$. We would like to prove that
909: $V_2-V_1>U_2-U_1$ is implied. Thus, we add $V_2-V_1\leq U_2-U_1$ to the set of
910: constraints and CLP-tools
911: easily prove unsatisfiability, and thus, that the required implication holds.
912: \end{example}
913: \wgefig{qmdl.eps}{Mapping for {\tt p}}{qmdl}{0.40\textwidth}
914:
915: In the case of the 91-function the mappings are given in Figure~\ref{qm91}.
916: (We omit the queries from the query-mapping pairs, since
917: they are identical to the corresponding domains.)
918: \wgefig{qm91.eps}{Mappings for McCarthy's 91 function}{qm91}{0.95\textwidth}
919:
920: In the examples above there were no interargument relations of the type considered in~\cite{Lindenstrauss:Sagiv}.
921: However, this need not
922: be the case in general. Consider the following program with the query
923: {\tt q($b$,$b$,$i$)}.
924: \begin{eqnarray*}
925: &(1)&\mathtt {q(s(X),X,\_).}\\
926: &(2)&\mathtt {q(s(X),X,N)\imp N>0, N1\;\;is\;\;N-1, q(s(X),X,N1).}\\
927: &(3)&\mathtt {q(s(s(X)),Z,N)\imp N=<0, N1\;\;is\;\;N-1, q(s(X),Y,N1),q(Y,Z,N1).}
928: \end{eqnarray*}
929: Note that constraint inference is an essential step for
930: proving termination---in order to infer that there is a decrease in the first argument
931: between the head of (3) and the second recursive call ($s(s(X))\succ Y$ with
932: respect to
933: the norm), one should infer that the second argument in {\tt q} is less than
934: the
935: first with respect to the norm ($s(X)\succ Y$ with respect to the norm). We get
936: among others circular query-mapping pairs having the mappings presented
937: in Figure~\ref{qmq}. The queries of the mappings coincide with the
938: corresponding domains. In the first mapping termination follows from the
939: decrease in the third
940: argument and the termination function {\sl arg3}$>0$.
941: In the second mapping termination
942: follows from the norm decrease in the first argument.
943: \wgefig{qmq.eps}{Mappings for {\tt q}}{qmq}{0.80\textwidth}
944:
945: %%%%%%%%%%%%%%%%%\input{algo}
946: \section{The Algorithm}
947: \label{Algorithm}
948: In this section we combine all the techniques suggested so far. The complete algorithm {\sf Analyse\_Termination
949: } is presented in
950: Figure~\ref{algo}. We use the common notation of {\bf continue} as a keyword,
951: that can be used only in the body of a looping command and invokes skipping
952: to the next iteration of the loop. Each step of the algorithm corresponds to
953: one of the previous sections.
954:
955: \begin{figure}[htb]
956: \begin{center}
957: \fbox{
958: \parbox{6in}{%%%\tt
959: \begin{tabbing}
960: AAAA \= AAAAA\= AAAAA\= AAAAA\= AAAAA\= AAAAA\= AAAAA\=\kill
961: {\bf Algorithm} \>\> {\sf Analyse\_Termination}\\
962: {\bf Input} \>\> A query pattern $q$ and a Prolog program $P$\\
963: {\bf Output} \>\> {\sf YES}, if termination is guaranteed\\
964: \>\> {\sf NO}, if no termination proof was found\\
965: \\
966: %%%%%
967: \ \,(1) \> {\bf If} {\sf TermiLog\_Algorithm($P$,$q$)=YES} {\bf then}\\
968: \ \,(2) \> \>{\bf Return} {\sf YES}.\\
969: \ \,(3) \> {\bf If} there is no numerical loop in $P$ {\bf then}\\
970: \ \,(4) \> \>{\bf Return} {\sf NO}.\\
971: \ \,(5) \> {\bf Guess} and {\bf verify} numerical argument positions;\\
972: \ \,(6) \> {\bf Compute} integer abstraction domain;\\
973: \ \,(7) \> {\bf Compute} abstractions of answers to queries (optional);\\
974: \ \,(8) \> {\bf Compute} query-mapping pairs;\\
975: \ \,(9) \> {\bf For each} circular query-mapping pair {\bf do}:\\
976: (10) \> \> {\bf If} its circular variant has a forward positive cycle {\bf then}\\
977: (11) \> \> \> {\bf Continue};\\
978: (12) \> \>{\bf Guess} bounded (integer-valued) termination function;\\
979: (13) \> \>{\bf Traverse} the query-mapping pair {\bf and compute}
980: values\\
981: \> \> \>of the termination function;\\
982: (14) \> \>{\bf If} the termination function decreases monotonically {\bf then}\\
983: (15) \> \> \> {\bf Continue};\\
984: (16) \> \> {\bf Return} {\sf NO}; \\
985: (17) \> {\bf Return} {\sf YES}.\\
986: \end{tabbing}
987: }}
988: \end{center}
989: \caption{Termination Analysis Algorithm}
990: \label{algo}
991: \end{figure}
992:
993: Note that Step 7, computing the abstractions of answers to queries, is
994: optional. If the algorithm returns {\sf NO}
995: it may be re-run either with Step 7 included or with a different integer
996: abstraction domain.
997:
998: The {\sf Analyse\_Termination} algorithm is sound:
999: \begin{theorem}
1000: Let $P$ be a program and $q$ a query pattern.
1001: \begin{itemize}
1002: \item {\sf Analyse\_Termination($P$, $q$)} terminates.
1003: \item If {\sf Analyse\_Termination($P$, $q$)} reports {\sf YES} then,
1004: for every query $Q$ matching the pattern $q$, the LD-tree of $Q$ w.r.t.\ $P$ is finite.
1005: \end{itemize}
1006: \end{theorem}
1007:
1008: %%%%%%%%%%%%%\input{conclusion}
1009: \section{Conclusion}
1010: \label{Conclusion}
1011: We have shown an approach that can extend the scope of existing automatic
1012: systems for proving termination to programs containing arithmetic predicates.
1013: To do so we first introduced a new kind of constraints. Second, we indicated how
1014: such constraints may be inferred. Finally, we showed that the query-mapping
1015: pairs technique is robust enough to incorporate them by using very simple
1016: termination functions that are derived from the constraints.
1017:
1018: We have not yet implemented the ideas discussed in this paper, but it is
1019: clear that even a simple implementation, without inference of comparisons,
1020: unfolding and application of abstract interpretation as suggested in
1021: Section~\ref{AbstrInterp}, will be very useful from a practical point of view,
1022: since many
1023: programs encountered in practice cannot be handled by systems that use norms to
1024: prove termination because of very simple numerical loops.
1025:
1026:
1027: \bibliography{%/home/nutt/Literature/strings,%
1028: %/home/nutt/Literature/literature}%,
1029: /home/alexande/M.Sc.Thesis/main}
1030: % /cs/visitor/nutt/Literature/literature}%,
1031: % references}
1032: % references}
1033: \bibliographystyle{abbrv}
1034: %\input{appendix}
1035: \end{document}
1036: