1: \documentclass{tlp}
2:
3:
4: \usepackage{latexsym}
5: \usepackage{harvard}
6:
7: \newtheorem{theorem}{Theorem}
8: \newtheorem{lemma}[theorem]{Lemma}
9: \newtheorem{proposition}[theorem]{Proposition}
10: \newtheorem{example}[theorem]{Example}
11: \newtheorem{definition}[theorem]{Definition}
12: \newtheorem{corollary}[theorem]{Corollary}
13: \newtheorem{remark}[theorem]{Remark}
14: \newtheorem{claim}[theorem]{Claim}
15:
16:
17: \newcommand{\la}{\mbox{$\:\leftarrow\:$}}
18: \newcommand{\U}{\ensuremath{\:\cup\:}}
19:
20:
21: \newenvironment{program}{\tt \begin{tabbing}pro\= {\tt pro}\= clause \kill}{\end{tabbing}}
22:
23:
24: \newenvironment{program2}{\tt \begin{tabbing}pro\= {\tt c1:} \= head\= hereisthebodyoftheclause \= \kill}{\end{tabbing}}
25:
26:
27:
28: %\newcommand{\cvd}{\rule{.15cm}{.15cm}}
29: %\def\qed{\relax\hfill \cvd}
30:
31: \newcommand{\ol}[1]{{\bf #1}}
32: \newcommand{\revtheta}{\stackrel{_{\mbox{\tiny \(\leftarrow\)}}}{
33: \vspace{0cm}\theta}}
34:
35: \title[Theory and Practice of Logic Programming]
36: {On Modular Termination Proofs of \\
37: General Logic Programs}
38:
39: \author[A. Bossi, N. Cocco, S. Etalle, and S. Rossi]
40: {ANNALISA BOSSI, NICOLETTA COCCO, SABINA ROSSI\\
41: Dipartimento di Informatica,
42: Universit\`a Ca' Foscari di Venezia \\
43: via Torino 155,
44: 30172 Venezia, Italy
45: %\email{\{bossi,srossi\}@dsi.unive.it}
46: \and
47: SANDRO ETALLE\\
48: Department of Computer Science, University of Twente\\
49: P.O. Box 217, 7500 AE Enschede, The Netherlands\\
50: and\\
51: CWI -- Center for Mathematics and Computer Science,\\
52: P.O.\ Box 94079, 1090 GB Amsterdam, The Netherlands}
53:
54: \begin{document}
55: \maketitle
56:
57: %%%%%%%%
58: \begin{abstract}
59: %%%%%%%%%%%
60: \noindent
61: We propose a modular method for proving termination of
62: general logic programs (i.e., logic programs with negation).
63: It is
64: based on the notion of acceptable programs, but
65: it allows us to prove termination in a truly modular way.
66: We consider programs consisting of a hierarchy of modules
67: and supply a general result for proving
68: termination by dealing with each module separately.
69: For programs which are in a certain sense
70: well-behaved,
71: namely well-moded or well-typed programs,
72: we derive both a simple verification technique and
73: an iterative proof method.
74: Some examples show how our system allows
75: for greatly simplified proofs.
76: \end{abstract}
77:
78:
79: %%%%%%%%%%%%%%%
80: \section{Introduction}
81: %%%%%%%%%%%%%%%
82:
83: It is standard practice to tackle a large proof by decomposing it into
84: more managea\-ble pieces (lemmata or modules) and proving them
85: separately. By composing appropriately these simpler results, one can
86: then obtain the final proof. This methodo\-logy has been recognized an
87: important one also when proving termination of logic programs.
88: Moreover most practical logic programs are
89: engineered by assembling different modules and libraries, some of
90: which might be pre-compiled or written in a different programming
91: language. In such a situation, a compositional methodology for proving
92: termination is of crucial importance.
93:
94: The first approach to modular termination proofs of logic programs
95: has been proposed
96: by Apt and Pedreschi in \cite{AP94}. It extends the seminal work
97: on \emph{acceptable} programs \cite{AP93} which provides
98: an algebraic characterization
99: of programs terminating under Prolog left-to-right selection rule.
100: The class of acceptable programs
101: contains programs which terminate on ground queries.
102: To prove acceptability one needs to determine a measure
103: on literals (\emph{level mapping}) such that,
104: in any clause, the measure of the head is greater than the measure
105: of each body literal.
106: This implies the decreasing of the measure of the literals resolved
107: during any computation starting from a ground or \emph{bounded}
108: query and hence termination.
109:
110:
111:
112:
113:
114:
115: The significance of
116: a modular approach to termination of logic programs has been
117: recognized also by other authors; more recent proposals can be found in
118: \cite{PR96,Mar96,VSD99,EBC99,VSD01}.
119:
120:
121:
122: All previous proposals (with the exception of \cite{VSD99,EBC99})
123: require the existence of a relation between the level mappings used
124: to prove acceptability
125: of distinct modules. This is not completely satisfactory:
126: it would be nice to be able to put together modules which
127: were independently proved terminating, and be sure that
128: the resulting program is still terminating.
129:
130: We propose a modular approach to termination which allows one
131: to reason independently on each single module and get a termination
132: result on the whole program.
133: We consider general logic programs, i.e., logic programs with negation,
134: employing SLDNF-resolution
135: together with the leftmost selection rule
136: (also called \emph{LDNF-resolution}) as computational mechanism.
137: We consider programs which can be divided into modules in a
138: hierarchical way, so that each module is an extension of the previous
139: ones. We show that in this context the termination proof of the entire
140: program can be given in terms of separate proofs for each module,
141: which are naturally much simpler than a proof for the whole program.
142: While assuming a hierarchy still allows one
143: to tackle most real-life programs, it leads to termination proofs
144: which, in most cases, are extremely simple.
145:
146:
147: We characterize the class of queries terminating for the
148: whole program by introducing a new notion of
149: boundedness, namely \emph{strong boundedness}.
150: Intuitively, strong boundedness
151: captures the queries which preserve
152: (standard) boundedness through the computation.
153: By proving acceptability of each module wrt.\
154: a level mapping which measures only the predicates
155: defined in that module,
156: we get a termination result for
157: the whole program which is valid for any strongly bounded query.
158: Whenever the original program is decomposed into a
159: hierarchy of small modules, the termination proof
160: %for strongly bounded queries
161: can be drastically simplified with respect to
162: previous modular approaches.
163: % In practice, the finer the hierarchy of modules we identify in the
164: %program, the more natural the level mappings and
165: %the simpler the termination proofs become.
166: Moreover strong boundedness can be naturally guaranteed by
167: common persistent properties of programs and queries, namely properties
168: preserved through LDNF-resolution such as
169: \emph{well-modedness} \cite{DM85}
170: or \emph{well-typedness} \cite{BLR92}.
171:
172:
173:
174: The paper is organized as follows. Section \ref{prel} contains some
175: preliminaries. In particular we briefly recall the key concepts of
176: LDNF-resolution, accepta\-bility, boundedness and program extension.
177: Section \ref{R-acc} contains our main results which show how
178: termination proofs of separate programs can be combined to obtain
179: proofs of larger programs. In particular we define the concept of
180: strongly bounded query and we prove that for general programs composed
181: by a hierarchy of $n$ modules, each one independently acceptable wrt.\
182: its own level mapping, any strongly bounded query terminates. In
183: Section \ref{sec:applications} we show how strong boundedness is naturally ensured
184: by some program properties which are preserved
185: through LDNF-resolution such as
186: well-modedness and well-typedness. In Section \ref{sec:iteration} we
187: show how these properties allow us to apply our general results also for
188: proving termination of modular programs in an iterative way. In Section
189: \ref{sec:comparisons} we compare our work with Apt and Pedreschi's approach.
190: Other related works and concluding remarks are discussed in
191: Section \ref{conclusion}.
192:
193: %%%%%%%%%%%%
194: \section{Preliminaries}
195: \label{prel}
196: %%%%%%%%%%%%
197:
198: We use standard notation and terminology of logic programming
199: \cite{Llo87,Apt90,Apt97}. Just note that general logic programs are called
200: in \cite{Llo87} normal logic programs.
201:
202: %%%%%%%%%%%%%%%%%%%%%%%%%%%%
203: \subsection{General Programs and LDNF-Resolution}
204: %%%%%%%%%%%%%%%%%%%%%%%%%%%%
205: A \emph{general clause} is a construct of the form
206: $$H\leftarrow L_1,\ldots, L_n$$
207: with $(n\geq 0)$, where $H$ is an atom and $L_1,\ldots,L_n$ are
208: literals (i.e.,
209: either atoms or the negation of atoms).
210: In turn, a \emph{general query} is a
211: possibly empty finite sequence of literals $ L_1,\ldots,L_n$,
212: with ($n\geq 0$).
213: %The empty query is denoted by $\Box$.
214: A \emph{general program} is a finite set of
215: general clauses\footnote{In the examples through the paper, we will
216: adopt the syntactic conventions of Prolog so that each query and
217: clause ends with the period ``.'' and ``$\leftarrow$'' is omitted in
218: the unit clauses.}.
219: Given a query $Q:=L_1,\ldots, L_n$, a \emph{non-empty prefix of}
220: $Q$ is any
221: query $ L_1,\ldots, L_i$ with $i\in\{1,\ldots,n\}$.
222: For a literal $L$, we denote by ${\it rel}(L)$ the predicate symbol of $L$.
223:
224:
225:
226: Following the convention
227: adopted in \cite{Apt97}, we use bold characters to denote
228: sequences of objects (so that \textbf{L} indicates a sequence of
229: literals $L_1,\ldots,L_n$, while \textbf{t} indicates a sequence of
230: terms $t_1,\ldots,t_n$).
231:
232: For a given program $P$, we use the following
233: notations: $B_P$ for the Herbrand base of $P$, ${\it ground}(P)$ for
234: the set of all ground instances of clauses from $P$, ${\it comp}(P)$
235: for the Clark's completion of $P$ \cite{Cla78}.
236:
237:
238: Since in this paper we deal with general queries, clauses and programs,
239: we omit from now on the qualification ``general'', unless some
240: confusion might arise.
241:
242:
243: We consider \emph{LDNF-resolution},
244: and following Apt and Pedreschi's approach
245: in studying the termination of
246: general programs \cite{AP93}, we view LDNF-resolution as
247: a top-down
248: interpreter which, given a general program $P$ and a general
249: query $Q$, attempts to build a search tree for $P\cup\{Q\}$
250: by constructing its branches in parallel.
251: The branches in this tree are called \emph{LDNF-derivations}
252: of $P\cup\{Q\}$ and the tree itself is called \emph{LDNF-tree}
253: of $P\cup\{Q\}$.
254: Negative literals are resolved using the {\em negation-as-failure} rule
255: which calls for the construction of a \emph{subsidiary LDNF-tree}.
256: If during this subsidiary construction the interpreter diverges, the (main)
257: LDNF-derivation
258: is considered to be infinite.
259: An LDNF-derivation is finite also if during its construction
260: the interpreter encounters a query with the first literal
261: being negative and non-ground.
262: In such a case we say that the LDNF-derivation {\em flounders}.
263:
264: By termination of a general program we actually mean
265: termination of the underlying interpreter.
266: Hence in order to ensure termination of a query $Q$
267: in a program $P$, we require that all LDNF-derivations of $P \cup
268: \{Q\}$ are finite.
269:
270:
271: By an \emph{LDNF-descendant} of $P\cup\{Q\}$ we mean
272: any query occurring during the LDNF-resolution of $P\cup\{Q\}$,
273: including $Q$
274: and all the queries occurring during the
275: construction of the subsidiary LDNF-trees for $P\cup\{Q\}$.
276:
277:
278:
279: For a non-empty query $Q$,
280: we denote by $\mathit{first}(Q)$ the first literal of $Q$.
281: Moreover we define $\mathit{Call}_P(Q)=\{ \mathit{first}(Q')\ |\
282: Q' \mbox{ is an LDNF-descendant of } P\cup\{Q\}\}$.
283: It is worth noting that if $\neg A\in\mathit{Call}_P(Q)$ and $A$
284: is a ground atom, then $A \in\mathit{Call}_P(Q)$ too.
285: Notice that, for definite programs, the set $\mathit{Call}_P(Q)$ coincides
286: with the call set $\mathit{Call}(P,\{Q\})$ in \cite{DVB92,DDV99}.
287:
288:
289: The following trivial proposition holds.
290:
291: \begin{proposition}
292: \label{prop-call}
293: Let $P$ be a program and $Q$ be a query.
294: All LDNF-derivations of $P\cup\{Q\}$ are finite
295: iff for all positive literals
296: $A\in \mathit{Call}_P(Q)$,
297: all LDNF-derivations of $P\cup\{A\}$ are finite.
298: \end{proposition}
299:
300:
301: %%%%%%%%%%%%%%%%%%%%%%%
302: \subsection{Acceptability and Boundedness}
303: %%%%%%%%%%%%%%%%%%%%%%%
304:
305: The method we are going to use for proving termination of modular programs
306: is based on the concept of {\em acceptable}
307: program \cite{AP93}. In order to introduce it, we
308: start by the following definition, originally due to \cite{Bez93} and
309: \cite{Cav89}.
310:
311: \begin{definition}[Level Mapping]
312: A \emph{level mapping} for a program $P$ is a function
313: $|\ |:B_P\rightarrow {\bf N}$ of ground atoms to natural numbers.
314: By convention, this definition is extended in a natural way to
315: ground literals by putting $|\neg A|=|A|$.
316: For a ground literal $L$, $|L|$ is called the \emph{level} of
317: $L$.
318: \end{definition}
319: %
320:
321: We will use the following notations.
322: %
323: Let $P$ be a program and $p$ and $q$ be relations.
324: We say that $p$ \emph{refers to} $q$ if there is a clause in
325: $P$ that uses $p$ in its head and $q$ in its body;
326: $p$ \emph{depends on} $q$ if $(p,q)$ is in the
327: reflexive, transitive closure of the relation \emph{refers to}.
328: We say that $p$ and $q$ are \emph{mutually recursive} and write
329: $p\simeq q$, if $p$ depends on $q$ and $q$ depends on $p$.
330: We also write $p\sqsupset q$, when $p$ depends on $q$ but $q$
331: does not depend on $p$.
332:
333: We denote by ${\it Neg}_P$ the set of relations in $P$ which occur in
334: a negative literal in a clause of $P$ and by
335: ${\it Neg}^*_P$ the set of relations in $P$ on which the
336: relations in ${\it Neg}_P$ depend.
337: $P^-$ denotes the set of clauses in $P$ defining a relation of
338: ${\it Neg}^*_P$.
339:
340:
341: In the sequel we refer to the standard definition of model of a
342: program and model of the completion of a program, see
343: \cite{Apt90,Apt97} for details. In particular we need the
344: following notion of {\em complete model} for a program.
345: %
346: \begin{definition}[Complete Model]
347: A model $M$ of a program $P$ is called \emph{complete} if its
348: restriction to the relations from ${\it Neg}^*_P$ is a model of
349: ${\it comp}(P^-)$.
350: \end{definition}
351: %
352: Notice that if $I$ is a model of ${\it comp}(P)$ then
353: its restriction to the relations in ${\it Neg}^*_P$ is a model
354: of ${\it comp}(P^-)$; hence $I$ is a complete model
355: of $P$.
356: %
357:
358: The following notion of acceptable program was introduced in \cite{AP93}.
359: Apt and Pedreschi proved that such a notion
360: fully characterizes left-termination, namely termination wrt.\ any ground
361: query, both for definite programs and for general programs which
362: have no LDNF-derivations which flounder.
363:
364:
365: \begin{definition}[Acceptable Program]
366: Let $P$ be a program, $|\ |$ be a level mapping for $P$ and $M$ be a
367: complete model of $P$.
368: $P$ is called \emph{acceptable wrt.\ $|\ |$ and $M$} if for every
369: clause $A\leftarrow {\bf A}, B,{\bf B}$ in ${\it ground}(P)$
370: the following implication holds:
371: $$ \mbox{ if } M\models {\bf A} \mbox{ then } |A|>|B|. $$
372:
373: \end{definition}
374: %
375: Note that if $P$ is a definite program, then both $P^-$
376: and ${\it Neg}^*_P$ are empty and $M$ can be
377: any model of $P$.
378: %
379:
380: We also need the notion of bounded atom.
381:
382: \begin{definition}[Bounded Atom]
383: \label{def-Boundedness}
384: Let $P$ be a program and $|\ |$ be a level mapping for $P$.
385: An atom $A$ is called \emph{bounded wrt.\ $|\ |$}
386: if the set of all $|A'|$, where $A'$ is a ground instance of $A$, is finite.
387: In this case we
388: denote by ${\it max}|A|$ the maximum value in this set.
389: \end{definition}
390:
391: Notice that if an atom $A$ is bounded then, by definition of level
392: mapping, also the corresponding negative literal, $\neg A$,
393: is bounded.
394:
395: Note also that, for atomic queries,
396: this definition coincides with the definition
397: of bounded query introduced in \cite{AP93}
398: in order to characterize terminating queries for acceptable
399: programs.
400: In fact, in case of atomic queries the notion of boundedness does
401: not depend on a model.
402:
403:
404: %%%%%%%%%%%%%%%%%%%%
405: \subsection{Extension of a Program}
406: %%%%%%%%%%%%%%%%%%%%
407:
408:
409: In this paper we consider a hierarchical situation where a program
410: uses another one as a subprogram. The following definition
411: formalizes this situation.
412:
413: \begin{definition}[Extension]
414: Let $P$ and $R$ be two programs.
415: A relation $p$ is \emph{defined in} $P$ if $p$
416: occurs in a head of a clause of $P$;
417: a literal $L$ is
418: \emph{defined in} $P$ if ${\it rel}(L)$ is defined in $P$;
419: $P$ \emph{extends} $R$, denoted
420: $P\sqsupset R$, if no relation defined in $P$
421: occurs in~$R$.
422: \end{definition}
423:
424: Informally, $P$ extends $R$ if $P$ defines new relations with respect to
425: $R$.
426: Note that $P$ and $R$ are independent if no relation defined in $P$
427: occurs in $R$ and no relation defined in $R$
428: occurs in $P$, i.e. $P\sqsupset R$ and $R\sqsupset P$.
429:
430: In the sequel we will study termination in a hierarchy of
431: programs.
432:
433: \begin{definition}[Hierarchy of Programs]
434: Let $P_1,\ldots, P_n$ be programs such that for all $i\in\{1,\dots,n-1\}$,
435: $P_{i+1} \sqsupset (P_1\cup
436: \cdots \cup P_{i})$.
437: Then we call $P_n \sqsupset \cdots \sqsupset P_1$
438: a \emph{hierarchy of
439: programs}.
440: \end{definition}
441:
442:
443:
444:
445:
446:
447: %%%%%%%%%%%%%%%%%%%%%%
448: \section{Hierarchical Termination}
449: \label{R-acc}
450: %%%%%%%%%%%%%%%%%%%%%%
451:
452:
453: This section contains our main results which show how termination
454: proofs of separate programs can be combined to obtain proofs of larger
455: programs.
456: We start with a technical result, dealing with the case in
457: which a program consists of a hierarchical combination of two
458: modules. This is the base both of a generalization to a hierarchy
459: of $n$ programs and of an iterative proof method for termination
460: presented in Section~\ref{sec:iteration}.
461: %We need a definition first.
462: Let us first introduce the following notion of {\em $P$-closed}
463: class of queries.
464:
465: \begin{definition} [P-closed Class]
466: Let ${\cal C}$ be a class of queries and $P$ be a program.
467: We say that ${\cal C}$ is {\em
468: $P$-closed} if it is closed under non-empty prefix (i.e.,
469: it contains all the non-empty prefixes of its elements) and for each query
470: $Q\in {\cal C}$,
471: every LDNF-descendant of $P\cup\{Q\}$ is contained in ${\cal C}$.
472: \end{definition}
473:
474: Note that if ${\cal C}$ is $P$-closed,
475: then for each query $Q \in {\cal C}$,
476: $\mathit{Call}_{P}(Q) \subseteq {\cal C}$.
477:
478: We can now state our first general theorem.
479: Notice that if $P$ extends $R$ and $P$ is acceptable
480: wrt.\ some level mapping $|\ |$ and model $M$, then
481: $P$ is acceptable also
482: wrt.\ the level mapping $|\ |'$ and $M$, where
483: $|\ |'$ is defined on
484: the Herbrand base of the union of the two programs $B_{P\cup R}$
485: and it takes the value
486: $0$ on the literals which are not defined in $P$
487: (and hence, in particular, on the literals which occur in $P$ but
488: are defined in $R$). This shows that in each module
489: it is sufficient to compare only the level of the literals defined inside it,
490: while we can ignore literals defined outside the module.
491: In the following we make use of this observation in order
492: to associate to each module in a hierarchy a level mapping
493: which is independent from the context.
494:
495: \begin{theorem}
496: \label{theo:generale-sulle-classi}
497: Let $P$ and $R$ be two programs such that $P$ extends $R$, $M$ be
498: a complete model of $P\cup R$ and ${\cal C}$ be a $(P\cup R)$-closed
499: class of queries.
500: Suppose that
501: \begin{itemize}
502: \item $P$ is acceptable wrt.\ a level mapping $|\ |$ and $M$,
503: \item for all queries $Q\in {\cal C}$, all LDNF-derivations of $R\cup\{Q\}$
504: are finite,
505: \item for all atoms $A\in {\cal C}$, if $A$ is defined in $P$
506: then $A$ is bounded wrt.\ $|\ |$.
507: \end{itemize}
508: Then for all queries $Q\in {\cal C}$,
509: all LDNF-derivations of $(P\cup R)\cup\{Q\}$ are finite.
510: \end{theorem}
511: \begin{proof}
512: By the fact that ${\cal C}$ is $(P\cup R)$-closed and Proposition
513: \ref{prop-call}, it is sufficient to prove that for all positive literals
514: $A\in {\cal C}$,
515: all LDNF-derivations of $(P\cup R)\cup\{A\}$ are finite.
516: Let us consider an atom $A\in {\cal C}$.
517:
518: If $A$ is defined in $R$, then the thesis trivially holds by
519: hypothesis.
520:
521: If $A$ is defined in $P$,
522: $A$ is bounded wrt.\ $|\ |$ by hypothesis
523: and thus $\mathit{max}|A|$ is defined.
524: The proof proceeds
525: by induction on $\mathit{max}|A|$.
526:
527: \emph{Base}.
528: Let $\mathit{max}|A|=0$.
529: In this case, by acceptability of $P$, there are no
530: clauses in $P$ whose head unifies with $A$
531: and whose body is non-empty.
532: Hence, the thesis holds.
533:
534:
535: \emph{Induction step}.
536: Let $\mathit{max}|A|>0$.
537: It is sufficient to prove that for all direct descendants
538: $(L_1,\ldots,L_n)$ in the LDNF-tree of $(P\cup R)\cup\{A\}$,
539: if
540: $\theta_i$ is a computed answer for $P\cup\{L_1,\ldots,L_{i-1}\}$
541: then all LDNF-derivations of
542: $(P\cup R)\cup \{L_i\theta_i\}$ are finite.
543:
544:
545: Let $c: H'\leftarrow L'_{1},\ldots , L'_{n}$ be a clause of $P$ such that
546: $\sigma = mgu(H', A)$.
547: Let $H=H'\sigma$ and for all
548: $i\in \{1,\ldots,n\}$, let $L_i=L'_i\sigma$
549: and $\theta_i$ be a substitution such that
550: $\theta_i$ is a computed answer of $L_1,\ldots,L_{i-1}$
551: in $P\cup R$.
552:
553:
554: We distinguish two cases. If $L_i$ is defined in $R$ then the thesis
555: follows by hypothesis.
556:
557: Suppose that $L_i$ is defined in $P$.
558: We prove that $L_i\theta_i$ is bounded and $\mathit{max}|A|>
559: \mathit{max}|L_i\theta_i|$. The thesis will follow by the
560: induction hypothesis.
561:
562:
563: Let $\gamma$ be a substitution such that $L_i\theta_i\gamma$ is ground.
564: By soundness of LDNF-resolution \cite{Cla78},
565: there exists $\gamma'$ such that
566: $M\models (L_1,\ldots, L_{i-1})\gamma'$ and
567: $c\sigma\gamma'$ is a ground instance of
568: $c$ and
569: $L_i\gamma'=L_i\theta_i\gamma$. Therefore
570: \[\begin{array}{lllll}
571: |L_i\theta_i\gamma | & = & |L_i\gamma'| &\\
572: & = & |L'_i\sigma \gamma'| & (\mbox{since } L_i=L'_i\sigma)\\
573: & < & |H'\sigma\gamma'| & (\mbox{since $P$ is acceptable})\\
574: & = & |A\sigma\gamma'| & (\mbox{since } \sigma = mgu (H', A)).
575: \end{array}\]
576: Since $A$ is bounded, we can conclude that $L_i\theta_i$ is bounded
577: and also that $\mathit{max}|A|> \mathit{max}|L_i \theta_i|$.
578: \end{proof}
579: \medskip
580:
581: We are going to extend the above theorem in order to handle the presence
582: of more than two modules. We need to introduce more notation.
583: Let us consider the case of a program $P$ consisting of a
584: hierarchy
585: $R_n\sqsupset \ldots \sqsupset R_1$ of distinct modules, and satisfying
586: the property that each module, $R_i$, is acceptable wrt.\ a distinct
587: level mapping, $|\ |_i$, and a complete model, $M$, of the whole
588: program. Under these
589: assumptions we identify a specific class of queries which terminate in
590: the whole program. We characterize the class of terminating queries
591: in terms of the following notion of strong boundedness. This class
592: enjoys the property of being $P$-closed.
593:
594: \begin{definition}[Strongly Bounded Query]
595: \label{def:strongn}
596: Let the program $P:=R_1\cup \ldots \cup R_n$ be a hierarchy
597: $ R_n\sqsupset \ldots \sqsupset R_1$ and $|\ |_1,\ldots,|\ |_n$
598: be level mappings for $R_1,\ldots,R_n$, respectively. A query
599: $Q$ is called \emph{strongly bounded wrt.\ $P$ and
600: $|\ |_1,\ldots,|\ |_n$} if
601: \begin{itemize}
602: \item
603: for all atoms $A\in \mathit{Call}_P(Q)$,
604: if $A$ is defined in $R_i$
605: (with $i\in \{1,\ldots,n\}$) then $A$ is bounded wrt.\ $|\ |_i$.
606: \end{itemize}
607: \end{definition}
608:
609: Notice that the notion of boundedness for an atom (see Definition
610: \ref{def-Boundedness}) does not depend on the choice of a particular
611: model of $P$. As a consequence, also the definition of strong
612: boundedness does not refer to any model of $P$; however, it refers to
613: the LDNF-derivations of $P$. For this reason, a ground atom is always
614: bounded but not necessarily strongly bounded. On the other hand, if $A$
615: is strongly bounded then it is bounded too.
616:
617: The following remark follows immediately.
618:
619: \begin{remark}
620: \label{i-strong}
621: Let the query $Q$ be strongly bounded wrt.\ $P$
622: and $|\ |_1,\ldots,|\ |_n$,
623: where $P$ is a hierarchy $R_n \sqsupset \cdots \sqsupset R_1$ .
624: Let $i\in\{1,\ldots,n\}$.
625: If $Q$ is defined in $R_1\cup \ldots \cup R_i$ then $Q$ is strongly bounded wrt.\
626: $R_1\cup \ldots\cup R_i$ and $|\ |_{1},\ldots,|\ |_{i}$.
627: \end{remark}
628:
629: In order to verify whether a query Q is strongly bounded wrt.\ a given
630: program $P$ one can perform a call-pattern analysis
631: \cite{JB92,GG94,CD95} which allows us to infer information about the
632: form of the call-patterns, i.e., the atoms that will be possibly
633: called during the execution of $P\cup \{Q\}$.
634: However this is not the only way
635: for guaranteeing strong boundedness. There are classes of programs
636: and queries for which strong boundedness can be proved in a
637: straightforward way. This is shown in the following section.
638:
639: Let us illustrate the notion of strong boundedness through an example.
640:
641: \begin{example}
642: \label{exa:sb}
643: Let \texttt{LIST01}
644: be the following program which defines
645: the proper lists of \texttt{0}'s and \texttt{1}'s, i.e.
646: lists
647: containing only \texttt{0}'s and \texttt{1}'s and at least
648: two distinct elements, as follows:
649:
650: %the lists containing only
651: %\texttt{0}'s and~\texttt{1}'s and counts the number of \texttt{0}'s and~\textt%t{1}'s which occur in them:
652: \begin{program2}
653: \> r1: \> list01([ ],0,0).\\
654: \> r2: \> list01([0|Xs],s(N0),N1) \la list01(Xs,N0,N1).\\
655: \> r3: \> list01([1|Xs],N0,s(N1)) \la list01(Xs,N0,N1).\\[2mm]
656: \> r4: \> length([ ],0).\\
657: \> r5: \> length([X|Xs],s(N)) \la length(Xs,N). \\[2mm]
658: \> r6: \> plist01(Ls) \la list01(Ls,N0,N1), \\
659: \> \> \> $\neg$length(Ls,N0),
660: $\neg$length(Ls,N1).
661: \end{program2}
662: Let us distinguish two modules in \texttt{LIST01}:
663: $R_1=\{\mathtt{r_1},\mathtt{r_2},\mathtt{r_3},\mathtt{r_4},\mathtt{r_5}\}$ and
664: $R_2=\{\mathtt{r_6}\}$ ($R_2$ extends $R_1$).
665: Let $|\ |_1$ be the natural level mapping for
666: $R_1$ defined by:
667:
668: \begin{program}
669: \> \(\mathtt{|list01(\mathit{ls},\mathit{n0},\mathit{n1})|_1 = |\mathit{ls}|_{length}}\)\\
670: \> \(\mathtt{|length(\mathit{ls},\mathit{n})|_1 = |\mathit{n}|_{size}}\)
671: \end{program}
672: %
673: where for a term $\mathit{t}$, if $\mathit{t}$ is a list then
674: \(\mathtt{|\mathit{t}|_{length}}\) is equal to
675: the length of the list, otherwise it is $0$, while
676: \(\mathtt{|\mathit{t}|_{size}}\)
677: is the number of function symbols occurring in the term $\mathit{t}$.
678: %
679: %Let $R_2$ be a program which extends $R_1$
680: %by defining the proper lists of \texttt{0}'s and \texttt{1}'s, i.e.,
681: %those containing both \texttt{0}'s and \texttt{1}'s, as follows:
682: %\begin{program2}
683: %\> r21: \> llist01(Ls,N) \la length(Ls,N), list01(Ls,N0,N1).\\[2mm]
684: %%\> r21: \> plist01(Ls) \la list01(Ls,N0,N1), \\
685: %\> \> \> $\neg$length(Ls,N0),
686: %$\neg$length(Ls,N1).
687: %\end{program2}
688: %
689: Let also $|\ |_2$ be the trivial level mapping for $R_2$ defined by:
690:
691: \begin{program}
692: %\> \(\mathtt{|llist01(\mathit{ls},\mathit{n})|_2 = 1}\)\\
693: \> \(\mathtt{|plist01(\mathit{ls})|_2 = 1}\)
694: \end{program}
695: and assume that $|L|_2 = 0$, if $L$ is not defined in $R_{2}$.
696:
697: Let us consider the following sets of atomic queries for
698: $\mathtt{LIST01}:=R_1\cup R_2$:
699:
700: \begin{program}
701: \({\cal Q}_1 \ =\ \{\mathtt{list01(\mathit{ls},\mathit{n0},\mathit{n1})} | \
702: \mathit{ls} \textrm{ is a list, possibly non-ground, of a fixed length}\};\)\\[1mm]
703: \({\cal Q}_2\ =\ \{\mathtt{length(\mathit{ls},\mathit{n})} | \ \mathit{n}
704: \textrm{ is a ground term of the form either 0 or } \texttt{s(s(\ldots(0)))} \};\)\\[1mm]
705: \({\cal Q}_3 \ =\ \{\mathtt{plist01(\mathit{ls})} | \
706: \mathit{ls} \textrm{ is a list, possibly non-ground, of a fixed length}\}\).
707: \end{program}
708: %
709:
710: By definition of $|\ |_1$, all the atoms in ${\cal Q}_1$ and
711: ${\cal Q}_2$ are
712: bounded wrt.\ $|\ |_1$. Analo\-gously, all the atoms in ${\cal Q}_3$
713: are bounded wrt.\ $|\ |_2$.
714: Notice that for all atoms
715: $A\in {\it Call}_P({\cal Q}_j)$,
716: with $j\in\{1,2,3\}$, there exists $k\in\{1,2,3\}$ such that
717: $A\in {\cal Q}_k$. Hence,
718: if $A$ is defined in $R_i$ then $A$ is
719: bounded wrt.\ $|\ |_i$.
720: This proves that the set of queries
721: ${\cal Q}_1$, ${\cal Q}_2$ and ${\cal Q}_3$
722: are strongly bounded wrt.\
723: $\mathtt{LIST01}$ and $|\ |_1$, $|\ |_2$.
724: \end{example}
725:
726:
727: Here we introduce our main result.
728:
729: \begin{theorem}
730: \label{theo:strongn}
731: Let $P:=R_1\cup \ldots \cup R_n$ be a program such that
732: $ R_n\sqsupset \ldots \sqsupset R_1$ is a hierarchy,
733: $|\ |_1,\ldots,|\ |_n$ be level mappings for $R_1,\ldots,R_n$,
734: respectively,
735: and $M$ be a complete model of $P$.
736: Suppose that
737: \begin{itemize}
738: \item
739: $R_i$ is acceptable wrt.\ $|\ |_i$ and $M$,
740: for all $i\in\{1,\ldots,n\}$.
741: \item $Q$ is a query strongly bounded wrt.\
742: $P$ and $|\ |_1,\ldots,|\ |_n$.
743: \end{itemize}
744: Then all LDNF-derivations of $P\cup \{Q\}$
745: are finite.
746: \end{theorem}
747: \begin{proof}
748: Let $Q$ be a query strongly bounded wrt.\ $P$ and
749: $|\ |_{1},\ldots,|\ |_n$.
750: We prove the theorem by induction on $n$.
751:
752: \textit{Base}.
753: Let $n=1$.
754: This case follows immediately by Theorem \ref{theo:generale-sulle-classi},
755: where $P=R_1$, $R$ is empty and ${\cal C}$ is the class of strongly
756: bounded queries wrt.\ $R_1$ and $|\ |_1$, and the fact that
757: a strongly bounded atom is also bounded.
758:
759: \emph{Induction step}.
760: Let $n>1$.
761: Also this case follows by Theorem \ref{theo:generale-sulle-classi},
762: where $P=R_n$, $R=R_1\cup \ldots \cup R_{n-1}$ and
763: ${\cal C}$ is the class of strongly
764: bounded queries wrt.\
765: $R_1\cup \ldots \cup R_n$ and $|\ |_1,\ldots,|\ |_n$. In fact,
766: \begin{itemize}
767: \item
768: $R_n$ is acceptable wrt.\ $|\ |_n$ and $M$;
769: \item
770: for all queries $Q\in {\cal C}$, all LDNF-derivations of $(R_1\cup \ldots \cup R_{n-1})\cup\{Q\}$
771: are finite, by Remark \ref{i-strong} and the inductive hypothesis;
772: \item
773: for all atoms $A\in {\cal C}$,
774: if $A$ is defined in $R_n$ then $A$ is bounded wrt.\ $|\ |_n$,
775: by definition of strong boundedness.
776: \end{itemize}
777: \end{proof}
778: %
779:
780: Here are a few examples applying Theorem \ref{theo:strongn}.
781: \begin{example}
782: \label{exa:teo1}
783: Let us reconsider the program of Example \ref{exa:sb}.
784: In the program {\tt LIST01}, $R_1$ and $R_2$ are
785: acceptable wrt.\ any complete model and
786: the level mappings $|\ |_1$ and $|\ |_2$, respectively.
787: We already showed that ${\cal Q}_1, {\cal Q}_2$ and
788: ${\cal Q}_3$ are strongly bounded wrt.\ ${\tt LIST01}$ and
789: $|\ |_1$, $|\ |_2$.
790: Hence, by Theorem \ref{theo:strongn},
791: all LDNF-derivations of ${\tt LIST01}\cup\{Q\}$,
792: where $Q$ is a query in ${\cal Q}_1, {\cal Q}_2$ or
793: ${\cal Q}_3$, are finite.
794: \end{example}
795: %
796: Notice that in the previous example the top module in the hierarchy,
797: $R_2$, contains no recursion. Hence it is intuitively clear that any
798: problem for termination cannot depend on it. This is reflected by the
799: fact that the level mapping for $R_2$ is completely trivial.
800: This shows how the hierarchical decomposition of the program can
801: simplify the termination proof.
802: %
803: \begin{example}
804: \label{exa:teo2}
805: Consider the sorting program \texttt{MERGESORT} \cite{Apt97}:
806: \begin{program2}
807: \> c1: \> mergesort([ ],[ ]).\\
808: \> c2: \> mergesort([X],[X]). \\
809: \> c3: \> mergesort([X,Y|Xs],Ys) \la \\
810: \> \> \> split([X,Y|Xs],X1s,X2s),\\
811: \> \> \> mergesort(X1s,Y1s),\\
812: \> \> \> mergesort(X2s,Y2s),\\
813: \> \> \> merge(Y1s,Y2s,Ys).\\[2mm]
814: \> c4: \> split([ ],[ ],[ ]).\\
815: \> c5: \> split([X|Xs],[X|Ys],Zs) \la split(Xs,Zs,Ys).\\[2mm]
816: \> c6: \> merge([ ],Xs,Xs).\\
817: \> c7: \> merge(Xs,[ ],Xs).\\
818: \> c8: \> merge([X|Xs],[Y|Ys],[X|Zs]) \la
819: X<=Y, merge(Xs,[Y|Ys],Zs).\\
820: \> c9: \> merge([X|Xs],[Y|Ys],[Y|Zs]) \la X>Y, merge([X|Xs],Ys,Zs).
821: \end{program2}
822:
823: Let us divide the program \texttt{MERGESORT} into three
824: modules, $R_1,R_2,R_3$, such that $ R_3 \sqsupset R_2 \sqsupset R_1$
825: as follows:
826:
827: \begin{itemize}
828: \item $R_3:=\{\mathtt{c1}, \mathtt{c2}, \mathtt{c3}\}$, it defines the relation
829: \texttt{mergesort},
830: \item $R_2:=\{\mathtt{c4}, \mathtt{c5}\}$, it
831: defines the relation
832: \texttt{split},
833: \item $R_1:=\{\mathtt{c6}, \mathtt{c7}, \mathtt{c8}, \mathtt{c9}\}$, it
834: defines the relation
835: \texttt{merge}.
836: \end{itemize}
837:
838: Let us consider the natural level mappings
839:
840: \begin{program}
841: \> \(\mathtt{|merge(\mathit{xs},\mathit{ys},\mathit{zs})|_{1} = |\mathit{xs}|_{length}+|\mathit{ys}|_{length}}\)\\[2mm]
842: \> \(\mathtt{|split(\mathit{xs},\mathit{ys},\mathit{zs})|_{2} = |\mathit{xs}|_{length}}\) \\[2mm]
843: \> \(\mathtt{|mergesort(\mathit{xs},\mathit{ys})|_{3} = |\mathit{xs}|_{length}}\)
844: \end{program}
845: and assume that for all $i\in\{1,2,3\}$,
846: \(\mathtt{|\textit{L}|_{i} = 0 \textrm{ if \textit{L} is not
847: defined in }} R_i\).
848:
849: All ground queries
850: are strongly bounded wrt.\ the program \texttt{MERGESORT} and
851: the level mappings $|\ |_1,|\ |_2,|\ |_3$.
852: Moreover, since the program is a definite one,
853: $R_1$ and $R_2$ are
854: acceptable wrt.\ any model and
855: the level mappings $|\ |_1$ and $|\ |_2$,
856: respectively, while
857: $R_3$ is acceptable wrt.\ the level mapping $|\ |_3$
858: and the model $M$ below:
859:
860: \begin{program2}
861: \> \(\mathit{M =}\) \>
862: \(\mathtt{[mergesort(Xs,Ys)]} \cup \mathtt{[merge(Xs,Ys,Zs)]} \cup \)\\
863: \> \> \(\mathtt{\{split([\;],[\;],[\;])\}} \cup \)\\
864: \> \> \(\mathtt{\{split([\mathit{x}],[\;],[\mathit{x}])|\
865: \mathit{x} \textrm{ is any ground term}\}} \cup \)\\
866: \> \> \(\mathtt{\{split([\mathit{x}],[\mathit{x}],[\;])|\
867: \mathit{x} \textrm{ is any ground term}\}} \cup \)\\
868: \>\> \(\mathtt{\{split(\mathit{xs},\mathit{ys},\mathit{zs})|\
869: \mathit{xs}, \mathit{ys}, \mathit{zs} \textrm{ are ground terms and} } \)\\
870: \> \> \(
871: |\mathit{xs}|_{length}\geq 2,\;
872: |\mathit{xs}|_{length}>|\mathit{ys}|_{length},
873: \mathtt{|\mathit{xs}|_{length}>
874: |\mathit{zs}|_{length}\}}\)
875: \end{program2}
876: where we denote by $[A]$ the set of all ground
877: instances of an atom $A$.
878:
879: Hence, by Theorem \ref{theo:strongn},
880: all LDNF-derivations of
881: ${\tt MERGESORT}\cup\{Q\}$, where $Q$ is a ground query, are finite.
882:
883: Note that by exchanging the roles of $R_{1}$ and $R_{2}$
884: we would obtain the same result. In fact the definition of
885: ${\tt merge}$ and ${\tt split}$ are independent from each other.
886: \end{example}
887:
888:
889: %%%%%%%%%%%%%%%%%%%%%
890: \section{Well-Behaving Programs}
891: \label{sec:applications}
892: %%%%%%%%%%%%%%%%%%%%%
893:
894: In this section we consider the problem of how to prove that a
895: query is strongly bounded. In fact one could argue that checking strong
896: boundedness is more difficult and less abstract than checking boundedness
897: itself in the sense of \cite{AP93}:
898: we have to refer to all LDNF-derivations instead of referring to a model, which
899: might well look like a step backwards in the proof of termination of a
900: program. This is only partly true: in order to check strong boundedness
901: we can either employ tools based on abstract interpretation
902: or concentrate our attention only on programs
903: which exhibit useful
904: persistence properties wrt.\ LDNF-resolution.
905:
906: We now show how the well-established notions of well-moded and
907: well-typed programs can be employed in order to verify strong boundedness
908: and how they can lead to simple termination proofs.
909:
910: %%%%%%%%%%%%%%%%%%%%%%%%%
911: \subsection{Well-Moded Programs}
912: %%%%%%%%%%%%%%%%%%%%%%%%%
913:
914: The concept of a well-moded program is due to \cite{DM85}. The formulation we use here is from
915: \cite{Ros91}, and it is equivalent to that in
916: \cite{Dra87}. The original definition was given for definite programs
917: (i.e., programs without negation), however it applies to general
918: programs as well, just by considering literals instead of atoms.
919: It relies on the concept of \emph{mode}, which is a function that
920: labels the positions
921: of each predicate in order to indicate how the arguments of a
922: predicate should be used.
923:
924: \begin{definition}[Mode]
925: Consider an $n$-ary predicate symbol $p$. By a \emph{mode} for $p$
926: we mean a function $m_p$ from $\{1,\ldots,n\}$ to the set $\{+,-\}$.
927: If $m_p(i)=+$ then we call $i$ an {\it input position} of $p$;
928: if $m_p(i)=-$ then we call $i$ an {\it output position} of $p$.
929: By a \emph{moding} we mean a collection of modes, one for each
930: predicate symbol.
931: \end{definition}
932:
933: In a moded program, we assume that each predicate symbol has a unique
934: mode associated to it.
935: Multiple moding may be obtained by simply renaming the predi\-cates.
936: We use the notation \(p(m_p(1),\ldots,m_p(n))\) to denote the moding
937: associated with a predicate $p$
938: (e.g., $\mathtt{append(\textrm{+},\textrm{+},\mathrm{-})}$).
939: Without loss of generality, we assume, when writing a literal as
940: $p({\bf s},{\bf t})$, that we are
941: indicating with ${\bf s}$ the sequence of terms filling in the input
942: positions of $p$ and with ${\bf t}$ the sequence of terms filling in
943: the output positions of $p$.
944: Moreover, we adopt the convention that $p({\bf s},{\bf t})$
945: could denote both negative and positive literals.
946:
947:
948: \begin{definition}[Well-Moded]
949: \label{def:well-moded}
950: \begin{itemize}
951: \item
952: A query $p_1({\bf s}_1,{\bf t}_1),\ldots,p_n({\bf s}_n,{\bf t}_n)$
953: is called \emph{well-moded} if for all $i\in\{1,\ldots,n\}$
954: $${\it Var}({\bf s}_i)\subseteq \bigcup_{j=1}^{i-1}{\it Var}({\bf
955: t}_j).$$
956: \item
957: A clause $p({\bf t}_0,{\bf s}_{n+1})\leftarrow
958: p_1({\bf s}_1,{\bf t}_1),\ldots,p_n({\bf s}_n,{\bf t}_n)$
959: is called \emph{well-moded} if for all $i\in\{1,\ldots,n+1\}$
960: $${\it Var}({\bf s}_i)\subseteq \bigcup_{j=0}^{i-1}{\it Var}({\bf t}_j).$$
961: \item A program is called \emph{well-moded} if all of its clauses are
962: well-moded.
963: \end{itemize}
964: \end{definition}
965:
966: %Thus a query is well-moded if every variable occurring in an input
967: %position of a literal occurs in an output position of an earlier
968: %literal in the query. A clause is well-moded if (i) every variable
969: %occurring in an input position of a body literal occurs either in an
970: %input position of the head, or in an output position of an earlier
971: %body literal; (ii) every variable occurring in an output position of
972: %the head occurs in an input position of the head, or in an output
973: %position of a body literal.
974:
975: Note that well-modedness can be syntactically checked
976: in a time which is linear wrt.\ the size of the program (query).
977:
978: \begin{remark}
979: \label{remark:prefix_wm}
980: If $Q$ is a well-moded query then all its prefixes are well-moded.
981: \end{remark}
982:
983:
984: The following lemma states that well-moded queries are closed under
985: LDNF-resolution. This result has been proved in \cite{AP94a}
986: for LD-derivations and definite programs.
987:
988: \begin{lemma}
989: \label{lemma:well-moded-closed}
990: Let $P$ and $Q$ be a well-moded program and query, respectively. Then all
991: LDNF-descendants of $P\cup\{Q\}$ are well-moded.
992: \end{lemma}
993: \begin{proof}
994: It is sufficient to extend the proof in \cite{AP94a}
995: by showing that if a query $\neg A, L_1,\ldots,L_n$
996: is well-moded and $A$ is ground
997: then both $A$ and $L_1,\ldots,L_n$ are well-moded.
998: This follows immediately by definition of well-modedness.
999: If $A$ is non-ground then the query above has no descendant.
1000: \end{proof}
1001:
1002:
1003:
1004: When considering well-moded programs, it is natural to
1005: measure atoms only in their input positions \cite{EBC99}.
1006:
1007: \begin{definition}[Moded Level Mapping]
1008: Let $P$ be a moded program. A function $|\;|$ is a \emph{moded
1009: level mapping for $P$} if it is a level mapping for $P$
1010: such that
1011: \begin{itemize}
1012: \item for any $\mathbf{ s}$, $\mathbf{ t}$ and $\mathbf{ u}$, $|p(\mathbf{
1013: s},\mathbf{ t})|=|p(\mathbf{ s},\mathbf{ u})|$.
1014: \end{itemize}
1015: \end{definition}
1016:
1017: Hence in a moded level mapping
1018: the level of an atom is independent from the terms
1019: in its output positions.
1020:
1021:
1022: The following Remark and Proposition allow us to exploit well-modedness
1023: for applying Theorem \ref{theo:strongn}.
1024:
1025:
1026: \begin{remark}
1027: \label{remark-modedlevelmapp}
1028: Let $P$ be a well-moded program.
1029: If $Q$ is well-moded, then $\emph{first}(Q)$ is ground in its input
1030: position and hence it is bounded wrt.\ any moded level mapping for $P$.
1031: Moreover, by
1032: Lemma \ref{lemma:well-moded-closed},
1033: every well-moded query is strongly bounded wrt.\ $P$
1034: and any moded level mapping for $P$.
1035: \end{remark}
1036:
1037: \begin{proposition}
1038: \label{pro:strongbound_wm}
1039: Let $P:=R_1\cup \ldots \cup R_n$ be a \emph{well-moded} program
1040: and
1041: $ R_n\sqsupset \ldots \sqsupset R_1$ a hierarchy, and
1042: $|\ |_1,\ldots,|\ |_n$ be
1043: \emph{moded} level mappings for $R_1,\ldots,R_n$,
1044: respectively.\\
1045: Then every well-moded query is
1046: strongly bounded wrt.\ $P$ and $|\ |_1,\ldots,|\ |_n$.
1047: \end{proposition}
1048:
1049: \begin{example}
1050: \label{exa:well-moded-program1}
1051: Let \texttt{MOVE} be the following program which defines
1052: a permutation between two lists such that only one element is moved.
1053: We introduce modes and we distinguish the two uses of \texttt{append}
1054: by renaming it as \texttt{append1} and \texttt{append2}.
1055: \begin{program2}
1056: \> mode \(\mathtt{delete(\mathit{+},\mathit{-},\mathit{-})}\).\\
1057: \> mode \(\mathtt{append1(\mathit{-},\mathit{-},\mathit{+}}\)). \\
1058: \> mode \(\mathtt{append2(\mathit{+},\mathit{+},\mathit{-})}\).\\
1059: \> mode \(\mathtt{move(\mathit{+},\mathit{-})}\).
1060: \end{program2}
1061: \begin{program2}
1062: \>r1: \> delete([X|Xs],X,Xs).\\
1063: \>r2: \> delete([X|Xs],Y,[X|Ys]) \la delete(Xs,Y,Ys). \\[2mm]
1064: \>r3: \> append1([ ],Ys,Ys).\\
1065: \>r4: \> append1([X|Xs],Ys,[X|Zs]) \la append1(Xs,Ys,Zs). \\[2mm]
1066: \>r5: \> append2([ ],Ys,Ys).\\
1067: \>r6: \> append2([X|Xs],Ys,[X|Zs]) \la append2(Xs,Ys,Zs). \\[2mm]
1068: \>r7: \> move(Xs,Ys) \la append1(X1s,X2s,Xs),\\
1069: \> \> \> delete(X1s,X,Y1s), append2(Y1s,[X|X2s],Ys).
1070: \end{program2}
1071: Let us partition \texttt{MOVE} into the modules
1072: $R_1=\{\mathtt{r_1},\mathtt{r_2},\mathtt{r_3},\mathtt{r_4}, \mathtt{r_5},\mathtt{r_6}\}$ and
1073: $R_2=\{\mathtt{r_7}\}$ ($R_2$ extends $R_1$).
1074: Let $|\ |_1$ be
1075: the natural level mapping for $R_1$ defined by:
1076:
1077: \begin{program}
1078: \> \(\mathtt{|append1(\mathit{xs},\mathit{ys},\mathit{zs})|_1 = |\mathit{zs}|_{length}}\)\\
1079: \> \(\mathtt{|append2(\mathit{xs},\mathit{ys},\mathit{zs})|_1 = |\mathit{xs}|_{length}}\). \\
1080: \> \(\mathtt{|delete(\mathit{xs},\mathit{x},\mathit{ys})|_1 = |\mathit{xs}|_{length}}\).
1081: \end{program}
1082: $R_2$ does not contain any recursive definition
1083: hence
1084: let $|\ |_2$ be the trivial level mapping defined by:
1085: \begin{program}
1086: \> \(\mathtt{|move(\mathit{xs},\mathit{ys})|_2 = 1}\)
1087: \end{program}
1088: and assume that
1089: $|L|_2 = 0$, if $L$ is not defined in $R_{2}$.
1090:
1091:
1092: The program
1093: ${\tt MOVE}:=R_1\cup R_2$ is well-moded
1094: and hence by Proposition \ref{pro:strongbound_wm}
1095: every well-moded query is strongly bounded wrt.\ {\tt MOVE}
1096: and
1097: $|\ |_1$, $|\ |_2$.
1098: \end{example}
1099:
1100:
1101: \begin{example}
1102: \label{exa:well-moded-program2}
1103: Let $R_1$ be the program
1104: which defines the relations \texttt{member} and
1105: \texttt{is},
1106: $R_2$ be the program
1107: defining the relation \texttt{count} and
1108: $R_3$ be the program
1109: defining the relation
1110: \texttt{diff} with the moding and the definitions below.
1111: \begin{program2}
1112: \> mode \(\mathtt{member(\mathit{+},\mathit{+})}\).\\
1113: \> mode \(\mathtt{is(\mathit{-},\mathit{+})}\).\\
1114: %\> mode \(\mathtt{\texttt{>=}(\mathit{+},\mathit{+})}\).\\
1115: %\> mode \(\mathtt{\texttt{<}(\mathit{+},\mathit{+})}\).\\
1116: \> mode \(\mathtt{diff(\mathit{+},\mathit{+},\mathit{+},\mathit{-})}\).\\
1117: \> mode \(\mathtt{count(\mathit{+},\mathit{+},\mathit{-})}\).\\[2mm]
1118:
1119:
1120: \> r1: \> member(X,[X|Xs]).\\
1121: \> r2: \> member(X,[Y|Xs]) \la member(X,Xs). \\[2mm]
1122: \> r3: \> diff(Ls,I1,I2,N) \la count(Ls,I1,N1), count(Ls,I2,N2), \\
1123: \> \> \> N is N1-N2.\\[2mm]
1124: \> r4: \> count([ ],I,0).\\
1125: \> r5: \> count([H|Ts],I,M) \la member(H,I), count(Ts,I,M1), \\
1126: \> \> \>M is M1+1.\\
1127: \> r6: \> count([H|Ts],I,M) \la \(\neg\) member(H,I), count(Ts,I,M).
1128: \end{program2}
1129: The relation
1130: $\mathtt{diff(\mathit{ls},\mathit{i1},\mathit{i2},\mathit{n})}$, given a list $\mathit{ls}$ and two check-lists
1131: $\mathit{i1}$ and $\mathit{i2}$, defines
1132: the difference $\mathit{n}$ between the number
1133: of elements of $\mathit{ls}$ occurring in $\mathit{i1}$ and the number of
1134: elements of $\mathit{ls}$ occurring in $\mathit{i2}$.
1135: Clearly $R_3\sqsupset R_2 \sqsupset R_1$.
1136: It is easy to see
1137: that $R_1$ is
1138: acceptable wrt.\ any complete model and the moded level mapping
1139:
1140: \begin{program}
1141: \> \(\mathtt{|member(\mathit{e},\mathit{ls})|_1 = |\mathit{ls}|_{length}}\)
1142: \end{program}
1143: $R_2$ is acceptable wrt.\ any complete model
1144: and the moded level mapping:
1145: \begin{program}
1146: \> \(\mathtt{|count(\mathit{ls},\mathit{i},\mathit{n})|_2 = |\mathit{ls}|_{length}}\)
1147: \end{program}
1148: and $R_3$ is acceptable wrt.\ any complete model
1149: and the trivial moded level mapping:
1150: \begin{program}
1151: \> \(\mathtt{|diff(\mathit{ls},\mathit{i1},\mathit{i2},\mathit{n}) |_3= 1}\)
1152: \end{program}
1153: where \(\mathtt{|\mathit{L}|_i = 0}\), if $L$ is not defined in $R_{i}$.
1154:
1155: The program ${\tt DIFF} := R_{1} \cup R_{2}\cup R_{3}$ is well-moded.
1156: Hence,
1157: by Proposition \ref{pro:strongbound_wm},
1158: every well-moded query is strongly bounded wrt.\ ${\tt DIFF}$ and
1159: $|\ |_1$, $|\ |_2$, $|\ |_3$.
1160: \end{example}
1161:
1162: Note that the class of strongly bounded queries is generally
1163: larger than the class of well-moded queries.
1164: Consider for instance the program \texttt{MOVE} and the query
1165: $Q:=$ $\mathtt{move([X1,X2],Ys), delete(Ys,Y,Zs)}$
1166: which is not well-moded since it is not ground in the input
1167: position of the first atom.
1168: However $Q$ can be easily recognized to be strongly
1169: bounded wrt.\ \texttt{MOVE} and
1170: $|\ |_{1}$, $|\ |_{2}$
1171: defined in Example \ref{exa:well-moded-program1}.
1172: We will come back to this query later.
1173:
1174: %%%%%%%%%%%%%%%%%%%
1175: \subsection{Well-Typed Programs}
1176: %%%%%%%%%%%%%%%%%%%
1177:
1178: A more refined well-behavior property of programs,
1179: namely well-typedness, can also be useful in order to ensure the
1180: strong boundedness property.
1181:
1182: The notion of well-typedness relies both on the concepts of \emph{mode}
1183: and \emph{type}. The following very general definition of a type is
1184: sufficient for our purposes.
1185:
1186:
1187: \begin{definition}[Type]
1188: A \emph{type} is a set of terms closed under substitution.
1189: \end{definition}
1190:
1191: Assume as given a specific set of types,
1192: denoted by \emph{Types}, which includes
1193: $Any$, the set of all terms, and $Ground$ the set of all ground terms.
1194:
1195: \begin{definition} [Type Associated with a Position]
1196: A \emph{type for an $n$-ary predicate symbol $p$} is
1197: a function $t_p$ from $\{1,\ldots,n\}$ to the set \emph{Types}.
1198: If $t_p(i)=T$, we call $T$ \emph{the type associated with the
1199: position $i$ of $p$}.
1200: Assuming a type $t_p$ for the predicate $p$, we say that a
1201: literal $p(s_1,\ldots,s_n)$ is \emph{correctly typed in position $i$}
1202: if $s_i\in t_p(i)$.
1203: \end{definition}
1204:
1205: In a typed program we assume that every predicate $p$ has a fixed
1206: mode $m_p$ and a fixed type $t_p$ associated with it and we denote
1207: it by \[p(m_p(1):t_p(1),\ldots,m_p(n):t_p(n)).\]
1208: So, for instance, we write
1209:
1210: \[\mathtt{append(\mathit{+:List},\mathit{+:List},\mathit{-:List})}\]
1211: %
1212: to denote the moded atom
1213: $\mathtt{append(\mathit{+},\mathit{+},\mathit{-})}$
1214: where the type associated with each argument position is
1215: $\mathit{List}$, i.e., the set of all lists.
1216:
1217: We can then talk about types of input and of output positions of an
1218: atom.
1219:
1220:
1221: The notion of well-typed queries and programs relies on the
1222: following concept of type judgement.
1223:
1224: \begin{definition}[Type Judgement]
1225: By a \emph{type judgement} we mean a statement of the form
1226: \(\mathbf{s:S\Rightarrow t:T}.\)
1227: We say that a type judgement \(\mathbf{s:S\Rightarrow t:T}\)
1228: \emph{is true}, and write
1229: \(\mathbf{\models s:S\Rightarrow t:T},\)
1230: if for all substitutions $\theta$,
1231: \(\mathbf{s}\theta\in \mathbf{S}\) implies
1232: \(\mathbf{t}\theta\in \mathbf{T}\).
1233: \end{definition}
1234:
1235: For example, the type judgements \((x: \mathit{Nat}, \; l:
1236: \mathit{ListNat}) \Rightarrow ([x|l]: \mathit{ListNat})\)
1237: and \(( [x|l]: \mathit{ListNat}) \Rightarrow (l:\mathit{ListNat})\)
1238: are both true.
1239:
1240: A notion of well-typed program has been first introduced in
1241: \cite{BLR92} and also studied in
1242: \cite{AE93} and in \cite{AL95}. Similarly to
1243: well-moding, the notion was developed for definite programs.
1244: Here we extend it to general programs.
1245:
1246: In the following definition, we assume that
1247: $\mathbf{i}_s: \mathbf{I}_s$
1248: is the sequence of typed terms filling in the input positions of $L_s$
1249: and $\mathbf{o}_s:\mathbf{O}_s$
1250: is the sequence of typed terms filling in the
1251: output positions of $L_s$.
1252:
1253: \begin{definition}[Well-Typed]
1254: \label{def:well-typed}
1255: \begin{itemize}
1256: \item
1257: A query \(L_1,\ldots, L_n\)
1258: is called \emph{well-typed}
1259: if for all $j\in\{1,\ldots,n\}$
1260: \[\models \mathbf{o}_{j_1}: \mathbf{O}_{j_1}, \ldots, \mathbf{o}_{j_k}: \mathbf{O}_{j_k} \Rightarrow
1261: \mathbf{i}_{j}: \mathbf{I}_{j}\]
1262: where $L_{j_1},\ldots , L_{j_k}$ are all the positive literals
1263: in $L_1,\ldots,L_{j-1}$.
1264: \item
1265: A clause \(L_0
1266: \leftarrow L_1,\ldots,L_n\)
1267: is called \emph{well-typed}
1268: if for all $j\in\{1,\ldots,n\}$
1269: \[\models \mathbf{i}_0: \mathbf{I}_0, \mathbf{o}_{j_1}: \mathbf{O}_{j_1}, \ldots, \mathbf{o}_{j_k}: \mathbf{O}_{j_k} \Rightarrow
1270: \mathbf{i}_j: \mathbf{I}_{j}\]
1271: where $L_{j_1},\ldots , L_{j_k}$ are all the positive literals
1272: in $L_1,\ldots,L_{j-1}$, and
1273: \[\models \mathbf{i}_0: \mathbf{I}_{0}, \mathbf{o}_{j_1}: \mathbf{O}_{j_1}, \ldots, \mathbf{o}_{j_h}: \mathbf{O}_{j_h} \Rightarrow
1274: \mathbf{o}_{0}: \mathbf{O}_{0}\]
1275: where $L_{j_1},\ldots , L_{j_h}$ are all the positive literals
1276: in $L_1,\ldots,L_{n}$.
1277: \item
1278: A program is called \emph{well-typed} if all of its clauses are
1279: well-typed.
1280: \end{itemize}
1281: \end{definition}
1282: %
1283: Note that an atomic query is well-typed iff it is correctly
1284: typed in its input positions and a unit clause
1285: \(p(\mathbf{s:S},\mathbf{t:T})\leftarrow\) is well-typed if \(\mathbf{\models
1286: s:S \Rightarrow t:T}\).
1287:
1288: The difference between Definition \ref{def:well-typed} and the one usually given
1289: for definite programs is that the correctness
1290: of the terms filling
1291: in the output positions of negative literals
1292: cannot be used to deduce
1293: the correctness of the terms filling
1294: in the input positions of a literal to the right
1295: (or the output positions of the head in a clause).
1296: The two definitions coincide either for definite programs or
1297: for general programs whose negative literals
1298: have only input positions.
1299:
1300: As an example, let us consider the trivial program
1301:
1302: \begin{program}
1303: \> p($\mathit{-:List}$).\\
1304: \>q($\mathit{+:List}$).\\[2mm]
1305: \>p([]).\\
1306: \> q([]).
1307: \end{program}
1308: By adopting a straightforward extension of well-typedness
1309: to normal programs which considers also the outputs of negative literals,
1310: we would have that the query $\mathtt{\neg p(a), q(a)}$ is well-typed
1311: even if $\mathtt{a}$ is not a list. Moreover well-typedness would
1312: not be persistent wrt.\ LDNF-resolution since
1313: $\mathtt{q(a)}$, which is the first LDNF-resolvent of the previous query,
1314: is no more well-typed.
1315: Our extended definition and the classical one
1316: coincide either for definite programs or for
1317: general programs whose negative literals have only input positions.
1318:
1319: For definite programs, well-modedness can be viewed as a special case of
1320: well-typedness if we consider only one type: $Ground$.
1321: With our extended definitions of well-moded and well-typed
1322: general programs this is no more true.
1323: We could have given a more complicated definition
1324: for well-typedness in order to capture
1325: also well-modedness as a special case.
1326: For the sake of simplicity, we prefer to give
1327: two distinct and simpler definitions.
1328:
1329: \begin{remark}
1330: \label{remark:prefix_wt}
1331: If $Q$ is a well-typed query, then all its non-empty prefixes are well-typed.
1332: In particular, $\mathit{first}(Q)$ is well-typed.
1333: \end{remark}
1334:
1335: The following Lemma
1336: shows that well-typed queries are closed under LDNF-resolution.
1337: It has been proved in \cite{BLR92}
1338: for definite programs.
1339:
1340: \begin{lemma}
1341: \label{lemma:well-typed-closed}
1342: Let $P$ and $Q$ be a well-typed program and query, respectively.
1343: Then all
1344: LDNF-descendants of $P\cup \{Q\}$ are well-typed.
1345: \end{lemma}
1346: \begin{proof}
1347: Similarly to the case of well-moded programs,
1348: to extend the result to general programs
1349: it is sufficient to show that if a query $Q:=\neg A, L_1,\ldots,L_n$
1350: is well-typed
1351: then both $A$ and $L_1,\ldots,L_n$ are well-typed.
1352: In fact, by Remark \ref{remark:prefix_wt},
1353: $\neg A= \mathit{first}(Q)$ is well-typed
1354: and by Definition \ref{def:well-typed}, if the first literal in a well-typed query is
1355: negative, then it is not used
1356: to deduce well-typedness of the rest of the query.
1357: \end{proof}
1358:
1359:
1360:
1361: It is now natural to exploit well-typedness in order to check strong
1362: boundedness.
1363: Analogously to well-moded programs, there are level mappings that are
1364: more natural in presence of type information. They are the level mappings
1365: for which every well-typed atom is bounded.
1366: By Lemma \ref{lemma:well-typed-closed} we have that
1367: a well-typed query $Q$ is strongly bounded wrt.\
1368: a well-typed program $P$ and any such level mapping.
1369: This is stated by the next proposition.
1370:
1371: \begin{proposition}
1372: \label{pro:strongbound_wt}
1373: Let $P:=R_1\cup \ldots \cup R_n$ be a \emph{well-typed} program and
1374: $ R_n\sqsupset \ldots \sqsupset R_1$ be a hierarchy, and
1375: $|\ |_1,\ldots,|\ |_n$ be
1376: level mappings for $R_1,\ldots,R_n$,
1377: respectively. Suppose that for
1378: every well-typed atom $A$, if $A$ is defined in $R_i$
1379: then $A$ is bounded wrt.\ $|\ |_i$,
1380: for $i\in\{1,\ldots,n\}$.
1381: Then every well-typed query is
1382: strongly bounded wrt.\ $P$ and $|\ |_1,\ldots,|\ |_n$.
1383: \end{proposition}
1384:
1385:
1386: \begin{example}
1387: \label{exa:typed1}
1388: Let us consider again the modular proof of
1389: termination for $\mathtt{MOVE}:=R_{1}\cup R_{2}$, where
1390: $R_{1}$ defines the relations
1391: \texttt{append1}, \texttt{append2} and \texttt{delete},
1392: while $R_{2}$, which extends $R_{1}$, defines the relation
1393: \texttt{move}.
1394: We consider the moding of Example~\ref{exa:well-moded-program1} with the
1395: following types:
1396: \begin{program}
1397: \> \(\mathtt{delete(\mathit{+:List},\mathit{-: Any},\mathit{-:List})}\)\\
1398: \> \(\mathtt{append1(\mathit{-:List},\mathit{-:List},\mathit{+:List}}\)) \\
1399: \> \(\mathtt{append2(\mathit{+:List},\mathit{+:List},\mathit{-:List})}\)\\
1400: \> \(\mathtt{move(\mathit{+:List},\mathit{-:List})}\).
1401: \end{program}
1402: Program $\mathtt{MOVE}$ is \emph{well-typed} in the assumed modes and
1403: types.
1404:
1405: Let us consider the same
1406: level mappings as
1407: used in Example~\ref{exa:well-moded-program1}.
1408: We have already seen that
1409: $R_{2}$ is acceptable wrt.\ $|\ |_{2}$ and any model, and
1410: $R_{1}$ is acceptable wrt.\
1411: $|\ |_{1}$ and any model.
1412: By definition of $|\ |_{2}$ and $|\ |_{1}$, one can easily see that
1413: \begin{itemize}
1414: \item
1415: every well-typed atom $A$ defined in $R_{i}$
1416: is bounded wrt.\ $|\ |_{i}$.
1417: \end{itemize}
1418: Hence, by Proposition \ref{pro:strongbound_wt},
1419: \begin{itemize}
1420: \item
1421: every well-typed query is strongly bounded wrt.\
1422: $\mathtt{MOVE}$ and $|\ |_{1}$, $|\ |_{2}$.
1423: \end{itemize}
1424: Let us consider again the query
1425: $Q:=\mathtt{move([X1,X2],Ys), delete(Ys,Y,Zs)}$ which is not
1426: well-moded but it is well-typed.
1427: We have that $Q$ is strongly bounded wrt.\ {\tt MOVE}
1428: and $|\ |_{1}$, $|\ |_{2}$,
1429: and consequently, by Theorem \ref{theo:strongn},
1430: that all LDNF-derivations of
1431: ${\tt MOVE} \cup\{Q\}$ are finite.
1432: \end{example}
1433:
1434: \begin{example}
1435: \label{exa:typed2}
1436: Consider the program \texttt{COLOR\_MAP} from
1437: \cite{SS86} which gene\-rates a coloring of a map in such
1438: a way that no two neighbors have the same color.
1439: The map is represented as a list of regions and colors as a list of
1440: available colors. In turn, each region is determined by its name,
1441: color and the
1442: colors of its neighbors, so it is represented as a term
1443: \texttt{region(name,color,neighbors)}, where \texttt{neighbors}
1444: is a list of colors of the neighboring regions.
1445:
1446: \begin{program2}
1447: \> c1: \> color\_map([ ],Colors).\\
1448: \> c2: \> color\_map([Region|Regions],Colors) \la \\
1449: \> \> \> color\_region(Region,Colors),\\
1450: \> \> \> color\_map(Regions,Colors).\\[2mm]
1451: \> c3: \> color\_region(region(Name,Color,Neighbors),Colors) \la \\
1452: \> \> \> select(Color,Colors,Colors1)\\
1453: \> \> \> subset(Neighbors,Colors1).\\[2mm]
1454: \> c4: \> select(X,[X|Xs],Xs).\\
1455: \> c5: \> select(X,[Y|Xs],[Y|Zs]) \la select(X,Xs,Zs).\\[2mm]
1456: \> c6: \> subset([ ],Ys). \\
1457: \> c7: \> subset([X|Xs],Ys) \la
1458: member(X,Ys), subset(Xs,Ys).\\[2mm]
1459: \> c8: \> member(X,[X|Xs]).\\
1460: \> c9: \> member(X,[Y|Xs]) \la member(X,Xs).
1461: \end{program2}
1462:
1463: Consider the following modes and types for the program
1464: \texttt{COLOR\_MAP}:
1465: \begin{program}
1466: \> \(\mathtt{color\_map}(\mathit{+: ListRegion}, \mathit{+: List})\)\\
1467: \> \(\mathtt{color\_region}(\mathit{+: Region}, \mathit{+: List})\)\\
1468: \> \(\mathtt{select}(\mathit{+: Any}, \mathit{+: List}, \mathit{-: List})\)\\
1469: \> \(\mathtt{subset}(\mathit{+: List}, \mathit{+: List})\)\\
1470: \> \(\mathtt{member}(\mathit{+: Any}, \mathit{+: List})\)
1471: \end{program}
1472: where
1473: \begin{itemize}
1474: \item \emph{Region} is the set of all terms of the form
1475: \texttt{region(name,color,neighbors)} with
1476: \(\mathtt{name},\mathtt{color}\in \mathit{Any}\) and
1477: \(\mathtt{neighbors}\in \mathit{List}\),
1478: \item \emph{ListRegion} is the set of all lists of regions.
1479: \end{itemize}
1480:
1481:
1482: We can check that \texttt{COLOR\_MAP} is well-typed
1483: in the assumed modes and types.
1484:
1485:
1486: We can divide the program \texttt{COLOR\_MAP} into four distinct modules,
1487: $R_1,R_2,R_3,R_4$, in the hierarchy
1488: $ R_4\sqsupset R_3 \sqsupset R_2 \sqsupset R_1$ as follows:
1489: \begin{itemize}
1490: \item $R_4:=\{\mathtt{c1}, \mathtt{c2}\}$ defines the relation
1491: \texttt{color\_map},
1492: \item $R_3:=\{\mathtt{c3}\}$ defines the relation
1493: \texttt{color\_region},
1494: \item $R_2:=\{\mathtt{c4}, \mathtt{c5},\mathtt{c6}, \mathtt{c7}\}$
1495: defines the relations
1496: \texttt{select} and \texttt{subset},
1497: \item $R_1:=\{\mathtt{c8}, \mathtt{c9}\}$
1498: defines the relation
1499: \texttt{member}.
1500: \end{itemize}
1501:
1502: Each $R_i$ is trivially acceptable wrt.\
1503: any model $M$ and the simple level mapping $|\ |_i$ defined below:
1504:
1505: \begin{program}
1506: \> \(\mathtt{|color\_map(\mathit{xs},\mathit{y}s)|_{4} = |\mathit{xs}|_{length}}\)\\[2mm]
1507: \> \(\mathtt{|color\_region(\mathit{x},\mathit{xs})|_{3} = 1}\)\\[2mm]
1508: \> \(\mathtt{|select(\mathit{x},\mathit{xs},\mathit{ys})|_{2} = |\mathit{xs}|_{length}}\)\\
1509: \> \(\mathtt{|subset(\mathit{xs},\mathit{ys})|_{2} = |\mathit{xs}|_{length}}\)\\[2mm]
1510: \> \(\mathtt{|member(\mathit{x},\mathit{xs})|_{1} = |\mathit{xs}|_{length}}\)
1511: \end{program}
1512: where for all $i\in\{1,2,3,4\}$,
1513: $|L|_{i} = 0$, if $L$ is not defined in $R_i$.
1514:
1515: Moreover, for
1516: every well-typed atom $A$ and $i\in\{1,2,3,4\}$,
1517: if $A$ is defined in $R_i$ then $A$
1518: is bounded wrt.\ $|\ |_i$.
1519: Hence, by Proposition \ref{pro:strongbound_wt},
1520: \begin{itemize}
1521: \item
1522: every well-typed query is strongly bounded
1523: wrt.\ the program $\mathtt{COLOR\_MAP}$ and
1524: $|\ |_1,\ldots,|\ |_4$.
1525: \end{itemize}
1526: This proves that
1527: all LDNF-derivations of the program \texttt{COLOR\_MAP}
1528: star\-ting in a well-typed query are finite.
1529: In particular, all the LDNF-derivations starting in a query
1530: of the form \(\mathtt{color\_map(\mathit{xs},\mathit{ys})} \), where
1531: $\mathit{xs}$ is a list of regions and
1532: $\mathit{ys}$ is a list,
1533: are finite.
1534: Note that in proving termination of
1535: such queries the choice of a model is irrelevant.
1536: Moreover, since such queries are well-typed,
1537: their input arguments are required
1538: to have a specified structure, but they
1539: are not required to be ground terms as in the
1540: case of well-moded queries.
1541: Hence, well-typedness allows us
1542: to reason about a larger class of queries with
1543: respect to well-modedness.
1544:
1545: This example is also discussed in \cite{AP94}.
1546: In order to prove its termination
1547: they define a particular level mapping $|\ |$, obtained by combining the level mappings of each module, and a special model $M$
1548: wrt.\ which the whole program \texttt{COLOR\_MAP} is acceptable.
1549: Both the level mapping $|\ |$ and the model $M$ are non-trivial.
1550: \end{example}
1551:
1552:
1553: %%%%%%%%%%%%%%%%%%%
1554: \section{Iterative Proof Method}
1555: \label{sec:iteration}
1556: %%%%%%%%%%%%%%%%%%%
1557:
1558: In the previous section we have seen how we can exploit
1559: properties which are preserved by LDNF-resolution,
1560: such as well-modedness and well-typedness, for developing a
1561: modular proof of termination in a hierarchy of programs.
1562: In this section we show how these properties allow us to
1563: apply our general result, i.e., Theorem \ref{theo:generale-sulle-classi},
1564: also in an iterative way.
1565:
1566:
1567: \begin{corollary}
1568: \label{theo:R-well-terminating}
1569: Let $P$ and $R$ be two programs such that
1570: $P\cup R$ is well-moded and $P$ extends
1571: $R$, and $M$ be a complete model of $P\cup R$.
1572: Suppose that
1573: \begin{itemize}
1574: \item $P$ is acceptable wrt.\ a moded level mapping $|\ |$ and $M$,
1575: \item for all well-moded queries $Q$,
1576: all LDNF-derivations $R\cup\{Q\}$ are finite.
1577: \end{itemize}
1578: Then for all well-moded queries $Q$,
1579: all LDNF-derivations of
1580: $(P\cup R)\cup \{Q\}$ are finite.
1581: \end{corollary}
1582: \begin{proof}
1583: Let ${\cal C}$ be the class of well-moded queries of $P\cup R$.
1584: By Remark \ref{remark:prefix_wm}
1585: and
1586: Lemma \ref{lemma:well-moded-closed},
1587: ${\cal C}$ is $(P\cup R)$-closed.
1588: Moreover
1589: \begin{itemize}
1590: \item
1591: $P$ is acceptable wrt.\ a moded level mapping $|\ |$ and $M$,
1592: by hypothesis;
1593: \item
1594: for all well-moded queries $Q$, all LDNF-derivations of $R\cup\{Q\}$
1595: are finite, by hypothesis;
1596: \item
1597: for all well-moded atoms $A$,
1598: if $A$ is defined in $P$ then $A$ is bounded wrt.\ $|\ |$,
1599: by Remark \ref{remark-modedlevelmapp}, since $|\ |$ is a moded
1600: level mapping.
1601: \end{itemize}
1602: Hence by Theorem \ref{theo:generale-sulle-classi} we get the thesis.
1603: \end{proof}
1604: \medskip
1605:
1606: Note that this result allows one to incrementally prove
1607: well-termination for general programs thus
1608: extending the result given in \cite{EBC99}
1609: for definite programs.
1610:
1611:
1612: A similar result can be stated also for well-typed programs and
1613: queries, provided that there exists a level mapping for $P$
1614: implying
1615: boundedness of atomic well-typed queries.
1616:
1617: \begin{corollary}
1618: \label{theo:R-typed-terminating}
1619: Let $P$ and $R$ be two programs such that $P\cup R$ is
1620: well-typed and $P$ extends
1621: $R$, and $M$ be a complete model of $P\cup R$. Suppose that
1622: \begin{itemize}
1623: \item $P$ is acceptable wrt.\ a level mapping $|\ |$ and $M$,
1624: \item every well-typed atom defined in $P$ is bounded wrt.\ $|\ |$,
1625: \item for all well-typed queries $Q$,
1626: all LDNF-derivations of
1627: $R\cup\{Q\}$ are finite.
1628: \end{itemize}
1629: Then for all well-typed queries $Q$,
1630: all LDNF-derivations of
1631: $(P\cup R)\cup \{Q\}$ are finite.
1632: \end{corollary}
1633:
1634: \begin{proof}
1635: Let ${\cal C}$ be the class of well-typed queries of $P\cup R$.
1636: By Remark \ref{remark:prefix_wt}
1637: and
1638: Lemma \ref{lemma:well-typed-closed},
1639: ${\cal C}$ is $(P\cup R)$-closed.
1640: Moreover
1641: \begin{itemize}
1642: \item
1643: $P$ is acceptable wrt.\ a level mapping $|\ |$ and $M$,
1644: by hypothesis;
1645: \item
1646: for all well-typed queries $Q$, all LDNF-derivations of $R\cup\{Q\}$
1647: are finite,
1648: by hypothesis;
1649: \item
1650: for all well-typed atoms $A$,
1651: if $A$ is defined in $P$ then $A$ is bounded wrt.\ $|\ |$,
1652: by hypothesis.
1653: \end{itemize}
1654: Hence by Theorem \ref{theo:generale-sulle-classi} we have the thesis.
1655: \end{proof}
1656:
1657:
1658: \begin{example}
1659: \label{exa:iterative-method1}
1660: Let us consider again the program \texttt{COLOR\_MAP}
1661: with the same modes and types
1662: as in Example \ref{exa:typed2}.
1663: We apply the iterative termination proof
1664: given by Corollary~\ref{theo:R-typed-terminating}
1665: to \texttt{COLOR\_MAP}.
1666:
1667: {\bf First step.}
1668: \indent
1669: We can consider at first two trivial modules,
1670: $R_{1}:=\{\mathtt{c8}, \mathtt{c9}\}$
1671: which defines the relation \texttt{member},
1672: and $R_{0}:=\emptyset $.
1673: We already know that
1674: \begin{itemize}
1675: \item
1676: $R_{1}$ is acceptable wrt.\ any model $M$ and
1677: the level mapping $|\ |_1$ already defined;
1678: \item
1679: all well-typed atoms $A$, defined in $R_{1}$,
1680: are bounded wrt.\ $|\ |_1$;
1681: \item for all well-typed queries $Q$,
1682: all LDNF-derivations of
1683: $R_{0}\cup\{Q\}$ are trivially finite.
1684: \end{itemize}
1685: Hence, by Corollary \ref{theo:R-typed-terminating},
1686: for all well-typed queries $Q$,
1687: all LDNF-derivations of
1688: $(R_{1}\cup R_{0})\cup\{Q\}$ are finite.
1689:
1690: {\bf Second step.}
1691: \indent
1692: We can now iterate the process one level up.
1693: Let us consider the two modules,
1694: $R_{2}:=\{\mathtt{c4}, \mathtt{c5},\mathtt{c6}, \mathtt{c7}\}$
1695: which defines the relations
1696: \texttt{select} and \texttt{subset},
1697: and $R_{1}:=\{\mathtt{c8}, \mathtt{c9}\}$
1698: which defines the relation
1699: \texttt{member} and it is equal to $(R_{1}\cup R_{0})$
1700: of the previous step.
1701: We already showed in Example \ref{exa:typed2} that
1702: \begin{itemize}
1703: \item
1704: $R_{2}$ is acceptable wrt.\ any model $M$ and
1705: the level mapping $|\ |_2$ already defined;
1706: \item
1707: all well-typed atoms $A$, defined in $R_{2}$,
1708: are bounded wrt.\ $|\ |_2$;
1709: \item for all well-typed queries $Q$,
1710: all LDNF-derivations of
1711: $R_{1}\cup\{Q\}$ are finite.
1712: \end{itemize}
1713: Hence, by Corollary \ref{theo:R-typed-terminating},
1714: for all well-typed queries $Q$,
1715: all LDNF-derivations of
1716: $(R_{2}\cup R_{1})\cup\{Q\}$ are finite.
1717:
1718: By iterating the same reasoning for two steps more,
1719: we can prove that all LDNF-derivations
1720: of the program \texttt{COLOR\_MAP}
1721: starting in a well-typed query are finite.
1722: \end{example}
1723: %
1724: Our iterative method applies
1725: to a hierarchy of programs
1726: where on the lowest module, $R$,
1727: we require termination wrt.\ a particular class of queries.
1728: This can be a weaker requirement on $R$
1729: than acceptability as shown in the following contrived example.
1730: %
1731: \begin{example}
1732: \label{exa:iterative-method2}
1733: Let $R$ define the
1734: predicate \texttt{lcount} which counts
1735: the number of natural numbers in a list.
1736:
1737: \begin{program2}
1738: \> \(\mathtt{lcount(\mathit{+:List},\mathit{-:Nat})}\)\\
1739: \> \(\mathtt{nat(\mathit{+:Any})}\). \\[2mm]
1740: \> r1: \> lcount([ ],0).\\
1741: \> r2: \> lcount([X|Xs],s(N)) \la nat(X), lcount(Xs,N).\\
1742: \> r3: \> lcount([X|Xs],N) \la $\neg$ nat(X), lcount(Xs,N).\\
1743: \> r4: \> lcount(0,N) \la lcount(0,s(N)).\\[2mm]
1744: \> r5: \> nat(0).\\
1745: \> r6: \> nat(s(N)) \la nat(N).
1746: \end{program2}
1747:
1748:
1749: $R$ is well-typed wrt.\ the specified modes and types.
1750: Note that $R$ cannot be acceptable
1751: due to the presence of clause \texttt{r4}.
1752: On the other hand, the program
1753: terminates for all well-typed queries.
1754:
1755: Consider now the following program $P$ which extends $R$.
1756: The predicate {\tt split}, given a list of lists, separates the list
1757: elements containing more than {\tt max} natural numbers from the other
1758: lists:
1759: \begin{program2}
1760: \>
1761: \( \mathtt{split(\mathit{+:ListList},\mathit{-:ListList},\mathit{-:ListList})}\) \\
1762: \> >\((\mathit{+:Nat},\mathit{+:Nat})\) \\
1763: \> <=\((\mathit{+:Nat},\mathit{+:Nat})\) \\[2mm]
1764: \> p1: \> split([ ],[ ],[ ]).\\
1765: \> p2: \> split([L|Ls],[L|L1],L2) \la lcount(L,N), N > max, \\
1766: \> \> \> split(Ls,L1,L2).\\
1767: \> p3: \> split([L|Ls],L1,[L|L2]) \la lcount(L,N), N <= max, \\
1768: \> \> \>
1769: split(Ls,L1,L2).
1770: \end{program2}
1771:
1772:
1773: where \textit{ListList}
1774: denotes the set of all lists of lists, and \texttt{max} is
1775: a natural number. The program $P\cup R$ is well-typed.
1776: Let us consider
1777: the simple level mapping $|\ |$ for $P$ defined by:
1778:
1779: \begin{program}
1780: \> \(\mathtt{|split(\mathit{ls},\mathit{l1},\mathit{l2})| = |\mathit{ls}|_{length}}\)
1781: \end{program}
1782: which assigns level $0$ to any literal not defined in $P$.
1783: Note that
1784: \begin{itemize}
1785: \item $P$ is acceptable wrt.\ the level mapping $|\ |$ and any complete
1786: model $M$,
1787: \item all well-typed atoms defined in $P$ are bounded wrt.\ $|\ |$,
1788: \item for all well-typed queries $Q$,
1789: all LDNF-derivations of
1790: $R\cup\{Q\}$ are finite.
1791: \end{itemize}
1792: Hence, by Corollary \ref{theo:R-typed-terminating},
1793: for all well-typed queries $Q$,
1794: all LDNF-derivations of
1795: $(P\cup R)\cup\{Q\}$ are finite.
1796:
1797: This example shows that well-typedness
1798: could be useful to exclude what
1799: might be called ``dead code''.
1800: \end{example}
1801:
1802:
1803: %%%%%%%%%%%%%%%%
1804: \section{Comparing with Apt and Pedreschi's Approach}
1805: \label{sec:comparisons}
1806: %%%%%%%%%%%%%%%%
1807:
1808: Our work can be seen as an extension of a proposal in \cite{AP94}.
1809: Hence we devote this section to a comparison
1810: with their approach.
1811:
1812: On one hand, since our approach applies to general programs, it clearly covers
1813: cases which cannot be treated with the method proposed in \cite{AP94},
1814: which was developed for definite programs.
1815: On the other hand, for definite programs the classes of queries and programs
1816: which can
1817: be treated by Apt and Pedreschi's approach
1818: are properly included in those which can be treated by
1819: our method as we show in this section.
1820:
1821: We first recall
1822: the notions of \emph{semi-acceptability} and \emph{bounded query}
1823: used in~\cite{AP94}.
1824:
1825:
1826: \begin{definition}[Semi-acceptable Program]
1827: Let $P$ be a definite program, $|\ |$ be a level mapping for $P$ and $M$ be
1828: a model of $P$.
1829: $P$ is called \emph{semi-acceptable wrt.\ $|\ |$ and $M$} if for every
1830: clause $A\leftarrow {\bf A}, B,{\bf B}$ in ${\it ground}(P)$ such that
1831: $ M\models {\bf A}$
1832: \begin{itemize}
1833: \item $|A|>|B|, \mbox{ if } rel(A) \simeq rel(B)$,
1834: \item $ |A|\geq |B|, \mbox{ if } rel(A) \sqsupset rel(B)$.
1835: \end{itemize}
1836: \end{definition}
1837:
1838: %In the following we refer to a query bounded with respect to a
1839: %level mapping and a model \cite{AP94}.
1840:
1841:
1842: \begin{definition}[Bounded Query]
1843: \label{def-ext-Boundedness}
1844: Let $P$ be a definite program, $|\ |$ be a level mapping for $P$, and
1845: $M$ be a model of $P$.
1846: \begin{itemize}
1847: \item[$\bullet$] With each query $Q:=L_1,\ldots,L_n$
1848: we associate $n$ sets of natural numbers defined as follows:
1849: For $i\in \{1,\ldots,n\}$,
1850: $$|Q|_i^M=\{|L'_i|\;|\; L'_1,\ldots,L'_n
1851: \mbox{ is a ground instance of } Q
1852: \mbox{ and } M\models L'_1,\ldots,L'_{i-1}\}.$$
1853: \item[$\bullet$] A query $Q$ is called \emph{bounded wrt.
1854: $|\ |$ and $M$} if $|Q|_i^M$ is finite
1855: (i.e., if $|Q|_i^M$ has a maximum in ${\bf N}$) for all $i\in\{1,\ldots,n\}$.
1856: \end{itemize}
1857: \end{definition}
1858:
1859: \begin{lemma}
1860: \label{lemma:semi-preservation}
1861: Let $P$ be a definite program
1862: which is semi-acceptable wrt.\ $|\ |$ and $M$.
1863: If $Q$ is a query bounded wrt.\ $|\ |$ and $M$
1864: then all LD-descendants of $P\cup\{Q\}$ are bounded
1865: wrt.\ $|\ |$ and $M$.
1866: \end{lemma}
1867: \begin{proof}
1868: It is a consequence of Lemma 3.6 in \cite{AP94}
1869: and (the proof of) Lemma 5.4 in \cite{AP94}.
1870: \end{proof}
1871: \medskip
1872:
1873:
1874: We can always decompose a definite program $P$ into a hierarchy of
1875: $n \geq 1$ programs $P:=R_1\cup \ldots \cup R_n$, where
1876: $ R_n\sqsupset \ldots \sqsupset R_1$ in such a way that for every
1877: $ i \in \{1, \ldots, n\}$ if the predicate symbols
1878: $p_i$ and $q_i$ are both defined in $R_i$
1879: then neither $p_i \sqsupset q_i$ nor $q_i \sqsupset p_i$
1880: (either they are mutually recursive or independent).
1881: We call such a hierarchy a
1882: \emph{finest decomposition}
1883: of $P$.
1884:
1885: The following property has two main applications.
1886: First it allows us to compare our approach with \cite{AP94},
1887: then it provides an extension of Theorem \ref{theo:strongn}
1888: to hierarchies of semi-acceptable programs.
1889:
1890: \begin{proposition}
1891: \label{prop:semi}
1892: Let $P$ be a semi-acceptable program wrt.\ a level mapping $|\ |$
1893: and a model $M$ and
1894: $Q$ be a query strongly bounded wrt. $P$ and $|\ |$.
1895: Let $P := R_1 \cup \ldots \cup R_n$
1896: be a finest decomposition of $P$ into a hierarchy of modules.
1897: Let $|\ |_{i}$, with $i\in\{1,\ldots,n\}$, be defined in the following way:
1898: if $A$ is defined in $R_i$ then
1899: $ |A |_{i}=|A|$ else $ |A |_{i}=0$.
1900: Then
1901: \begin{itemize}
1902: \item every $R_i$
1903: is acceptable wrt.\ $|\ |_{i}$ and $M$ (with $i\in \{1,\ldots,n\}$),
1904: \item $Q$ is strongly bounded wrt. $R_1 \cup \ldots \cup R_n$
1905: and $|\ |_{1},\ldots,|\ |_{n}$.
1906: \end{itemize}
1907: \end{proposition}
1908: \begin{proof}
1909: Immediate by the definitions of semi-acceptability and
1910: strongly boundedness, since
1911: we are considering a finest decomposition.
1912: \end{proof}
1913: \medskip
1914:
1915: In order to compare our approach to the one presented in \cite{AP94}
1916: we consider only Theorem 5.8 in \cite{AP94}, since
1917: this is their most general result which implies the other ones, namely
1918: Theorem 5.6 and Theorem~5.7.
1919:
1920:
1921: \begin{theorem} [Theorem 5.8 in \cite{AP94}]
1922: \label{theo:apt-modular}
1923: Let $P$ and $R$ be two definite programs such that $P$ extends $R$, and let $M$ be
1924: a model of $P\cup R$. Suppose that
1925: \begin{itemize}
1926: \item $R$ is semi-acceptable wrt.\ $|\ |_R$ and $M\cap B_R$,
1927: \item $P$ is semi-acceptable wrt.\ $|\ |_P$ and $M$,
1928: \item there exists a level mapping $|\!|\ |\!|_P$ such that for every
1929: ground instance of a clause from $P$, $A\la \ol A, B, \ol B$, such that
1930: $M\models \ol A$
1931: \begin{itemize}
1932: \item $|\!|A |\!|_P \geq |\!|B |\!|_P$, if $\mathit{rel}(B)$ is defined in $P$,
1933: \item $|\!|A |\!|_P \geq |B |_R$, if $\mathit{rel}(B)$ is defined in $R$.
1934: \end{itemize}
1935: \end{itemize}
1936: Then $P\cup R$ is semi-acceptable wrt.\ $|\ |$ and $M$, where $|\ |$
1937: is defined as follows:
1938: \begin{itemize}
1939: \item[] $|A|=|A|_P + |\!|A |\!|_P$, if $\mathit{rel}(A)$ is defined in $P$,
1940: \item[] $|A|=|A|_R$, if $\mathit{rel}(A)$ is defined in $R$.
1941: \end{itemize}
1942: \end{theorem}
1943:
1944:
1945: The following remark follows from Lemma 5.4 in \cite{AP94} and
1946: Corollary 3.7 in \cite{AP94}. Together with Theorem \ref{theo:apt-modular},
1947: it implies termination of bounded queries in~\cite{AP94}.
1948:
1949:
1950: \begin{remark}
1951: If $P\cup R$ is semi-acceptable wrt.\ $|\ |$ and $M$ and $Q$ is bounded
1952: wrt.\ $|\ |$ and $M$ then all LD-derivations of $(P\cup R)\cup\{Q\}$
1953: are finite.
1954: \end{remark}
1955:
1956:
1957: We now show that
1958: whenever Theorem \ref{theo:apt-modular}
1959: can be applied to prove termination
1960: of all the queries bounded wrt.\ $|\ |$ and $M$,
1961: then also our method can be used to
1962: prove termination of the same class of queries
1963: with no need of $|\!|\ |\!|_P$ for relating the proofs of the
1964: two modules.
1965:
1966:
1967: In the following theorem for the sake of simplicity
1968: we assume that $P \sqsupset R$ is a finest
1969: decomposition of $P \cup R$. We
1970: discuss later how to
1971: extend the result to the general case.
1972:
1973:
1974:
1975:
1976: \begin{theorem}
1977: Let $P$ and $R$ be two programs such that $P$ extends $R$, and let $M$ be
1978: a model of $P\cup R$. Suppose that
1979: \begin{itemize}
1980: \item $R$ is semi-acceptable wrt.\ $|\ |_R$ and $M\cap B_R$,
1981: \item $P$ is semi-acceptable wrt.\ $|\ |_P$ and $M$,
1982: \item there exists a level mapping $|\!|\ |\!|_P$ defined as in Theorem
1983: \ref{theo:apt-modular}.
1984: \end{itemize}
1985: Let $|\ |$ be the level mapping defined by Theorem
1986: \ref{theo:apt-modular}. Moreover, suppose $P\sqsupset R$ is
1987: a finest decomposition of $P\cup R$.
1988: If $Q$ is bounded wrt.\ $|\ |$, then $Q$ is strongly bounded wrt.\
1989: $P \cup R$ and $|\ |_P$ and $|\ |_R$.
1990: \end{theorem}
1991: \begin{proof}
1992: Since we are considering a finest decomposition of
1993: $P\cup R$, by Proposition~\ref{prop:semi},
1994: $R$ is acceptable wrt.\ $|\ |_R$, while $P$ is
1995: acceptable wrt.\ $|\ |'_P$ such that
1996: if $A$ is defined in $P$ then
1997: $ |A |'_{P}=|A|_P$ else $ |A |'_{P}=0$.
1998:
1999: By Lemma \ref{lemma:semi-preservation}
2000: all LD-descendants of $(P\cup R)\cup \{Q\}$ are bounded wrt.\
2001: $|\ |$ and $M$.
2002: By definition of boundedness,
2003: for all LD-descendants $Q'$ of $(P\cup R)
2004: \cup\{Q\}$, ${\it first}(Q')$ is bounded wrt.\ $|\ |$.
2005: By definition
2006: of $|\ |$, for all atoms $A$ bounded wrt.\ $|\ |$ we have that:
2007: if $A$ is defined in $R$ then $A$ is bounded wrt.\ $|\ |_R$,
2008: while if $A$ is defined in $P$ then $A$ is bounded wrt.\ $|\ |_P$
2009: and hence wrt.\ $|\ |'_P$ (since $|A |'_P =|A |_P$).
2010: Hence the thesis follows.
2011: \end{proof}
2012: \medskip
2013:
2014: If the hierarchy $P \sqsupset R$ is not
2015: a finest one and
2016: $|\ |_{P}$ and $|\ |_{R}$ are the level mappings
2017: corresponding to $P$ and $R$ respectively,
2018: then we can decompose $P$
2019: into a finest decomposition, $P:= P_n\sqsupset \ldots \sqsupset P_1$ ,
2020: and consider instead
2021: of $|\ |_{P}$ the derived level
2022: mappings $|\ |_{P_i}$ defined in the following way:
2023: if $A$ is defined in $P_i$ then
2024: $ |A |_{P_i}=|A|_{P}$ else $ |A |_{P_i}=0$.
2025: Similarly we can decompose $R:= R_n\sqsupset \ldots \sqsupset R_1$
2026: and define the corresponding level mappings.
2027: The derived level mappings
2028: satisfy all the properties we need for proving that
2029: if $Q$ is bounded wrt.\ $|\ |$, then $Q$ is strongly bounded wrt.\
2030: $P \cup R$ and $|\ |_{P_1}, \ldots,|\ |_{P_n},
2031: |\ |_{R_1}, \ldots,|\ |_{R_n} $.\\
2032:
2033:
2034: To complete the comparison with \cite{AP94},
2035: we can observe that
2036: our method is applicable also for proving termination
2037: of queries in modular programs
2038: which are not (semi-)acceptable.
2039: Such programs clearly cannot be
2040: dealt with Apt and Pedreschi's method.
2041: The program of Example \ref{exa:iterative-method2}
2042: is a non-acceptable program for which we proved
2043: termination of all well-typed queries by applying
2044: Corollary \ref{theo:R-typed-terminating}.
2045: The following is a simple example of a non-acceptable
2046: program to which we can apply
2047: the general Theorem \ref{theo:strongn}.
2048:
2049:
2050: \begin{example}
2051: \label{exa:more-programs}
2052:
2053: Let $R$ be the following trivial program:
2054:
2055: \begin{program2}
2056: \> r1: \> q(0).\\
2057: \> r2: \> q(s(Y)) \la q(Y).
2058: \end{program2}
2059:
2060: The program $R$ is acceptable wrt.\ the following
2061: natural level mapping $|\ |_R$ and any model $M$:
2062:
2063: \begin{program}
2064: \> \(\mathtt{|q(\mathit{t})|}_R = \mathtt{|\mathit{t}|}_{size}\).
2065: \end{program}
2066:
2067: Let $P$ be a program, which extends $R$, defined as follows:
2068:
2069: \begin{program2}
2070: \> p1: \> r(0,0).\\
2071: \> p2: \> r(s(X),Y).\\
2072: \> p3: \> p(X) \la r(X,Y), q(Y).
2073: \end{program2}
2074:
2075: The program $P$ is acceptable wrt.\ the following
2076: trivial level mapping $|\ |_P$ and any model $M$:
2077:
2078: \begin{program}
2079: \> \(\mathtt{|q(\mathit{y})|}_P = 0\),\\
2080: \> \(\mathtt{|r(\mathit{x},\mathit{y})|}_P = 0\),\\
2081: \> \(\mathtt{|p(\mathit{x})|}_P = 1\).
2082: \end{program}
2083:
2084: Note that, even if each module is acceptable,
2085: $P\cup R$ cannot be acceptable wrt.\ any level mapping
2086: and model. In fact $P\cup R $ is not left-terminating: for example
2087: it does not terminate for the ground query \texttt{p(s(0))}.
2088: As a consequence Apt and Pedreschi's method
2089: does not apply to $P\cup R$.
2090: On the other hand, there are ground queries,
2091: such as \texttt{p(0)}, which terminate in $P\cup R$.
2092: We can prove it as follows.
2093:
2094:
2095: \begin{itemize}
2096: \item
2097: By Theorem \ref{theo:strongn},
2098: for all strongly bounded queries $Q$ wrt.\ $P \cup R$ and
2099: $|\ |_R$, $|\ |_P$,
2100: all LD-derivations of $(P\cup R)\cup\{Q\}$ are finite.
2101: \item
2102: \texttt{p(0)} is strongly bounded wrt.\ $P \cup R$ and
2103: $|\ |_R$, $|\ |_P$.
2104: In fact, $\mathit{Call}_{(P\cup R)}(\texttt{p(0)})
2105: =\{\texttt{p(0)}, \texttt{r(0,Y)}, \texttt{q(0)}\}$
2106: and all these atoms are bounded wrt.\ their corresponding level mapping.
2107: \end{itemize}
2108: \end{example}
2109:
2110:
2111:
2112:
2113: %%%%%%%%%%%%%%%%
2114: \section{Conclusions}
2115: \label{conclusion}
2116: %%%%%%%%%%%%%%%%
2117:
2118: In this paper we propose a modular approach
2119: to termination proofs of general programs
2120: by following the proof style introduced by Apt and Pedreschi.
2121: Our technique allows one to give simple proofs
2122: in hierarchically structured programs,
2123: namely programs which can be partitioned into $n$ modules,
2124: $R_1\cup \ldots \cup R_n$,
2125: such that for all $i \in \{1,\ldots,n-1\}$,
2126: $ R_{i+1}$ extends
2127: $R_1\cup \ldots \cup R_{i}$.
2128:
2129: We supply the general Theorem \ref{theo:generale-sulle-classi}
2130: which can be iteratively applied
2131: to a hierarchy of two programs and a class of queries
2132: enjoying persistence properties through LDNF-resolution.
2133: We then use such a result to deal with a general hierarchy of
2134: acceptable programs, by introducing an extension of the
2135: concept of boundedness for hierarchical programs, namely
2136: strong boundedness.
2137: Strong boundedness is a property on queries which can be easily
2138: ensured for hierarchies of programs behaving well, such as
2139: well-moded or well-typed programs. We show how specific and simple
2140: hierarchical termination proofs can be derived for such classes of
2141: programs and queries.
2142: We believe this is a valuable proof technique since realistic programs are
2143: typically well-moded and well-typed.
2144:
2145:
2146:
2147: The simplifications in the termination proof derive from the fact
2148: that for proving the termination of a modular program,
2149: we simply prove acceptability of each module by
2150: choosing a level mapping which focuses
2151: only on the predicates defined in it,
2152: with no concern of the module context.
2153: Generally this can be done by using very simple
2154: and natural level mappings which are completely independent
2155: from one module to another.
2156: A complicated level mapping is generally required when
2157: we prove the termination of a program as a whole
2158: and we have to consider a level mapping which appropriately
2159: relates all the predicates defined in the program.
2160: Hence the finer the modularization of the program
2161: the simpler the level mappings.
2162: Obviously we cannot completely ignore how predicates defined in
2163: different modules relate to each other.
2164: On one hand, when we prove acceptability for each module,
2165: we consider a model for the whole program.
2166: This guarantees the compatibility among the definitions
2167: in the hierarchy.
2168: On the other hand, for queries we use the notion of strong boundedness.
2169: The intuition is that we consider only what may influence the evaluation
2170: of queries in the considered class.
2171:
2172: The proof method of Theorem \ref{theo:generale-sulle-classi}
2173: can be applied also to programs which are not
2174: acceptable. In fact, the condition on the
2175: lower module is just that it terminates on all the queries in
2176: the considered class and not on all ground queries as required
2177: for acceptable programs. From Theorem \ref{theo:generale-sulle-classi}
2178: we could also derive a method to deal with
2179: pre-compiled modules (or even modules written in a different language)
2180: provided that we already know termination properties
2181: and we have a complete specification.
2182:
2183: For sake of simplicity, in the first part of the paper we consider the
2184: notion of acceptability
2185: instead of the less requiring notion of
2186: semi-acceptability.
2187: This choice makes proofs of our results much simpler.
2188: On the other hand, as we show in Section \ref{sec:comparisons},
2189: our results can be applied also to hierarchies
2190: of semi-acceptable programs.
2191:
2192:
2193: We have compared our proposal with
2194: the one in \cite{AP94}.
2195: They propose a modular approach
2196: to left-termination proofs in a hierarchy of two definite programs
2197: $P \sqsupset R$.
2198: They require both the (semi)-acceptability of the two modules $R$ and $P$
2199: wrt.\ their respective level mappings and
2200: a condition relating the two level mappings
2201: which is meant to connect the two termination proofs.
2202:
2203: Our method is more powerful both because we consider also general
2204: programs and because we capture definite programs and
2205: queries which cannot be treated by the method developed in \cite{AP94}.
2206: In fact there are
2207: non-acceptable programs for which we can single out
2208: a class of terminating queries.
2209:
2210: For the previous reasons our method improves also with respect to
2211: \cite{PR96,PR99} where
2212: hierarchies of modules are considered. In \cite{PR96,PR99} a
2213: unifying framework for the verification of total correctness
2214: of logic programs is provided. The authors consider modular termination
2215: by following the approach in \cite{AP94}.
2216:
2217: In \cite{Mar96} a methodology for proving termination of
2218: general logic programs is proposed which is based on
2219: modularization.
2220: In this approach, the {\em acyclic} modules, namely
2221: modules that terminate independently from
2222: the selection rule, play a distinctive
2223: role. For such modules, the termination proof
2224: does not require a model. In combination with
2225: appropriate notions of {\em up-acceptability} and {\em low-acceptability}
2226: for the modules which are not acyclic,
2227: this provides a practical technique for proving termination of the
2228: whole program.
2229: Analogously to \cite{AP94},
2230: also in \cite{Mar96} a relation between
2231: the level mappings of all modules is required.
2232: It is interesting to note that the idea
2233: of exploiting acyclicity is completely orthogonal
2234: to our approach: we could integrate it into our framework.
2235:
2236: Another related work is \cite{DDV99}, even if it does not
2237: aim explicitly at modularity.
2238: In fact they propose a technique for automatic
2239: termination analysis of definite programs which is highly efficient
2240: also because they use a rather operational notion
2241: of acceptability with respect to a set of queries,
2242: where decreasing levels are required only on (mutually)
2243: recursive calls as in \cite{DVB92}. Effectively, this
2244: corresponds to considering a finest decomposition of
2245: the program and having independent level mappings
2246: for each module. However, their notion of acceptability
2247: is defined and verified on call-patterns
2248: instead of program clauses.
2249: In a sense, such an acceptability with respect to a set
2250: of queries combines the
2251: concepts of strongly boundedness and (standard) acceptability.
2252: They start from a class of queries and try to derive automatically a
2253: termination proof for such a class, while we start from
2254: the program and derive
2255: a class of queries for which it terminates.
2256:
2257: In \cite{VSD99} termination in the context of tabled execution is
2258: considered. Also in this case modular results are inspired by
2259: \cite{DVB92}
2260: by adapting the notion of acceptability wrt. call-patterns
2261: to tabled executions. This work is further developed
2262: in \cite{VSD01} where their modular termination conditions
2263: are refined following the approach by \cite{AP94}.
2264:
2265: In \cite{EBC99} a method for modular termination proofs for well-moded
2266: definite programs is proposed.
2267: Our present work generalizes such
2268: result to general programs.
2269:
2270: Our method may help in designing more powerful automatic
2271: systems for veri\-fying termination \cite{DVB92,SSS97,DDV99,CT99}.
2272: We see two directions which could be pursued for a
2273: fruitful integration with existing automatic tools.
2274: The first one exploits the fact that in each single module
2275: it is sufficient to synthesize a level mapping which
2276: does not need to measure atoms defined in other modules.
2277: The second one concerns tools based on call-patterns analysis
2278: \cite{DVB92,GG94,CD95}.
2279: They can take advantage of the concept of strong boundedness which, as we
2280: show, can be implied by well-behavior of programs \cite{DW88,Deb89}.
2281:
2282: %%%%%%%%%%%%%%%%%%%%%%%%%%%%
2283: \paragraph{Acknowledgements.}
2284: %%%%%%%%%%%%%%%%%%%%%%%%%%%%
2285: This work has been partially supported by
2286: MURST with the National Research Project
2287: ``Certificazione automatica di programmi mediante interpretazione astratta''.
2288:
2289: \bibliographystyle{dcu}
2290: \bibliography{BCER}
2291:
2292: \end{document}
2293:
2294: