1: \documentclass{tlp}
2: %\usepackage{aopmath}
3: \usepackage{amssymb}
4: \usepackage{latexsym}
5: \usepackage{epsfig}
6: \usepackage{graphicx}
7: \usepackage{epic}
8: \usepackage{rotating}
9: %\usepackage{harvard}
10:
11: \newcommand{\indexentry}[2]{\item #1 \dotfill #2}
12: \newcommand{\iindexentry}[2]{\subitem #1 \dotfill #2}
13:
14: \include{defs}
15:
16: \begin{document}
17: %\bibliographystyle{dcu}
18: \bibliographystyle{tlp}
19:
20: \title{Classes of Terminating Logic Programs}
21: \author[D. Pedreschi, S. Ruggieri and J.--G. Smaus]
22: {DINO PEDRESCHI and SALVATORE RUGGIERI\\
23: Dipartimento di Informatica, Universit{\`a} di Pisa\\
24: Corso Italia 40, 56125 Pisa, Italy,\\
25: \email{\{pedre,ruggieri\}@di.unipi.it}
26: \and
27: JAN--GEORG SMAUS\thanks{
28: Supported by the ERCIM fellowship programme.}\\
29: Institut f{\"u}r Informatik, Universit{\"a}t Freiburg, \\
30: Georges-K{\"o}hler-Allee 52, 79110 Freiburg im Breisgau, Germany\\
31: \email{smaus@informatik.uni-freiburg.de}
32: }
33:
34: \maketitle
35:
36: \noindent
37: %{\bf Note:} This article has been accepted for publication in
38: %\emph{Theory and Practice of Logic Programming}, \copyright Cambridge
39: %University Press.\\
40: {\bf Note:} This article has been published in
41: \emph{Theory and Practice of Logic Programming},
42: 2(3), 369--418,
43: \copyright Cambridge
44: University Press.\\
45: On July 22, 2002, the following mistake was corrected:
46: In figure \ref{permute-prog}, the first clause for $\mathtt{insert}$
47: was \verb!insert([],X,[X])!.\\
48: \enlargethispage{6ex}
49:
50:
51: \begin{abstract}
52: Termination of logic programs depends critically on the selection
53: rule, i.e.~the rule that determines which atom is selected in each
54: resolution step. In this article, we classify programs (and queries)
55: according to the selection rules for which they terminate. This is a
56: survey and unified view on different approaches in the literature.
57: For each class, we present a sufficient, for most classes even
58: necessary, criterion for determining that a program is in that
59: class. We study six classes: a program {\em strongly} terminates if
60: it terminates for {\em all} selection rules; a program {\em input
61: terminates} if it terminates for selection rules which only select
62: atoms that are sufficiently instantiated in their input positions,
63: so that these arguments do not get instantiated any further by the
64: unification; a program {\em local delay} terminates if it terminates
65: for local selection rules which only select atoms that are bounded
66: w.r.t.~an appropriate level mapping; a program {\em left-terminates}
67: if it terminates for the usual left-to-right selection rule; a
68: program {\em $\exists$-terminates} if there exists a selection rule
69: for which it terminates; finally, a program has {\em bounded
70: nondeterminism} if it only has finitely many refutations. We
71: propose a semantics-preserving transformation from programs with
72: bounded nondeterminism into strongly terminating programs.
73: Moreover, by unifying different formalisms and making appropriate
74: assumptions, we are able to establish a formal hierarchy between the
75: different classes.
76: \end{abstract}
77:
78: \section{Introduction}\label{intro-sec}
79:
80: The paradigm of logic programming originates from the discovery that a
81: fragment of first order logic can be given an elegant computational
82: interpretation. Kowalski \shortcite{Kow79} advocates the separation of the
83: {\em logic} and {\em control} aspects of a logic program and has
84: coined the famous formula
85: \begin{quote}
86: Algorithm = Logic + Control.
87: \end{quote}
88: The programmer should be responsible for the logic part, and hence a
89: logic program should be a (first order logic) specification. The
90: control should be taken care of by the logic programming system. One
91: aspect of control in logic programs is the {\em selection rule}. This
92: is a rule stating which atom in a query is selected in each derivation
93: step. It is well-known that soundness and completeness of
94: SLD-resolution is independent of the selection rule \cite{Apt97}.
95: However, a stronger property is usually required
96: for a selection rule to be useful in programming, namely termination.
97:
98:
99:
100:
101: \begin{definition} \label{c2:def:comp}
102: A {\em terminating control\/} for a program $P$ and a query $Q$ is a
103: selection rule $s$ such that every SLD-derivation of $P$ and $Q$ via
104: $s$ is finite.
105: \end{definition}
106:
107:
108: In reality, logic programming is far from the ideal that the logic
109: and control aspects are separated. Without the programmer being aware
110: of the control and writing programs accordingly, logic programs would
111: usually be hopelessly inefficient or even non-terminating.
112:
113: The usual selection rule of early systems is the {\em LD} selection
114: rule: in each derivation step, the leftmost atom in a query is
115: selected for resolution. This selection rule is based on the
116: assumption that programs are written in such a way that the data flow
117: within a query or clause body is from left to right. Under this
118: assumption, this selection rule is usually a terminating control. For
119: most applications, this selection rule is appropriate in that it
120: allows for an efficient implementation.
121:
122: Second generation logic languages adopt more flexible control
123: primitives, which allow for addressing logic and control separately.
124: Program clauses have their usual logical reading.
125: In addition, programs are augmented by {\em delay declarations\/} or
126: {\em annotations\/} that specify restrictions on the admissible
127: selection rules. These languages include NU-Prolog \cite{nuprolog},
128: G{\"o}del \cite{HL94} \index{G{\"o}del} and Mercury \cite{SHC96}.
129:
130: In this survey, we classify programs and queries according to the
131: selection rules under which they terminate, hence investigating the
132: influence of the selection rule on termination. As most approaches to
133: the termination problem, we are interested in {\em universal}
134: termination of logic programs and queries, that is, showing that {\em
135: all} derivations for a program and query (via a certain selection
136: rule) are finite. This is in contrast to {\em existential} termination
137: \cite{Bau92,SD94,Mar96}. Also, we consider \emph{definite} logic
138: programs, as opposed to logic programs that also contain negated
139: literals in clause bodies.
140:
141: Figure~\ref{overview-fig} gives an overview of the classes we
142: consider. Arrows drawn with solid lines stand for set inclusion
143: (``$\to$ corresponds to $\subset$'').
144: The numbers in the figure correspond to propositions in
145: section~\ref{relations-sec}.
146:
147: \setlength{\unitlength}{0.35cm}
148: \begin{figure}\figrule
149: \begin{center}
150: \begin{picture}(33,30)
151: \put(16,1){\vector(0,1){0}}
152: \put(8,1){\makebox(16,1){\em (Strong Termination)}}
153: \put(8,2){\makebox(16,1){\bf Recurrent Programs}}
154: \put(14,3){\vector(-1,1){8}}
155: \put(16,3){\vector(0,1){13}}
156: \put(14,5){\makebox(2,1){\ref{c2:r:rec}}}
157: \put(18,3){\vector(1,1){3}}
158: \put(16,6){\makebox(16,1){\em (Input Termination)}}
159: \put(16,7){\makebox(16,1){\bf Simply-Acceptable Programs}}
160: \dashline{0.3}(20,8)(12,11)
161: \put(12,11){\vector(-3,1){0}}
162: \put(18,8.7){\makebox(2,1){\ref{input-implies-local-prop}}}
163: \dashline{0.3}(24,8)(18,16)
164: \put(18,16){\vector(-3,4){0}}
165: \put(21,12){\makebox(2,1){\ref{input-implies-left-prop}}}
166: \dashline{0.3}(28,8)(20,21)
167: \put(20,21){\vector(-2,3){0}}
168: \put(25,13){\makebox(2,1){\ref{input-implies-exists-prop}}}
169: \put(0,11){\makebox(16,1){\em (Local delay termination)}}
170: \put(0,12){\makebox(16,1){\bf Delay-Recurrent Programs}}
171: \dashline{0.3}(8,13)(14,16)
172: \put(14,16){\vector(2,1){0}}
173: \put(8,14){\makebox(2,1){\ref{local-implies-left-prop}}}
174: \dashline{0.3}(4,13)(12,21)
175: \put(12,21){\vector(1,1){0}}
176: \put(6,17){\makebox(2,1){\ref{local-implies-exists-prop}}}
177: \put(8,16){\makebox(16,1){\em (Left-Termination)}}
178: \put(8,17){\makebox(16,1){\bf Acceptable Programs}}
179: \put(16,18){\vector(0,1){3}}
180: \put(14,19){\makebox(2,1){\ref{c2:r:rec}}}
181: \put(8,21){\makebox(16,1){\em (Exists-Termination)}}
182: \put(8,22){\makebox(16,1){\bf Fair-Bounded Programs}}
183: \put(16,23){\vector(0,1){3}}
184: \put(14,24){\makebox(2,1){\ref{c2:r:rec}}}
185: \put(8,26){\makebox(16,1){\em (Bounded Nondeterminism)}}
186: \put(8,27){\makebox(16,1){\bf Bounded Programs}}
187: \dottedline{0.4}(16,28)(16,29)(33,29)(33,0)(16,0)(16,1)
188: \put(31,24){\makebox(2,1){\ref{c2:bn:transfcorr}}}
189: \put(19,29){\makebox(14,1){\bf Inference+Transformation}}
190: \end{picture}
191: \end{center}
192: \caption{An overview of the classes\label{overview-fig}}
193: \figrule\end{figure}
194:
195: A program $P$ and query $Q$ {\em strongly terminate} if they terminate
196: for {\em all} selection rules. This class of programs has been studied
197: mainly by Bezem \shortcite{Bez93}. Naturally, this class is the
198: smallest we consider. A program $P$ and query $Q$ {\em
199: left-terminate} if they terminate for the {\em LD} selection rule.
200: The vast majority of the literature is concerned with this class;
201: see \cite{SD94} for an overview. A program $P$ and query $Q$ {\em
202: $\exists$-terminate} if there {\em exists} a selection rule for which
203: they terminate. This notion of termination has been introduced by
204: Ruggieri \shortcite{RugTCS98,Rug99}. Surprisingly, this is still not the
205: largest class we consider. Namely, there is the class of programs for
206: which there are only finitely many {\em successful} derivations
207: (although there could also be infinite derivations). We say that these
208: programs have {\em bounded nondeterminism}, a notion studied by
209: Pedreschi \& Ruggieri \shortcite{PR99}. Such programs can be transformed
210: into equivalent programs which strongly terminate, as indicated in the
211: figure and stated in Theorem~\ref{c2:bn:transfcorr}.
212:
213: To explain the two remaining classes shown in the figure, and their
214: relationship with left-terminating programs, we have to introduce the
215: concept of {\em modes}. A mode is a labelling of each argument
216: position of a predicate as either input or output. It indicates the
217: intended data flow in a query or clause body.
218:
219: An {\em input-consuming} derivation is a derivation where an atom can
220: be selected only when its input arguments are instantiated to a
221: sufficient degree, so that unification with the head of the clause
222: does not instantiate them further. A program and a query {\em
223: input terminate} if all input-consuming
224: derivations for this program and query are finite. This class of
225: programs has been studied by Smaus \shortcite{Sma99} and Bossi
226: {\em et al.} \shortcite{BER99,BER00,BERS01}.
227:
228: A {\em local} selection rule is a selection rule specifying that an
229: atom can only be selected if there is no other atom which was
230: introduced (by resolution) more recently. Marchiori \&
231: Teusink~\shortcite{MT99} have
232: studied termination for selection rules that are both local and
233: {\em delay-safe}, i.e., they respect the {\em delay
234: declarations}. We will call termination w.r.t.~such
235: selection rules {\em local delay} termination. A priori, the LD
236: selection rule, input-consuming selection rules and local delay-safe
237: selection rules are not formally comparable. Under reasonable
238: assumptions however, one can say that assuming input-consuming
239: selection rules is weaker than assuming local and delay-safe selection
240: rules, which is again weaker than assuming the LD selection rule. This
241: is indicated in the figure by arrows drawn with dashed lines.
242: Again, the numbers in the figure correspond to propositions in
243: section~\ref{relations-sec}.
244:
245: In this survey, we present declarative characterisations of the
246: classes of programs and queries that terminate with respect to each of
247: the mentioned notions of termination. The characterisations make use
248: of level mappings and Herbrand models in order to provide proof
249: obligations on program clauses and queries. All characterisations are
250: sound. Except for the case of local delay termination, they are also
251: complete (in the case of input termination, this holds only under
252: certain restrictions).
253:
254:
255:
256:
257: This survey is organised as follows. The next section introduces some
258: basic concepts and fixes the notation. Then we have six sections
259: corresponding to the six classes in figure~\ref{overview-fig}, defined
260: by increasingly strong assumptions about the selection rule. In each
261: section, we introduce a notion of termination and provide a
262: declarative characterisation for the corresponding class of
263: terminating programs and queries. In section~\ref{relations-sec}, we
264: establish relations between the classes, formally showing the
265: implications of figure~\ref{overview-fig}. Section~\ref{related-sec}
266: discusses the related work, and section~\ref{conc-sec} concludes.
267:
268:
269: \section{Background and Notation}\label{prelim-sec}
270:
271: We use the notation of Apt \shortcite{Apt97}, when not otherwise
272: specified. In particular, throughout this article we consider a fixed
273: language $L$ in which programs and queries are written. All the
274: results are {\it parametric\/} with respect to $L$, provided that $L$
275: is rich enough to contain the symbols of the programs and queries
276: under consideration. We denote with $U_L$ and $B_L$ the Herbrand
277: universe and the Herbrand base on $L$. $Term_L$ and $Atom_L$ denote
278: the set of terms and atoms on $L$.
279: We use typewriter font for logical variables,
280: e.g.~$\mathtt{X},\mathtt{Ys}$,
281: upper case letters for arbitrary terms, e.g. $\mathit{Xs}$, and
282: lower case letters for ground terms, e.g.~$t, x, \mathit{xs}$.
283: We denote by $\inst_L(P)$ ($\groun{L}{P}$) the set of (ground)
284: instances of all clauses
285: in $P$ that are in language $L$. The notation
286: $\groun{L}{Q}$ for a query $Q$ is defined analogously.
287:
288: The domain (resp., set of variables in the range)
289: of a substitution $\theta$ is denoted as $\dom(\theta)$ (resp.,
290: $\codom(\theta)$).
291:
292: \subsection{Modes}\label{modes-subsec}
293: For a predicate $p/n$, a {\em mode} is an atom $p(m_1,\dots,m_n)$,
294: where $m_i \in \{{\tt \inp,\out} \}$ for $i \in [1,n]$. Positions
295: with $\inp$ are called {\em input positions}, and positions with
296: $\out$ are called {\em output positions} of $p$. To simplify the
297: notation, an atom written as $p(\vect{s},\vect{t})$ means: $\vect{s}$
298: is the vector of terms filling in the input positions, and $\vect{t}$ is
299: the vector of terms filling in the output positions. An atom
300: $p(\vect{s},\vect{t})$ is {\em input-linear} if $\vect{s}$ is linear,
301: i.e.~each variable occurs at most once in $\vect{s}$. The atom is
302: {\em output-linear} if $\vect{t}$ is linear.
303:
304: In the literature, several correctness criteria concerning the modes
305: have been proposed, the most important ones being nicely-modedness and
306: well-modedness~\cite{Apt97}. In this article, we need {\em simply}
307: moded programs~\cite{AE93}, which are a special case of nicely
308: moded programs, as well as {\em well moded} programs.
309:
310:
311: \begin{definition}
312: \label{simply-moded-def}
313: A clause
314: $p(\vect{t}_0,\vect{s}_{n+1})\la
315: p_1(\vect{s}_1,\vect{t}_1),\ldots,p_n(\vect{s}_n,\vect{t}_n)$
316: is
317: \emph{simply moded} if $\vect{t}_1,\ldots,\vect{t}_n$ is a linear
318: vector of variables and for all $i\in [1,n]$
319:
320: $${\it Var}(\vect{t}_i)\cap {\it Var}(\vect{t}_0) = \emptyset
321: \quad \mbox{and} \quad
322: {\it Var}(\vect{t}_i)\cap
323: \bigcup_{j=1}^i{\it Var}(\vect{s}_j)=\emptyset.$$
324:
325: A query $\vect{B}$ is \emph{simply moded} if the clause $q
326: \la \vect{B}$ is simply moded, where $q$ is any variable-free atom.
327: A program is simply moded if all of its clauses are.
328:
329: A query (clause, program) is {\em permutation simply moded} if it is
330: simply moded modulo reordering of the atoms of the query (each clause body).
331: \end{definition}
332:
333: Thus, a clause is simply moded if the output positions of body atoms
334: are filled in by distinct variables, and every variable occurring in
335: an output position of a body atom does not occur in an earlier input
336: position. In particular, every unit clause is simply moded.
337:
338: \begin{definition}\label{well-moded}
339: A query $Q =
340: p_1(\vect{s}_1,\vect{t}_1),\dots,p_n(\vect{s}_n,\vect{t}_n)$ is {\em
341: well moded} if for all $i \in [1,n]$ and $K=1$
342: \begin{equation}
343: \vars(\vect{s}_i) \subseteq
344: \bigcup_{j = K}^{i-1}
345: \vars(\vect{t}_j) \label{wm-eq}
346: \end{equation}
347: The clause
348: $p(\vect{t}_0,\vect{s}_{n+1}) \gets Q$
349: is {\em well moded} if (\ref{wm-eq}) holds
350: for all $i \in [1,n+1]$ and $K = 0$.
351: A program is {\em well moded} if all of its clauses are well moded.
352:
353: A query (clause, program) is {\em permutation well moded} if it is
354: well moded modulo reordering of the atoms of the query (each clause body).
355: \end{definition}
356:
357: Almost all programs we consider in this article are permutation well
358: and
359: simply moded with respect to the same set of modes. The program in
360: figure~\ref{transp-prog} is an exception due to the fact that our
361: notion of modes cannot capture that sub-arguments of a term can have
362: different modes. We do not always give the modes explicitly, but they are
363: usually easy to guess.
364:
365: %The parametrisation of such correctness criteria by a permutation has
366: %been proposed by Smaus {\em et al.}~\shortcite{SHK01}. It allows to treat
367: %explicitly programs where the textual order of atoms is not identical
368: %to the intended data flow.
369:
370: \subsection{Selection Rules}
371: Let $\mathit{INIT}$ be the set of initial fragments of SLD-derivations in which
372: the last query is non-empty. The standard definition of
373: {\em selection rule\/} is as follows: a selection rule is a function
374: that, when applied to an element in $\mathit{INIT}$, yields an
375: occurrence of an atom in its last query \cite{Apt97}. In this article,
376: we assume an extended definition:
377: we also allow that a selection rule may select no
378: atom (a situation called {\em deadlock}), and we allow that it
379: not only returns the selected atom, but also specifies the set of program
380: clauses that may be used to resolve the atom. Whenever we want to
381: emphasise that a selection rule always selects exactly one atom together
382: with the entire set of clauses for that atom's predicate, we speak of a
383: {\em standard selection rule}.
384: Note that for the extended definition, completeness of SLD-resolution is lost in general.
385: Selection rules are denoted by $s$.
386:
387:
388: We now define the selection rules used in this article, except for
389: {\em delay-safe} selection rules, since these
390: rely on notions introduced only later.
391:
392: Input-consuming selection rules are defined w.r.t.~a given mode. A
393: selection rule $s$ is {\em input-consuming} for a program $P$ if
394: either
395: \begin{itemize}
396: \item
397: $s$ selects an atom $p(\vect{s},\vect{t})$ and a non-empty set of
398: clauses of $P$ such that $p(\vect{s},\vect{t})$
399: and each head of a clause in the set are unifiable with an mgu
400: $\sigma$, and $\dom(\sigma) \cap \vars(\vect{s}) = \emptyset$, or
401: \item
402: $s$ selects an atom $p(\vect{s},\vect{t})$ that unifies with no clause head from $P$,
403: together with all clauses in $P$ (this models {\em failure}), or
404: \item
405: if the previous cases are impossible, $s$ selects no atom
406: (i.e.\ we have {\em deadlock}).
407: \end{itemize}
408: Consider a query, containing atoms $A$ and $B$, in an initial fragment
409: $\xi$ of a derivation. Then $A$ is {\em introduced more recently} than
410: $B$ if the derivation step introducing $A$ comes after the step
411: introducing $B$, in $\xi$. A {\em local selection rule} is a
412: selection rule that specifies that an atom in a query can be selected
413: only if there is no more recently introduced atom in the query.
414:
415: The usual {\em LD} selection rule (also called {\em leftmost}
416: selection rule) always selects the leftmost atom in the last query of
417: an element in $\mathit{INIT}$. The {\em RD} selection rule (also
418: called {\em rightmost}) always selects the rightmost atom.
419:
420: A standard selection rule $s$ is {\em fair\/} if for every
421: SLD-derivation $\xi$ via $s$ either $\xi$ is finite or for every atom
422: $A$ in $\xi$, (some further instantiated version of) $A$ is eventually
423: selected.
424:
425:
426: \subsection{Universal Termination}
427: In general terms, the problem of universal termination of a
428: program $P$ and a query $Q$ w.r.t.~a set of admissible selection rules
429: consists of showing that every rule in the set is a terminating
430: control for $P$ and $Q$.
431:
432: \begin{definition}\label{c2:def:ut}
433: A program $P$ and a query $Q$ {\em universally terminate\/} w.r.t.~a
434: set of selection rules ${\cal S}$ if every SLD-derivation of $P$ and
435: $Q$ via any selection rule from ${\cal S}$ is finite.
436: \end{definition}
437:
438: Note that, since SLD-trees are finitely branching, by K{\"o}nig's
439: Lemma, ``every SLD-derivation for $P$ and $Q$ via a selection rule $s$
440: is finite'' is equivalent to stating that the SLD-tree of $P$ and $Q$
441: via $s$ is finite.
442:
443: We say that a class of programs and queries is a {\em sound}
444: characterisation of universal termination w.r.t.~${\cal S}$ if every
445: program and query in the class universally terminate w.r.t.~${\cal
446: S}$. Conversely, it is {\em complete} if every program and query that
447: universally terminate w.r.t.~${\cal S}$ are in the class.
448:
449:
450: \subsection{Norms and Level Mappings}\label{norms-subsec}
451: All the characterisations of terminating programs we propose make
452: use of the notions of norm and level mapping
453: \cite{Cav89}. Depending on the
454: approach, such notions are defined on ground or arbitrary objects.
455:
456: In the following definition, $Term_L/\!\!\sim$
457: denotes the set of equivalence classes of terms modulo variance.
458: Similarly, we define $Atom_L/\!\!\sim$.
459:
460: \begin{definition} \label{c2:def:nlm}
461: A {\em norm\/} is a function $|.|: U_L \ra \nat$. A
462: {\em level mapping\/} is a function $|.|: B_L \ra \nat$. For a ground
463: atom $A$, $|A|$ is called the level of $A$.
464:
465: An atom $A$ is {\em bounded} w.r.t.~the level mapping
466: $|.|$ if there exists $k \in \nat$ such that for every
467: $A' \in \groun{L}{A}$, we have $k > |A'|$.
468:
469: A {\em generalised norm\/} is a function
470: $|.|: \mathit{Term}_L/\!\!\sim \ra \nat$. A
471: {\em generalised level mapping\/} is a function
472: $|.|: \mathit{Atom}_L/\!\!\sim \ra \nat$ . Abusing notation,
473: we write $|T|$ ($|A|$) to denote the value
474: of $|.|$ on the equivalence class of the term $T$ (the atom $A$).
475: \end{definition}
476:
477: %Note that if for a non-ground atom $A$ and a generalised level mapping
478: %$|.|$, we have $|A| = k$, then this should not be confused with $|A|$
479: %being bounded by $k$.
480:
481: (Generalised) level mappings are used to measure the ``size'' of a
482: query and show that this size decreases along a derivation, hence
483: showing termination. They are usually defined based on (generalised)
484: norms.
485: Therefore we often use the same notation $|.|$ for a norm and a level
486: mapping based on it.
487:
488: Of course, a generalised norm or level mapping can be interpreted as
489: an ordinary norm or level mapping by restricting its domain to ground
490: objects. Therefore, we now give some examples of {\em generalised}
491: norms and level mappings.
492:
493: One commonly used generalised norm is the term size norm, defined as
494: \[
495: \begin{array}{rcll}
496: size( f(\tn{T}{n}) ) & = & 1 + size(T_1) + \ldots + size(T_n) &
497: \mbox{if $n > 0$}\\
498: size(T) & = & 0 &
499: \mbox{if $T$ constant/variable.}
500: \end{array}
501: \]
502: Intuitively, the size of a term $T$ is the number of
503: function symbols occurring in $T$, excluding constants.
504: Another widely used norm is the list-length function, defined as
505: \[
506: \begin{array}{rcll}
507: | [T|Ts] | & = & 1 + |Ts| \\
508: | f(\ldots) | & = & 0 & \mbox{if}\ f \neq [\: .\: |\: .\: ].
509: \end{array}
510: \]
511: In particular, for a nil-terminated list $[T_1,\ldots,T_n]$, the
512: list-length is $n$.
513:
514: We will see later that usually, level mappings measure the {\em input}
515: arguments of a query, even though this is often just an intuitive
516: understanding and not explicit. Moreover, the choice of a particular
517: selection rule often reflects a particular mode of the program.
518: In this sense, the choice of the level mapping must depend on the
519: selection rule, via the modes. This will be seen in our examples.
520:
521: However, apart form the dependency just mentioned, the choice of level
522: mapping is an aspect of termination which is rather independent from
523: the choice of the selection rule. In particular, one does not find any
524: interesting relationship between the underlying {\em norms} and the
525: selection rule. This is why the detailed study of various norms and
526: level mappings is beyond the scope of this article, although it is an important
527: aspect of automated proofs of termination \cite{DDF93,BCF94}.
528:
529: We now define level mappings where the dependency on the modes is made
530: explicit \cite{EBC99}.
531:
532: \begin{definition} \label{moded-level-mapping}
533: A {\em moded (generalised) level mapping}
534: $|.|$ is a (generalised) level
535: mapping such that for any (not necessarily) ground
536: $\vect{s}$, $\vect{t}$ and $\vect{u}$,
537: $|p(\vect{s},\vect{t})| = |p(\vect{s},\vect{u})|$.
538: \end{definition}
539:
540: The condition
541: $|p(\mathbf{s},\mathbf{t})|=|p(\mathbf{s},\mathbf{u})|$ states
542: that the \emph{level} of an atom is independent from
543: the terms in its output positions.
544:
545: \subsection{Models}
546: Several of the criteria for termination we consider rely on
547: information supplied by a model of the program under consideration.
548: We provide the definition of Herbrand interpretations and models
549: \cite{Apt97}.
550:
551: A {\em Herbrand interpretation} $I$ is a set of ground atoms. A ground
552: atom $A$ is {\em true in $I$}, written $I\models A$, if $A\in I$. This
553: notation is extended to ground queries in the obvious way. $I$ is a
554: Herbrand {\em model} of program $P$ if for each $\clausab \in
555: \groun{L}{P}$, we have that $I\models B_1,\dots,B_n$ implies $I\models
556: A$.
557:
558: When speaking of the {\em least} Herbrand model of $P$, we mean
559: least w.r.t.~set inclusion. In termination analysis, it is usually not
560: necessary to consider the least Herbrand model, which may be difficult
561: or impossible to determine. Instead, one uses
562: models that capture some {\em argument size relationship} between the
563: arguments of each predicate \cite{SD94}. For example, a model for the
564: usual $\mathtt{append}$ predicate is
565: $$\{\mathtt{append}(xs,ys,zs) \mid |zs| = |xs| + |ys| \}$$
566: where $|.|$ is the list-length function.
567:
568:
569: \section{Strong Termination}\label{strong-sec}
570:
571: \termination
572: Early approaches to the termination problem treated universal
573: termination w.r.t.\ {\em all} selection rules, called {\em strong}
574: termination. Generally speaking, strongly terminating programs and
575: queries are either very trivial or especially written for theoretical
576: considerations.
577:
578: \begin{definition} \label{c2:def:strongt}
579: A program $P$ and query $Q$ {\em strongly terminate} if they
580: universally terminate w.r.t.~the set of all selection rules.
581: \end{definition}
582:
583: \decrease
584: In the following, we recall the approach of Bezem
585: \shortcite{Bez93}, who defined the class of
586: recurrent programs and queries. Intuitively, a program is recurrent
587: if for every ground instance of a clause, the level of the body atoms
588: is smaller than the level of the head.
589:
590: \begin{definition} \label{c2:def:recp}\label{c2:def:recq}
591: Let $|.|$ be a level mapping.
592:
593: A program $P$ is {\em recurrent by}
594: $|.|$ if for every $\clausab$ in $\groun{L}{P}$:
595: \[
596: \mbox{ for $i \in [1,n]$} \quad |A| > |B_i|.
597: \]
598: A query $Q$ is {\em recurrent by $|.|$\/} if there exists
599: $k \in \nat$ such that for
600: every $\tn{A}{n} \in \groun{L}{Q}$:
601: \[
602: \mbox{ for $i \in [1,n]$ } \quad k > |A_i|.
603: \]
604: \end{definition}
605:
606: In the above definition, the proof obligations for a query $Q$ are
607: derived from those for the program $\{ {\tt p} \la Q \}$, where {\tt
608: p} is a fresh predicate symbol. Intuitively, this is justified by
609: the fact that the termination behaviour of the query $Q$ and a program
610: $P$ is the same as for the query {\tt p} and the program $P \U \{ {\tt
611: p} \la Q\}$. So $k$ plays the role of the level of the atom {\tt
612: p}. In the original work \cite{Bez93}, the query was called
613: {\em bounded}. Throughout the
614: paper, we prefer to maintain a uniform naming convention both for
615: programs and queries.
616:
617: In subsection~\ref{characterisations-subsec}, we will compare
618: recurrence to other characterisations.
619:
620: \maintheorem
621: Termination properties of recurrent programs are summarised in
622: the following theorem.
623:
624: %\removebrackets
625: \begin{theorem}[\cite{Bez93}] \label{c2:rec:thm}
626: Let $P$ be a program and $Q$ a query.
627:
628: If $P$ and $Q$ are both recurrent by a level mapping $|.|$,
629: then they strongly terminate.
630:
631: Conversely, if $P$ and every {\em ground query\/} strongly
632: terminate, then $P$ is recurrent by some level mapping $|.|$. If
633: in addition $P$ and $Q$ strongly terminate, then $P$ and $Q$ are
634: both recurrent by some level mapping $|.|$.
635: \end{theorem}
636: \begin{proof}
637: The result is shown in \cite{Bez93} for standard selection
638: rules. It easily extends to our generalisation of selection rules by
639: noting that $P$ and $Q$ strongly terminate iff they universally
640: terminate w.r.t.\ the set of standard selection rules. The only-if
641: part is immediate. The if-part follows by noting that a derivation
642: via an arbitrary selection rule is a (prefix of a) derivation via a
643: {\em standard} selection rule.
644: \end{proof}
645:
646: \examples
647: \begin{example} \label{ex:sat-is-recurrent}
648: The program {\tt SAT} in figure~\ref{sat-prog}
649: decides propositional satisfiability.
650: The program is readily checked to be recurrent by $|.|$, where
651: we define
652: \[
653: |\mathtt{sat}(t)| = |\mathtt{inval}(t)| =
654: size(t).
655: \]
656: Note that Definition~\ref{c2:def:recp} imposes no proof obligations for unit
657: clauses. The query {\tt sat($X$)} is recurrent iff there exists a natural
658: $k$ such that for every ground instance
659: $x$ of $X$, we have that $size(x)$ is bounded by $k$.
660: Obviously, this is the case iff $X$ is already a ground term. For
661: instance, the query {\tt sat(not(true) $\land$ false)} is recurrent,
662: while the query {\tt sat(false $\land$ X)} is not.
663: \end{example}
664:
665: \begin{figure}\figrule
666: \begin{minipage}[t]{5cm}
667: \begin{janprogram}
668: \%\> sat(Formula) $\la$ \\
669: \%\> \> \mbox{\rm there is a true instance of} Formula\\[2ex]
670: \> sat(true).\\
671: \> sat(X $\land$ Y) \la \\
672: \> \> sat(X), sat(Y).\\
673: \> sat(not X) \la \ inval(X).
674: \end{janprogram}
675: \end{minipage}
676: \hfill
677: \begin{minipage}[t]{5cm}
678: \begin{janprogram}
679: \> inval(false).\\
680: \> inval(X $\land$ Y) \la \ inval(X).\\
681: \> inval(X $\land$ Y) \la \ inval(Y).\\
682: \> inval(not X) \la \ sat(X).
683: \end{janprogram}
684: \end{minipage}
685: \caption{\tt SAT\label{sat-prog}}
686: \figrule\end{figure}
687:
688: Note that the choice of an appropriate level
689: mapping depends on the intended mode of the program and query.
690: Even though this is usually not explicit, level mappings measure
691: the size of the {\em input} arguments of an atom \cite{EBC99}.
692:
693: \begin{example} \label{ex:append-is-recurrent}
694: Figure~\ref{append-prog} shows the {\tt APPEND} program.
695: It is easy to check that {\tt APPEND} is recurrent by the level
696: mapping $|\mathtt{append}(xs,ys,zs)| = |xs|$ and also by
697: $|\mathtt{append}(xs,ys,zs)| = |zs|$
698: (recall that
699: $|.|$ is the list-length function). A query
700: {\tt append($\mathit{Xs}$,$\mathit{Ys}$,$\mathit{Zs}$)} is recurrent
701: by the first level mapping iff
702: $\mathit{Xs}$ is a list, and by the second iff $\mathit{Zs}$ is a list. The level
703: mapping
704: \[
705: |\mathtt{append}(xs,ys,zs)| = min\{ |xs|, |zs| \}
706: \]
707: combines the advantages of both level mappings. {\tt APPEND} is
708: easily seen to be recurrent by it, and if $\mathit{Xs}$
709: {\em or\/} $\mathit{Zs}$
710: is a list,
711: $\mathtt{append}(\mathit{Xs},\mathit{Ys},\mathit{Zs})$ is recurrent by it.
712: \end{example}
713:
714: \begin{figure}\figrule
715: \begin{janprogram}
716: \%\> append(Xs,Ys,Zs) \la \ \\
717: \%\> \> {\rm {\tt Zs} is the result of concatenating the
718: lists {\tt Xs} and {\tt Ys}.} \\[2mm]
719: \> append([],Ys,Ys). \\
720: \> append([X|Xs],Ys,[X|Zs]) \la \ append(Xs,Ys,Zs).
721: \end{janprogram}
722: \caption{\tt APPEND\label{append-prog}}
723: \figrule\end{figure}
724:
725: \incompleteness \label{recurrency-restricted-completeness}
726: Note that completeness is not stated in full general terms,
727: i.e.~recurrence is not a complete proof method for strong termination.
728: Informally speaking, incompleteness is due to the use of level
729: mappings, which are functions that must specify a value for every
730: ground atom.
731: Therefore, if $P$ strongly terminates for a certain ground query $Q$
732: but not for all ground queries, we cannot conclude that $P$ is recurrent.
733: We provide a general
734: completeness result in section~\ref{left-sec} for a class of
735: programs containing recurrent programs.
736:
737:
738: \section{Input Termination}\label{IC-sec}
739: \limitation
740: We have said above that the class of strongly terminating programs and
741: queries is very limited. Even if a program is recurrent, it may not
742: strongly terminate for a query of interest since the query is not
743: recurrent.
744:
745: \begin{example} \label{ex:even-query-is-not-recurrent}
746: The program {\tt EVEN} in figure~\ref{even-prog}
747: is recurrent by defining
748: \begin{eqnarray*}
749: |\mathtt{even}(x)| & = & size(x)\\[-0.5ex]
750: |\mathtt{lte}(x,y) | & = & size(y).
751: \end{eqnarray*}
752: Now consider the query
753: $Q = \mathtt{even(X),\ lte(X,s^\mathit{100}(0))}$,
754: which is supposed to compute the even numbers not exceeding 100. By
755: always selecting the leftmost atom, one can easily obtain an infinite
756: derivation for {\tt EVEN} and $Q$. As a consequence of
757: Theorem~\ref{c2:rec:thm}, $Q$ is not recurrent.
758: \end{example}
759:
760: \begin{figure}\figrule
761: \begin{minipage}[t]{5cm}
762: \begin{janprogram}
763: \%\> even(X) \la \ \\
764: \%\> \> {\tt X} {\rm is an even natural number.} \\[2mm]
765: \> even(s(s(X))) \la \ even(X). \\
766: \> even(0).
767: \end{janprogram}
768: \end{minipage}
769: \hfill
770: \begin{minipage}[t]{5cm}
771: \begin{janprogram}
772: \%\> lte(X,Y) \la \ \\
773: \%\> \> X,Y {\rm are natural numbers}\\
774: \%\> \> {\rm s.t. {\tt X} is
775: smaller or equal
776: than {\tt Y}}.\\[2mm]
777: \> lte(s(X),s(Y)) \la \ lte(X,Y). \\
778: \> lte(0,Y).
779: \end{janprogram}
780: \end{minipage}
781: \caption{\tt EVEN\label{even-prog}}
782: \figrule\end{figure}
783:
784:
785: \termination
786: We now define termination for input-consuming
787: derivations~\cite{BERS01}, i.e.~derivations via an input-consuming
788: selection rule.
789:
790: \begin{definition} \label{c2:def:ict}
791: A program $P$ and query $Q$ {\em input terminate\/} if
792: they universally terminate w.r.t.~the set consisting of
793: the input-consuming selection rules.
794: \end{definition}
795:
796: The requirement of input-consuming derivations merely
797: reflects the very meaning of {\em input}: an atom must only consume
798: its own input, not produce it. In existing implementations,
799: input-consuming derivations can be ensured using control constructs
800: such as delay-declarations \cite{HL94,sicstus,SHC96,nuprolog}.
801:
802: In the above example, the obvious mode is
803: $\tt even(\inp),\ lte(\out,\inp)$.
804: With this mode, we will show that {\tt EVEN} and
805: $Q$ input terminate. If we assume a selection rule
806: that is input-consuming while always selecting the leftmost atom if
807: possible, then the above example is a contrived instance of the {\em
808: generate-and-test} paradigm. This paradigm involves two procedures,
809: one which generates a set of candidates, and another which tests
810: whether these candidates are solutions to the problem. The test occurs
811: to the left of the generator so that tests take place as soon as
812: possible, i.e.~as soon as sufficient input has been generated for the
813: derivation to be input-consuming.
814:
815: %\onlyhere{Discussion on limited depth of SLD trees at selection time}
816: Proofs of input termination differ from proofs of strong
817: termination in an important respect. For the latter, we require that
818: the initial query is recurrent, and as a consequence we have that all
819: queries in any derivation from it are recurrent (we say that
820: recurrence is {\em persistent} under resolution). This means that, at
821: the time an atom is selected, the depth of its SLD tree is bounded. In
822: contrast, input termination does not need such a strong
823: requirement on each selected atom.
824:
825: \begin{example}\label{non-pindown-ex}
826: Consider the {\tt EVEN} program and the following input-consuming
827: derivation, where we underline the selected atom in each step
828: \[
829: \begin{array}{l}
830: \tt even(X),\ \underline{lte(X,s^\mathit{100}(0))} \longrightarrow \quad
831: even(s(X')),\ \underline{lte(X',s^\mathit{99}(0))} \longrightarrow\\
832: \tt \underline{even(s(s(X'')))},\ lte(X'',s^\mathit{98}(0)) \longrightarrow \quad
833: even(X''),\ \underline{lte(X'',s^\mathit{98}(0))} \dots
834: \end{array}
835: \]
836: At the time when $\tt even(s(s(X'')))$ is selected, the depth of its
837: SLD-tree is not bounded (without knowing the eventual instantiation of
838: $\tt X''$).
839: \end{example}
840:
841: \onlyhere{Information on Data Flow: Simply-local Substitutions and Models}
842: Since the depth of the SLD-tree of the selected atom depends on
843: further instantiation of the atom, it is important that programs are
844: well-behaved w.r.t.~the modes. This is illustrated in the following
845: example.
846:
847: \begin{example} \label{circular-ex}
848: Consider the {\tt APPEND} program
849: in mode $\tt append(\inp,\inp,\out)$ and the query
850: \[
851: \tt append([1|As],[],Bs), append(Bs,[],As).
852: \]
853: Then we have the following infinite
854: input-consuming derivation:
855: \[
856: \begin{array}{l}
857: \tt \underline{append([1|As],[],Bs)},\ append(Bs,[],As) \longrightarrow \\
858: \tt append(As,[],Bs'),\ \underline{append([1|Bs'],[],As)} \longrightarrow \\
859: \tt \underline{append([1|As'],[],Bs')},\ append(Bs',[],As') \longrightarrow
860: \dots
861: \end{array}
862: \]
863: This well-known termination problem of programs with coroutining has
864: been identified as {\em circular modes} by Naish \shortcite{Nai92c}.
865: \end{example}
866:
867: To avoid the above situation, we require programs to be simply moded
868: (see subsection~\ref{modes-subsec}).
869:
870: We now define \emph{simply-local} substitutions,
871: which reflect the way simply moded clauses become instantiated in
872: input-consuming derivations. Given a clause
873: $\cequals p(\vect{t}_0,\vect{s}_{n+1})\la
874: p_1(\vect{s}_1,\vect{t}_1),\ldots,p_n(\vect{s}_n,\vect{t}_n)$ used
875: in an input-consuming derivation, first $\vect{t}_0$ becomes
876: instantiated, and the range of that substitution contains only
877: variables from outside of $c$. Then, by resolving
878: $p_1(\vect{s}_1,\vect{t}_1)$, the vector $\vect{t}_1$ becomes
879: instantiated, and the range of that substitution contains variables
880: from outside of $c$ in addition to variables from $\vect{s}_1$.
881: Continuing in the same way, finally, by resolving
882: $p_n(\vect{s}_n,\vect{t}_n)$, the vector $\vect{t}_n$ becomes
883: instantiated, and the range of that substitution contains variables
884: from outside of $c$ in addition to variables from $\vect{s}_1\dots\vect{s}_n$.
885: A substitution is \emph{simply-local} if it is composed from
886: substitutions as sketched above. The formal definition is as follows.
887:
888: \begin{definition}
889: \label{def:simply-local}
890: A substitution $\theta$ is \emph{simply-local} w.r.t.\
891: the clause
892: $\cequals p(\vect{t}_0,\vect{s}_{n+1})\la
893: p_1(\vect{s}_1,\vect{t}_1),$ $\ldots,$ $p_n(\vect{s}_n,\vect{t}_n)$
894: if
895: there exist substitutions $\sigma_0,\sigma_1\ldots,\sigma_n$
896: and disjoint sets of fresh (w.r.t.\ $c$) variables
897: $v_0,v_1,\ldots,v_n$
898: such that
899: $\theta=\sigma_0\sigma_1\cdots\sigma_n$
900: where for $i\in \{0,\ldots,n\}$,
901: \begin{itemize}
902: \item $\dom(\sigma_i)\subseteq \vars(\vect{t}_i)$,
903: \item $\codom(\sigma_i)\subseteq
904: \vars(\vect{s}_i \sigma_0\sigma_1\cdots\sigma_{i-1}) \cup
905: v_i$.\footnote{
906: Note that $\vect{s}_0$ is undefined. By abuse of notation,
907: $\vars(\vect{s}_0 \dots) = \emptyset$.}
908: \end{itemize}
909:
910: $\theta$ is \emph{simply-local} w.r.t.\ a query $\vect{B}$ if
911: $\theta$ is simply-local w.r.t.\ the clause $q \la \vect{B}$ where $q$ is
912: any variable-free atom.
913: \end{definition}
914:
915: Note that in the case of a simply-local substitution w.r.t.~a query, $\sigma_0$ is
916: the empty substitution, since
917: $\mathit{Dom}(\sigma_0)\subseteq \mathit{Var}(q)$ where $q$ is an (imaginary)
918: variable-free atom. Note also that if
919: $\vect{A},B,\vect{C}
920: \longrightarrow
921: (\vect{A},\vect{B},{\bf C})\theta$
922: is an input-consuming derivation step using clause
923: $\cequals H\gets \vect{B}$, then
924: $\theta_{|H}$ is simply-local w.r.t.~the clause $H\la$ and
925: $\theta_{|B}$ is simply-local w.r.t.~the atom $B$~\cite{BERS01}.
926:
927: \begin{example}\label{ex:local-substitutions}
928: Consider \texttt{APPEND} in mode $\mathtt{append}(\inp,\inp,\out)$, and its
929: recursive clause
930: \[
931: \cequals \tt append([H|Xs],Ys,[H|Zs]) \la append(Xs,Ys,Zs).
932: \]
933: The substitution
934: $\theta = \{\tt H/V, Xs/[], Ys/[W], Zs/[W]\}$ is simply-local w.r.t.\ $c$: let
935: $\sigma_0 = \{\tt H/V, Xs/[], Ys/[W]\}$ and
936: $\sigma_1 = \{\tt Zs/[W]\}$; then
937: $\dom(\sigma_0)\subseteq \{\tt H, Xs, Ys\}$, and
938: $\codom(\sigma_0)\subseteq v_0$ where
939: $v_0 = \{\tt V, W\}$, and
940: $\dom(\sigma_1)\subseteq \{\tt Zs\}$, and
941: $\codom(\sigma_1)\subseteq
942: \vars({\tt (Xs,Ys)}\sigma_0)$.
943: \end{example}
944:
945: Based on simply-local substitutions, we now define a restricted notion
946: of model.
947:
948: \begin{definition}\label{sl-model-def}
949: Let $I\subseteq \mathit{Atom}_L$.
950: We say that $I$ is a \emph{simply-local model} of
951: $\cequals H\gets B_1,\ldots,B_n$ if for every substitution
952: $\theta$ simply-local w.r.t.\ $c$,
953: \begin{equation}
954: \mbox{if $B_1\theta,\ldots,B_n\theta\in I$ then $ H\theta\in I$.}
955: \label{SL-model-eq}
956: \end{equation}
957: %\item
958: $I$ is a \emph{simply-local model} of a program $P$ if it is a
959: simply-local model of each clause of it.
960: %\end{itemize}
961: \end{definition}
962:
963: Note that a simply-local model
964: is not necessarily a model in the classical sense, since
965: $I$ is not necessarily a set of ground atoms, and
966: the substitution in (\ref{SL-model-eq}) is required to be
967: simply-local.
968: For example, given the program
969: $\{\tt q(1),\; p(X) \!\la\! q(X)\}$
970: with modes
971: $\tt q(\inp),\ p(\out)$, a model must contain the atom
972: $\tt p(1)$, whereas a simply-local model does not necessarily contain
973: $\tt p(1)$, since $\{\tt X/1\}$ is not simply-local w.r.t.\
974: $\tt p(X) \la q(X)$.
975: The next subsection will further clarify the role of simply-local
976: models.
977:
978:
979:
980: Let $\mathit{SM}_P$ be the set of all simply moded atoms in
981: $\mathit{Atom}_L$.
982: It has been shown that the
983: least simply-local model of $P$
984: containing $\mathit{SM}_P$ exists and can be computed by a variant of
985: the well-known $T_P$-operator~\cite{BERS01}.
986: We denote the least
987: simply-local model of $P$ containing $\mathit{SM}_P$ by
988: $\mathit{PM}^{SL}_P$, for \emph{partial model}.
989:
990:
991: \begin{example}\label{ex:local-model}
992: Consider \texttt{APPEND}. To compute
993: $\mathit{PM}^{SL}_{\tt APPEND}$, we must iterate
994: the abovementioned variant of the $T_P$-operator starting from
995: the fact clause `\verb:append([],Ys,Ys).:' and any
996: simply moded atom. It turns out that
997: \begin{eqnarray*}
998: \mathit{PM}^{SL}_{\tt APPEND}
999: & =\;\; \displaystyle \bigcup_{n=0}^{\infty}\;\; ( \!\!\!\!\!\! &
1000: \{ {\tt append}([T_1,\ldots,T_n],T,[T_1,\ldots,T_n|T]) \} \cup \\
1001: & &
1002: \{
1003: {\tt append}([T_1,\ldots,T_n|S],T,[T_1,\ldots,T_n|\mathtt{X}])\mid
1004: \mathtt{X} \mbox{ is fresh}\}).
1005: \end{eqnarray*}
1006: We refer to \cite{BERS01} for the details of this calculation.
1007: \end{example}
1008:
1009:
1010:
1011: \decrease
1012: We now define {\em simply-acceptability}, which is the notion of
1013: decrease used for proving input termination.
1014:
1015: We write $p \simeq q$ if $p$ and $q$ are mutually recursive
1016: predicates \cite{Apt97}. Abusing notation, we also use $\simeq$ for
1017: {\em atoms}, where $p(\vect{s},\vect{t}) \simeq q(\vect{u},\vect{v})$
1018: stands for $p \simeq q$.
1019:
1020: \begin{definition}
1021: Let $P$ be a program, $|.|$ a moded generalised\footnote{
1022: In \cite{BERS01}, the word ``generalised'' is dropped, but
1023: here we prefer to emphasise that non-ground atoms are
1024: included in the domain.}
1025: level mapping and
1026: $I$ a simply-local model of $P$ containing $\mathit{SM}_P$.
1027: A clause \clausab\ is
1028: \emph{simply-acceptable by
1029: $|.|$ and $I$} if for
1030: every substitution $\theta$ simply-local w.r.t.~it,
1031: \[
1032: \mbox{\rm for all}\ i \in [1,n], \quad
1033: (B_1, \ldots, B_{i-1})\theta\in I \ \mbox{and} \
1034: A \simeq B_i \quad
1035: \mbox{implies} \quad |A\theta| > |B_i\theta|.
1036: \]
1037: The program $P$ is \emph{simply-acceptable by $|.|$ and $I$} if
1038: each clause of $P$ is simply-acceptable by $|.|$ and $I$.
1039: \end{definition}
1040:
1041: Admittedly, the proof obligations may be difficult to verify,
1042: especially in the cases where a small (precise) simply-local model is
1043: required. However, as our examples show, often it is not necessary at
1044: all to consider the model, as one can show the decrease for arbitrary
1045: instantiations of the clause.
1046:
1047: \comparison
1048: Unlike all other characterisations in this article,
1049: simply-acceptability is not based on ground instances of clauses, but
1050: rather on instances obtained by applying simply-local substitutions,
1051: which arise in input-consuming derivations of simply moded
1052: programs. This is also why we use {\em generalised} level mappings and
1053: a special kind of models.
1054:
1055: Also note that in contrast to recurrence and other decreasing notions
1056: to be defined later, simply-acceptability has no proof obligation on
1057: queries (apart from the requirement that queries must be simply
1058: moded). Intuitively, such a proof obligation is made redundant by the
1059: mode conditions (simply-acceptability and moded level mapping) and the
1060: fact that derivations must be input-consuming. We also refer to
1061: subsection~\ref{characterisations-subsec}.
1062:
1063:
1064: \maintheorem
1065: We can now show that this concept
1066: allows to characterise the class of input terminating programs.
1067:
1068: \begin{theorem}[\cite{BERS01}]
1069: \label{input-termination-thm}
1070: Let $P$ and $Q$ be a simply moded program and query.
1071:
1072: If $P$ is simply-acceptable by some $|.|$ and $I$,
1073: then $P$ and $Q$ input terminate.
1074:
1075: Conversely, if $P$ and every simply moded query input
1076: terminate, then $P$ is simply-acceptable
1077: by some $|.|$ and $\mathit{PM^{SL}_P}$.
1078: \end{theorem}
1079:
1080: Note that the formulation of the theorem differs slightly
1081: from the original for reasons of consistency, but one can
1082: easily see that the formulations are equivalent.
1083:
1084: The definition of input-consuming derivations is
1085: independent from the textual order of atoms in a query, and so the
1086: textual order is irrelevant for termination. This means of course that
1087: if we can prove input termination for a program and query, we have
1088: also proven termination for a program obtained by permuting the body
1089: atoms of each clause and the query in an arbitrary way. This will be
1090: seen in the next example. It would have been possible to state this
1091: explicitly in the above theorem, but that would have complicated the
1092: definition of simply-local substitution and subsequent definitions.
1093: Generally, the question of whether or not it is necessary to make the
1094: permutations of body atoms explicit is discussed in \cite{Sma99t}.
1095:
1096: \examples
1097: \begin{example}\label{ex:even-is-simply-acceptable}
1098: The program {\tt EVEN} in
1099: figure~\ref{even-prog} is simply-acceptable with modes
1100: $\tt even(\inp),\ lte(\out,\inp)$ by using the
1101: level mapping in Example~\ref{ex:even-query-is-not-recurrent},
1102: interpreted as moded {\em generalised} level mapping in the obvious
1103: way,
1104: %\begin{eqnarray*}
1105: %|\mathtt{even}(X)| & = & size(X)\\[-0.5ex]
1106: %|\mathtt{lte}(X,Y) | & = & size(Y)
1107: %\end{eqnarray*}
1108: and using any simply-local model.
1109: Moreover, the query
1110: $\tt even(X),\ lte(X,s^{100}(0))$ is permutation simply moded.
1111: Hence {\tt EVEN} and this query input terminate.
1112: \end{example}
1113:
1114: \begin{example} \label{ex:permute-is-simply-acceptable}
1115: Figure~\ref{permute-prog} shows the program {\tt PERMUTE}.
1116: Note that
1117: $\tt permute \not\simeq insert$. Assume the modes
1118: $\tt permute(\inp,\out)$, $\tt insert(\inp,\inp,\out)$. The program is
1119: readily checked to be simply-acceptable, using the moded generalised level mapping
1120: \[
1121: |\mathtt{permute}(Xs,Ys)| =
1122: |\mathtt{insert}(Xs,Ys,Zs)| = \mathit{size}(Xs)
1123: \]
1124: and any simply-local model. Thus the program and any simply moded
1125: query input terminate.
1126: It can also easily be shown that the program is not recurrent.
1127: \end{example}
1128:
1129: \begin{figure}\figrule
1130: \begin{minipage}[t]{5cm}
1131: \begin{janprogram}
1132: \%\> permute(Xs,Ys) \la \ \\
1133: \%\> \> {\rm {\tt Ys} is a permutation of the list {\tt Xs}.}\\[2mm]
1134: \> permute([X|Xs],Ys) \la \\
1135: \> \> permute(Xs,Zs), \\
1136: \> \> insert(Zs,X,Ys). \\
1137: \> permute([],[]).
1138: \end{janprogram}
1139: \end{minipage}
1140: \hfill
1141: \begin{minipage}[t]{5cm}
1142: \begin{janprogram}
1143: \%\> insert(Xs,X,Zs) \la \ \\
1144: \%\> \> {\rm {\tt Zs} is obtained by inserting {\tt X} into {\tt Xs}}.\\[2mm]
1145: %\> insert([],X,[X]). \\
1146: \> insert(Xs,X,[X|Xs]). \\
1147: \> insert([U|Xs],X,[U|Zs]) \la \\
1148: \> \> insert(Xs,X,Zs).
1149: \end{janprogram}
1150: \end{minipage}
1151: \caption{\tt PERMUTE\label{permute-prog}}
1152: \figrule\end{figure}
1153:
1154: \begin{example}\label{ex:quicksort-is-simply-acceptable}
1155: Figure~\ref{fig:qs} shows program 15.3 from \cite{SS86}: \texttt{QUICKSORT}
1156: using a form of difference lists (we permuted two body atoms for the
1157: sake of clarity). This program is simply moded with the modes
1158: $\tt quicksort(\inp,\out)$, $\tt quicksort\_dl(\inp,\out,\inp)$, $\tt
1159: partition(\inp,\inp,\out,\out)$, $\texttt{=<}(\inp,\inp)$,
1160: $\texttt{>}(\inp,\inp)$.
1161:
1162: Let $|.|$ be the list-length function (see subsection~\ref{norms-subsec}).
1163: We use the following moded generalised level mapping (positions with
1164: $\_$ are irrelevant)
1165: \begin{eqnarray*}
1166: |\mathtt{quicksort\_dl}(Xs,\_,\_)| &=& |Xs|,\\
1167: |\mathtt{partition}(Xs,\_,\_,\_)| &=& |Xs|.
1168: \end{eqnarray*}
1169: The level mapping of all other atoms
1170: can be set to 0. Concerning the model, the simplest solution is to use
1171: the model that expresses the dependency between the list lengths of
1172: the arguments of $\mathtt{partition}$, i.e., $I$ should
1173: contain all atoms of the form
1174: $\mathtt{partition}(S_1,X,S_2,S_3)$ where
1175: $|S_1| \geq |S_2|$ and
1176: $|S_1| \geq |S_3|$ ($|.|$ being the list-length function).
1177: Note that this includes all simply-moded atoms using
1178: $\mathtt{partitition}$, and that this model is a fortiori
1179: simply-local since (\ref{SL-model-eq}) in
1180: Definition~\ref{sl-model-def} is true even for arbitrary
1181: $\theta$.
1182:
1183:
1184: The program is then simply-acceptable by $|.|$ and $I$ and hence
1185: input terminates for every simply moded query.
1186: \end{example}
1187:
1188: \begin{figure}\figrule
1189: \begin{program}
1190: \% \> quicksort(Xs, Ys) \la Ys {\rm is an ordered permutation of } Xs.
1191: \\[2mm]
1192: \> quicksort(Xs,Ys) \la quicksort\_dl(Xs,Ys,[]).\\[2mm]
1193: \> quicksort\_dl([X|Xs],Ys,Zs) \la \\
1194: \> \> partition(Xs,X,Littles,Bigs),\\
1195: \> \> quicksort\_dl(Bigs,Ys1,Zs). \\ %\> \% atom a2 \\
1196: \> \> quicksort\_dl(Littles,Ys,[X|Ys1]),\\ %\hspace{2cm}\= \% atom a1\\
1197: \> quicksort\_dl([],Xs,Xs).\\[2mm]
1198: \> partition([X|Xs],Y,[X|Ls],Bs) \la X =< Y, partition(Xs,Y,Ls,Bs).\\
1199: \> partition([X|Xs],Y,Ls,[X|Bs]) \la X > Y, partition(Xs,Y,Ls,Bs).\\
1200: \> partition([],Y,[],[]).
1201: \end{program}
1202: \caption{\texttt{QUICKSORT}\label{fig:qs}}
1203: \figrule\end{figure}
1204:
1205:
1206: \section{Local Delay Termination}\label{local-sec}
1207: \limitation The class of programs and queries that terminate for all
1208: input-consuming derivations is considerable, but there are still many
1209: interesting programs not contained in it.
1210:
1211: \begin{example} \label{ex:ic-strictly-lds}
1212: Consider again the {\tt PERMUTE} program
1213: (figure~\ref{permute-prog}), but this time assume the mode
1214: $\tt permute(\out,\inp), \tt insert(\out, \out, \inp)$.
1215: Consider also the query $\tt permute(X,[1])$. It is easy to check
1216: that there is an infinite {\em input-consuming} derivation for this
1217: query obtained by selecting always the leftmost atom that can be
1218: selected. In fact, \texttt{PERMUTE} in this mode
1219: cannot be simply-acceptable,
1220: not even after reordering of atoms in clause bodies.
1221: To see this, we first reorder the body atoms of the recursive clause
1222: to obtain
1223: \begin{janprogram}
1224: \> permute([X|Xs],Ys) \la \\
1225: \> \> insert(Zs,X,Ys), \\
1226: \> \> permute(Xs,Zs).
1227: \end{janprogram}
1228: so that the program is simply moded and thus our method
1229: showing input termination is applicable in principle. Now
1230: $\mathit{PM}^{SL}_\mathtt{PERMUTE}$ contains every atom of the form
1231: $\mathtt{insert}(\mathtt{Us},\mathtt{U},\mathit{Vs})$, i.e., every simply moded
1232: atom whose predicate is $\mathtt{insert}$. Therefore in particular
1233: $\mathtt{insert}(\mathtt{Us},\mathtt{U},\mathtt{Vs})
1234: \in \mathit{PM}^{SL}_\mathtt{PERMUTE}$ (note that $\mathtt{Vs}$ is a
1235: variable). The substitution
1236: $\theta = \{\tt Ys/Vs, Zs/Us, X/U \}$ is simply-local w.r.t.~the
1237: clause. Therefore, for the clause to be simply-acceptable,
1238: there would have to be a moded generalised level mapping such that
1239: $\tt |permute([U|Xs],Vs)| > |permute(Xs,Us)|$. This is a contradiction
1240: since a {\em moded} generalised level mapping is necessarily defined
1241: as a generalised norm of the second argument of $\mathtt{permute}$,
1242: and $\mathtt{Vs}$ and $\mathtt{Us}$ are equivalent modulo variance.
1243:
1244: However, all derivations for this query are finite w.r.t.~the RD
1245: selection rule, which for this example happens to be an instance of
1246: the selection rules considered in this section.
1247: \end{example}
1248:
1249: \termination
1250: Marchiori and Teusink \shortcite{MT99} have considered local selection
1251: rules controlled by delay declarations. They define a {\em safe delay
1252: declaration} so that an atom can be selected only when it is bounded
1253: w.r.t.~a level mapping. In order to avoid even having to define delay
1254: declarations, we take a shortcut, by defining the following.
1255:
1256: \begin{definition}\label{delay-safe-def}
1257: A selection rule is {\em delay-safe (w.r.t.~$|.|$)} if it specifies
1258: that an atom $A$ can be selected only when $A$ is bounded
1259: w.r.t.~$|.|$.
1260: \end{definition}
1261:
1262: Note that delay-safe selection rules imply that the depth of the
1263: SLD-tree of the selected atom does not depend on further instantiation
1264: as in the previous section.
1265:
1266: \begin{definition} \label{c2:def:ldst}
1267: A program $P$ and query $Q$ {\em local delay terminate}
1268: (w.r.t.~$|.|$) if they universally terminate w.r.t.~the set of
1269: selection rules that are both local and delay-safe (w.r.t.~$|.|$).
1270: \end{definition}
1271:
1272: \contrived Unlike in the previous section, modes are not used
1273: explicitly in the definition of delay-safe selection rules.
1274: Therefore it is possible to invent an example of a program and a query
1275: that input terminate but do not local delay terminate. Such an
1276: example is of course contrived, in that the level mapping is chosen
1277: in an inappropriate way.
1278:
1279: \begin{example}\label{ex:ic-yes-lds-no}
1280: The {\tt APPEND} program and the query
1281: {\tt append([],[],X),\ append(X,[],Y)}
1282: input terminate for the mode
1283: {\tt append(\inp,\inp,\out)}. However, they do not local delay
1284: terminate w.r.t.~a level mapping $|.|$ such that $|A| = 0$ for every
1285: $A$ (e.g., consider the RD selection rule).
1286: \end{example}
1287:
1288: However, in section~\ref{relations-sec} we will see
1289: that under natural assumptions (in particular, the
1290: level mapping must be moded) delay-safe selection rules are
1291: also input-consuming. Then, input termination implies
1292: local delay termination, and as is witnessed by
1293: Example~\ref{ex:ic-strictly-lds}, this implication is strict.
1294:
1295: \onlyhere{Information on Data Flow: Covers}
1296: Delay-safe selection rules ensure that selected atoms are bounded.
1297: To ensure that the level mapping {\em decreases} during a derivation,
1298: we exploit additional information provided by a model of the program.
1299: Given an atom $B$ in a query, we are interested in other atoms that
1300: share variables with $B$, so that instantiating these variables makes
1301: $B$ bounded. A set of such atoms is called a {\em direct cover}. The only way
1302: of making $B$ bounded is by resolving away one of its direct covers.
1303: The formal definition is as follows.
1304:
1305: \begin{definition}\label{cover-def}
1306: Let $|.|$ be a level mapping, $A \la Q$ a clause containing a body
1307: atom $B$, and $\tilde{C}$ a subset\footnote{By abuse of terminology,
1308: here we identify a query with the set of atoms it contains.}
1309: of $Q$ such that $B \not \in
1310: \tilde{C}$. We say that $\tilde{C}$ is a {\em direct cover for $B$
1311: (w.r.t.~$A \la Q$ and $|.|$)} if there exists a substitution
1312: $\theta$ such that $B\theta$ is bounded w.r.t.~$|.|$ and
1313: $\dom(\theta) \subseteq \vars(A,\tilde{C})$.
1314:
1315: A direct cover is {\em minimal} if no proper subset is a direct
1316: cover.
1317: \end{definition}
1318:
1319: Note that the above concept is similar to well-modedness, assuming a
1320: moded level mapping. In this case, for each atom, the atoms to the
1321: left of it are a direct cover. This generalises in the obvious way to
1322: {\em permutation} well moded queries.
1323:
1324: Considering an atom $B$, we have said that the only way of making $B$
1325: bounded is by resolving away one of $B$'s direct covers. However, for an
1326: atom in a direct cover, say atom $A$, to be selected, $A$ must be
1327: bounded, and the only way of making $A$ bounded is by resolving away
1328: one of $A$'s direct covers. Iterating this reasoning gives rise to
1329: a kind of closure of the notion of direct cover.
1330:
1331: \begin{definition}
1332: Let $|.|$ be a level mapping and $A \la Q$ a clause.
1333: Consider the least set $\cal C$, subset of
1334: ${\mathcal P}(Q \times {\mathcal P}(Q))$, such that
1335: \begin{enumerate}
1336: \item
1337: $\langle B, \emptyset \rangle \in {\cal C}$ whenever $B$ has
1338: $\emptyset$ as minimal direct cover for $B$ in $A \la Q$;
1339: \item
1340: $\langle B, \tilde{C} \rangle \in {\cal C}$ whenever
1341: $B\not\in \tilde{C}$, and
1342: $\tilde{C} = \{C_1,\dots,C_k\}\cup \tilde{D}_1 \cup \dots \tilde{D}_k$,
1343: where $\{C_1,\dots,C_k\}$ is a minimal direct
1344: cover of $B$ in $A \la Q$, and for $i \in [1,k]$,
1345: $\langle C_i,\tilde{D}_i\rangle \in {\cal C}$.
1346: \end{enumerate}
1347: The set
1348: $Covers(A \la Q) \subseteq Q \times {\mathcal P}(Q)$
1349: is defined as the set obtained by deleting from ${\cal
1350: C}$ each element of the form $\langle B, \tilde{C} \rangle$ if there
1351: exists another element of ${\cal C}$ of the form $\langle B,
1352: \tilde{C}' \rangle$ such that $\tilde{C}' \subset \tilde{C}$.
1353:
1354: We say that $\tilde{C}$ is a {\em cover for $B$ (w.r.t.~$A \la Q$ and
1355: $|.|$)} if $\langle B, \tilde{C} \rangle$ is an element of
1356: $Covers(A \la Q)$.
1357: \end{definition}
1358:
1359: \decrease
1360: The following concept is used to show that programs terminate
1361: for local and delay-safe selection rules. We present a definition slightly
1362: different from the original one \cite{MT99}, albeit equivalent.
1363:
1364: \begin{definition}\label{delay-recurrent}
1365: Let $|.|$ be a level mapping and $I$ a Herbrand interpretation.
1366: A program $P$ is \emph{delay-recurrent by $|.|$ and $I$} if
1367: $I$ is a model of $P$, and for
1368: every clause $\cequals A \la \tn{B}{n}$ of $P$, for every $i \in [1,n]$,
1369: for every cover $\tilde{C}$ for $B_i$, for every substitution
1370: $\theta$ such that $c\theta$ is ground,
1371: \[ \mbox{if} \ \ I \Mo \tilde{C}\theta \ \
1372: \mbox{then} \ \ |A\theta| > |B_i\theta|.
1373: \]
1374: \end{definition}
1375:
1376: We believe that this notion should have better been called {\em
1377: delay-acceptable}, since the convention is to call decreasing notions
1378: that involve models {\em (\dots)-acceptable}, and the ones that do not
1379: involve models {\em (\dots)-recurrent}.
1380:
1381: The most essential
1382: differences between delay-recurrence and simply-acceptability are that
1383: the former is based on models, whereas the latter is based on
1384: simply-local models, and that the former requires decreasing for
1385: all body atoms, whereas the latter only for mutually recursive calls.
1386:
1387: Just as simply-acceptability, delay-recurrence imposes no proof
1388: obligation on queries. Such a proof obligation is made redundant by
1389: the fact that selected atoms must be bounded. Note that if no most
1390: recently introduced atom in a query is bounded, we obtain termination
1391: by deadlock.
1392: We also refer to subsection~\ref{characterisations-subsec}.
1393:
1394: \maintheorem
1395: In order for delay-recurrence to ensure termination, it is crucial
1396: that when an atom is selected, its cover is resolved away completely
1397: (this allows to use the premise $I \models \tilde{C}\theta$ in
1398: Definition~\ref{delay-recurrent}). To this end, local selection rules must
1399: be adopted. We can now state the result of this section.
1400:
1401:
1402: \begin{theorem}[\cite{MT99}]\label{local-thm}
1403: Let $P$ be a program.
1404:
1405: If $P$ is delay-recurrent by a level mapping $|.|$ and a Herbrand
1406: interpretation $I$, then for every query $Q$, $P$ and $Q$ local
1407: delay terminate.
1408: \end{theorem}
1409:
1410: \subsection{Example}
1411: \begin{example}\label{permute-is-delay-recurrent-ex}
1412: Consider again {\tt PERMUTE} (figure~\ref{permute-prog}),
1413: with the level mapping and model
1414: \begin{eqnarray*}
1415: |\mathtt{permute}(xs,ys)| & = & |ys| + 1\\[-0.5ex]
1416: |\mathtt{insert}(xs,ys,zs)| & = & |zs|\\[0.5ex]
1417: I & = &
1418: \{ \mathtt{permute}(xs,ys) \mid |xs| = |ys| \} \U \\[-0.5ex]
1419: & &
1420: \{ \mathtt{insert}(xs,y,zs) \mid |zs| = |xs| + 1 \}.
1421: \end{eqnarray*}
1422: The program is delay-recurrent by $|.|$ and $I$. We check the
1423: recursive clause for $\tt permute$. Consider an arbitrary ground instance
1424: \begin{equation} \label{permuteexcit}
1425: \mathtt{permute}([x|xs],ys) \la \mathtt{permute}(xs,zs),\
1426: \mathtt{insert}(zs,x,ys).
1427: \end{equation}
1428: First, we observe that $I$ is a model of this instance. In fact, if
1429: its body is true in $I$, then
1430: $|ys| = |zs| + 1$ and
1431: $|xs| = |zs|$. This implies $|ys| = |xs| + 1$, and hence
1432: $\mathtt{permute}([x|xs],ys)$ is true in $I$.
1433:
1434: Let us now show the decrease from the head to the $\tt permute$ body
1435: atom. There is only one cover $\tt insert(Zs,X,Ys)$, so we must
1436: show that
1437: \[
1438: |ys| = |zs| + 1 \quad \mbox{implies} \quad |ys| + 1 > |zs| + 1,
1439: \]
1440: which is clearly true. Now consider the second body atom. It has
1441: an empty cover. This time, for every instance of the clause such that
1442: the head is ground, we have that $|ys| + 1 > |ys|$. Hence we have
1443: shown that the clause is delay-recurrent.
1444: %, and so
1445: %for every $Q$, every local and delay-safe derivation is
1446: %finite.
1447:
1448: It is interesting to compare this to Example~\ref{ex:ic-strictly-lds},
1449: where we were not able to show a decrease.
1450: \end{example}
1451:
1452: \incompleteness
1453: Note that delay-recurrence is a sufficient but not necessary condition
1454: for local delay termination. The limitation lies in the notion of
1455: cover: to make an atom bounded, one has to resolve one of its covers;
1456: but conversely, it is not true that resolving any cover will make the
1457: atom bounded.
1458:
1459: \begin{example} \label{ex:delay-recursive-incomplete}
1460: Consider the following simple program
1461: \begin{janprogram}
1462: \> z $\la$ p(X), q(X), r(X).\\
1463: \> p(0).\\
1464: \> q(s(X)) $\la$ q(X).\\
1465: \> r(X).
1466: \end{janprogram}
1467: The program and any query $Q$ local delay terminate w.r.t.~the level
1468: mapping:
1469: \[
1470: \begin{array}{c}
1471: |\mathtt{z}| = |\mathtt{p}(t)| = |\mathtt{r}(t)| = 0\\
1472: |\mathtt{q}(t)| = size(t)
1473: \end{array}
1474: \]
1475: In fact, the only source of non-termination for a query might be an atom
1476: {\tt q($X$)}. However, for any such atom selected
1477: by a delay-safe selection rule, $X$ is a ground term. Hence the
1478: recursive clause in the program cannot generate an infinite
1479: derivation. On the other hand, it is not the case that the program is
1480: delay-recurrent. Consider, in fact, the first clause. Since {\tt r(X)}
1481: is a cover for {\tt q(X)}, we would have to show for some $|.|'$ that
1482: for every $t$:
1483: \[
1484: |\tt z|' > |\mathtt{q}(t)|'.
1485: \]
1486: This is impossible, since delay-recurrence on the third clause implies
1487: $|\mathtt{q}(\mathtt{s}^k(0))|' \geq k$ for any natural $k$.
1488: \end{example}
1489:
1490:
1491:
1492:
1493: \section{Left-Termination}\label{left-sec}
1494: \limitation
1495: In analogy to previous sections, we should start this section with an
1496: example illustrating that the assumption of local delay-safe selection
1497: rules is sometimes too weak to ensure termination, and thereby
1498: motivate the ``stronger'' assumption of the LD selection rule.
1499: Such an example can easily be given.
1500:
1501: \begin{example}\label{ex:lds-strictly-left}
1502: Consider the program
1503: \begin{janprogram}
1504: \> p $\la$ q, p.
1505: \end{janprogram}
1506: with query $\tt p$, where $\tt |p| = |q| = 0$.
1507: It left-terminates but does not local delay terminate.
1508: \end{example}
1509:
1510: However, the example is somewhat artificial, and in fact, we believe
1511: that assuming the LD selection rule is only slightly stronger than
1512: assuming an arbitrary local delay-safe selection rule, as far as
1513: termination is concerned. Nevertheless, there are several reasons for
1514: studying this selection rule in its own right. First, the conditions
1515: for termination are easier to formulate than for local delay
1516: termination. Secondly, the vast majority of works consider this rule,
1517: being the standard selection rule of Prolog. Finally, for the class of
1518: programs and queries that terminate w.r.t. the LD selection rule we
1519: are able to provide a sound and complete characterisation.
1520:
1521: \termination
1522:
1523: \begin{definition} \label{c2:def:leftt}
1524: A program $P$ and query $Q$ {\em left-terminate\/} if they
1525: universally terminate w.r.t.~the set consisting of only the LD
1526: selection rule.
1527: \end{definition}
1528:
1529: \contrived
1530: Formally comparing this class to the two previous
1531: ones is difficult. In particular,
1532: left-termination is not necessarily
1533: stronger than input or local delay termination.
1534:
1535: \begin{example} \label{ex:lds-yes-left-no}
1536: We have shown in Example~\ref{permute-is-delay-recurrent-ex} that
1537: {\tt PERMUTE} and every query local delay terminate w.r.t.~the level
1538: mapping given there.
1539: Moreover, no derivation deadlocks. However, {\tt PERMUTE}
1540: and the query $\tt permute(X,[1])$ do not left
1541: terminate. Similarly to Example~\ref{ex:ic-strictly-lds}, this example is
1542: contrived since the program is intended for the RD selection rule.
1543:
1544: One could easily construct a similar example comparing left
1545: termination with input termination.
1546: \end{example}
1547:
1548: Also, local delay termination may not imply left-termination
1549: because of the deadlock problem.
1550:
1551: \incompleteness
1552: Left-termination was addressed by Apt \& Pedreschi \shortcite{AP93r},
1553: who introduced the class of acceptable logic programs. However, their
1554: characterisation encountered a completeness problem similar to the one
1555: highlighted for Theorem~\ref{c2:rec:thm}.
1556:
1557: \begin{example} \label{transp-ex}
1558: Figure~\ref{transp-prog} shows {\tt TRANSP}, a program that terminates on
1559: a strict subset of ground queries only.
1560: In the intended meaning of the program,
1561: $\mathtt{trans}(x,y,e)$ succeeds iff
1562: $x \leadsto_e y$, i.e.~if $\mathtt{arc}(x,y)$ is
1563: in the transitive closure of a direct acyclic graph (DAG) $e$, which
1564: is represented as a list of arcs. It is readily checked that if $e$ is
1565: a graph that contains a cycle, infinite derivations may occur.
1566: \begin{figure}\figrule
1567: \begin{minipage}[t]{5cm}
1568: \begin{janprogram}
1569: \%\> trans($x$,$y$,$e$) \la \mbox{\rm $x \leadsto_e y$ for a DAG $e$}\\[2ex]
1570: \> trans(X,Y,E) \la\\
1571: \> \> member(arc(X,Y),E).\\[2ex]
1572: \> trans(X,Y,E) \la\\
1573: \> \> member(arc(X,Z),E), trans(Z,Y,E).
1574: \end{janprogram}
1575: \end{minipage}
1576: \hfill
1577: \begin{minipage}[t]{5cm}
1578: \begin{janprogram}
1579: \\[2ex]
1580: \> member(X,[X|Xs]).\\[2ex]
1581: \> member(X,[Y|Xs]) \la\\
1582: \> \> member(X,Xs).
1583: \end{janprogram}
1584: \end{minipage}
1585: \caption{\tt TRANSP\label{transp-prog}}
1586: \figrule\end{figure}
1587:
1588: In the approach by Apt \& Pedreschi, {\tt TRANSP} cannot be reasoned
1589: about, since the same incompleteness problem as for recurrent programs
1590: occurs, namely that they characterise a class of programs that
1591: (left-)terminate for every ground query.
1592: \end{example}
1593:
1594: %\onlyhere{Extended level mappings}
1595: The cause of the restricted form of completeness of
1596: Theorem~\ref{c2:rec:thm} lies in the use of level mappings, which must
1597: specify a natural number for every ground atom --- hence termination is
1598: forced for every ground query. A more subtle problem with using level
1599: mappings is that one must specify values also for {\em uninteresting
1600: atoms}, such as $\mathtt{trans}(x,y,e)$ when $e$ is not a DAG.
1601: The solution to both problems is to consider
1602: {\em extended} level mappings~\cite{Rug97t,Rug99}.
1603:
1604: \begin{definition} \label{c2:def:lm}
1605: An {\em extended level mapping\/} is a function $|.|:B_L \ra
1606: \nat^{\infty}$ of ground atoms to $\nat^{\infty}$, where
1607: $\nat^{\infty} = \nat \U \{ \infty \}$.
1608: \end{definition}
1609:
1610: The inclusion of $\infty$ in the codomain is intended to model
1611: non-termination and uninteresting instances of program clauses.
1612: First, we extend the $>$ order on $\nat$ to a relation $\ma$ on
1613: $\nat^{\infty}$.
1614:
1615: \begin{definition} \index{$\ma$}
1616: We define $n \ma m$ for $n, m \in \nat^{\infty}$ iff $n = \infty$ or
1617: $n > m$. We write $n \maeq m$ iff $n \ma m$ or $n = m$.
1618: \end{definition}
1619:
1620: \decrease
1621: Therefore, $\infty \ma m$ for every $m \in \nat^{\infty}$.
1622: With this additional notation we are now ready to introduce (a revised
1623: definition of) acceptable programs and queries. A program $P$ is
1624: acceptable \index{acceptable programs} if for every ground instance of
1625: a clause from $P$, the level of the head is greater than the level of
1626: each atom in the body such that the body atoms to its left are true in
1627: a Herbrand model of the program.
1628:
1629: \begin{definition} \label{c2:def:accp}\label{c2:def:accq}
1630: Let $|.|$ be an extended level mapping, and $I$ a Herbrand
1631: interpretation. A program $P$ is \emph{acceptable by $|.|$ and
1632: $I$} if $I$ is a model of $P$, and for every \clausab\ in
1633: $\groun{L}{P}$:
1634: \[
1635: \mbox{\rm for all}\ i \in [1,n], \quad
1636: I \Mo B_1, \ldots, B_{i-1} \quad
1637: \mbox{implies} \quad |A| \ma |B_i|.
1638: \]
1639: A query $Q$ is {\em acceptable by $|.|$ and $I$\/} if there exists
1640: $k \in \nat$ such that for every $\tn{A}{n}$ $\in$ $\groun{L}{Q}$:
1641: \[
1642: \mbox{\rm for all}\ i \in [1,n], \quad
1643: I \Mo A_1, \ldots, A_{i-1} \quad
1644: \mbox{implies} \quad k\ \ma |A_i|.
1645: \]
1646: \end{definition}
1647:
1648: \comparison
1649: Let us compare this definition with the
1650: definition of delay-recurrence (Definition~\ref{delay-recurrent}). In
1651: the case of local and delay-safe selection rules, an atom cannot be
1652: selected before one of its covers is completely resolved. In the case
1653: of the LD selection rule, an atom cannot be selected before the atoms
1654: to its left are completely resolved. Because of the correctness of LD
1655: resolution~\cite{Apt97}, this explains why, in both cases, a decrease
1656: is only required if the instance of the cover, resp.~the instance of
1657: the atoms to the left, are in some model of the program. We also
1658: refer to subsection~\ref{characterisations-subsec}.
1659:
1660: \maintheorem
1661: Acceptable programs and queries precisely characterise left-termination.
1662:
1663: %\removebrackets
1664: \begin{theorem}[\cite{AP93r,Rug97t}] \label{c2:acc:tcor}
1665: Let $P$ be a program and $Q$ a query.
1666:
1667: If $P$ and $Q$ are both acceptable by an extended level mapping $|.|$
1668: and a Herbrand interpretation $I$, then $P$ and $Q$ left-terminate.
1669:
1670: Conversely, if $P$ and $Q$ left-terminate, then there exist
1671: an extended level mapping $|.|$ and a Herbrand interpretation $I$
1672: such that $P$ and $Q$ are both acceptable by $|.|$ and $I$.
1673: \end{theorem}
1674:
1675:
1676: \subsection{Example}
1677: \begin{example} \label{ex:transp-is-acceptable}
1678: We will show that {\tt TRANSP} is acceptable. We have pointed out
1679: that in the intended use of the program, $e$ is supposed to be a
1680: DAG. We define:
1681: \begin{eqnarray*}
1682: |\mathtt{trans}(x,y,e)| & = &
1683: \left\{
1684: \begin{array}{ll}
1685: |e| + 1 + Card \{ v \mid x \leadsto_e v \}
1686: & \mbox{if $e$ is a DAG}\\
1687: \infty & \mbox{otherwise}\\
1688: \end{array}
1689: \right. \\[-0.5ex]
1690: |\mathtt{member}(x,e)| & = & |e|\\[0.5ex]
1691: I & = &
1692: \{ \mathtt{trans}(x,y,e) \mid x, y, e \in U_L \} \U \\[-0.5ex]
1693: & &
1694: \{ \mathtt{member}(x,e) \mid x\ \mbox{is in the list}\ e \}.
1695: \end{eqnarray*}
1696: where $Card$ is the set cardinality operator. It is easy to
1697: check that {\tt TRANSP} is acceptable by $|.|$ and $I$. In
1698: particular, consider a ground instance of the second clause:
1699: \[
1700: \mathtt{trans}(x,y,e) \la
1701: \mathtt{member}(\mathtt{arc}(x,z),e), \mathtt{trans}(z,y,e).
1702: \]
1703: It is immediate to see that $I$ is a model of it. In addition, we
1704: have the proof obligations:
1705: \begin{eqnarray*}
1706: \mbox{\it (i)\/}& & |\mathtt{trans}(x,y,e)| \ma
1707: |\mathtt{member}(\mathtt{arc}(x,z),e)|\\
1708: \mbox{\it (ii)\/} & \mathtt{arc}(x,z)\ \mbox{is in}\ e \ \Ra &
1709: |\mathtt{trans}(x,y,e)| \ma
1710: |\mathtt{trans}(z,y,e)|.
1711: \end{eqnarray*}
1712: The first one is easy to show since
1713: $|\mathtt{trans}(x,y,e)| \ma |e|$.
1714: Considering the second one, we distinguish two cases.
1715: If $e$ is not a DAG, the conclusion is immediate. Otherwise,
1716: $\mathtt{arc}(x,z)$ in $e$ implies that
1717: $Card \{ v \mid x \leadsto_e v \} >
1718: Card \{ v \mid z \leadsto_e v \}$, and so:
1719: \begin{eqnarray*}
1720: |\mathtt{trans}(x,y,e)|
1721: & = & |e| + 1 + Card \{ v \mid x \leadsto_e v \} \\
1722: & \ma & |e| + 1 + Card \{ v \mid z \leadsto_e v \} =
1723: |\mathtt{trans}(z,y,e)|.
1724: \end{eqnarray*}
1725: Finally, observe that for a DAG $e$, the queries
1726: $\mathtt{trans}(x,\mathtt{Y},e)$ and
1727: $\mathtt{trans}(\mathtt{X,Y},e)$ are acceptable by $|.|$ and $I$.
1728: The first one is intended to compute all nodes $y$ such
1729: that $x \leadsto_e y$, while the second one computes the binary
1730: relation $\leadsto_e$.
1731: Therefore, the {\tt TRANSP} program and those queries
1732: left-terminate.
1733:
1734: \label{ex:strong-strictly-left}
1735: Note that this is of course also an example of a program and a query which
1736: left-terminate but do not strongly terminate (e.g., consider the RD
1737: selection rule).
1738: \end{example}
1739:
1740:
1741: \section{$\exists$-Termination} \label{c2:sec:ex}\label{exists-sec}
1742: \limitation
1743: So far we have considered four classes of terminating programs, making
1744: increasingly strong assumptions about the selection rule, or in other
1745: words, considering in each section a smaller set of selection rules. In the
1746: previous section we have arrived at a singleton set containing the LD
1747: selection rule. Therefore we can clearly not strengthen our
1748: assumptions, in the same sense as before, any further.
1749:
1750: We will now consider an assumption about the selection rule which is
1751: equally abstract as assuming {\em all} selection rules
1752: (section~\ref{strong-sec}).
1753: We introduce {\em $\exists$-termination\/} of logic
1754: programs, claiming that it is an essential concept for separating the
1755: {\em logic\/} and {\em control} aspects of a program.
1756:
1757: Before, however, we motivate the limitations of left-termination.
1758:
1759: \begin{example} \label{ex:left-strictly-exists}
1760: The program {\tt PRODCONS} in figure~\ref{prodcons-prog}
1761: abstracts a (concurrent) system
1762: composed of a producer and a consumer.
1763: For notational convenience, we identify the term {\tt s$^n$(0)} with
1764: the natural number $n$. Intuitively, {\tt prod} is the producer of a
1765: non-deterministic sequence of $1$'s and $2$'s, and {\tt cons} the
1766: consumer of the sequence. The shared variable {\tt Bs} in clause
1767: {\it (s)\/} acts as an unbounded buffer.
1768: The overall system is started by the query $\mathtt{system}(n)$. Note
1769: that the program is well moded with the obvious mode
1770: $\{\tt prod(\out), cons(\inp,\inp), wait(\inp)\}$, but assuming LD
1771: (and hence, input-consuming) derivations does not ensure
1772: termination. The crux is that {\tt prod} can produce a message
1773: sequence of arbitrary length. Now {\tt cons} can only consume a message
1774: sequence of length $n$, but for this to ensure termination, atoms
1775: using $\tt cons$ must be eventually selected.
1776: We will see that a selection rule exists for which this program and
1777: the query $\mathtt{system}(n)$ terminate.
1778: \end{example}
1779:
1780: \begin{figure}\figrule
1781: \begin{minipage}[t]{5cm}
1782: \begin{programma}
1783: {\it (s)\/}\> system(N) \la\\
1784: \> \> prod(Bs), cons(Bs,N).\\[2mm]
1785: {\it (p1)\/}\> prod([s(0)|Bs])) \la \\
1786: \> \> prod(Bs).\\
1787: {\it (p2)\/}\> prod([s(s(0))|Bs])) \la \\
1788: \> \> prod(Bs).\\
1789: {\it \/}\> prod([]).
1790: \end{programma}
1791: \end{minipage}
1792: \hfill
1793: \begin{minipage}[t]{5cm}
1794: \begin{programma}
1795: {\it (c)\/}\> cons([D|Bs],s(N)) \la \\
1796: \> \> cons(Bs,N), wait(D).\\
1797: {\it \/}\> cons([], 0).\\[2mm]
1798: {\it (w)\/}\> wait(s(D)) \la \\
1799: \> \> wait(D). \\
1800: {\it \/} \> wait(0).
1801: \end{programma}
1802: \end{minipage}
1803: \caption{\tt PRODCONS\label{prodcons-prog}}
1804: \figrule\end{figure}
1805:
1806: \termination
1807: We introduce next the notion of $\exists$-termination.
1808:
1809: \begin{definition}\label{c2:def:eut}
1810: A program $P$ and a query $Q$ $\exists$-terminate if there exists a
1811: non-empty set ${\cal S}$ of standard selection rules such that $P$
1812: and $Q$ universally terminate w.r.t.~$\cal S$.
1813: \end{definition}
1814:
1815: %\onlyhere{On the notion of ``existence''}
1816: If $P$ and $Q$ do not $\exists$-terminate, then
1817: no standard selection rule can be terminating. For extensions of the
1818: standard definition of selection rule, such as input-consuming and
1819: delay-safe rules, this is not always true.
1820:
1821: \begin{example} \label{ex:ic-or-lds-not-imply-exists}
1822: The simple program
1823: \begin{janprogram}
1824: \> p(s(X)) $\la$ p(X).\\
1825: \> p(X).
1826: \end{janprogram}
1827: with mode $\tt p(\inp)$ and query $\tt p(X)$ input
1828: terminates, but does not $\exists$-terminate.
1829: The same program and query
1830: local delay terminate (w.r.t.~$|${\tt p($t$)}$| = size(t)$).
1831: \end{example}
1832:
1833: In section~\ref{relations-sec}, we will show that {\em permutation
1834: well-modedness} is a sufficient condition to ensure that if $P$ and
1835: $Q$ input terminate then they $\exists$-terminate.
1836:
1837:
1838: Here, we observe that $\exists$-termination coincides with
1839: universal termination w.r.t. the set of fair selection rules.
1840: Therefore, any fair selection rule is a terminating control for any
1841: program and query for which a terminating control exists.
1842:
1843: %\removebrackets
1844: \begin{theorem}[\cite{RugTCS98,Rug99}] \label{c2:fair:unifair}
1845: A program $P$ and a query $Q$ $\exists$-terminate
1846: iff they universally terminate w.r.t.~the set of fair selection rules.
1847: \end{theorem}
1848:
1849: Concerning Example~\ref{ex:left-strictly-exists}, it can be said that
1850: viewed as a concurrent system, the program inherently
1851: relies on fairness for termination.
1852:
1853: \decrease
1854: Ruggieri \shortcite{RugTCS98,Rug99} offers a characterisation of
1855: $\exists$-termination using the notion of {\em fair-bounded\/}
1856: programs and queries. Just as
1857: Definition~\ref{c2:def:accp}, it is based on {\em extended} level mappings.
1858:
1859: \begin{definition} \label{c2:def:fairp} \label{c2:def:fairq}
1860: Let $|.|$ be an extended level mapping, and $I$ a Herbrand interpretation. A
1861: program $P$ is \emph{fair-bounded by $|.|$ and $I$} if $I$ is
1862: a model of $P$ such that for every $\clausab$ in $\groun{L}{P}$:
1863: \begin{enumerate}
1864: \item[{\em (a)\/}]
1865: $I \Mo \tn{B}{n}
1866: \ \mbox{\rm implies that for every}\
1867: i \in [1,n],\
1868: |A| \ma |B_i|$, and
1869: \item[{\em (b)\/}]
1870: $I \not \models \tn{B}{n}
1871: \ \mbox{implies that there exists}\
1872: i \in [1,n]
1873: \ \mbox{with}\
1874: I \not \models B_i \A |A| \ma |B_i|$.
1875: \end{enumerate}
1876:
1877: A query $Q$ is {\em fair-bounded by $|.|$ and $I$\/} if there exists
1878: $k \in \nat$ such that for every $\tn{A}{n} \in \groun{L}{Q}$:
1879: \begin{enumerate}
1880: \item[{\em (a)\/}]
1881: $I \Mo A_1, \ldots, A_n
1882: \ \mbox{\rm implies that for every}\
1883: i \in [1,n],\
1884: k \ma |A_i|$, and
1885: \item[{\em (b)\/}]
1886: $I \not \models A_1, \ldots, A_n
1887: \ \mbox{implies that there exists}\
1888: i \in [1,n]
1889: \ \mbox{with}\
1890: I \not \models A_i \A k \ma |A_i|$.
1891: \end{enumerate}
1892: \end{definition}
1893:
1894: Note that the hypotheses of conditions {\it (a)\/} and {\it (b)\/}
1895: are {\em mutually exclusive\/}.
1896:
1897: \comparison
1898: Let us discuss in more detail the meaning of proof obligations {\it
1899: (a)\/} and {\it (b)\/} in Definition~\ref{c2:def:fairp}. Consider a
1900: ground instance $\clausab$ of a clause.
1901:
1902: If the body \tn{B}{n} is true in the model $I$, then there might exist a
1903: SLD-refutation for it. Condition {\it (a)\/} is then intended to bound the
1904: length of the refutation.
1905:
1906: If the body is not true in the model $I$, then it cannot have a
1907: refutation. In this case, termination actually means that there is an
1908: atom in the body that has a finitely failed SLD-tree.
1909: Condition {\it (b)\/} is then intended to bound the depth of the finitely failed
1910: SLD-tree. As a consequence of this, the complement of $I$ is
1911: necessarily included in the finite failure set of the program.
1912:
1913: Compared to acceptability, the model and the extended level mapping in
1914: the proof of fair-boundedness have to be chosen more carefully, due to
1915: more binding proof obligations. As we will see in
1916: section~\ref{relations-sec}, however, the simpler proof obligations of
1917: recurrence and acceptability are sufficient conditions for proving
1918: fair-boundedness.
1919: Note also that, as in the case of
1920: acceptable programs, the inclusion of $\infty$ in the codomain of
1921: extended level mapping allows for excluding {\em unintended atoms\/}
1922: and {\em non-terminating atoms\/} from the termination analysis. In
1923: fact, if $|A| = \infty$ then {\it (a, b)\/} in Definition~\ref{c2:def:fairp}
1924: are trivially satisfied.
1925:
1926:
1927: \maintheorem
1928: Fair-bounded programs and queries precisely characterise
1929: $\exists$-termination, i.e.~the class of logic programs and queries
1930: for which a terminating control exists.
1931:
1932:
1933: \begin{theorem}[\cite{RugTCS98,Rug99}] \label{c2:fair:ncscorr}
1934: Let $P$ be a program and $Q$ a query.
1935:
1936: If $P$ and $Q$ are both fair-bounded by an extended level mapping $|.|$
1937: and a Herbrand interpretation $I$, then $P$ and $Q$ $\exists$-terminate.
1938:
1939: Conversely, if $P$ and $Q$ $\exists$-terminate, then there exist
1940: an extended level mapping $|.|$ and a Herbrand interpretation $I$
1941: such that $P$ and $Q$ are both fair-bounded by $|.|$ and $I$.
1942: \end{theorem}
1943:
1944: \subsection{Example}
1945:
1946: \begin{example} \label{ex:prodcons-is-fair-bounded}
1947: The {\tt PRODCONS} program is fair-bounded. First, we introduce the
1948: {\em list-max\/} norm: \index{$lmax()$}
1949: \[
1950: \begin{array}{rcll}
1951: lmax( f ( x_1 , \LL , x_n ) ) & = & 0
1952: & \mbox{if} \ f \neq [ \: . \: | \: . \: ] \\
1953: lmax([x | xs]) & = &
1954: max\{ lmax( xs ), size(x) \}
1955: & \mbox{otherwise.}
1956: \end{array}
1957: \]
1958: Note that for a ground list $xs$, $lmax(xs)$ equals the maximum size
1959: of an element in $xs$. Then we define:
1960: \begin{eqnarray*}
1961: | \mathtt{system}(n) | & = & size(n) + 3 \\[-0.5ex]
1962: | \mathtt{prod}(bs) | & = & |bs| \\ [-0.5ex]
1963: | \mathtt{cons}(bs,n) | & = &
1964: \left\{ \begin{array}{ll}
1965: size(n) + lmax(bs) & \mbox{ if } I\models \mathtt{cons}(bs,n) \\
1966: size(n) & \mbox{ if } I\not \models \mathtt{cons}(bs,n)
1967: \end{array} \right.\\[-0.5ex]
1968: | \mathtt{wait}(t) | & = & size(t)\\[0.5ex]
1969: I & = & \{ \mathtt{system}(n) \mid n \in U_L \}
1970: \U \{ \mathtt{prod}(bs) \mid lmax(bs) \leq 2 \} \U \\[-0.5ex]
1971: & & \{ \mbox{\tt cons($bs$,$n$)} \mid|bs| = size(n) \}
1972: \U \{ \mathtt{wait}(x) \mid x \in U_L \}.
1973: \end{eqnarray*}
1974: Let us show the proof obligations of Definition~\ref{c2:def:fairp}. Those for
1975: unit clauses are trivial. Consider now the recursive clauses
1976: {\it (w), (c), (p1), (p2),\/} and {\it (s)\/}.
1977:
1978: \paragraph{\it (w).}
1979: $I$ is obviously a model of {\it (w)\/}. In
1980: addition,
1981: $|\mathtt{wait(s}(d))|$ $=$
1982: $size(d) + 1$ $\ma$
1983: $size(d)$ $=$
1984: $|\mathtt{wait}(d)|$.
1985: This implies {\it (a, b)\/}.
1986:
1987: \paragraph{\it (c).}
1988: %\item[{\it (c)\/}]
1989: Consider a ground instance
1990: $\mathtt{cons}([d|bs],\mathtt{s}(n)) \la
1991: \mathtt{cons}(bs,n),\ \mathtt{wait}(d)$
1992: of {\it (c)\/}. If
1993: $I \Mo \mathtt{cons}(bs,n),\ \mathtt{wait}(d)$, then
1994: $|bs| = size(n)$, and so
1995: \[
1996: |[d|bs]| = |bs| + 1 = size(n) + 1
1997: = size(\mathtt{s}(n)),
1998: \]
1999: i.e.~$I \Mo \mathtt{cons}([d|bs],\mathtt{s}(n))$.
2000: Therefore, $I$ is a model of {\it (c)\/}. Let us show proof
2001: obligations {\it (a, b)\/} of Definition~\ref{c2:def:fairp}.
2002:
2003: \begin{itemize}
2004: \item[{\it (a)\/}]
2005: Suppose that
2006: $I \models \mathtt{cons}(bs,n),\ \mathtt{wait}(d)$.
2007: We have already shown that
2008: $I$ $\models$ $\mathtt{cons}([d|bs],\mathtt{s}(n))$.
2009: We calculate:
2010: \begin{eqnarray*}
2011: |\mathtt{cons}([d|bs],\mathtt{s}(n))|
2012: & = & size(n) + 1 + max\{ lmax(bs), size(d) \} \\
2013: & \ma & size(n) + lmax(bs) = |\mathtt{cons}(bs,n)|\\
2014: |\mathtt{cons}([d|bs],\mathtt{s}(n))|
2015: & = & size(n) + 1 + max\{ lmax(bs), size(d) \} \\
2016: & \ma & size(d)
2017: = |\mathtt{wait}(d)|.
2018: \end{eqnarray*}
2019: These two inequalities show that {\it (a)\/} holds.
2020:
2021: \item[{\it (b)\/}]
2022: If
2023: $I \not \models \mathtt{cons}(bs,n),\ \mathtt{wait}(d)$,
2024: then necessarily
2025: $I \not \models \mathtt{cons}(bs,n)$. Therefore
2026: \begin{eqnarray*}
2027: |\mathtt{cons}([d|bs],\mathtt{s}(n))|
2028: & \maeq & size(n) + 1 \\
2029: & \ma & size (n) =
2030: |\mathtt{cons}(bs,n)|,
2031: \end{eqnarray*}
2032: and so we have {\it (b)\/}.
2033: Recall that {\it (b)\/} states that the
2034: depth of the finitely failed SLD-tree must be bounded. In fact, it is
2035: the decrease of the ``counter'', the second argument of
2036: $\mathtt{cons}$, which in this case bounds the depth of the SLD-tree.
2037: \end{itemize}
2038:
2039: \paragraph{\it (p1,p2).}
2040: %\item[{\it (p1,p2)\/}]
2041: $I$ is obviously a model of {\it (p1)\/}. Moreover we have
2042: \[
2043: |\mathtt{prod}([\mathtt{s}(0)|bs])| = |bs| + 1
2044: \ \ma \ |bs|
2045: \ = \ |\mathtt{prod}(bs)|,
2046: \]
2047: which implies {\it (a)\/} and {\it (b)\/}. The reasoning for {\it (p2)\/}
2048: is analogous.
2049:
2050: \paragraph{\it (s).}
2051: %\item[{\it (s)\/}]
2052: Consider a ground instance
2053: $\mathtt{system}(n) \la \mathtt{prod}(bs),\ \mathtt{cons}(bs,n)$
2054: of {\it (s)\/}.
2055: Obviously $I$ is a model of {\it (s)\/}. Let us show
2056: {\it (a,b)\/}.
2057:
2058: \begin{itemize}
2059: \item[{\it (a)\/}] Suppose that
2060: $I \Mo \mathtt{prod}(bs),\ \mathtt{cons}(bs,n)$.
2061: This implies $lmax(bs) \leq 2$ and $|bs|$ $=$
2062: $size(n)$. These imply:
2063: \begin{eqnarray*} \label{c2:lb:fin2}
2064: |\mathtt{system}(n)| = size(n) + 3
2065: & \ma &
2066: |bs| = |\mathtt{prod}(bs)|\\
2067: |\mathtt{system}(n)| = size(n) + 3
2068: & \ma &
2069: size(n) + lmax(bs) = |\mathtt{cons}(bs,n)|.
2070: \end{eqnarray*}
2071: These two inequalities show {\it (a)\/}.
2072: \item[{\it (b)\/}] Suppose that $I \not \models \mathtt{prod}(bs),\
2073: \mathtt{cons}(bs,n)$. Intuitively, this means that
2074: $\mathtt{prod}(bs)$,
2075: $\mathtt{cons}(bs,n)$ has no refutation. We distinguish two cases.
2076: If $I \not \models \mathtt{cons}(bs,n)$ ($\mathtt{cons}(bs,n)$
2077: has no refutation) then:
2078: \[
2079: |\mathtt{system}(n)| \ = \ size(n) + 3 \ \ma \ size(n) \ = \
2080: |\mathtt{cons}(bs,n)|,\] i.e. the depth of the SLD-tree of
2081: $\mathtt{cons}(bs,n)$ is bounded (hence, the SLD-tree is finitely
2082: failed). If $I \models \mathtt{cons}(bs,n)$ and $I \not \models
2083: \mathtt{prod}(bs)$ ($\mathtt{prod}(bs)$
2084: has no refutation) then $|bs| = size(n)$, which implies:
2085: \begin{eqnarray*} \label{c2:lb:fin4}
2086: |\mathtt{system}(n)|
2087: = size(n) + 3 \ma |bs| = |\mathtt{prod}(bs)|,
2088: \end{eqnarray*}
2089: i.e. the depth of the SLD-tree of $\mathtt{prod}(bs)$ is bounded.
2090: \end{itemize}
2091:
2092: %\end{enumerate}
2093: We conclude this example by noting that for every $n \in \nat$ the query
2094: {\tt system($n$)} is fair-bounded by $|.|$ and $I$, and so
2095: every fair SLD-derivation of {\tt PRODCONS} and
2096: $\mathtt{system}(n)$ is finite.
2097: \end{example}
2098:
2099: \section{Bounded Nondeterminism} \label{c2:sec:bn}\label{nondet-sec}
2100: \limitation
2101: In the previous section, we have made the strongest possible
2102: assumption about the selection rule, in that we considered programs
2103: and queries for which there {\em exists} a terminating control. In
2104: general, a terminating control may not exist. Even in this case
2105: however, all is not lost. If we can establish that a program and query
2106: have only finitely many successful derivations, then we can transform
2107: the program so that it terminates.
2108:
2109: \begin{example} \label{ex:exists-strictly-bounded}
2110: The program {\tt ODDEVEN} in figure~\ref{oddeven-prog}
2111: defines the {\tt even} and {\tt odd} predicates,
2112: with the usual intuitive meaning. The query
2113: $\, \mathtt{even(X),\; odd(X)}\, $ is
2114: intended to check whether there is a number that is both even and odd.
2115: It is readily checked that {\tt ODDEVEN} and the query do not
2116: $\exists$-terminate. However,
2117: {\tt ODDEVEN} and the query have only finitely many, namely 0,
2118: successful derivations.
2119: \end{example}
2120:
2121: \begin{figure}\figrule
2122: \begin{minipage}[t]{5cm}
2123: \begin{janprogram}
2124: \%\> even(X) \la \ \\
2125: \%\> \> {\tt X} {\rm is an even natural number.} \\[2mm]
2126: \> even(s(X)) $\la$ odd(X).\\
2127: \> even(0).
2128: \end{janprogram}
2129: \end{minipage}
2130: \hfill
2131: \begin{minipage}[t]{5cm}
2132: \begin{janprogram}
2133: \%\> odd(X) \la \ \\
2134: \%\> \> {\tt X} {\rm is an odd natural number.} \\[2mm]
2135: \> odd(s(X)) $\la$ even(X).
2136: \end{janprogram}
2137: \end{minipage}
2138: \caption{\tt ODDEVEN \label{oddeven-prog}}
2139: \figrule\end{figure}
2140:
2141:
2142: \termination
2143: Pedreschi \& Ruggieri \shortcite{PR99} propose the notion of
2144: {\em bounded nondeterminism\/} to model
2145: programs and queries with finitely many refutations.
2146:
2147: \begin{definition} \label{c2:bn:bndef}
2148: A program $P$ and query $Q$ have {\em bounded nondeterminism} if
2149: for every standard selection rule $s$ there are finitely many
2150: SLD-refutations of $P$ and $Q$ via $s$.
2151: \end{definition}
2152:
2153: By the Switching Lemma \cite{Apt97}, each refutation via some
2154: standard selection rule is isomorphic to some refutation via any other
2155: standard selection rule. Therefore, bounded nondeterminism could have
2156: been defined by requiring finitely many SLD-refutations of $P$ and $Q$
2157: via {\em some} standard selection rule. Also, note that, while bounded
2158: nondeterminism implies that there are finitely many refutations also
2159: for non-standard selection rules, the converse implication does not
2160: hold, in general (see Example~\ref{ex:ic-or-lds-not-imply-exists}).
2161:
2162: Bounded nondeterminism, although not being a notion of termination in
2163: the strict sense, is closely related to termination. In
2164: fact, if $P$ and $Q$ $\exists$-terminate, then $P$ and $Q$ have
2165: bounded nondeterminism. Conversely, if $P$ and $Q$ have bounded
2166: nondeterminism then there exists an upper bound for the length of the
2167: SLD-refutations of $P$ and $Q$. If the upper bound is known, then we
2168: can syntactically transform $P$ and $Q$ into an equivalent program and
2169: query that strongly terminate, i.e.~any selection rule will be a
2170: terminating control for them. Note that this transformation is even
2171: interesting for programs and queries that $\exists$-terminate, since
2172: few existing systems adopt fair selection rules. In addition, even if
2173: we adopt a selection rule that ensures termination, we may apply the
2174: transformation to prune the SLD-tree from unsuccessful branches.
2175:
2176: \decrease
2177: In the following, we present a declarative characterisation of
2178: programs and queries that have bounded nondeterminism, by introducing
2179: the class of {\em bounded\/} programs and queries.
2180: Just as Definitions~\ref{c2:def:accp} and~\ref{c2:def:fairp},
2181: it is based on {\em extended} level mappings.
2182:
2183: \begin{definition}\label{c2:def:bfcp} \label{c2:def:bq} \index{bounded programs}
2184: Let $|.|$ be an extended level mapping, and $I$ a Herbrand interpretation. A
2185: program $P$ is \emph{bounded by $|.|$ and $I$} if $I$ is a
2186: model of $P$ such that for every $\clausab$ in $\groun{L}{P}$:
2187: \[
2188: I \Mo \tn{B}{n}
2189: \ \mbox{\rm implies that for every}\
2190: i \in [1,n],\
2191: |A| \ma |B_i|.
2192: \]
2193: A query $Q$ is {\em bounded by $|.|$ and $I$\/} if
2194: there exists $k \in \nat$ such that for every $\tn{A}{n} \in
2195: \groun{L}{Q}$:
2196: \[
2197: I \Mo A_1, \ldots, A_n
2198: \ \mbox{\rm implies that for every}\
2199: i \in [1,n],\
2200: k \ma |A_i|.
2201: \]
2202: \end{definition}
2203:
2204: \comparison
2205: It is straightforward to check that the definition of bounded programs
2206: is a simplification of Definition~\ref{c2:def:fairp} of fair-bounded
2207: programs, where proof obligation {\it (b)\/} is discarded.
2208: Intuitively, the definition of boundedness only requires the
2209: decreasing of the extended level mapping when the body atoms are true
2210: in some model of the program, i.e.~they might have a refutation.
2211:
2212: \maintheorem
2213: Bounded programs and queries precisely characterise the
2214: notion of bounded nondeterminism.
2215:
2216: \begin{theorem}[\cite{PR99,Rug99}]
2217: Let $P$ be a program and $Q$ a query.
2218:
2219: If $P$ and $Q$ are both bounded by an extended level mapping $|.|$ and
2220: a Herbrand interpretation $I$, then $P$ and $Q$ have bounded
2221: nondeterminism.
2222:
2223: Conversely, if $P$ and $Q$ have bounded nondeterminism, then there exist
2224: an extended level mapping $|.|$ and a Herbrand interpretation $I$
2225: such that $P$ and $Q$ are both bounded by $|.|$ and $I$.
2226: \end{theorem}
2227:
2228: \examples
2229: \begin{example} \label{oddeven-is-bounded}
2230: Consider again the {\tt ODDEVEN} program. It is readily checked that
2231: it is bounded by defining:
2232: \begin{eqnarray*}
2233: |\mathtt{even}(x)| = |\mathtt{odd}(x)| & = & size(x)\\[-0.5ex]
2234: I & = &
2235: \{
2236: \mathtt{even}(\mathtt{s}^{2\cdot i}(0)),\
2237: \mathtt{odd}(\mathtt{s}^{2\cdot i + 1}(0)) \mid i \geq 0 \}.
2238: \end{eqnarray*}
2239: The query
2240: $\,\mathtt{even(X),\; odd(X)}\,$ is bounded by $|.|$ and $I$. In fact, since no
2241: instance of it is true in $I$, Definition~\ref{c2:def:bq} imposes no
2242: requirement. Therefore, {\tt ODDEVEN} and the query above have bounded
2243: nondeterminism.
2244: \end{example}
2245:
2246: Generally, for a query that has no instance in a model of the program
2247: (it is {\em unsolvable}), the $k$ in Definition~\ref{c2:def:bfcp} can
2248: be chosen as $0$. An automatic method to check whether a query (at a
2249: node of a SLD-tree) is unsolvable has been proposed by \cite{BVWD98}.
2250: Of course, the example is somewhat a limit case, since one does not
2251: even need to run a query if it has been shown to be unsolvable. However,
2252: we have already mentioned that the benefits of characterising bounded
2253: nondeterminism also apply to programs and queries belonging to the
2254: previously introduced classes. In addition, it is still possible to
2255: devise an example program and a {\em satisfiable} query that do not
2256: $\exists$-terminate but have bounded nondeterminism.
2257:
2258: \begin{example} \label{all-is-bounded}
2259: We now define the predicate
2260: {\tt all} such that the query
2261: $\mathtt{all}(n_0,n_1,\mathtt{Xs})$ collects in
2262: {\tt Xs} the answers of a query
2263: $\mathtt{q}(m,A)$ for
2264: values $m$ ranging from $n_0$ to $n_1$.
2265: \begin{janprogram}
2266: \> all(N,N,[A]) $\la$ q(N,A).\\
2267: \> all(N,N1,[A|As]) $\la$ q(N,A), all(s(N),N1,As).\\
2268: \> q(Y, Y). \%just as an example
2269: \end{janprogram}
2270: \end{example}
2271:
2272: The program and the query {\tt all(0,s(s(0)),As)} do not
2273: $\exists$-terminate, but they have only one computed answer, namely
2274: {\tt As = [0,s(0),s(s(0))]}. The program and the query are bounded
2275: (and thus have bounded nondeterminism) by defining:
2276: \begin{eqnarray*}
2277: |\mathtt{all}(n, m, x)| & = & max\{ size(m) - size(n), 0 \} + 1\\[-0.5ex]
2278: |\mathtt{q}(x,y)| & = & 0 \\[0.5ex]
2279: I & = &
2280: \{
2281: \mathtt{all}(n, m, x) \mid size(n) \leq size(m) \} \U \\[-0.5ex]
2282: & = & \{\mathtt{q}(x,y)\}.
2283: \end{eqnarray*}
2284:
2285: \section{Relations between Classes} \label{c2:sec:class}\label{relations-sec}
2286: We have introduced six classes of programs and queries, which
2287: provide declarative characterisations of operational notions of
2288: universal termination and bounded nondeterminism. In this section we
2289: summarise the relationships between these classes.
2290:
2291: \subsection{Comparison of Characterisations}\label{characterisations-subsec}
2292: We now try to provide an intuitive understanding of the significance
2293: of the technical differences between the characterisations of
2294: termination we have proposed. These are summarised in Table~\ref{char-table}.
2295:
2296: \begin{table}
2297: \normalsize
2298: \caption{Comparison of characterisations\label{char-table}}
2299: \begin{tabular}{rc@{\hspace{1.7em}}c@{\hspace{1.7em}}c@{\hspace{1.7em}}c@{\hspace{1.7em}}c@{\hspace{1.7em}}cc}
2300: %\cline{2-5}
2301: \hline\\[4.5ex]
2302: & \begin{rotate}{25} only ground? \end{rotate} &
2303: \begin{rotate}{25} only recursive?\end{rotate} &
2304: \begin{rotate}{25} uses model? \end{rotate} &
2305: \begin{rotate}{25} query oblig.? \end{rotate} &
2306: \begin{rotate}{25} $\infty$ in codomain?\end{rotate} &
2307: \begin{rotate}{25} neg.~model info.?\end{rotate} &
2308: \hspace*{4em}\\ \hline
2309: boundedness & yes & no & yes & yes & yes & no\\
2310: %\cline{1-5}
2311: fair-boundedness & yes & no & yes & yes & yes & yes\\
2312: %\cline{1-5}
2313: acceptability & yes & no & yes & yes & yes & no\\
2314: %\cline{1-5}
2315: delay-recurrence & yes & no & yes & no & no & no\\
2316: %\cline{1-5}
2317: simply-acceptability & no & yes & yes & no & no & no\\
2318: %\cline{1-5}
2319: recurrence & yes & no & no & yes & no & n.a.\\
2320: %\cline{1-5}
2321: \hline
2322: \end{tabular}
2323: \end{table}
2324:
2325: The first difference concerns the question of whether a decrease is
2326: defined for all ground instances of a clause, or rather for instances
2327: specified in some other way. All characterisations, except
2328: simply-acceptability, require a decrease for all ground instances of a
2329: clause. One cannot clearly say that this difference lies in the nature
2330: of the termination classes themselves: the first characterisation of
2331: input-termination by Smaus~\shortcite{Sma99} also required a decrease
2332: for the ground instances of a clause, just as there are
2333: characterisations of left-termination \cite{BCF94,SVB92} based on
2334: generalised level mappings and hence non-ground instances of clauses.
2335: However, one can say that our characterisation of input-termination
2336: inherently relies on measuring the level of non-ground atoms, which
2337: may change via further instantiation. Nevertheless, this instantiation
2338: is not arbitrary: it is controlled by the fact that derivations are
2339: input-consuming and the programs are simply moded. This is reflected
2340: in the condition that a decrease holds for all simply-local
2341: instantiations of a clause.
2342:
2343: The second difference concerns the question of whether a decrease is
2344: required for recursive body atoms only, or whether recursion plays
2345: no role. Simply-acceptability is the only characterisation that
2346: requires a decrease for recursive body atoms only. We attribute this
2347: difference essentially to the explicit use of modes. Broadly
2348: speaking, modes restrict the data flow of a program in a way that
2349: allows for termination proofs that are inherently {\em modular}.
2350: Therefore one does not explicitly require a decrease for non-recursive
2351: calls, but rather one requires that for the predicate of the
2352: non-recursive call, termination has already been shown
2353: (independently). To support this explanation, we refer
2354: to~\cite{EBC99}: there left-termination for {\em well moded} programs
2355: is shown, using {\em well-acceptability}. Well-acceptability requires
2356: a decrease only for recursive body atoms.
2357:
2358: The third difference concerns the question of whether the method
2359: relies on (some kind of) models or not. It is not surprising that a
2360: method for showing strong termination cannot rely on models: one
2361: cannot make any assumptions about certain atoms being resolved before
2362: an atom is selected. However, the original methods of showing
2363: termination for input-consuming derivations were also not based on
2364: models~\cite{Sma99,BER99}, and it was remarked that the principle
2365: underlying the use of models in proofs of left-termination cannot be
2366: easily transferred to input termination. By
2367: restricting to simply moded programs and defining a special notion of
2368: model, this was nevertheless achieved. For a clause $H \la
2369: A_1,\dots,A_n$, assuming that $A_i$ is the selected atom, we exploited
2370: that provided that programs and queries are simply moded, we know that
2371: even though $A_1,\dots,A_{i-1}$ may not be resolved completely,
2372: $A_1,\dots,A_{i-1}\theta$ will be in any ``partial model'' of the
2373: program.
2374:
2375: The fourth difference concerns the question of whether proof
2376: obligations are imposed on queries. Delay-recurrence and
2377: simply-acceptability are the characterisations that impose no proof
2378: obligations for queries (except that in the latter case, the query
2379: must be simply moded). The reason is that the restrictions on the
2380: selectability of an atom, which depends on the degree of
2381: instantiation, take the role of such a proof obligation.
2382:
2383: The fifth difference concerns the question of whether $\infty$ is
2384: in the codomain of level mappings. This is the case for
2385: acceptability, fair-boundedness and boundedness. In all three cases,
2386: this allows for excluding {\em unintended atoms\/} and {\em
2387: non-terminating atoms\/} from the termination analysis. For an atom
2388: $A$ with $|A| = \infty$ the proof obligations are trivially satisfied.
2389: Also, the use of $\infty$ allows to achieve full
2390: completeness of the characterisation.
2391:
2392: A final difference concerns
2393: the way information on data flow (modes, simply-local models, covers,
2394: Herbrand models) is used in the declarative characterisations.
2395: For recurrence this is not applicable. Apart from that, in all
2396: except fair-boundedness, such information is used only
2397: in a ``positive'' way, i.e., ``if \ldots {\em is\/} in the model then
2398: \ldots''. In fair-boundedness, it is also used in a ``negative''
2399: way, namely ``if \ldots {\em is not\/} in the model then \ldots''.
2400: Intuitively, in all characterisation, except fair-boundedness, the
2401: relevant part of the information concerns a characterisation of atoms
2402: that are logical consequences of the program. In fair-boundedness,
2403: it is also relevant the characterisation of atoms that are not
2404: logical consequences, since for those atoms we must ensure finite
2405: failure.
2406:
2407:
2408: \subsection{From Strong Termination to Bounded Nondeterminism}\label{from-st-to-bn-subsec}
2409: In this subsection, we show inclusions between the introduced classes, i.e., we justify
2410: each arrow in figure~\ref{overview-fig}.
2411: We first leave aside input termination and local delay
2412: termination, since for these classes, the comparison is much less
2413: clearcut.
2414:
2415: Looking at the four remaining classes from an operational point of
2416: view, we note that strong termination of a program and a query
2417: implies left-termination, which in turn implies
2418: $\exists$-termination, which in turn implies bounded nondeterminism.
2419: Examples~\ref{ex:strong-strictly-left},
2420: \ref{ex:left-strictly-exists} and \ref{ex:exists-strictly-bounded} show
2421: that these implications are strict.
2422:
2423: Since the declarative characterisations of those notions are sound and
2424: complete, the same strict inclusions hold among recurrence,
2425: acceptability, fair-boundedness and boundedness. This allows for
2426: reusing or simplifying termination proofs.
2427:
2428: %\removebrackets
2429: \begin{theorem} \label{c2:r:rec}
2430: Let $P$ be a program and $Q$ a query, $|.|$ an extended level mapping
2431: and $I$ a Herbrand model of $P$. Each of the following statements
2432: strictly implies the statements below it:
2433: \begin{itemize}
2434: \item[{\it (i)\/}] $P$ and $Q$ are recurrent by $|.|$,
2435: \item[{\it (ii)\/}] $P$ and $Q$ are acceptable by $|.|$ and $I$,
2436: \item[{\it (iii)\/}] $P$ and $Q$ are fair-bounded by $|.|$ and $I$,
2437: \item[{\it (iv)\/}] $P$ and $Q$ are bounded by $|.|$ and $I$.
2438: \end{itemize}
2439: \end{theorem}
2440:
2441: In the following example, we show how the above theorem allows for
2442: reuse of termination proofs.
2443:
2444: \begin{example}\label{ex:reuse}
2445: In Example~\ref{ex:transp-is-acceptable} we showed that the {\tt TRANSP} program
2446: is acceptable by a level mapping $|.|$ and a model $I$. The proof
2447: obligations of acceptability had to be shown for every clause of the
2448: program.
2449:
2450: However, we note that the clauses defining the predicate {\tt member}
2451: are a sub-program which is readily checked to be recurrent by the same
2452: $|.|$. By Theorem~\ref{c2:r:rec}, we conclude that the proof obligations
2453: for clauses defining {\tt member} are satisfied for every Herbrand
2454: model of {\tt TRANSP} and thus in particular for $I$.
2455:
2456: We refer the reader to \cite{AP94m} for a collection
2457: of results on reuse of proofs of recurrence to show acceptability, and
2458: on proving acceptability of $P \U P'$ by reusing separate proofs for
2459: $P$ and $P'$.
2460: \end{example}
2461:
2462: Consider now local delay termination. Obviously, it is implied by
2463: strong termination. However, we have observed with the programs and
2464: queries of Examples~\ref{ex:lds-yes-left-no}
2465: and~\ref{ex:ic-or-lds-not-imply-exists} that local delay termination
2466: does not imply left-termination or $\exists$-termination, in general.
2467: These results can be obtained under reasonable assumptions, which, in
2468: particular, rule out deadlock.
2469:
2470: The following proposition relates local delay termination with
2471: $\exists$-termination.
2472:
2473: \begin{proposition}\label{local-implies-exists-prop}
2474: Let $P$ and $Q$ be a permutation well moded program and query, and
2475: $|.|$ a moded level mapping.
2476:
2477: If $P$ and $Q$ local delay terminate (w.r.t.~$|.|$) then
2478: they $\exists$-terminate.
2479:
2480: If $P$ is delay-recurrent by $|.|$ and some Herbrand interpretation
2481: then $P$ and $Q$ are fair-bounded by some extended level mapping and
2482: Herbrand interpretation.
2483: \end{proposition}
2484: \begin{proof}
2485: Since $P$ and $Q$ are permutation well moded, every query $Q'$ in a
2486: derivation of $P$ and $Q$ is permutation well moded \cite{Sma99t},
2487: i.e., there exists a permutation $\tilde{Q'}$ of $Q'$ which is well
2488: moded. By Definition~\ref{well-moded}, the leftmost atom in $\tilde{Q'}$
2489: is ground in its input positions and hence bounded
2490: w.r.t.~$|.|$. Consider the selection rule which always selects this
2491: ``leftmost'' (modulo the permutation) atom. This selection rule is
2492: local and delay-safe, and it is a standard selection rule (since
2493: there is always a selected atom). Therefore, local delay termination
2494: implies $\exists$-termination.
2495:
2496: Concerning the second claim, since fair-boundedness is a complete
2497: characterisation of $\exists$-termination, we have the conclusion.
2498: \end{proof}
2499:
2500: The next proposition relates local delay termination with
2501: left-termination. In this case, programs must be
2502: well moded, not just {\em permutation} well moded. The proof is
2503: similar to the previous one but simpler.
2504:
2505: \begin{proposition}\label{local-implies-left-prop}
2506: Let $P$ and $Q$ be a well moded program and query, and $|.|$ a moded
2507: level mapping.
2508:
2509: If $P$ and $Q$ local delay terminate (w.r.t.~$|.|$) then
2510: they left-terminate.
2511:
2512: If $P$ is delay-recurrent by $|.|$ and some Herbrand interpretation
2513: then $P$ and $Q$ are acceptable by some extended level mapping and
2514: Herbrand interpretation.
2515: \end{proposition}
2516:
2517:
2518: Marchiori \& Teusink \shortcite{MT99} propose a
2519: program transformation such that the original program is
2520: delay-recurrent iff the transformed program is acceptable. This
2521: transformation allows us to use automated proof methods originally
2522: designed for acceptability for the purpose of showing delay-recurrence.
2523:
2524: Consider now input termination. As before, it is
2525: implied by strong termination. However, as observed in
2526: Examples~\ref{ex:ic-yes-lds-no},~\ref{ex:lds-yes-left-no} and \ref{ex:ic-or-lds-not-imply-exists},
2527: input termination does not imply local delay termination,
2528: left-termination, or $\exists$-termination, in general. Again, these
2529: results can be obtained under reasonable assumptions.
2530:
2531: The following proposition relates input termination to
2532: $\exists$-termination.
2533:
2534: \begin{proposition}\label{input-implies-exists-prop}
2535: Let $P$ and $Q$ be a permutation well moded program and query. If $P$
2536: and $Q$ input terminate then they $\exists$-terminate.
2537:
2538: Let $P$ and $Q$ be a permutation well and simply moded program and
2539: query. If $P$ is simply-acceptable by some $|.|$ and $I$ then $P$ and
2540: $Q$ are fair-bounded by some extended level mapping and Herbrand
2541: interpretation.
2542: \end{proposition}
2543: \begin{proof}
2544: Since $P$ and $Q$ are permutation well moded, every query $Q'$ in a
2545: derivation of $P$ and $Q$ is permutation well moded \cite{Sma99t},
2546: and so $Q'$ contains an atom that is ground in its input
2547: position. The selection rule $s$ that always selects this atom
2548: together with all program clauses is an input-consuming selection
2549: rule, and also a standard selection rule. Therefore,
2550: input termination implies universal termination
2551: w.r.t.~$\{s\}$ and hence $\exists$-termination.
2552:
2553: Concerning the second claim, by Theorem~\ref{input-termination-thm},
2554: $P$ and $Q$ input terminate. As shown above, this implies
2555: that they $\exists$-terminate. Since fair-boundedness is a complete
2556: characterisation of $\exists$-termination, we have the conclusion.
2557: \end{proof}
2558:
2559: The next proposition gives a direct comparison between
2560: input and left-termina\-tion. The proof is similar to the
2561: previous one.
2562:
2563: \begin{proposition}\label{input-implies-left-prop}
2564: Let $P$ and $Q$ be a well moded program and query. If $P$ and $Q$
2565: input terminate then they left-terminate.
2566:
2567: Let $P$ and $Q$ be a well and simply moded program and query. If $P$
2568: is simply-acceptable by some $|.|$ and $I$ then $P$ and $Q$ are
2569: acceptable by some extended level mapping and Herbrand interpretation.
2570: \end{proposition}
2571:
2572:
2573: To relate input termination to local delay termination,
2574: we introduce a notion that relates delay-safe derivations with
2575: input-consuming derivations, based on an a similar concept
2576: from \cite{AL95}.
2577:
2578: \begin{definition}\label{implies-matching}
2579: Let $P$ be a program and $|.|$ a moded level mapping.
2580:
2581: We say that $|.|$ {\em implies matching\/}
2582: (w.r.t.~$|.|$) if for every atom
2583: $A = p({\mathbf s}, {\mathbf t})$
2584: bounded w.r.t.~$|.|$ and for every
2585: $B = p({\mathbf v}, {\mathbf u})$
2586: head of a renaming of a clause from $P$ which is variable-disjoint
2587: with $A$, if $A$ and $B$ unify, then $\mathbf s$ is an instance of
2588: $\mathbf v$.
2589: \end{definition}
2590:
2591: Note that, in particular, $|.|$ implies matching if every atom
2592: bounded by $|.|$ is ground
2593: in its input positions.
2594:
2595: \begin{proposition} \label{ic-imp-ld}\label{input-implies-local-prop}
2596: Let $P$ and $Q$ be a permutation simply moded program and query, and
2597: $|.|$ a moded level mapping that implies matching.
2598:
2599: If $P$ and $Q$ input terminate then they local delay
2600: terminate (w.r.t.~$|.|$).
2601: \end{proposition}
2602: \begin{proof}
2603: The conclusion follows by
2604: showing that any derivation of $P$ and any permutation simply moded
2605: query $Q'$ via a local delay-safe selection rule (w.r.t.~$|.|$) is
2606: also a derivation via an input-consuming selection rule. So, let $s$
2607: be a local delay-safe selection rule and $Q'$ a permutation
2608: simply-well moded query such that $s$ selects atom $A = p({\mathbf
2609: s},{\mathbf t})$. Then by Definition~\ref{implies-matching}, for each $B =
2610: p({\mathbf v},{\mathbf u})$, head of a renaming of a clause from $P$,
2611: if $A$ and $B$ unify, then $\mathbf s$ is an instance of $\mathbf v$,
2612: i.e. ${\mathbf s} = {\mathbf v}\theta$ for some substitution $\theta$
2613: such that $dom(\theta) \sse \vars(\vect{v})$.
2614: By \cite[(Apt \& Luitjes, 1995, Corollary 31)]{AL95},
2615: this implies that the resolvent of $Q'$ and any clause in
2616: $P$ is again permutation simply moded. Moreover, by applying the
2617: unification algorithm \cite{Apt97}, it is readily checked that, if $A$
2618: and $B$ unify, then $\sigma = \theta \U \{ {\mathbf t}/{\mathbf
2619: u}\theta \}$ is an mgu. Permutation simply-modedness implies that ${\mathbf s}$
2620: and ${\mathbf t}$ are variable-disjoint. Moreover, ${\mathbf s}$ and
2621: ${\mathbf v}$ are variable-disjoint. This implies that $\dom(\sigma)
2622: \cap \vars(\vect{s}) = \emptyset$, and so the derivation step is
2623: input-consuming.
2624:
2625: By repeatedly applying this argument to all queries in the
2626: SLD-derivation of $P$ and $Q$ via $s$, it follows that the derivation
2627: is via some input-consuming selection rule.
2628: \end{proof}
2629:
2630: It remains an open question whether simply-acceptability implies
2631: delay-recurrence under some general hypotheses. The problem with
2632: showing such a result lies in the fact that delay-recurrence is a
2633: sufficient but not necessary condition for local delay termination.
2634:
2635: \begin{example}\label{ex:open-question}
2636: Consider again the program and the level mapping $|.|$ of
2637: Example~\ref{ex:delay-recursive-incomplete}.
2638: We have already observed that the program and any
2639: query local delay terminate.
2640:
2641: In addition, given the mode $\{ {\tt p(\out)}$, ${\tt q(\inp)}$, ${\tt
2642: r(\inp)} \}$, it is readily checked that the program is
2643: simply moded, and that the level mapping is moded and implies
2644: matching. Also, note that the program is simply-acceptable
2645: by $|.|$ and any simply-local model.
2646:
2647: However, this is not sufficient to show that the program is
2648: delay-recurrent, as proved in
2649: Example~\ref{ex:delay-recursive-incomplete}. Intuitively, the
2650: problem with showing delay-recurrence lies in the fact that the notion
2651: of cover does not appropriately describe the data flow in this program
2652: given by the modes.
2653: \end{example}
2654:
2655:
2656: \subsection{From Bounded Nondeterminism to Strong Termination}
2657: Consider now a program $P$ and a query $Q$ which either do not
2658: universally terminate for a set of selection rules in question, or
2659: simply for which we (or our compiler) fail to {\em prove} termination.
2660: We have
2661: already mentioned that, if $P$ and $Q$ have bounded nondeterminism
2662: then there exists an upper bound for the length of the SLD-refutations
2663: of $P$ and $Q$. If the upper bound is known, then we can syntactically
2664: transform $P$ and $Q$ into an equivalent program and query that
2665: strongly terminate. As shown by Pedreschi \& Ruggieri \shortcite{PR99},
2666: such an upper bound is
2667: related to the natural number $k$ of Definition~\ref{c2:def:bq} of
2668: bounded queries. As in our notation for moded atoms, we use boldface
2669: letters to denote vectors of (possibly non-ground) terms.
2670:
2671: \begin{definition} \label{c2:def:bntrans}
2672: Let $P$ be a program and $Q$ a query both bounded by $|.|$ and $I$,
2673: and let $k \in \nat$. We define $Ter(P)$ as the program such that:
2674: \begin{itemize}
2675: \item for every clause
2676: $p_0(\mathbf{t}_0) \la
2677: p_1(\mathbf{t}_1),\ldots,p_n(\mathbf{t}_n)$
2678: in $P$, with $n > 0$,
2679: the clause
2680: \[
2681: p_0(\mathbf{t}_0,\mathtt{s(D)}) \la
2682: p_1(\mathbf{t}_1,\mathtt{D}),\ldots,p_n(\mathbf{t}_n,\mathtt{D})\]
2683: is in $Ter(P)$, where {\tt D} is a fresh variable,
2684: \item and, for every clause
2685: $p_0(\mathbf{t}_0)$ in $P$,
2686: the clause
2687: \[
2688: p_0(\mathbf{t}_0,\_)\la
2689: \]
2690: is in $Ter(P)$.
2691: \end{itemize}
2692: Also, for the query
2693: $Q = p_1(\mathbf{t}_1),\ldots,p_n(\mathbf{t}_n)$,
2694: we define $Ter(Q,k)$ as the query
2695: \[
2696: p_1(\mathbf{t}_1,\mathtt{s}^k(0)),\ldots,p_n(\mathbf{t}_n,\mathtt{s}^k(0))
2697: \]
2698: \end{definition}
2699:
2700:
2701: The transformed program relates to the original one as shown in
2702: the following theorem.
2703:
2704: %\removebrackets
2705: \begin{theorem}[\cite{PR99,Rug99}]
2706: \label{c2:bn:transfcorr}
2707: Let $P$ be a program and $Q$ a query both bounded by $|.|$ and $I$,
2708: and let $k$ be a given natural number satisfying Definition~\ref{c2:def:bq}.
2709:
2710: Then, for every $n \in \nat$, $Ter(P)$ and $Ter(Q, n)$
2711: strongly terminate.
2712:
2713: Moreover, there is a bijection between SLD-refutations of $P$ and $Q$
2714: via a selection rule $s$ and SLD-refutations of $Ter(P)$ and $Ter(Q,
2715: k - 1 )$ via $s$.
2716: \end{theorem}
2717:
2718: The intuitive reading of this result is that the transformed
2719: program and query maintain the same {\em success semantics\/} of the
2720: original program and query. Note that no assumption is
2721: made on the selection rule $s$, i.e.~any selection rule is a
2722: terminating control for the transformed program and query.
2723:
2724:
2725: \begin{example}\label{ex:oddeven-transformed}
2726: Reconsider the program {\tt ODDEVEN} and the query
2727: $Q = \mathtt{even(X),\; odd(X)}$ of Example~\ref{ex:exists-strictly-bounded}.
2728: The transformed program $Ter(\mathtt{ODDEVEN})$ is:
2729: \begin{janprogram}
2730: \> even(s(X),s(D)) $\la$ odd(X,D).\\
2731: \> even(0,\_).\\[2ex]
2732: \> odd(s(X),s(D)) $\la$ even(X,D).
2733: \end{janprogram}
2734: and the transformed query $Ter(Q, k - 1)$ for $k = 3$ is {\tt
2735: even(X,s$^2$(0)),odd(X,s$^2$(0))}. By Theorem~\ref{c2:bn:transfcorr}, the
2736: transformed program and query terminate for {\em any} selection rule,
2737: and the semantics w.r.t.~the original program is preserved modulo the
2738: extra argument added to each predicate.
2739: \end{example}
2740:
2741: The transformations $Ter(P)$ and $Ter(Q, k)$ are of purely theoretical
2742: interest. In practice, one would implement these counters directly
2743: into the compiler/interpreter. Also, the compiler/interpreter should
2744: include a module that infers an upper bound $k$ automatically.
2745: Approaches to the automatic inference of level mappings and models are
2746: briefly recalled in the next section. Pedreschi \& Ruggieri
2747: \shortcite{PR99} give an example showing how the approach of Decorte
2748: {\em et~al.}\ \shortcite{DDV99} could be rephrased to infer
2749: boundedness.
2750:
2751:
2752:
2753: \section{Related Work}\label{related-sec}
2754: The survey on termination of logic programs by De Schreye \& Decorte
2755: \shortcite{SD94} covers most work in this area until 1994. The authors
2756: distinguish three types of approaches: the ones that express necessary
2757: and sufficient conditions for termination, the ones that provide
2758: decidable {\em sufficient\/} conditions, and the ones that prove
2759: decidability or undecidability for subclasses of programs and queries.
2760: Under this classification, our survey falls in the first type. In the
2761: following, we mainly mention works published since 1994. We group the
2762: works according to the main focus or angle they take.
2763:
2764:
2765: \subsection{Other Characterisations of Left-termination}
2766:
2767: Apt \& Pedreschi \shortcite{AP94m} refined acceptability to make the
2768: method {\em modular}. Here, modularity means that the termination
2769: proof for a program $P \U P'$ can be obtained from separate
2770: termination proofs for $P$ and $P'$. Also, in \cite{AMP94},
2771: acceptability is extended to reason on first-order built-in's of
2772: Prolog.
2773:
2774: Etalle {\em et~al.}~\index{Etalle} \shortcite{EBC99} propose a
2775: refinement of acceptability (called {\em well-acceptability}) for
2776: well moded programs and queries. The requirement of well-modedness
2777: simplifies proofs of acceptability. On the one hand, no proof
2778: obligation is imposed on the \emph{queries}. On the other hand, the
2779: decrease of the level mapping is now required only from the head to
2780: the mutually recursive clause body atoms. It is interesting to observe
2781: that the definition of well-acceptability is then very close to
2782: simply-acceptability. Actually, well-modedness of a program and a query
2783: implies that atoms selected by the LD selection rule are ground in
2784: their input positions, hence a derivation via the LD selection rule is
2785: input-consuming.
2786:
2787: Serebrenik and De Schreye \shortcite{SS01} show that, when restricting
2788: to well moded programs and queries and moded level mappings (they call
2789: them {\em output-independent}), acceptability can be generalised by
2790: having any well-founded ordering, not necessarily $\nat$, as co-domain
2791: of level mappings. This simplifies the proof of programs where complex
2792: level mappings may be required.
2793:
2794: Also, a characterisation of acceptability in the context of metric
2795: spaces was provided by Hitzler \& Seda \shortcite{HS99}.
2796:
2797: Alternative characterisations of left-termination consider proof
2798: obligations on generalised level mappings and thus on possibly
2799: non-ground instances of clauses and queries. Bossi {\em
2800: et~al.}~\shortcite{BCF94} provide sufficient and necessary conditions
2801: that involve: (1) generalised level mappings (with an arbitrary
2802: well-founded ordering as the codomain) that do not increase w.r.t.\
2803: substitutions; (2) a specification (\pre, \post), with \pre, \post
2804: \sse $Atom_L$, which is intended to characterise call patterns (\pre)
2805: and correct instances (\post) of atomic queries. Call patterns
2806: provide information on the structure of selected atoms, while correct
2807: instances provide information on data flow. The method has the
2808: advantage of reasoning both on
2809: termination and on partial correctness within the same framework.
2810: However, proof obligations are not well suited for {\em paper \& pencil}
2811: proofs, since they require to reason on the strongly connected
2812: components of a graph abstracting the flow of control of the program
2813: under consideration. An adaption of acceptability to total correctness
2814: is presented in \cite{PR95v}. Also, we mention the works of Bronsard
2815: {\em et~al.}~\shortcite{BLR92} and Deransart \&
2816: Ma{\l}uszy{\'n}ski~\shortcite{DM93}, which rely on partial correctness
2817: or typing information to characterise call patterns. Deransart \&
2818: Ma{\l}uszy{\'n}ski generalise the proof obligations on the
2819: left-to-right order of the LD selection rule to any acyclic ordering of
2820: body atoms. Another characterisation of left-termination particularly
2821: suited for automation is due to De Schreye {\em
2822: et~al.}~\shortcite{SVB92,DDV99}. Their notion is similar to the one of
2823: Bossi {\em et~al.}, but it uses: (1) generalised level mappings that are
2824: constant w.r.t.\ substitution (called {\em rigid} level mappings); (2)
2825: a pair (\pre, \post), with \pre, \post \sse $Atom_L$, where \post\ is
2826: a model of the program and \pre\ is a characterisation of call
2827: patterns computed using abstract interpretation.
2828:
2829:
2830: A generalisation of the definition of left-termination considers a
2831: program together with a {\em set} of queries \cite{SVB92,BCF94}, while
2832: we considered a program and a single query. We say that a
2833: program $P$ and a set of queries $\cal Q$
2834: left-terminate if every derivation for $P$ and any $Q \in \cal Q$ via
2835: the leftmost selection rule is finite. The benefit of such a
2836: definition consists of having just one single proof of termination for
2837: a set of queries rather than a set of proofs, one for each query in
2838: the set. However, we observe that in our examples on acceptability,
2839: proofs can easily be generalised to a set of queries. For instance,
2840: for a level mapping such that $|${\tt p($t$)}$| = |t|$, it is
2841: immediate to conclude that all queries {\tt p($T$)}, where $T$ is a
2842: list, are acceptable. Conversely, is it the case that if $P$ and
2843: ${\cal Q}$ left-terminate then $P$ and any $Q \in \cal Q$ are
2844: acceptable by a same $|.|$ and $I$? The answer is affirmative. In
2845: fact, from the proof of the Completeness Theorem~\ref{c2:acc:tcor}
2846: \cite[(Ruggieri, 1999, Theorem~2.3.20)]{Rug99},
2847: if $P$ and $Q$ left-terminate
2848: then they are acceptable by a level mapping $|.|_P$ and a Herbrand
2849: model $I_P$ that {\em only} depend on $P$. This implies that every $Q
2850: \in \cal Q$ is acceptable by $|.|_P$ and $I_P$. In conclusion,
2851: acceptability by $|.|_P$ and $I_P$ precisely characterises the maximal
2852: set $\cal Q$ such that $P$ and $\cal Q$ left-terminate.
2853:
2854: Finally, instead of considering left-termination of a program $P$ and
2855: a query $Q$, one may be
2856: interested in proving left-termination of some permutation $P'$ and
2857: $Q'$ of them. A permutation of $P$ ($Q$) is any program (query)
2858: obtained by reordering clause body atoms in $P$ ($Q$).
2859: This notion is called $\sigma$-termination in \cite{HM01}, where a
2860: system for automatic inference is presented. $\sigma$-termination is
2861: strictly weaker than left-termination, and strictly stronger than
2862: $\exists$-termination (e.g., program {\tt PRODCONS} in
2863: figure~\ref{prodcons-prog} and {\tt system($n$)}, with $n \in \nat$,
2864: $\exists$-terminate but do not $\sigma$-terminate).
2865:
2866:
2867: \subsection{Writing Left-Terminating Programs}
2868: There are also works that are not directly concerned with proving an
2869: existing program left-terminating, but rather with heuristics and
2870: transformations that help write left-terminating programs.
2871:
2872: Hoarau \& Mesnard \shortcite{HM98} studied inferring and
2873: compiling termination for (constraint) logic programs. {\em Inferring}
2874: termination means inferring a set of queries for which a program
2875: ``potentially'' terminates, that is to say, it terminates after
2876: possible reordering of atoms. This phase uses abstract interpretation and the
2877: Boolean $\mu$-calculus. {\em Compiling} termination means reordering
2878: the body atoms so that the program terminates. The method is
2879: implemented.
2880:
2881: Neumerkel \& Mesnard \shortcite{NM99} studied the problem of localising
2882: and explaining reasons for nontermination in a logic programs. The
2883: work aims at assisting programmers in writing terminating programs and
2884: helping them to {\em understand} why their program does not
2885: terminate. The method has been implemented and is intended as a
2886: debugging tool, in particular for beginners (it has been used for
2887: teaching purposes). The idea is to localise a fragment of a program
2888: that is in itself already non-terminating, and hence constitutes an
2889: explanation for non-termination of the whole program.
2890:
2891: \subsection{Transformational Approaches}
2892: It is possible to investigate termination of logic programs by
2893: transforming them to some other formal system. If the transformation
2894: preserves termination, one can resort to the compendium of techniques
2895: of those formal systems for the purpose of proving termination of
2896: the original logic program.
2897:
2898: Baudinet \shortcite{Bau92} considered transforming logic programs
2899: into functional programs. Termination of the transformed programs can
2900: then be studied by structural induction. Her approach covers general
2901: logic programs, existential termination and the effects of Prolog cut.
2902:
2903: There is a considerable amount of literature on transforming logic
2904: programs to term rewriting systems (TRSs), which are perhaps the
2905: generic formalism for studying termination as such. It is very common
2906: in these transformational approaches to use modes. The intuitive idea
2907: is usually that the input of an atom has to rewrite into the output of
2908: that atom. Most of those works assume the left-to-right selection
2909: rule. One valuable exception is due to Krishna Rao {\em
2910: et~al.}~\shortcite{KRKS98}, where termination is considered
2911: w.r.t.~selection rules that respect a producer-consumer relation among
2912: variables in clauses. Such a producer-consumer relation is formalised
2913: with an extension of the notion of well-modedness. The approach improves
2914: over the original proposal of the authors \cite{KKS92}, where
2915: the LD selection rule was assumed.
2916:
2917:
2918: The approach by Aguzzi \& Modigliani \shortcite{AguMod93} takes into
2919: account that logic programs can be used in several modes, even within
2920: the same run of a program. Moreover, the approach is able to handle
2921: {\em local} variables, i.e., variables occurring only in a clause body
2922: but not in the head. Such variables model what is
2923: sometimes called {\em sideways information passing}. One remarkable
2924: property of the transformation is that it provides a characterisation
2925: of termination, albeit only for the limited class of {\em input
2926: driven\/} logic programs \cite{AE93}. So for this limited class, a
2927: program terminates if and only if the corresponding TRS terminates.
2928:
2929: Ganzinger \& Waldmann \shortcite{GW92} proposed a transformation of
2930: logic programs into {\em conditional} TRSs. In such TRSs, the rules
2931: have the form $u_1\to v_1,\dots,u_n\to v_n \Rightarrow
2932: s\to t$, which is to be read as ``if each $u_i$ rewrites to
2933: $v_i$, then $s$ rewrites to $t$''. Well moded logic program clauses
2934: are transformed into such rules, where there is a correspondence
2935: between each $u_i$ and the input of the $i$th body atom, each $v_i$
2936: and the output of the $i$th body atom, $s$ and the input of the head,
2937: and $t$ and the output of the head. The method improves over
2938: \cite{KKS92} in applicability and simplicity.
2939:
2940: Marchiori \shortcite{MarM94} improves over the transformations of
2941: \cite{AguMod93} and \cite{GW92} by adopting enhanced methods to detect
2942: unification-freeness, i.e. situations where unification (used by
2943: SLD-resolution) boils down to matching (used by TRS operational
2944: semantics). Another contribution lies in the fact that the
2945: transformation proposed is modular, i.e., it considers each clause in
2946: isolation.
2947:
2948: More recently, Arts \shortcite{Art97} investigated a new termination
2949: method for TRSs called \emph{innermost normalisation} and applied it
2950: also to TRSs obtained by transforming well moded logic programs. The
2951: technique improves over \cite{KKS92}.
2952:
2953:
2954: \subsection{Dynamic Selection Rules}
2955: By {\em dynamic\/} selection rules we mean those rules where selection
2956: depends on the degree of instantiation of atoms at run-time. Second
2957: generation logic languages adopt dynamic selection rules as control
2958: primitives. We mention here delay
2959: declarations, input-consuming derivations and guarded clauses.
2960:
2961:
2962: Apt \& Luitjes \shortcite{AL95} consider deterministic programs, i.e.,
2963: programs where for each selectable atom (according to the delay
2964: declarations), there is at most one clause head unifiable with it. For
2965: such programs, the existence of one successful derivation implies that
2966: all derivations are finite. Apt \& Luitjes also give conditions for
2967: the termination of {\tt append}, but these are ad-hoc and do not
2968: address the general problem.
2969:
2970:
2971: L{\"u}ttringhaus-Kappel~\shortcite{Lut93} proposes a method for
2972: generating control (delay declarations) automatically. The method
2973: finds {\em acceptable} delay declarations, ensuring that the most
2974: general selectable atoms have finite SLD-trees. What is required
2975: however are {\em safe} delay declarations, ensuring that {\em
2976: instances} of most general selectable atoms have finite SLD-trees. A
2977: {\em safe} program is a program for which every acceptable delay
2978: declaration is safe. L{\"u}ttringhaus-Kappel states that all programs
2979: he has considered are safe, but gives no hint as to how this might be
2980: shown in general. This work is hence not about {\em proving}
2981: termination. In some cases, the delay declarations that are generated
2982: require an argument of an atom to be a list before that atom can be
2983: selected. This is similar to requiring the atom to be bounded, i.e. to
2984: the approach of \cite{MT99,MK97} and of section~\ref{local-sec}.
2985:
2986: Naish \shortcite{Nai92c} considers delay declarations that test for
2987: partial instantiation of certain predicate arguments. Such delay
2988: declarations implicitly ensure input-consu\-ming derivations. He gives
2989: good intuitive explanations about possible causes of loops,
2990: essentially {\em circular modes} and {\em speculative output
2991: bindings}. The first cause (see Example~\ref{circular-ex}) can be
2992: eliminated by requiring programs to be {\em permutation
2993: nicely\footnote{A slightly more general notion than permutation {\em
2994: simply}-modedness.} moded}. Speculative output bindings are indeed a
2995: good explanation for the fact that $\tt permute(\out,\inp)$ (see
2996: Example~\ref{ex:ic-strictly-lds}) does not input terminate. Naish then
2997: makes the additional assumption that the selection rule always selects
2998: the leftmost selectable atom, and proposes to put recursive calls last
2999: in clause bodies. Effectively, this guarantees that the recursive
3000: calls are {\em ground} in their input positions, which goes beyond
3001: assuming input-consuming derivations.
3002:
3003: Naish's proposal has been formalised and refined by Smaus {\em
3004: et~al.}~\shortcite{SHK01}. They consider atoms that may loop when
3005: called with insufficient input, or in other words, atoms for which
3006: assuming input-consuming derivations is insufficient to guarantee
3007: termination. It is proposed to place such atoms sufficiently late; all
3008: producers of input for such atoms must occur textually earlier.
3009: Effectively, this is an assumption about the selection rule that lies
3010: between input-consuming derivations and local delay-safe derivations.
3011:
3012: Our characterisation of input termination only requires (permutation)
3013: simply moded programs and queries. The first sound but incomplete
3014: characterisation of \cite{Sma99} assumed well and nicely moded
3015: programs. It was then found that the condition of well-modedness could
3016: easily be lifted~\cite{BER99}. It was only by restricting to {\em
3017: simply} moded programs that one could give a characterisation that
3018: is also complete. This means of course that the method of \cite{BER99}
3019: does not subsume the method of \cite{BERS01} surveyed here, but
3020: nevertheless, we believe that the fact that the characterisation is
3021: complete is more important. Input-consuming derivations can be
3022: ensured in existing systems using {\em delay declarations} such as
3023: provided by G{\"o}del \cite{HL94} or SICStus \cite{sicstus}. This is
3024: shown in \cite{BER00,BERS01,Sma99t}.
3025:
3026: The definition of input-consuming derivations has a certain
3027: resemblance with derivations in the parallel logic language of {\em
3028: (Flat) Guarded Horn Clauses} \cite{Ued88}. In (F)GHC, an atom and
3029: clause may be resolved only if the atom is an instance of the clause
3030: head, and a test ({\em guard}) on clause selectability is satisfied.
3031: Termination of GHC programs was studied by Krishna Rao {\em
3032: et~al.}~\shortcite{KKS97} by transforming them into TRSs.
3033:
3034: Pedreschi \& Ruggieri \shortcite{PR99fail} characterised a
3035: class of programs with guards and queries that have no
3036: failed derivation. For those programs, termination for one selection
3037: rule implies termination (with success) for all selection rules. This
3038: situation has been previously described as saying that a program does
3039: not make speculative bindings~\cite{SHK01}. The approach by Pedreschi
3040: \& Ruggieri is an improvement w.r.t.~the latter one, since what might
3041: be called ``shallow'' failure does not count as failure. For example,
3042: the program \texttt{QUICKSORT} is considered failure-free in the
3043: approach of Pedreschi \& Ruggieri.
3044:
3045:
3046:
3047: \subsection{$\exists$-Termination and Bounded Nondeterminism}
3048:
3049: Concerning termination w.r.t. fair selection rules, i.e.,
3050: $\exists$-termination, we are aware only of the works of Gori
3051: \shortcite{Gor00} and McPhee \shortcite{McPhee00}. Gori proposes an
3052: automatic system based on abstract interpretation analysis that infers
3053: $\exists$-termination. McPhee proposes the notion of {\em prioritised
3054: fair selection rules}, where atoms that are known to terminate are
3055: selected first, with the aim of improving efficiency of fair selection
3056: rules. He adopts the automatic test of Lindenstrauss \& Sagiv
3057: \shortcite{LS97} to infer
3058: (left-)termination, but, in principle, the idea applies to any
3059: automatic termination inference system.
3060:
3061:
3062: Concerning bounded nondeterminism, Martin \& King \shortcite{MK97}
3063: define a transformation for G{\"o}del programs, which shares with the
3064: transformation of Definition~\ref{c2:def:bntrans}
3065: the idea of not following derivations longer than a certain length.
3066: However, they rely on sufficient conditions for inferring the length
3067: of refutations, namely termination via a class of selection rules
3068: called {\em semilocal}. Their transformation adds run-time overhead,
3069: since the maximum length is computed at run-time. On the other hand, a
3070: run-time analysis is potentially able to generate more precise upper
3071: bounds than our static transformation, and thus to cut more
3072: unsuccessful branches. Also, the idea of pruning SLD-derivations at
3073: run-time is common to the research area of loop checking \cite{BAK91}.
3074:
3075: Sufficient (semi-)automatic methods to approximate the number of
3076: computed instances by means of lower and upper bounds have been
3077: studied in the context of cost analysis of logic programs \cite{DL93}
3078: and of cardinality analysis of Prolog programs \cite{BCMV94}. Of
3079: course, if $\infty$ is a lower bound to the number of computed
3080: instances of $P$ and $Q$ then they do not have bounded nondeterminism.
3081: Dually, if $n \in N$ is an upper bound then $P$ and $Q$ have bounded
3082: nondeterminism. In this case, however, we are still left with the
3083: problem of determining a depth of the SLD-tree that includes all the
3084: refutations.
3085:
3086: \subsection{Automatic Termination Inference}\label{subsec:automatic}
3087: On a theoretical level, the problem of deciding whether a program
3088: belongs to one of the classes studied in this article is undecidable.
3089: This was formally shown by Bezem \shortcite{Bez93} for recurrence, and
3090: by Ruggieri \shortcite{Rug99} for acceptability, fair-boundedness and
3091: boundedness. On a practical level, however, many methods have been
3092: proposed to infer (usually: left-) termination automatically. This
3093: research stream is currently very active, and some efficient tools
3094: are already integrated in compilers.
3095:
3096: A challenging topic of the research in automatic termination inference
3097: consists in finding standard forms of level mappings and models,
3098: so that the solution of the resulting proof obligations can be
3099: reduced to known problems for which efficient algorithms exist
3100: \cite{BCF94,BK97,DDF93,Plu90,vG91}.
3101:
3102: As an example, we mention the detailed account of automatic
3103: termination analysis by Decorte {\em et~al.}\ \shortcite{DDV99}.
3104: The main idea is as follows. Termination analysis is
3105: parametrised by several factors, such as the choice of modes and
3106: level mappings. In practice, these are usually inferred using abstract
3107: interpretation techniques. This is often not very efficient.
3108: Therefore Decorte {\em et~al.} propose to encode
3109: all those parameters and the conditions that have to hold for
3110: them as constraints. So for example, there are constraint
3111: variables for each weighting parameter used in the definition of
3112: (semi-) linear norms and level mappings. To show termination of the
3113: analysed program, one has to find a solution to the constraint system.
3114:
3115:
3116: Lindenstrauss \& Sagiv \shortcite{LS97} developed the system {\em
3117: TermiLog\/} for checking termination. They use linear
3118: norms, (monotonicity and equality) constraint inference and the
3119: termination test of Sagiv \shortcite{Sag91}, originally designed for
3120: Datalog programs. The implementation of the static termination
3121: analysis algorithm of the Mercury system ~\cite{SSS97} exploits mode
3122: and type information provided by the programmer. Speirs {\em et~al.}
3123: claim a better performance than the {\em TermiLog\/} system in the
3124: average case. The implementation of fair selection rules has been
3125: announced for future releases of Mercury. Codish \index{Codish} \&
3126: Taboch \index{Taboch} \shortcite{CT99} proposed a formal semantics
3127: basis that facilitates abstract interpretation for inferring
3128: left-termination.
3129:
3130: Recently, Mesnard {\em et~al.}~\shortcite{Mesnard00} developed the cTI
3131: system for {\em bottom-up} left-termination inference of logic
3132: programs. Bottom-up refers to the use of abstract interpretation based
3133: fixpoint computations whose output is a set of queries for which the
3134: system infers termination. The results show that, on several benchmark
3135: programs, the sets of queries inferred by cTI strictly include the set
3136: of queries for which the top-down methods of \cite{DDV99,LS97,SSS97}
3137: can show termination.
3138:
3139: Finally, we recall the approach by St{\"a}rk~\shortcite{Sta98} to prove
3140: both termination and partial correctness together. His system, called
3141: LPTP, is implemented in Prolog and consists of an interactive theorem
3142: prover able to prove termination and correctness of Prolog programs
3143: with negation, arithmetic built-in's and meta-predicates such as {\tt
3144: call}. The formal theory underlying LPTP is an
3145: inductive extension of pure Prolog programs that allows to express
3146: modes and types of predicates.
3147:
3148:
3149: \subsection{Extensions of Pure Logic Programming}
3150: In this article, we have assumed the standard definition of
3151: SLD-derivations for definite logic programs. We now briefly discuss
3152: termination of alternative or generalised execution models of logic
3153: programs.
3154:
3155: A declarative characterisation of strong termination for {\em general}
3156: logic programs and queries (i.e., with negation) was proposed by Apt
3157: \& Bezem \shortcite{AB91}. The execution model assumed is {\em SLDNF}
3158: resolution with a {\em safe} (not to be confused with {\em delay-safe}
3159: \cite{MT99}) selection rule, meaning that negative literals can be
3160: selected only if they are ground. Also, we mention the bottom-up approach of
3161: Balbiani~\shortcite{Bal91}, where an operator $T_P$ is provided such
3162: that its ordinal closure coincides with those ground atoms $A$ such
3163: that $P$ and $A$ strongly terminate.
3164:
3165: Apt \& Pedreschi \shortcite{AP93r} have generalised acceptability to
3166: reason on programs with negation under SLDNF resolution. The
3167: characterisation is sound. Also, it is complete for safe selection
3168: rules. Marchiori \shortcite{Mar95c} proposes a modification of
3169: acceptability to reason on programs with Chan's
3170: constructive negation resolution.
3171:
3172: Termination of {\em abductive} logic programs has been studied by Verbaeten
3173: \shortcite{Ver99}. The execution model of abductive logic programs,
3174: called {\em SLDNFA} resolution, extends SLDNF resolution.
3175: Just as for Apt \& Bezem \shortcite{AB91}, the selection rule is an
3176: arbitrary safe one, but
3177: the definition of safe is weaker in this context. Essentially,
3178: SLDNFA resolution behaves worse than SLDNF resolution
3179: w.r.t.~termination, which is why the conditions given by Apt \& Bezem
3180: \shortcite{AB91}
3181: have to be strengthened. Finally, we point out that the conditions
3182: given are sufficient but not necessary.
3183:
3184: {\em Tabled} logic programming is particularly interesting in the
3185: context of termination analysis since tabling improves the termination
3186: behaviour of a logic program, compared to ordinary execution. The
3187: works we discuss in the following take advantage of this, i.e., they can show
3188: termination in interesting cases where ordinary execution does not
3189: terminate. They assume tabled execution based on the left-to-right
3190: selection rule.
3191:
3192: A declarative characterisation of tabled termination has been given by
3193: Decorte {\em et~al.}~\shortcite{DDLMS98}. To automate termination
3194: proofs of tabled logic programs, this work has been combined by
3195: Verbaeten \& De Schreye \shortcite{VD01} with the constraint-based
3196: approach to proving left-termination automatically, discussed above
3197: \cite{DDV99}. Verbaeten {\em et~al.}~\shortcite{VSD01} have studied
3198: termination of programs using a mix of tabled and ordinary execution.
3199:
3200: Concerning {\em constraint} logic programming (CLP), Colussi
3201: {\em et al.}~\shortcite{CMM95} first proposed a necessary and sufficient condition for
3202: left-termination, inspired by the method of Floyd for termination of
3203: flowchart programs. Their method consists of assigning a data flow
3204: graph to a program, and then to state conditions to prevent the
3205: program to enter an infinite loop in the graph.
3206:
3207: Also, Ruggieri~\shortcite{Rug97t} proposed an extension of
3208: acceptability that is sound and complete for {\em ideal} CLP
3209: languages. A CLP language is ideal if its constraint solver, the
3210: procedure used to test consistency of constraints, returns $true$ on a
3211: consistent constraint and $false$ on an inconsistent one. In
3212: contrast, a non-ideal constraint solver may return $unknown$ if it is
3213: unable to determine (in)consistency. An example of non-ideal
3214: CLP language is the CLP(${\cal R}$) system, for which Ruggieri
3215: proposes additional proof obligations (based on a notion of modes) to
3216: acceptability in order to obtain a sound characterisation of
3217: left-termination.
3218:
3219: Mesnard~\shortcite{Mes96} provides sufficient termination conditions
3220: based on approximation techniques and boolean $\mu$-calculus, with the
3221: aim of {\em inferring\/} a class of left-terminating CLP queries. The
3222: approach has been refined and implemented by Hoarau and
3223: Mesnard~\shortcite{HM98}.
3224:
3225: \section{Conclusion}\label{conc-sec}
3226: In this article, we have surveyed six different classes of terminating
3227: logic programs and queries. For each class, we have provided a sound
3228: declarative characterisation of termination. Except for local delay
3229: termination, this characterisation was also complete. We have offered
3230: a unified view of those classes allowing for non-trivial formal
3231: comparisons.
3232:
3233: In subsection~\ref{characterisations-subsec}, we have compared the
3234: different characterisations w.r.t.~certain technical details with the
3235: aim of understanding the role each technical detail plays.
3236:
3237: In subsection~\ref{from-st-to-bn-subsec}, we have compared
3238: the classes themselves. The inclusion relations among them are
3239: summarised in the hierarchy of figure~\ref{overview-fig}.
3240: Intuitively, as the assumptions about the selection rule become
3241: stronger, the proof obligations about programs become weaker.
3242:
3243: One may ask: in how far is such a hierarchy ad-hoc, and could other
3244: classes be considered? We believe that the interest in strong
3245: termination, $\exists$-termination and bounded nondeterminism is
3246: evident because they are cornerstones of the whole spectrum of
3247: classes. The interest in left-termination is motivated by the fact
3248: that the standard selection rule of Prolog is assumed.
3249:
3250: The interest in input termination and local delay termination is more
3251: arguable. We cannot claim that there are no other interesting classes
3252: in the surroundings of those two classes. Nevertheless, we believe
3253: that the distinction between input-consuming and local delay-safe
3254: selection rules captures an important difference among dynamic selection
3255: rules: requiring derivations to be input-consuming can be considered a
3256: reasonable minimum requirement to ensure termination, as we have
3257: argued that only very simple or contrived programs strongly
3258: terminate. In particular, the selection rule does not allow for
3259: methods showing termination that rely on boundedness of the selected
3260: atom. At the time of the selection, the depth of the SLD tree of an
3261: atom is not determined (by the atom itself). In contrast, local
3262: delay-safe selection rules require that the selected atom is bounded,
3263: and thus the depth of the SLD tree of an atom is determined.
3264:
3265: We thus hope that we have captured much of the essence of the effect
3266: different choices of selection rules have on termination. This should
3267: be a step towards a possible automatic choice of selection rule and
3268: thus towards realising Kowalski's ideal.
3269:
3270: \bibliography{class}
3271:
3272: \end{document}
3273:
3274: