1: \documentclass[acmtocl]{acmtrans2m}
2:
3: \acmVolume{TBD}
4: \acmNumber{TBD}
5: \acmYear{TBD}
6: \acmMonth{TBD}
7:
8: \newtheorem{theorem}{Theorem}[section]
9: \newtheorem{conjecture}[theorem]{Conjecture}
10: \newtheorem{corollary}[theorem]{Corollary}
11: \newtheorem{proposition}[theorem]{Proposition}
12: \newtheorem{lemma}[theorem]{Lemma}
13: \newdef{definition}[theorem]{Definition}
14: \newdef{remark}[theorem]{Remark}
15: \newtheorem{example}{Example}[section]
16:
17: \markboth{Yi-Dong Shen et al.}{Characterizing
18: Termination of General Logic Programs}
19:
20: \title{A Dynamic Approach to Characterizing
21: Termination of General Logic Programs}
22: \author{YI-DONG SHEN\\Chongqing University\\
23: JIA-HUAI YOU, LI-YAN YUAN and SAMUEL S. P. SHEN\\University of Alberta
24: \and
25: QIANG YANG\\Simon Fraser University}
26:
27: \begin{abstract}
28: We present a new characterization of termination of general
29: logic programs. Most existing termination analysis approaches
30: rely on some static information about the structure
31: of the source code of a logic program, such as
32: modes/types, norms/level mappings, models/interargument
33: relations, and the like. We propose a dynamic approach
34: which employs some
35: key dynamic features of an infinite (generalized) SLDNF-derivation,
36: such as repetition of selected subgoals and recursive
37: increase in term size. We also introduce a new formulation of
38: SLDNF-trees, called generalized SLDNF-trees.
39: Generalized SLDNF-trees deal with
40: negative subgoals in the same way as Prolog and
41: exist for any general logic programs.
42: \end{abstract}
43:
44: \category{D.1.6}{Programming Techniques}{Logic Programming}
45:
46: \category{D.1.2}{Programming Techniques}{Automatic Programming}
47:
48: \category{F.4.1}{Mathematical Logic
49: and Formal Languages}{Mathematical Logic}[logic programming]
50:
51: \terms{Languages, Theory}
52:
53: \keywords{Termination analysis, dynamic characterization, Prolog}
54:
55: \begin{document}
56:
57: \begin{bottomstuff}
58: Author's address: Yi-Dong Shen, Department of Computer Science,
59: Chongqing University, Chongqing 400044, China.
60: Email: ydshen@cs.ualberta.ca.
61: Jia-Huai You and Li-Yan Yuan, Department of Computing Science, University of
62: Alberta, Edmonton, Canada T6G 2H1. Email: \{you, yuan\}@cs.ualberta.ca.
63: Samuel S. P. Shen, Department of Mathematics, University of
64: Alberta, Edmonton, Canada T6G 2H1. Email: shen@ualberta.ca.
65: Qiang Yang, School of Computing Science,
66: Simon Fraser University, Burnaby, BC, Canada V5A 1S6.
67: Email: qyang@cs.sfu.ca.
68: \end{bottomstuff}
69: \maketitle
70:
71: \section{Introduction}
72: For a program in any computer language, in addition to having to be logically
73: correct, it should be terminating. Due to frequent use of recursion in
74: logic programming, however, a logic program may more likely be
75: non-terminating than a procedural program. Termination of
76: logic programs then becomes an important topic in
77: logic programming research. Because the problem is extremely hard (undecidable
78: in general), it has been considered as a {\em never-ending story}; see
79: \cite{DD93} for a comprehensive survey.
80:
81: The goal of termination analysis is to establish a characterization
82: of termination of a logic program and design algorithms for automatic
83: verification. A lot of methods for termination analysis have been
84: proposed in the last decade.
85: A majority of these existing methods are the {\em norm-} or {\em level
86: mapping-based} approaches, which consist of inferring mode/type information, inferring
87: norms/level mappings, inferring models/interargument relations, and verifying
88: some well-founded conditions (constraints). For example,
89: Ullman and Van Gelder \cite{UVG88} and
90: Pl\"{u}mer \cite{Pl90a,Pl90b} focused on
91: establishing a decrease in term size of some recursive calls based on
92: interargument relations; Apt, Bezem and Pedreschi \cite{Apt1,Bezem92},
93: and Bossi, Cocco and Fabris \cite{BCF94}
94: provided characterizations of Prolog left-termination based on level
95: mappings/norms and models; Verschaetse \cite{V92}, Decorte, De Schreye
96: and Fabris \cite{DDF93}, and Martin, King and Soper \cite{MKS96} exploited inferring
97: norms/level mappings from mode and type information;
98: De Schreye and Verschaetse \cite{DV95}, Brodsky and Sagiv \cite{BS91},
99: and Lindenstrauss and Sagiv \cite{LS97} discussed
100: automatic inference of interargument/size relations;
101: De Schreye, Verschaetse and Bruynooghe \cite{DVB92}
102: addressed automatic verification of the well-founded constraints.
103: Very recently, Decorte, De Schreye and Vandecasteele \cite{DDV99}
104: presented an elegant unified termination analysis that integrates all
105: the above components to produce a set of constraints that, when solvable,
106: yields a termination proof.
107:
108: It is easy to see that the above methods
109: are {\em compile-time} (or {\em static})
110: approaches in the sense that they make termination
111: analysis only relying on some {\em static} information about the structure
112: (of the source code) of a logic program, such as
113: modes/types, norms (i.e. term sizes of atoms of clauses)/level
114: mappings, models/interargument relations, and the like.
115: Our observation shows that some {\em dynamic}
116: information about the structure of a concrete infinite SLDNF-derivation,
117: such as {\em repetition} of selected subgoals and {\em recursive
118: increase} in term size, plays a crucial role in characterizing the
119: termination. Such dynamic features are hard to capture by
120: applying a compile-time approach. This suggests that methods
121: of extracting and utilizing
122: dynamic features for termination analysis are worth exploiting.
123:
124: In this note, we present a {\em dynamic} approach
125: by employing dynamic features
126: of an infinite (generalized) SLDNF-derivation to
127: characterize termination of general logic programs.
128: In Section 2, we introduce a notion
129: of a generalized SLDNF-tree, which is the basis of our method. Roughly
130: speaking, a generalized SLDNF-tree is a set of standard
131: SLDNF-trees augmented
132: with an ancestor-descendant relation on their subgoals. In Section 3, we
133: define a key concept, {\em loop goals}, which captures both repetition
134: of selected subgoals and recursive increase in term size of these
135: subgoals. We then prove
136: a necessary and sufficient condition for an infinite generalized
137: SLDNF-derivation in terms of loop goals.
138: This condition allows us to establish a dynamic
139: characterization of termination of general logic programs (Section 4).
140: In Section 5, we mention the related work, and
141: in Section 6 we conclude the paper with our future work.
142:
143: \subsection{Preliminaries}
144:
145: We present our notation and review some standard
146: terminology of logic programs as described in \cite{Ld87}.
147:
148: Variables begin with a capital letter, and predicate, function
149: and constant symbols with a lower case letter.
150: A term is a constant, a variable, or a function
151: of the form $f(T_1, ..., T_m)$ where $f$ is a function symbol
152: and the $T_i$s are terms.
153: An atom is of the form
154: $p(T_1, ..., T_m)$ where $p$ is a predicate symbol
155: and the $T_i$s are terms. A literal is of the form
156: $A$ or $\neg A$ where $A$ is an atom. Let $A$ be an atom/term.
157: The size of $A$, denoted $|A|$, is the
158: number of occurrences of function symbols,
159: variables and constants in $A$.
160: By $\{A_i\}_{i=1}^n$ we denote a sequence $A_1$, $A_2$, ..., $A_n$.
161: Two atoms, $A$ and $B$, are said to be {\em variants} if
162: they are the same up to variable renaming.
163:
164: Lists are commonly used terms. A list is of the form
165: $[]$ or $[T|L]$ where $T$ is a term and $L$ is a list.
166: For our purpose, the symbols $[$, $]$ and $|$ in a list
167: are treated as function symbols.
168:
169: \begin{definition}
170: A (general) {\em logic program} is a finite set
171: of clauses of the form
172:
173: $\qquad A\leftarrow L_1,..., L_n$
174:
175: \noindent where $A$ is an atom and $L_i$s are literals.
176: When $n=0$, the ``$\leftarrow$'' symbol is omitted.
177: $A$ is called the {\em head} and $L_1,...,L_n$ is called the
178: {\em body} of the clause. If a general logic program has no clause with negative
179: literals like $\neg A$ in its body, it is called a {\em positive} logic program.
180: \end{definition}
181:
182: \begin{definition}
183: A {\em goal} is a headless clause
184: $\leftarrow L_1,..., L_n$ where each literal $L_i$ is called a {\em subgoal}.
185: $L_1,..., L_n$ is called a (concrete) {\em query}.
186: \end{definition}
187:
188: The initial goal, $G_0=\leftarrow L_1,..., L_n$, is called
189: a {\em top} goal. Without loss of generality, we shall assume throughout
190: the paper that a top goal consists only of one atom, i.e. $n=1$ and $L_1$
191: is a positive literal.
192:
193: \begin{definition}
194: A {\em control strategy} consists of two rules, one for selecting
195: a goal from among a set of goals and the other for selecting
196: a subgoal from the selected goal.
197: \end{definition}
198:
199: The second rule in a control strategy is usually called
200: a {\em selection} or {\em computation}
201: rule in the literature. To facilitate our presentation,
202: throughout the paper we choose to use the best-known
203: {\em depth-first, left-most} control strategy (used in Prolog)
204: to describe our approach (It can be adapted
205: to any other fixed control strategies).
206: So the {\em selected} subgoal in each goal is the
207: left-most subgoal. Moreover, the clauses in a logic program
208: are used in their textual order.
209:
210: Trees are commonly used to represent
211: the search space of a top-down proof procedure. For convenience,
212: a node in such a tree is represented by $N_i:G_i$ where $N_i$ is the name
213: of the node and $G_i$ is a goal labeling the node. Assume no two
214: nodes have the same name. Therefore, we can refer to nodes by their names.
215:
216: \section{Generalized SLDNF-Trees}
217:
218: In order to characterize infinite
219: derivations more precisely,
220: in this section we extend the standard SLDNF-trees
221: \cite{Ld87} to include some new features.
222: We first define the ancestor-descendant relation on selected subgoals.
223: Informally, $A$ is an ancestor subgoal of $B$ if the proof of $A$
224: needs (or in other words goes via) the proof of $B$. For example,
225: let $M:\leftarrow A,A_1,...,A_m$ be a node in an SLDNF-tree, and
226: $N:\leftarrow B_1,...,B_n,A_1,...,A_m$ be a child node of $M$ that
227: is generated by resolving $M$ on the subgoal $A$ with a clause
228: $A\leftarrow B_1,...,B_n$. Then $A$ at $M$ is an ancestor subgoal
229: of all $B_i$s at $N$. However, such relationship does not
230: exist between $A$ at $M$ and any $A_j$ at $N$. It is easily seen
231: that all $B_i$s at $N$ inherit the ancestor subgoals of $A$ at $M$.
232:
233: The ancestor-descendant relation can be explicitly expressed using
234: an {\em ancestor list}.
235: The ancestor list of a subgoal $A$ at a node $M$,
236: denoted $AL_{A@M}$, is of the form $\{(N_1,D_1),...,(N_l,D_l)\}$ $(l\geq 0)$,
237: where for each $(N_i, D_i)\in AL_{A@M}$, $N_i$ is a node
238: name and $D_i$ a subgoal such that $D_i$ at $N_i$
239: is an ancestor subgoal of $A$ at $M$.
240: For instance, in the above example,
241: the ancestor list of each $B_i$ at node $N$
242: is $AL_{B_i@N}=\{(M,A)\}\cup AL_{A@M}$ and
243: the ancestor list of each $A_i$ at node $N$
244: is $AL_{A_i@N}=AL_{A_i@M}$.
245:
246: Let $N_i:G_i$ and $N_k:G_k$ be two nodes and
247: $A$ and $B$ be the selected subgoals in $G_i$ and $G_k$,
248: respectively. We use $A\prec_{anc}B$ to denote that
249: $A$ is an ancestor subgoal of $B$.
250: When $A$ is an ancestor subgoal of $B$, we refer to $B$ as a {\em descendant
251: subgoal} of $A$, $N_i$ as an {\em ancestor node} of $N_k$, and $N_k$ as
252: a {\em descendant node} of $N_i$.
253:
254: Augmenting SLDNF-trees with ancestor lists leads to the
255: following definition of SLDNF$^*$-trees.
256:
257: \begin{definition}[(SLDNF$^*$-trees)]
258: \label{tree}
259: Let $P$ be a general logic program,
260: $G_r= \leftarrow A_r$ a goal with $A_r$ an atom,
261: and $R$ the depth-first, left-most control strategy.
262: The {\em SLDNF$^*$-tree} $T_{N_r:G_r}$
263: for $P \cup \{G_r\}$ via $R$ is defined inductively as follows.
264:
265: \begin{enumerate}
266: \item
267: $N_r:G_r$ is its root node, and the tree
268: is completed once a
269: node marked as {\bf LAST} is generated
270: or when all its leaf nodes have been marked as
271: $\Box_t$, $\Box_f$ or $\Box_{fl}$.
272:
273: \item
274: \label{tree2}
275: For each node $N_i: \leftarrow L_1,...,L_m$
276: in the tree that is selected by $R$, if $m=0$ then
277: (1) $N_i$ is a {\em success} leaf marked as $\Box_t$
278: and (2) if $AL_{A_r@N_r}\neq \emptyset$ then
279: $N_i$ is also a node marked as {\bf LAST}.
280: Otherwise (i.e. $m>0$), we distinguish between the following three cases.
281:
282: \begin{enumerate}
283: \item
284: \label{tree21}
285: $L_1$ is a positive literal. For each clause
286: $B \leftarrow B_1,...,B_n$ in $P$ such that $L_1$ and $B$
287: are unifiable, $N_i$ has a child node
288:
289: $\qquad N_s: \leftarrow (B_1,...,B_n,L_2,...,L_m)\theta$
290:
291: \noindent where $\theta$ is an mgu (i.e. most general unifier) of $L_1$
292: and $B$, the ancestor list for each $B_k\theta$, $k\in \{1, \ldots, n\}$, is
293: $AL_{B_k\theta @N_s}=\{(N_i,L_1)\}\cup AL_{L_1@N_i}$,
294: and the ancestor list for each $L_k\theta$, $k\in \{2, \ldots, m\}$,
295: is $AL_{L_k\theta @N_s}=AL_{L_k@N_i}$.
296: If there exists no clause in $P$ whose head can unify with $L_1$ then
297: $N_i$ has a single child node $-$ a
298: {\em failure} leaf marked as $\Box_f$.
299:
300: \item
301: \label{tree22}
302: $L_1=\neg A$ is a ground negative literal. Let $T_{N_{i+1}:\leftarrow A}$
303: be an (subsidiary) SLDNF$^*$-tree for $P\cup \{\leftarrow A\}$
304: via $R$ with $AL_{A@N_{i+1}}=AL_{L_1@N_i}$. We have the following four
305: cases:
306: \begin{enumerate}
307: \item
308: \label{tree221}
309: $T_{N_{i+1}:\leftarrow A}$ has
310: a success leaf. Then $N_i$ has a single child node
311: $-$ a failure leaf marked as $\Box_f$.
312:
313: \item
314: \label{tree222}
315: $T_{N_{i+1}:\leftarrow A}$ has no success leaf but has
316: a flounder leaf. Then $N_i$ has a single child node
317: $-$ a flounder leaf marked as $\Box_{fl}$.
318:
319: \item
320: \label{tree223}
321: All branches of
322: $T_{N_{i+1}:\leftarrow A}$ end with a failure leaf. Then
323: $N_i$ has a single child node
324:
325: $\qquad N_s:\leftarrow L_2,...,L_m$
326:
327: \noindent with $AL_{L_k@N_s}=AL_{L_k@N_i}$ for each
328: $k\in \{2, \ldots, m\}$.
329:
330: \item
331: \label{tree224}
332: Otherwise, $N_i$ has no child node. It is
333: the last node of $T_{N_r:G_r}$ so that it
334: is marked as {\bf LAST}.
335:
336: \end{enumerate}
337:
338: \item
339: \label{tree23}
340: $L_1=\neg A$ is a non-ground negative literal. Then
341: $N_i$ has a single child node
342: $-$ a {\em flounder} leaf marked as $\Box_{fl}$.
343:
344: \end{enumerate}
345:
346: \end{enumerate}
347: \end{definition}
348:
349: Starting from the root node $N_r:G_r$,
350: we expand the nodes of the SLDNF$^*$-tree $T_{N_r:G_r}$ following
351: the depth-first order. The expansion for $T_{N_r:G_r}$ stops when either
352: a node marked as {\bf LAST} is generated or
353: all of its leaf nodes have been marked
354: as $\Box_t$, $\Box_f$ or $\Box_{fl}$.
355:
356: In this paper we do not consider floundering
357: $-$ a situation where
358: a non-ground negative subgoal is selected by $R$ (see the case
359: \ref{tree23}).
360: See \cite{chan88} for discussion on such topic.
361:
362: We first prove the following.
363:
364: \begin{theorem}
365: \label{sontree}
366: Let $T_{N_{i+1}:\leftarrow A}$ be a subsidiary SLDNF$^*$-tree
367: built for proving a negative subgoal $L_1=\neg A$ at a node $N_i$
368: (see the case \ref{tree22}).
369: Then $AL_{A@N_{i+1}}\neq \emptyset$.
370: \end{theorem}
371:
372: \begin{proof}
373: Note that $AL_{A@N_{i+1}}=AL_{L_1@N_i}$. Since the subgoal
374: $L_1$ at $N_i$ is negative, $N_i$ cannot be the root node of
375: the SLDNF$^*$-tree that contains $N_i$. Therefore, $L_1$ at $N_i$
376: has at least one ancestor subgoal (i.e. the subgoal at the root
377: node of the tree), which means $AL_{A@N_{i+1}}\neq \emptyset$.
378: \end{proof}
379:
380: In order to solve a top goal $G_0=\leftarrow A_0$, we build an
381: SLDNF$^*$-tree $T_{N_0:\leftarrow A_0}$ for $P\cup \{G_0\}$
382: via $R$ with $AL_{A_0@N_0} = \emptyset$.
383: It is easy to see that $T_{N_0:\leftarrow A_0}$ is
384: an enhancement of the standard
385: SLDNF-tree for $P\cup \{G_0\}$ via $R$ with
386: the following three new features.
387: \begin{enumerate}
388: \item
389: Each node $N_i$ is associated with an ancestor list $AL_{L_j@N_i}$
390: for each $L_j$ of its subgoals.
391: In particular, subgoals
392: of a subsidiary SLDNF$^*$-tree $T_{N_{i+1}:\leftarrow A}$
393: built for solving a negative subgoal
394: $L_1=\neg A$ at $N_i$ inherit the ancestor list $AL_{L_1@N_i}$
395: (see the case \ref{tree22}). This bridges the ancestor-descendant
396: relationships across SLDNF$^*$-trees and is especially
397: useful in identifying infinite derivations across
398: SLDNF$^*$-trees (see Example \ref{eg1}). Note that a negative subgoal
399: will never be an ancestor subgoal.
400:
401: \item
402: In a standard SLDNF-tree, to handle a ground negative subgoal
403: $L_1=\neg A$ at $N_i$ a full subsidiary
404: SLDNF-tree $FT$ for $P\cup \{\leftarrow A\}$ via
405: $R$ must be generated. In an SLDNF$^*$-tree, however,
406: the subsidiary SLDNF$^*$-tree
407: $T_{N_{i+1}:\leftarrow A}$ may not include all branches of $FT$
408: because it will terminate at the first success leaf
409: (see the case \ref{tree2} where by Theorem \ref{sontree}
410: $AL_{A@N_{i+1}}\neq \emptyset$).
411: The intuition behind this is that it is absolutely
412: unnecessary to exhaust the remaining branches of $FT$
413: because they would never generate any new answers for $A$ (and $\neg A$).
414: Such a pruning mechanism embedded in SLDNF$^*$-trees is very
415: useful in not only improving
416: the efficiency of query evaluation but also avoiding some possible
417: infinite derivations (see Example \ref{eg2}). In fact, Prolog
418: performs the same pruning by using a {\em cut}
419: operator to skip the remaining branches
420: of $FT$ once the first success leaf is generated
421: (e.g. see SICStus Prolog \cite{SICSTUS}).
422:
423: \item
424: A well-known problem with the standard SLDNF-tree approach
425: (formally called {\em SLDNF-resolution} \cite{Cl79,Ld87}) is that for some
426: programs, such as $P=\{A\leftarrow \neg A\}$ and $G_0=\leftarrow A$,
427: no SLDNF-trees exist \cite{AD94,KK89,MT92}. The main reason for
428: this abnormality lies in the fact that to solve a negative subgoal $\neg A$
429: it generates a subsidiary SLDNF-tree $FT$ for
430: $P\cup \{\leftarrow A\}$ via $R$ {\em which is supposed either to contain
431: a success leaf or to consist of failure leaves}.
432: When $FT$ neither contains a success leaf nor finitely fails by
433: going into an infinite derivation,
434: the negative subgoal cannot be handled.
435:
436: In contrast, SLDNF$^*$-trees exist for any general logic programs.
437: A ground negative subgoal $\neg A$ at a node $N_i$ succeeds
438: if all branches of the subsidiary SLDNF$^*$-tree $T_{N_{i+1}:\leftarrow A}$
439: end with a failure leaf (see the case \ref{tree223}), and
440: fails if $T_{N_{i+1}:\leftarrow A}$ has a success leaf
441: (see the case \ref{tree221}). Otherwise, the value of the subgoal
442: $\neg A$ is undetermined and thus $N_i$ is marked
443: as {\bf LAST}, showing that it is the last node of the underlying
444: SLDNF$^*$-tree which can be finitely generated
445: (see the case \ref{tree224}).\footnote{This case occurs when either
446: $T_{N_{i+1}:\leftarrow A}$ or some of its descendant SLDNF$^*$-trees
447: is infinite, or $T_{N_{i+1}:\leftarrow A}$ has an infinite number of
448: descendant SLDNF$^*$-trees. Note that {\bf LAST} is used here only
449: for the purpose of formulating an SLDNF$^*$-tree $-$
450: showing that $N_i$ is the last node of the SLDNF$^*$-tree.
451: In practical implementation
452: of SLDNF$^*$-trees, in such a case $N_i$ will never be marked by
453: {\bf LAST} since it requires an infinitely long time to
454: build $T_{N_{i+1}:\leftarrow A}$ together with all
455: of its descendant SLDNF$^*$-trees. However, the SLDNF$^*$-tree
456: is always completed at $N_i$, whether $N_i$ is marked by {\bf LAST} or not,
457: because (1) such a case occurs at most one time in an
458: SLDNF$^*$-tree and (2) it always occurs at the last generated node $N_i$.}
459: The tree is then completed here.
460:
461: \end{enumerate}
462:
463: For convenience, we use dotted edges ``$\cdot\cdot\cdot\triangleright''$
464: to connect parent and child (subsidiary) SLDNF$^*$-trees,
465: so that infinite derivations across SLDNF$^*$-trees
466: can be clearly identified. Formally, we have
467:
468: \begin{definition}
469: Let $P$ be a general logic program, $G_0$ a top goal
470: and $R$ the depth-first, left-most control strategy.
471: Let $T_{N_0:G_0}$ be the SLDNF$^*$-tree for $P \cup \{G_0\}$ via $R$
472: with $AL_{A_0@N_0} = \emptyset$.
473: A {\em generalized SLDNF-tree} for $P\cup \{G_0\}$ via $R$,
474: denoted $GT_{G_0}$, is rooted at $N_0:G_0$ and consists of $T_{N_0:G_0}$
475: along with all its descendant SLDNF$^*$-trees, where
476: parent and child SLDNF$^*$-trees are connected
477: via ``$\cdot\cdot\cdot\triangleright''$.
478: \end{definition}
479:
480: Therefore, a path of a generalized SLDNF-tree may come
481: across several SLDNF$^*$-trees through dotted edges. Any such a path
482: starting at the root node $N_0:G_0$ is called a {\em generalized
483: SLDNF-derivation}.
484:
485: Thus, there may occur two types of edges in a generalized SLDNF-derivation,
486: ``$\stackrel{C}{\longrightarrow}$''
487: and $``\cdot\cdot\cdot\triangleright''$. For convenience,
488: we use $``\Rightarrow''$ to refer to either of them.
489: Moreover, for any node $N_i:G_i$ we use
490: $L_i^1$ to refer to the selected (i.e. left-most) subgoal in $G_i$.
491:
492: \begin{example}
493: \label{eg1}
494: {\em
495: Let $P_1$ be a general logic program and $G_0$ a top goal, given by
496: \begin{tabbing}
497: $\qquad$ \= $P_1:$ $\quad$ \= $p(X)\leftarrow \neg p(f(X))$. \`$C_{p_1}$\\
498: \> $G_0:$ \> $\leftarrow p(a).$
499: \end{tabbing}
500: The generalized SLDNF-tree $GT_{\leftarrow p(a)}$
501: for $P_1\cup \{G_0\}$ is shown in
502: Figure \ref{fig1}, where $\infty$ represents an infinite extension.
503: Note that to expand the node $N_1$, we build a subsidiary SLDNF$^*$-tree
504: $T_{N_2:\leftarrow p(f(a))}$. Since $T_{N_2:\leftarrow p(f(a))}$
505: neither contains a success leaf nor finitely fails
506: (i.e. not all of its leaf nodes are marked as $\Box_f$), $N_1$
507: is the last node of $T_{N_0:\leftarrow p(a)}$, marked as {\bf LAST}.
508: We see that $GT_{\leftarrow p(a)}$ is infinite,
509: although all of its SLDNF$^*$-trees are finite.
510:
511: \begin{figure}[htb]
512: \centering
513:
514: \setlength{\unitlength}{3947sp}%
515: %
516: \begingroup\makeatletter\ifx\SetFigFont\undefined%
517: \gdef\SetFigFont#1#2#3#4#5{%
518: \reset@font\fontsize{#1}{#2pt}%
519: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
520: \selectfont}%
521: \fi\endgroup%
522: \begin{picture}(3975,1716)(676,-1006)
523: \thinlines
524: \put(2251, 89){\vector( 1, 0){0}}
525: \multiput(1876, 89)(75.00000,0.00000){5}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}
526: \put(2776, 14){\vector( 0,-1){300}}
527: \put(4051,-436){\vector( 1, 0){0}}
528: \multiput(3676,-436)(75.00000,0.00000){5}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}
529: \put(4576,-511){\vector( 0,-1){300}}
530: \put(1201,539){\vector( 0,-1){300}}
531: \put(4501,-961){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\infty$}}}
532: \put(1276,389){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}
533: \put(751,614){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0$: $\leftarrow p(a)$}}}
534: \put(2851,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}
535: \put(4651,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}
536: \put(4126,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4$: $\leftarrow p(f(f(a)))$}}}
537: \put(2251,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3$: $\leftarrow \neg p(f(f(a)))$ }}}
538: \put(676, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1$: $\leftarrow \neg p(f(a))$ }}}
539: \put(2326, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2$: $\leftarrow p(f(a))$}}}
540: \put(976,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}{\bf LAST}}}}
541: \put(2551,-661){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}{\bf LAST}}}}
542: \end{picture}
543:
544:
545: \caption{The generalized SLDNF-tree $GT_{\leftarrow p(a)}$.}\label{fig1}
546: \end{figure}
547: }
548: \end{example}
549:
550: \begin{example}
551: \label{eg2}
552: {\em
553: Consider the following general logic program and top goal.
554: \begin{tabbing}
555: $\qquad$ \= $P_2:$ $\quad$ \= $p\leftarrow \neg q$. \`$C_{p_1}$\\
556: \>\> $q$. \`$C_{q_1}$ \\
557: \>\> $q \leftarrow q$. \`$C_{q_2}$ \\
558: \> $G_0:$ \> $\leftarrow p.$
559: \end{tabbing}
560: The generalized SLDNF-tree
561: $GT_{\leftarrow p}$ for $P_2\cup \{G_0\}$ is depicted in
562: Figure \ref{fig2} (a).
563: $GT_{\leftarrow p}$ consists of two SLDNF$^*$-trees,
564: $T_{N_0:\leftarrow p}$ and $T_{N_2:\leftarrow q}$, which
565: are constructed as follows. Initially, $T_{N_0:\leftarrow p}$
566: has only the root node $N_0:\leftarrow p$. Expanding the root
567: node against the clause $C_{p_1}$ leads to the child node
568: $N_1:\leftarrow \neg q$. We then build a subsidiary SLDNF$^*$-tree
569: $T_{N_2:\leftarrow q}$ for $P_2\cup \{\leftarrow q\}$ via the
570: depth-first, left-most control strategy, where the expansion
571: stops right after the node $N_3$ is marked as {\bf LAST}.
572: Since $T_{N_2:\leftarrow q}$ has a success leaf, $N_1$ gets
573: a failure child node $N_5$. $T_{N_0:\leftarrow p}$
574: is then completed.
575:
576: For the purpose of comparison,
577: the standard SLDNF-trees for $P_2\cup \{\leftarrow p\}$
578: are shown in Figure \ref{fig2} (b).
579: Note that Figure \ref{fig2} (a) is finite,
580: whereas Figure \ref{fig2} (b) is not.
581:
582: \begin{figure}[h]
583: \centering
584:
585: \setlength{\unitlength}{3947sp}%
586: %
587: \begingroup\makeatletter\ifx\SetFigFont\undefined%
588: \gdef\SetFigFont#1#2#3#4#5{%
589: \reset@font\fontsize{#1}{#2pt}%
590: \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
591: \selectfont}%
592: \fi\endgroup%
593: \begin{picture}(5337,1971)(2776,-1261)
594: \put(3901,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}(a)}}}
595: \thinlines
596: \put(3301,-436){\vector(-2,-3){150}}
597: \put(7501,539){\vector(-2,-3){150}}
598: \put(7651,539){\vector( 2,-3){150}}
599: \put(7801, 14){\vector(-2,-3){150}}
600: \put(7951, 14){\vector( 2,-3){150}}
601: \put(4201, 14){\vector( 2,-3){150}}
602: \put(3601,-436){\vector( 2,-3){150}}
603: \put(3601,-211){\vector(-2,-3){0}}
604: \multiput(3751, 14)(-37.50000,-56.25000){4}{\makebox(1.6667,11.6667){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}
605: \put(6751,-1261){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}(b)}}}
606: \put(8101,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\infty$}}}
607: \put(3976,539){\vector( 0,-1){300}}
608: \put(6151, 14){\vector( 0,-1){300}}
609: \put(4051,389){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}
610: \put(3601, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1$: $\leftarrow \neg q$ }}}
611: \put(6226,389){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{p_1}$}}}
612: \put(5776,614){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0$: $\leftarrow p$}}}
613: \put(5776, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_1$: $\leftarrow \neg q$ }}}
614: \put(3601,614){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_0$: $\leftarrow p$}}}
615: \put(7126,389){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}
616: \put(7576, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4$: $\leftarrow q$}}}
617: \put(7801,389){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}
618: \put(7276,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5$: $\Box_t$}}}
619: \put(7426,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}
620: \put(8101,-136){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}
621: \put(7276,614){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2$: $\leftarrow q$}}}
622: \put(4126,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_5:\Box_f$}}}
623: \put(5776,-436){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_{\infty}$: $\Box_f$}}}
624: \put(3226,-361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_2$: $\leftarrow q$}}}
625: \put(2926,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_1}$}}}
626: \put(3676,-511){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{9.6}{\rmdefault}{\mddefault}{\updefault}$C_{q_2}$}}}
627: \put(3526,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_4$: $\leftarrow q$}}}
628: \put(2776,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3$: $\Box_t$}}}
629: \put(2851,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{7}{8.4}{\rmdefault}{\mddefault}{\updefault}{\bf LAST}}}}
630: \put(6976, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\rmdefault}{\mddefault}{\updefault}$N_3$: $\Box_t$}}}
631: \put(6151,539){\vector( 0,-1){300}}
632: \end{picture}
633:
634:
635: \caption{The generalized SLDNF-tree $GT_{\leftarrow p}$ (a)
636: and its two corresponding standard SLDNF-trees (b).}\label{fig2}
637: \end{figure}
638: }
639: \end{example}
640:
641:
642: \section{Characterizing an Infinite Generalized SLDNF-Derivation}
643:
644: In this section we establish a necessary and sufficient condition for
645: an infinite generalized SLDNF-derivation. We begin by introducing
646: a few concepts.
647:
648: \begin{definition}
649: \label{symbol-seq}
650: Let $T$ be a term or an atom and $S$ be
651: a string that consists of all predicate symbols, function
652: symbols, constants
653: and variables in $T$, which is obtained
654: by reading these symbols sequentially from left to
655: right. The {\em symbol string} of $T$, denoted
656: $S_T$, is the string $S$ with every variable
657: replaced by ${\cal X}$.
658: \end{definition}
659:
660: For instance, let $T_1=a$,
661: $T_2=f(X,g(X,f(a,Y)))$ and $T_3=[X,a]$.
662: Then $S_{T_1}=a$, $S_{T_2}=f{\cal X}g{\cal X}fa{\cal X}$
663: and $S_{T_3}=[{\cal X}|[a|[]]]$. Note that
664: $[X,a]$ is a simplified representation for the
665: list $[X|[a|[]]]$.
666:
667: \begin{definition}
668: \label{sub-seq}
669: Let $S_{T_1}$ and $S_{T_2}$ be two symbol strings.
670: $S_{T_1}$ is a {\em projection} of $S_{T_2}$, denoted
671: $S_{T_1}\subseteq_{proj}S_{T_2}$,
672: if $S_{T_1}$ is obtained from $S_{T_2}$ by
673: removing zero or more elements.
674: \end{definition}
675:
676: For example,
677: $a{\cal X}{\cal X}bc\subseteq_{proj}fa{\cal X}e{\cal X}b{\cal X}cd$.
678: It is easy to see
679: that the relation $\subseteq_{proj}$ is reflexive and transitive. That is,
680: for any symbol strings $S_1$, $S_2$ and $S_3$,
681: we have $S_1\subseteq_{proj}S_1$,
682: and that $S_1\subseteq_{proj}S_2$ and $S_2\subseteq_{proj}S_3$ implies
683: $S_1\subseteq_{proj}S_3$.
684:
685: \begin{definition}
686: \label{gvar}
687: Let $A_1=p(.)$ and $A_2=p(.)$
688: be two atoms. $A_1$ is said to {\em loop into} $A_2$,
689: denoted $A_1\leadsto_{loop}A_2$, if
690: $S_{A_1}\subseteq_{proj}S_{A_2}$.
691: Let $N_i:G_i$ and $N_j:G_j$ be two nodes in a generalized
692: SLDNF-derivation with $L_i^1\prec_{anc}L_j^1$ and
693: $L_i^1 \leadsto_{loop} L_j^1$.
694: Then $G_j$ is called a {\em loop goal} of $G_i$.
695: \end{definition}
696:
697: The following result is immediate.
698: \begin{theorem}
699: \label{th}
700: \begin{enumerate}
701: \item
702: The relation $\leadsto_{loop}$ is reflexive and transitive.
703: \item
704: If $A_1 \leadsto_{loop} A_2$ then $|A_1|\leq |A_2|$.
705: \item
706: If $G_3$ is a loop goal of $G_2$ that is a loop goal
707: of $G_1$ then $G_3$ is a loop goal of $G_1$.
708: \end{enumerate}
709: \end{theorem}
710:
711: Observe that since a logic program has only
712: a finite number of clauses, an infinite generalized SLDNF-derivation results
713: from repeatedly applying the same set of clauses, which leads to
714: infinite repetition of selected variant subgoals or
715: infinite repetition of selected subgoals with recursive
716: increase in term size. By recursive increase of term size
717: of a subgoal $A$ from a subgoal $B$ we mean that $A$ is $B$
718: with a few function/constant/variable symbols added
719: and possibly with some variables changed to
720: different variables. Such crucial dynamic
721: characteristics of an infinite generalized SLDNF-derivation
722: are captured by loop goals, as shown by the following principal
723: theorem.
724:
725: \begin{theorem}
726: \label{th4}
727: $D$ is an infinite generalized SLDNF-derivation
728: if and only if it is of the form
729: \begin{tabbing}
730: $\qquad$ $N_0:G_0\Rightarrow ... N_{g_1}:G_{g_1}\Rightarrow
731: ...N_{g_2}:G_{g_2}\Rightarrow ... N_{g_3}:G_{g_3}\Rightarrow ...$
732: \end{tabbing}
733: such that for any $j \geq 1$,
734: $G_{g_{j+1}}$ is a loop goal of $G_{g_j}$.
735: \end{theorem}
736:
737: We need Higman's Lemma to
738: prove this theorem.\footnote{It is one of the anonymous
739: reviewers who brought this lemma to our attention.}
740:
741: \begin{lemma}[(Higman's Lemma \cite{Hig52,Bol91})]
742: \label{hig}
743: Let $\{A_i\}_{i=1}^\infty$ be an infinite
744: sequence of strings over a finite alphabet $\Sigma$.
745: Then for some $i$ and $k>i$, $A_i \subseteq_{proj} A_k$
746: \end{lemma}
747:
748: The following result follows from Lemma \ref{hig}.
749:
750: \begin{lemma}
751: \label{hig2}
752: Let $\{A_i\}_{i=1}^\infty$ be an infinite
753: sequence of strings over a finite alphabet $\Sigma$.
754: Then there is an infinite
755: increasing integer sequence $\{n_i\}_{i=1}^\infty$ such that for all $i$
756: $A_{n_i} \subseteq_{proj} A_{n_{i+1}}$.
757: \end{lemma}
758:
759: \begin{proof}\footnote{This proof is suggested by an anonymous
760: reviewer.}
761: Suppose this is not true. Let us take a finite maximal subsequence
762: \[A_{n_1} \subseteq_{proj} A_{n_2} \subseteq_{proj} ...
763: \subseteq_{proj} A_{n_{k_1}}\]
764: The subsequence is maximal in the sense that
765: for no $i > n_{k_1}$ do we have
766: $A_{n_{k_1}} \subseteq_{proj} A_i$.
767: We know that such a subsequence with length
768: at least 2 must exist from Lemma \ref{hig} and the assumption that the
769: assertion of the lemma does not hold for the sequence $\{A_i\}_{i=1}^\infty$.
770: Now look at the elements of the original sequence with indices larger
771: than $n_{k_1}$ and take another such finite maximal subsequence from them.
772: Continuing in this way,
773: we get infinitely many such maximal subsequences.
774: Let $\{A_{n_{k_i}}\}_{i=1}^\infty$ be the sequence
775: of last elements of the maximal subsequences.
776: By Lemma \ref{hig}, this sequence has two elements,
777: $A_{n_{k_i}}$ and $A_{n_{k_j}}$ with $n_{k_i} < n_{k_j}$,
778: such that $A_{n_{k_i}} \subseteq_{proj} A_{n_{k_j}}$.
779: This contradicts the assumption that $A_{n_{k_i}}$ is
780: the last element of some finite maximal subsequence. \end{proof}
781:
782: The following lemma is needed to prove Theorem \ref{th4}.
783:
784: \begin{lemma}
785: \label{th2}
786: Let $D$ be an infinite generalized SLDNF-derivation.
787: Then there are infinitely many goals
788: $G_{g_1}, G_{g_2}, ...$
789: in $D$ such that for any $j \geq 1$,
790: $L_j^1 \prec_{anc} L_{j+1}^1$.
791: \end{lemma}
792:
793: \begin{proof}
794: Let $D$ be of the form
795: \[N_0:G_0\Rightarrow N_1:G_1 \Rightarrow ... \Rightarrow
796: N_i:G_i\Rightarrow N_{i+1}:G_{i+1} \Rightarrow ...\]
797: Consider derivation steps like
798: $N_i:G_i \stackrel{C}{\longrightarrow} N_{i+1}:G_{i+1}
799: \cdot\cdot\cdot\triangleright N_{i+2}:G_{i+2}$, where
800: $L_i^1$ is a positive subgoal and $L_{i+1}^1=\neg A$ a negative subgoal.
801: So $L_{i+2}^1=A$. We see that both $L_i^1$ and $L_{i+1}^1$ need the proof of
802: $L_{i+2}^1$. Moreover, given $L_{i+2}^1$ the provability of
803: $L_i^1$ does not depend on
804: $L_{i+1}^1$. Since $L_{i+1}^1$ has no descendant subgoals, removing
805: it would affect neither the provability nor the ancestor-descendant
806: relationships of other subgoals in $D$. Therefore, we delete
807: $L_{i+1}^1$ by marking $N_{i+1}$ with \#.
808:
809: For each derivation step
810: $N_i:G_i \stackrel{C}{\longrightarrow} N_{i+1}:G_{i+1}$, where
811: $L_i^1$ is a positive subgoal and $C=A\leftarrow B_1,...B_n$
812: such that $A\theta = L_i^1\theta$ under an mgu $\theta$, we do the following:
813: \begin{enumerate}
814: \item
815: If $n=0$, which means $L_i^1$ is proved at this step,
816: mark node $N_i$ with \#.
817:
818: \item
819: Otherwise, the proof of $L_i^1$ needs the proof of $B_j\theta$ $(j=1,...,n)$.
820: If all descendant nodes of $N_i$ in $D$ have been marked with \#, which means that
821: all $B_j\theta$ have been proved at some steps in $D$, mark node $N_i$
822: with \#.
823: \end{enumerate}
824:
825: Note that the root node $N_0$ will never be marked with \#, for otherwise
826: $G_0$ would have been proved and $D$ should have ended at a success
827: or failure leaf. After the
828: above marking process, let $D$ become
829: \begin{tabbing}
830: $\qquad$ $N_0:G_0\Rightarrow ... \Rightarrow N_{i_1}:G_{i_1} \Rightarrow ... \Rightarrow
831: N_{i_2}:G_{i_2}\Rightarrow ... \Rightarrow N_{i_k}:G_{i_k} \Rightarrow ...$
832: \end{tabbing}
833: where all nodes except $N_0,N_{i_1},N_{i_2},...,N_{i_k},...$ are marked with
834: \#. Since we use the depth-first, left-most control strategy, for any
835: $j\geq 0$ the proof of $L_{i_j}^1$ needs the proof of $L_{i_{j+1}}^1$ (let
836: $i_0=0$), for otherwise $N_{i_j}$ would have been marked with \#. That is,
837: $L_{i_j}^1$ is an ancestor subgoal of $L_{i_{j+1}}^1$.
838: Moreover, $D$ must contain
839: an infinite number of such nodes because
840: if $N_{i_k}:G_{i_k}$ was the last one,
841: which means that all nodes after $N_{i_k}$ were
842: marked with \#, then $L_{i_k}^1$
843: would be proved, so that $N_{i_k}$ should be marked with \#, a contradiction.
844: \end{proof}
845:
846: We are ready to prove Theorem \ref{th4}.
847:
848: \begin{proof}[(Proof of Theorem \ref{th4})]
849: $(\Longleftarrow)$ Straightforward.
850:
851: $(\Longrightarrow)$
852: By Lemma \ref{th2}, $D$ contains an infinite
853: sequence of selected subgoals $H_1=\{L_{j_i}^1\}_{i=1}^\infty$ such that
854: for any $i$ $L_{j_i}^1 \prec_{anc} L_{j_{i+1}}^1$.
855: Since any logic program has only a finite number of predicate
856: symbols, $H_1$ must have
857: an infinite subsequence $H_2=\{L_{k_i}^1\}_{i=1}^\infty$
858: such that all $L_{k_i}^1$ have the same predicate symbol, say $p$.
859: We now show that
860: $H_2$ has an infinite subsequence
861: $\{L_{g_i}^1\}_{i=1}^\infty$
862: such that for any $i$ $L_{g_i}^1\leadsto_{loop}L_{g_{i+1}}^1$.
863:
864: Let $T$ be the (finite) set of all constant
865: and function symbols in the logic program and let $\Sigma = T\cup \{{\cal X}\}$.
866: Then the symbol string
867: $S_{L_{k_i}^1}$ of each $L_{k_i}^1$ in $H_2$ is a string over $\Sigma$
868: that begins with $p$. These symbol strings
869: constitute an infinite sequence $\{p A_i\}_{i=1}^\infty$
870: with each $A_i$ being a substring.
871: By Lemma \ref{hig2} there is an infinite increasing
872: integer sequence $\{n_i\}_{i=1}^\infty$ such that
873: for any $i$ $p A_{n_i} \subseteq_{proj} p A_{n_{i+1}}$.
874: Therefore, $H_2$ has an infinite subsequence
875: $H_3=\{L_{g_i}^1\}_{i=1}^\infty$
876: with $S_{L_{g_i}^1}=p A_{n_i}$
877: being the symbol string of $L_{g_i}^1$. That is, for any $i$
878: $S_{L_{g_i}^1}\subseteq_{proj}S_{L_{g_{i+1}}^1}$.
879: Thus, for any $i$ $L_{g_i}^1\leadsto_{loop}L_{g_{i+1}}^1$.
880: \end{proof}
881:
882: \section{Characterizing Termination of General Logic Programs}
883: \label{verify}
884:
885: In \cite{DD93}, a generic definition of termination of
886: logic programs is presented as follows.
887:
888: \begin{definition}[(\cite{DD93})]
889: \label{term-def1}
890: Let $P$ be a general logic program, $S_Q$ a set of queries and $S_R$
891: a set of selection rules. $P$ is terminating w.r.t. $S_Q$ and $S_R$
892: if for each query $Q_i$ in $S_Q$ and for each selection rule $R_j$ in $S_R$,
893: all SLDNF-trees for $P\cup \{\leftarrow Q_i\}$ via $R_j$ are finite.
894: \end{definition}
895:
896: Observe that the above definition considers finite SLDNF-trees
897: for termination. That is, $P$ is terminating w.r.t. $Q_i$ only if all (complete)
898: SLDNF-trees for $P\cup \{\leftarrow Q_i\}$ are finite. This does not
899: seem to apply to Prolog where there exist cases in which $P$ is terminating
900: w.r.t. $Q_i$ and $R_j$, although some (complete) SLDNF-trees
901: for $P\cup \{\leftarrow Q_i\}$ are
902: infinite. Example \ref{eg2} gives such an illustration, where Prolog
903: terminates with a negative answer to the top goal $G_0$.
904:
905: In view of the above observation, we present the following
906: slightly different definition of termination based on
907: a generalized SLDNF-tree.
908:
909: \begin{definition}
910: \label{term-def2}
911: Let $P$ be a general logic program, $S_Q$ a finite set of queries and $R$
912: the depth-first, left-most control strategy.
913: $P$ is terminating w.r.t. $S_Q$ and $R$
914: if for each query $Q_i$ in $S_Q$, the generalized SLDNF-tree
915: for $P\cup \{\leftarrow Q_i\}$ via $R$ is finite.
916: \end{definition}
917:
918: The above definition implies that $P$ is terminating w.r.t. $S_Q$ and $R$
919: if and only if there is no infinite generalized SLDNF-derivation
920: in any generalized SLDNF-tree $GT_{\leftarrow Q_i}$.
921: This obviously applies to Prolog.
922: We then have the following immediate result from Theorem \ref{th4},
923: which characterizes termination of a general logic program.
924:
925: \begin{theorem}
926: \label{th-iff}
927: $P$ is terminating w.r.t. $S_Q$ and $R$ if and only if
928: for each query $Q_i$ in $S_Q$
929: there is no generalized SLDNF-derivation
930: in $GT_{\leftarrow Q_i}$ of the form
931: \begin{tabbing}
932: $\qquad$ $N_0:G_0\Rightarrow ... N_{g_1}:G_{g_1}\Rightarrow
933: ...N_{g_2}:G_{g_2}\Rightarrow ... N_{g_3}:G_{g_3}\Rightarrow ...$
934: \end{tabbing}
935: such that for any $j \geq 1$,
936: $G_{g_{j+1}}$ is a loop goal of $G_{g_j}$.
937: \end{theorem}
938:
939: \section{Related Work}
940: \label{related-work}
941:
942: Concerning termination analysis, we refer the reader to the papers of
943: Decorte, De Schreye and Vandecasteele \cite{DD93,DDV99}
944: for a comprehensive bibliography.
945: Most existing termination analysis techniques are
946: static approaches, which only make use of the syntactic structure of
947: the source code of a logic program to establish some well-founded
948: conditions/constraints that, when satisfied, yield a termination
949: proof. Since non-termination is caused by an infinite generalized
950: SLDNF-derivation, which contains some essential dynamic characteristics
951: that are hard to capture in a static way,
952: static approaches appear to be less precise than a dynamic one.
953: For example, it is difficult to apply a static approach to prove
954: the termination of program $P_2$ in Example \ref{eg2} with respect to
955: a query pattern $p$.
956:
957: The concept of generalized SLDNF-trees is the basis of our approach.
958: There are several new definitions of SLDNF-trees
959: presented in the literature, such as that of
960: Apt and Doets \cite{AD94}, Kunen \cite{KK89},
961: or Martelli and Tricomi \cite{MT92}.
962: Generalized SLDNF-trees have two distinct features as
963: compared to these definitions.
964: First, the ancester-descendent relation is explicitly expressed
965: (using ancester lists) in a generalized SLDNF-tree, which
966: is essential in identifying loop goals.
967: Second, a ground negative subgoal $\neg A$ at a node $N_i$ in a
968: SLDNF$^*$-tree $T_{N_r:G_r}$ is formulated in the same way
969: as in Prolog, i.e. (1) the subsidiary SLDNF$^*$-tree
970: $T_{N_{i+1}:\leftarrow A}$ for the
971: subgoal terminates at the first success leaf, and
972: (2) $\neg A$ succeeds
973: if all branches of $T_{N_{i+1}:\leftarrow A}$
974: end with a failure leaf and
975: fails if $T_{N_{i+1}:\leftarrow A}$ has a success leaf.
976: When $T_{N_{i+1}:\leftarrow A}$ goes into an infinite
977: extension, the node $N_i$ is treated as the last node of
978: $T_{N_r:G_r}$ which can be finitely generated.
979: As a result, a generalized SLDNF-tree
980: exists for any general logic programs.
981:
982: Our work is also related to loop checking $-$ another research topic
983: in logic programming which focuses
984: on detecting and eliminating infinite loops.
985: Informally, a derivation
986: \begin{center}
987: $N_0:G_0 \Rightarrow N_1:G_1 \Rightarrow ...\Rightarrow
988: N_i:G_i \Rightarrow ...
989: \Rightarrow N_k:G_k \Rightarrow ...$
990: \end{center}
991: is said to step into a loop at a node $N_k:G_k$ if there is a
992: node $N_i:G_i$ ($0 \leq i < k$) in the
993: derivation such that $G_i$ and $G_k$ are {\em sufficiently
994: similar}. Many mechanisms related to loop checking
995: have been presented in the literature
996: (e.g. \cite{BAK91,shen001}).
997: However, most of them apply only to {\em SLD-derivations}
998: for positive logic programs and thus
999: cannot deal with infinite recursions through
1000: negation like that in Figure \ref{fig1} or \ref{fig2}.
1001:
1002: Loop goals are defined on a generalized SLDNF-derivation for general
1003: logic programs and can be used to define the sufficiently similar
1004: goals in loop checking. For such an application, they play a role
1005: similar to {\em expanded variants} defined in \cite{shen001}.
1006: Informally, expanded variants are variants except that some terms
1007: may grow bigger. However, expanded variants
1008: have at least three disadvantages as compared to loop goals:
1009: their definition is less intuitive, their computation
1010: is more expensive, and they
1011: are not transitive in the sense that $A$ being an expanded variant of
1012: $B$ that is an expanded variant of $C$ does not necessarily
1013: imply $A$ is an expanded variant of $C$.
1014:
1015: \section{Conclusions and Future Work}
1016:
1017: We have presented an approach to characterizing termination of
1018: general logic programs by making use of dynamic features.
1019: A concept of generalized SLDNF-trees
1020: is introduced, a necessary and sufficient condition
1021: for infinite generalized SLDNF-derivations
1022: is established, and a new characterization
1023: of termination of a general logic program is developed.
1024:
1025: We have recently developed an algorithm for automatically
1026: predicting termination of general logic programs based on the
1027: characterization established in this paper. The algorithm
1028: identifies the most-likely non-terminating programs.
1029: Let $P$ be a general logic program,
1030: $S_Q$ a set of queries and $R$ the depth-first, left-most control strategy.
1031: $P$ is said to be {\em most-likely} non-terminating w.r.t. $S_Q$ and $R$
1032: if for some query $Q_i$ in $S_Q$, there is a generalized SLDNF-derivation
1033: with a few (e.g. two or three) loop goals.
1034: Our experiments show that for most representative
1035: general logic programs we have collected in the literature,
1036: they are not terminating w.r.t. $S_Q$ and $R$ if and only if
1037: they are most-likely non-terminating w.r.t. $S_Q$ and $R$.
1038: This algorithm can be incorporated into Prolog as a debugging tool,
1039: which would provide the users with valuable debugging
1040: information for them to understand the causes of non-termination.
1041:
1042: Tabled logic programming is receiving increasing attention
1043: in the community of logic programming
1044: (e.g. \cite{chen96,shen003}).
1045: Verbaeten, De Schreye and Sagonas \cite{VDK001}
1046: recently exploited termination proofs for positive logic programs
1047: with tabling. For future research, we are considering extending the work of
1048: the current paper to deal with general logic programs with tabling.
1049:
1050: \begin{acks}
1051: We are particularly grateful to Danny De Schreye,
1052: Krzysztof Apt, Jan Willem Klop and
1053: the three anonymous referees for their
1054: constructive comments on our work
1055: and valuable suggestions for its improvement.
1056: One anonymous reviewer brought the Higman's lemma to our attention.
1057: Another anonymous reviewer suggested the proof of Lemma \ref{hig2}
1058: and presented us a different yet interesting proof
1059: to the Higman's lemma based on an idea from Dershowitz's paper \cite{Der87}.
1060: The work of Yi-Dong Shen is supported in part by Chinese National
1061: Natural Science Foundation and Trans-Century Training Program
1062: Foundation for the Talents by the Chinese Ministry of Education.
1063: Qiang Yang is supported by NSERC and IRIS III grants.
1064: \end{acks}
1065:
1066: \bibliographystyle{acmtrans}
1067: %\bibliography{term}
1068:
1069:
1070: \begin{thebibliography}{}
1071:
1072: \bibitem[\protect\citeauthoryear{Apt and Doets}{Apt and Doets}{1994}]{AD94}
1073: {\sc Apt, K.~R.} {\sc and} {\sc Doets, K.} 1994.
1074: \newblock A new definition of sldnf-resolution.
1075: \newblock {\em Journal of Logic Programming\/}~{\em 18}, 177--190.
1076:
1077: \bibitem[\protect\citeauthoryear{Apt and Pedreschi}{Apt and
1078: Pedreschi}{1993}]{Apt1}
1079: {\sc Apt, K.~R.} {\sc and} {\sc Pedreschi, D.} 1993.
1080: \newblock Reasoning about termination of pure prolog programs.
1081: \newblock {\em Information and Computation\/}~{\em 106}, 109--157.
1082:
1083: \bibitem[\protect\citeauthoryear{Bezem}{Bezem}{1992}]{Bezem92}
1084: {\sc Bezem, M.} 1992.
1085: \newblock Characterizing termination of logic programs with level mapping.
1086: \newblock {\em Journal of Logic Programming\/}~{\em 15,\/}~1/2, 79--98.
1087:
1088: \bibitem[\protect\citeauthoryear{Bol}{Bol}{1991}]{Bol91}
1089: {\sc Bol, R.~N.} 1991.
1090: \newblock Loop checking in logic programming.
1091: \newblock Ph.D. thesis, The University of Amsterdam, Amsterdam.
1092:
1093: \bibitem[\protect\citeauthoryear{Bol, Apt, and Klop}{Bol
1094: et~al\mbox{.}}{1991}]{BAK91}
1095: {\sc Bol, R.~N.}, {\sc Apt, K.~R.}, {\sc and} {\sc Klop, J.~W.} 1991.
1096: \newblock An analysis of loop checking mechanisms for logic programs.
1097: \newblock {\em Theoretical Computer Science\/}~{\em 86,\/}~1, 35--79.
1098:
1099: \bibitem[\protect\citeauthoryear{Bossi, Cocco, and Fabris}{Bossi
1100: et~al\mbox{.}}{1994}]{BCF94}
1101: {\sc Bossi, A.}, {\sc Cocco, N.}, {\sc and} {\sc Fabris, M.} 1994.
1102: \newblock Norms on terms and their use in proving universal termination of a
1103: logic program.
1104: \newblock {\em Theoretical Computer Science\/}~{\em 124,\/}~1, 297--328.
1105:
1106: \bibitem[\protect\citeauthoryear{Brodsky and Sagiv}{Brodsky and
1107: Sagiv}{1991}]{BS91}
1108: {\sc Brodsky, A.} {\sc and} {\sc Sagiv, Y.} 1991.
1109: \newblock Inference of inequality constraints in logic programs.
1110: \newblock In {\em Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium
1111: on Principles of Database Systems}. ACM Press, Denver, 227--240.
1112:
1113: \bibitem[\protect\citeauthoryear{Chan}{Chan}{1988}]{chan88}
1114: {\sc Chan, D.} 1988.
1115: \newblock Constructive negation based on the completed database.
1116: \newblock In {\em Proceedings of the Fifth International Conference and
1117: Symposium on Logic Programming}. MIT Press, Seattle, 111--125.
1118:
1119: \bibitem[\protect\citeauthoryear{Chen and Warren}{Chen and
1120: Warren}{1996}]{chen96}
1121: {\sc Chen, W.~D.} {\sc and} {\sc Warren, D.~S.} 1996.
1122: \newblock Tabled evaluation with delaying for general logic programs.
1123: \newblock {\em J. ACM\/}~{\em 43,\/}~1, 20--74.
1124:
1125: \bibitem[\protect\citeauthoryear{Clark}{Clark}{1978}]{Cl79}
1126: {\sc Clark, K.~L.} 1978.
1127: \newblock Negation as failure.
1128: \newblock In {\em (H.Gallaire and J. Minker, eds.) Logic and Databases}.
1129: Plenum, New York, 293--322.
1130:
1131: \bibitem[\protect\citeauthoryear{Decorte, Schreye, and Fabris}{Decorte
1132: et~al\mbox{.}}{1993}]{DDF93}
1133: {\sc Decorte, S.}, {\sc Schreye, D.~D.}, {\sc and} {\sc Fabris, M.} 1993.
1134: \newblock Automatic inference of norms: A missing link in automatic termination
1135: analysis.
1136: \newblock In {\em Proceedings of the 1993 International Symposium on Logic
1137: Programming}. MIT Press, Vancouver, Canada, 420--436.
1138:
1139: \bibitem[\protect\citeauthoryear{Decorte, Schreye, and Vandecasteele}{Decorte
1140: et~al\mbox{.}}{1999}]{DDV99}
1141: {\sc Decorte, S.}, {\sc Schreye, D.~D.}, {\sc and} {\sc Vandecasteele, H.}
1142: 1999.
1143: \newblock Constraint-based termination analysis of logic programs.
1144: \newblock {\em ACM Transactions on Programming Languages and Systems\/}~{\em
1145: 21,\/}~6, 1137--1195.
1146:
1147: \bibitem[\protect\citeauthoryear{Dershowitz}{Dershowitz}{1987}]{Der87}
1148: {\sc Dershowitz, N.} 1987.
1149: \newblock Termination of rewriting.
1150: \newblock {\em J. Symbolic Computation\/}~{\em 3}, 69--116.
1151:
1152: \bibitem[\protect\citeauthoryear{Higman}{Higman}{1952}]{Hig52}
1153: {\sc Higman, G.} 1952.
1154: \newblock Ordering by divisibility in abstract algebras.
1155: \newblock {\em Proceedings of the London Mathematical Society\/}~{\em 3,\/}~2,
1156: 326--336.
1157:
1158: \bibitem[\protect\citeauthoryear{ISLAB}{ISLAB}{1998}]{SICSTUS}
1159: {\sc ISLAB}. 1998.
1160: \newblock {\em SICStus Prolog User's Manual}.
1161: \newblock Intelligent Systems Laboratory, Swedish Institute of Computer
1162: Science, Available from
1163: http://www.sics.se/sicstus/docs/3.7.1/html/sicstus\_toc.html.
1164:
1165: \bibitem[\protect\citeauthoryear{Kunen}{Kunen}{1989}]{KK89}
1166: {\sc Kunen, K.} 1989.
1167: \newblock Signed data dependencies in logic programming.
1168: \newblock {\em Journal of Logic Programming\/}~{\em 7}, 231--246.
1169:
1170: \bibitem[\protect\citeauthoryear{Lindenstrauss and Sagiv}{Lindenstrauss and
1171: Sagiv}{1997}]{LS97}
1172: {\sc Lindenstrauss, N.} {\sc and} {\sc Sagiv, Y.} 1997.
1173: \newblock Automatic termination analysis of logic programs.
1174: \newblock In {\em Proceedings of the Fourteenth International Conference on
1175: Logic Programming}. MIT Press, Leuven, Belgium, 63--77.
1176:
1177: \bibitem[\protect\citeauthoryear{Lloyd}{Lloyd}{1987}]{Ld87}
1178: {\sc Lloyd, J.~W.} 1987.
1179: \newblock {\em Foundations of Logic Programming}.
1180: \newblock Springer-Verlag, Berlin.
1181:
1182: \bibitem[\protect\citeauthoryear{Martelli and Tricomi}{Martelli and
1183: Tricomi}{1992}]{MT92}
1184: {\sc Martelli, M.} {\sc and} {\sc Tricomi, C.} 1992.
1185: \newblock A new sldnf-tree.
1186: \newblock {\em Information Processing Letters\/}~{\em 43,\/}~2, 57--62.
1187:
1188: \bibitem[\protect\citeauthoryear{Martin, King, and Soper}{Martin
1189: et~al\mbox{.}}{1997}]{MKS96}
1190: {\sc Martin, J.~C.}, {\sc King, A.}, {\sc and} {\sc Soper, P.} 1997.
1191: \newblock Typed norms for typed logic programs.
1192: \newblock In {\em Proceedings of the 6th International Workshop on Logic
1193: Programming Synthesis and Transformation}. Springer, Stockholm, Sweden,
1194: 224--238.
1195:
1196: \bibitem[\protect\citeauthoryear{Plumer}{Plumer}{1990a}]{Pl90b}
1197: {\sc Plumer, L.} 1990a.
1198: \newblock {\em Termination Proofs for Logic Programs}.
1199: \newblock Lecture Notes in Computer Science 446, Springer-Verlag, Berlin.
1200:
1201: \bibitem[\protect\citeauthoryear{Plumer}{Plumer}{1990b}]{Pl90a}
1202: {\sc Plumer, L.} 1990b.
1203: \newblock Termination proofs for logic programs based on predicate
1204: inequalities.
1205: \newblock In {\em Proceedings of the Seventh International Conference on Logic
1206: Programming}. MIT Press, Cambridge, MA, 634--648.
1207:
1208: \bibitem[\protect\citeauthoryear{Schreye and Decorte}{Schreye and
1209: Decorte}{1993}]{DD93}
1210: {\sc Schreye, D.~D.} {\sc and} {\sc Decorte, S.} 1993.
1211: \newblock Termination of logic programs: the never-ending story.
1212: \newblock {\em Journal of Logic Programming\/}~{\em 19,\/}~20, 199--260.
1213:
1214: \bibitem[\protect\citeauthoryear{Schreye and Verschaetse}{Schreye and
1215: Verschaetse}{1995}]{DV95}
1216: {\sc Schreye, D.~D.} {\sc and} {\sc Verschaetse, K.} 1995.
1217: \newblock Deriving linear size relations for logic programs by abstract
1218: interpretation.
1219: \newblock {\em New Generation Computing\/}~{\em 13,\/}~2, 117--154.
1220:
1221: \bibitem[\protect\citeauthoryear{Schreye, Verschaetse, and Bruynooghe}{Schreye
1222: et~al\mbox{.}}{1992}]{DVB92}
1223: {\sc Schreye, D.~D.}, {\sc Verschaetse, K.}, {\sc and} {\sc Bruynooghe, M.}
1224: 1992.
1225: \newblock A framework for analyzing the termination of definite logic programs
1226: with respect to call patterns.
1227: \newblock In {\em Proceedings of the International Conference on Fifth
1228: Generation Computer Systems}. IOS Press, Tokyo, Japan, 481--488.
1229:
1230: \bibitem[\protect\citeauthoryear{Shen, Yuan, and You}{Shen
1231: et~al\mbox{.}}{2001}]{shen001}
1232: {\sc Shen, Y.~D.}, {\sc Yuan, L.~Y.}, {\sc and} {\sc You, J.~H.} 2001.
1233: \newblock Loop checks for logic programs with functions.
1234: \newblock {\em Theoretical Computer Science\/}~{\em 266,\/}~1/2, 441--461.
1235:
1236: \bibitem[\protect\citeauthoryear{Shen, Yuan, and You}{Shen
1237: et~al\mbox{.}}{2002}]{shen003}
1238: {\sc Shen, Y.~D.}, {\sc Yuan, L.~Y.}, {\sc and} {\sc You, J.~H.} 2002.
1239: \newblock Slt-resolution for the well-founded semantics.
1240: \newblock {\em Journal of Automated Reasoning\/}~{\em 28,\/}~1, 53--97.
1241:
1242: \bibitem[\protect\citeauthoryear{Ullman and Gelder}{Ullman and
1243: Gelder}{1988}]{UVG88}
1244: {\sc Ullman, J.~D.} {\sc and} {\sc Gelder, A.~V.} 1988.
1245: \newblock Efficient tests for top-down termination of logical rules.
1246: \newblock {\em J. ACM\/}~{\em 35,\/}~2, 345--373.
1247:
1248: \bibitem[\protect\citeauthoryear{Verbaeten, Schreye, and Sagonas}{Verbaeten
1249: et~al\mbox{.}}{2001}]{VDK001}
1250: {\sc Verbaeten, S.}, {\sc Schreye, D.~D.}, {\sc and} {\sc Sagonas, K.} 2001.
1251: \newblock Termination proofs for logic programs with tabling.
1252: \newblock {\em ACM Transactions on Computational Logic\/}~{\em 2,\/}~1, 57--92.
1253:
1254: \bibitem[\protect\citeauthoryear{Verschaetse}{Verschaetse}{1992}]{V92}
1255: {\sc Verschaetse, K.} 1992.
1256: \newblock Static termination analysis for definite horn clause programs.
1257: \newblock Ph.D. thesis, Department of Computer Science, K. U. Leuven, Available
1258: at http://www.cs.kuleuven.ac.be/~lpai.
1259:
1260: \end{thebibliography}
1261:
1262:
1263:
1264:
1265:
1266:
1267:
1268: \begin{received}
1269: Received June 2000;
1270: revised August 2001 and December 2001;
1271: accepted April 2002
1272: \end{received}
1273:
1274:
1275: \end{document}
1276:
1277:
1278: