text:
# Properties of Input-Consuming Derivations

## 1 Introduction

Most of the recent logic programming languages provide the possibility of employing *dynamic scheduling*, i.e., a runtime mechanism determining which atoms in a query are *selectable* and which ones are not. In fact, dynamic scheduling has proven to be useful in a number of applications; among other things, it allows one to model coroutining, as shown in \[Nai92, HL94\], and parallel executions, as shown in \[Nai88\].

Let us use the following simple examples to show how dynamic scheduling can be enforced by using *delay declarations* and how it can prevent nontermination and unnecessary computations. Consider the program APPEND

| app(\[ \],Ys,Ys). |
| --- |
| app(\[H|Xs\],Ys,\[H|Zs\]) $``$app(Xs,Ys,Zs). |

together with the query

| $`Q_1:=`$ | app(Xs,,Ys), app(,,Xs). |
| --- | --- |

In this query, if we select and resolve the leftmost atom, we could easily have to face one of the following two problems. First, the possibility of nontermination: This is the case if we repeatedly resolve the leftmost atom against the second clause. The second problem is that of inefficiency. If, for instance, in $`Q_1`$ we resolve the leftmost atom against the first clause, we obtain the query app(,,\[ \]). This will eventually fail, yielding to (unnecessary) backtracking. Notice that if one employs the rightmost selection rule, $`Q_1`$ would terminate with success and without backtracking. Basically, the problem when selecting app(Xs,,Ys), is that we do not know which clause we should use for resolving it, and the only practical way for getting to know this is by waiting until the outermost functor of Xs is known: If it is the empty list \[ \] we know that we should use the first clause, if it is the list-constructor symbol we know that we should use the second clause, if it is something else again, we know then that the query *fails*. Notice that the same problems arise for the query

| $`Q_2:=`$ | app(,,Xs), app(Xs,,Ys). |
| --- | --- |

if the rightmost selection rule is considered.

This shows the usefulness of a mechanism for preventing the selection of those atoms which are not sufficiently instantiated. Such a mechanism is in fact offered by most modern languages: In GHC \[Ued88\] programs are augmented with *guards* in order to control the selection of atoms dynamically. Moded Flat GHC \[UM94\] uses an extra condition on the input positions, which is extremely similar to the concept of input-consuming derivation step we refer to the sequel: The resolution of an atom with a definition must not instantiate the input arguments of the resolved atom. On the other hand, Gödel \[HL94\] and ECLiPSe \[WNS97\] use *delay declarations*, and SICStus Prolog \[SIC97\] employs block declarations (which are a special kind of delay declarations). Both delay and block declarations check the partial instantiation of some arguments of calls. For instance, the standard delay declaration for APPEND is

| $`d_1:=`$ | delay app(Ls, \_, \_) until nonvar(Ls). |
| --- | --- |

This declaration forbids the selection of an atom of the form $`\text{app}(s,t,u)`$ unless $`s`$ is a non-variable term, which is precisely what we need in order to run the queries $`Q_1`$ or $`Q_2`$ efficiently.

The adoption of dynamic scheduling has the disadvantage that various program properties that have been proven for logic and pure Prolog programs do not apply any longer.

The goal of our research is the study of termination properties. This is motivated by the fact that most of the literature on termination of logic programs (see De Schreye and Decorte \[DD94\] for a survey on this subject) assumes the standard Prolog selection rule, i.e., the leftmost one. Notable exceptions are Bezem \[Bez93\] and Cavedon \[Cav89\] who provide results for all selection rules. There are only few authors who tackled the specific problem of verifying the termination of logic programs with dynamic scheduling. Namely, Apt and Luitjes \[AL95\], Marchiori and Teusink \[MT95\] and Smaus \[Sma99b\]. We compare our results with the ones in \[AL95, MT95, Sma99b\] in the concluding section.

Another feature of logic programs which does not hold in presence of dynamic scheduling is the well-known *switching lemma*, which is, for instance, at the base of the result on the independence of the selection rule. In this paper we show that – under certain conditions – a weak form of the well-known switching lemma holds.

In order to recuperate at least part of the declarative reading of logic programming, we follow here the same approach to dynamic scheduling as \[Sma99b\] and we substitute the use of delay declarations by the restriction to *input-consuming* derivations. The definition of input-consuming derivation is done in two phases. First we give the program a *mode*, that is, we partition the positions of each atom into *input* and *output* positions. Then, in presence of modes, *input-consuming* derivation steps are precisely those in which the input arguments of the selected atom will not be instantiated by the unification with the clause’s head. If in a query no atom is resolvable via an input-consuming derivation step and a failure does not arise then we have a *deadlock* situation111As we discuss in Section 3.2, this notion of deadlock differs, in some way, from the usual one, which is given in the case of programs employing delay declarations..

For example, the standard mode for the program APPEND reported above, when used for concatenating two lists, is app(In,In,Out). Notice that in this case the delay declaration $`d_1`$ serves precisely the purpose of guaranteeing that if an atom of the form $`\mathrm{𝚊𝚙𝚙}(s,t,X)`$ (with $`X`$ being a variable) is selectable and unifiable with a clause head, then the resulting derivation step is input-consuming.

It is also worth remarking that, as a large body of literature shows, the vast majority of “usual” programs are actually moded and are, in a well-defined sense consistent wrt. to their modes (e.g., well-moded, nicely-moded, simply-moded, etc.); see for example \[AP94b, AM94\], or more simply, the tables of programs we report in Section 7, or consider for instance the logic programming language Mercury \[SHC96\], which requires that its programs are moded (and well-moded).

### Contributions of this paper

In this paper we study some properties of input-consuming derivations.

In the first place we show that, if we restrict ourselves to programs and queries which are nicely-moded, then a weak form of the well-known switching lemma holds.

Furthermore, we study the termination properties of input-consuming derivations. For this we define the class of *input terminating* programs which characterizes programs whose input-consuming derivations starting in a nicely-moded query are finite. In order to prove that a program is input terminating, we use the concept of *quasi recurrent* program (similar to, but noticeably less restrictive than the concept of semi-recurrent program introduced in \[AP94a\]). We show that if $`P`$ is nicely-moded and quasi recurrent then all its input-consuming derivations starting from a nicely-moded query terminate.

Furthermore, we demonstrate that under mild additional constraints (namely, simply-modedness and input-recurrency) the above condition is both sufficient and *necessary* for ensuring that all input-consuming derivations starting from a nicely-moded query terminate.

This approach generalizes the method described in \[Sma99b\] in two ways: First because we also provide conditions which are both necessary and sufficient, and secondly because we do not require programs and queries to be well-moded; we only assume that they are nicely-moded. This is actually crucial: When programs and queries are well-moded, derivations cannot *deadlock*. Thus, as opposed to \[Sma99b\], our results capture also termination by deadlock. For instance, we can easily prove that the query $`\mathrm{𝚊𝚙𝚙}(X,Y,Z)`$ terminates. A more detailed comparison is presented in the concluding section.

We also show that the results presented in this paper can be extended to programs and queries which are *permutation* nicely- or simply-moded, \[SHK98\].

To evaluate the practicality of the results we present, we consider the programs from various well-known collections, and we check whether they satisfy the conditions of our main theorem.

The paper is organized as follows. Section 2 contains some preliminary notations and definitions. In Section 3 input-consuming derivations are introduced and some properties of them are proven. In Section 4 we prove that, for nicely-moded input-consuming programs, a left switching lemma holds. In Section 5 a method for proving input termination of programs is presented, first in a non-modular way, then for modular programs. In Section 6 we show that this method is necessary for the class of simply-moded and input-recursive programs. Section 7 discusses the applicability of our results through simple examples of programs and reports the results obtained by applying our method to various benchmarks. Finally, Section 8 concludes the paper.

## 2 Preliminaries

The reader is assumed to be familiar with the terminology and the basic results of logic programs \[Apt90, Apt97, Llo87\].

### 2.1 Terms and Substitutions

Let $`𝒯`$ be the set of terms built on a finite set of *data constructors* $`𝒞`$ and a denumerable set of *variable symbols* $`𝒱`$. A *substitution* $`\theta `$ is a mapping from $`𝒱`$ to $`𝒯`$ such that $`\mathrm{𝐷𝑜𝑚}(\theta )=\{X|\theta (X)X\}`$ is finite. For any syntactic object $`o`$, we denote by $`\mathrm{𝑉𝑎𝑟}(o)`$ the set of variables occurring in $`o`$. A syntactic object is linear if every variable occurs in it at most once. We denote by $`ϵ`$ the empty substitution. The *composition* $`\theta \sigma `$ of the substitutions $`\theta `$ and $`\sigma `$ is defined as the functional composition, i.e., $`\theta \sigma (X)=\sigma (\theta (X))`$. We consider the pre-ordering $``$ (more general than) on substitutions such that $`\theta \sigma `$ iff there exists $`\gamma `$ such that $`\theta \gamma =\sigma `$. The result of the application of a substitution $`\theta `$ to a term $`t`$ is said an *instance* of $`t`$ and it is denoted by $`t\theta `$. We also consider the pre-ordering $``$ (more general than) on terms such that $`tt^{}`$ iff there exists $`\theta `$ such that $`t\theta =t^{}`$. We denote by $``$ the associated equivalence relation (variance). A substitution $`\theta `$ is a *unifier* of terms $`t`$ and $`t^{}`$ iff $`t\theta =t^{}\theta `$. We denote by $`\text{mgu}(t,t^{})`$ any *most general unifier* (*mgu*, in short) of $`t`$ and $`t^{}`$. An mgu $`\theta `$ of terms $`t`$ and $`t^{}`$ is called relevant iff $`\mathrm{𝑉𝑎𝑟}(\theta )\mathrm{𝑉𝑎𝑟}(t)\mathrm{𝑉𝑎𝑟}(t^{})`$.

### 2.2 Programs and Derivations

Let $`𝒫`$ be a finite set of *predicate symbols*. An *atom* is an object of the form $`p(t_1,\mathrm{},t_n)`$ where $`p𝒫`$ is an $`n`$-ary predicate symbol and $`t_1,\mathrm{},t_n𝒯`$. Given an atom $`A`$, we denote by $`\mathrm{𝑅𝑒𝑙}(A)`$ the predicate symbol of $`A`$. A *query* is a finite, possibly empty, sequence of atoms $`A_1,\mathrm{},A_m`$. The empty query is denoted by $`\mathrm{}`$. Following the convention adopted in \[Apt97\], we use bold characters to denote queries. A *clause* is a formula $`H𝐁`$ where $`H`$ is an atom (the *head*) and $`𝐁`$ is a query (the *body*). When $`𝐁`$ is empty, $`H𝐁`$ is written $`H`$ and is called a *unit clause*. A *program* is a finite set of clauses. We denote atoms by $`A,B,H,\mathrm{},`$ queries by $`Q,𝐀,𝐁,𝐂,\mathrm{},`$ clauses by $`c,d,\mathrm{},`$ and programs by $`P`$.

Computations are constructed as sequences of “basic” steps. Consider a non-empty query $`𝐀,B,𝐂`$ and a clause $`c`$. Let $`H𝐁`$ be a variant of $`c`$ variable disjoint from $`𝐀,B,𝐂`$. Let $`B`$ and $`H`$ unify with mgu $`\theta `$. The query $`(𝐀,𝐁,𝐂)\theta `$ is called a *resolvent of* $`𝐀,B,𝐂`$ *and* $`c`$ *with selected atom* $`B`$ *and mgu* $`\theta `$. A *derivation step* is denoted by

$$𝐀,B,𝐂\underset{P,c}{\overset{\theta }{}}(𝐀,𝐁,𝐂)\theta $$

The clause $`H𝐁`$ is called its *input clause*. The atom $`B`$ is called the *selected atom* of $`𝐀,B,𝐂`$.

If $`P`$ is clear from the context or $`c`$ is irrelevant then we drop the reference to them. A derivation is obtained by iterating derivation steps. A maximal sequence

$$\delta :=Q_0\underset{P,c_1}{\overset{\theta _1}{}}Q_1\underset{P,c_2}{\overset{\theta _2}{}}\mathrm{}Q_n\underset{P,c_{n+1}}{\overset{\theta _{n+1}}{}}Q_{n+1}\mathrm{}$$

is called a *derivation of $`P\{Q_0\}`$* provided that for every step the standardization apart condition holds, i.e., the input clause employed is variable disjoint from the initial query $`Q_0`$ and from the substitutions and the input clauses used at earlier steps.

Derivations can be finite or infinite. If $`\delta :=Q_0\underset{P,c_1}{\overset{\theta _1}{}}\mathrm{}\underset{P,c_n}{\overset{\theta _n}{}}Q_n`$ is a finite prefix of a derivation, also denoted $`\delta :=Q_0\stackrel{\theta }{}Q_n`$ with $`\theta =\theta _1\mathrm{}\theta _n`$, we say that $`\delta `$ is a *partial derivation* and $`\theta `$ is a *partial computed answer substitution* of $`P\{Q_0\}`$. If $`\delta `$ is maximal and ends with the empty query then $`\theta `$ is called *computed answer substitution* (*c.a.s.*, for short). The length of a (partial) derivation $`\delta `$, denoted by $`\mathrm{𝑙𝑒𝑛}(\delta )`$, is the number of derivation steps in $`\delta `$.

The following definition of $`𝐁`$-step is due to Smaus \[Sma99a\].

###### Definition 1 (B-step)

Let $`𝐀,B,𝐂\stackrel{\theta }{}(𝐀,𝐁,𝐂)\theta `$ be a derivation step. We say that each atom in $`𝐁\theta `$ is a *direct descendant of B*, and for each atom $`E`$ in $`(𝐀,𝐂)`$, $`E\theta `$ is a *direct descendant of E*. We say that $`E`$ is a descendant of $`F`$ if the pair $`(E,F)`$ is in the reflexive, transitive closure of the relation *is a direct descendant of*. Consider a derivation $`Q_0\stackrel{\theta _1}{}\mathrm{}\stackrel{\theta _i}{}Q_i\mathrm{}\stackrel{\theta _j}{}Q_j\stackrel{\theta _{j+1}}{}Q_{j+1}\mathrm{}`$. We say that $`Q_j\stackrel{\theta _{j+1}}{}Q_{j+1}\mathrm{}`$ is a $`𝐁`$-step if $`𝐁`$ is a subquery of $`Q_i`$ and the selected atom in $`Q_j`$ is a descendant of an atom in $`𝐁`$.

## 3 Modes and Input-Consuming Derivations

In this section we introduce the concept of input-consuming derivation which is strictly related to the notion of mode; we discuss the relations between input-consuming derivations and programs using delay declarations; we recall the notion of nicely-moded program and state some properties.

### 3.1 Input-Consuming Derivations

Let us first recall the notion of mode. A *mode* is a function that labels as *input* or *output* the positions of each predicate in order to indicate how the arguments of a predicate should be used.

###### Definition 2 (Mode)

Consider an $`n`$-ary predicate symbol $`p`$. A *mode* for $`p`$ is a function $`m_p`$ from $`\{1,\mathrm{},n\}`$ to $`\{\mathrm{𝐼𝑛},\mathrm{𝑂𝑢𝑡}\}`$.

If $`m_p(i)=\mathrm{𝐼𝑛}`$ (resp. *Out*), we say that $`i`$ is an $`\mathrm{𝑖𝑛𝑝𝑢𝑡}`$ (resp. *output*) *position of* $`p`$ (wrt. $`m_p`$). We assume that each predicate symbol has a unique mode associated to it; multiple modes may be obtained by simply renaming the predicates.

If $`Q`$ is a query, we denote by $`\mathrm{𝐼𝑛}(Q)`$ (resp. $`\mathrm{𝑂𝑢𝑡}(Q)`$) the sequence of terms filling in the input (resp. output) positions of predicates in $`Q`$. Moreover, when writing an atom as $`p(𝐬,𝐭)`$, we are indicating with $`𝐬`$ the sequence of terms filling in the input positions of $`p`$ and with $`𝐭`$ the sequence of terms filling in the output positions of $`p`$.

The notion of input-consuming derivation was introduced in \[Sma99b\] and is defined as follows.

###### Definition 3 (Input-Consuming)

* An atom $`p(𝐬,𝐭)`$ is called *input-consuming resolvable wrt. a clause $`c:=p(𝐮,𝐯)Q`$ and a substitution $`\theta `$* iff $`\theta =\mathrm{𝑚𝑔𝑢}(p(𝐬,𝐭),p(𝐮,𝐯))`$ and $`𝐬=𝐬\theta `$.
* A derivation step

$$𝐀,B,𝐂\underset{c}{\overset{\theta }{}}(𝐀,𝐁,𝐂)\theta $$

is called *input-consuming* iff the selected atom $`B`$ is input-consuming resolvable wrt. the input clause $`c`$ and the substitution $`\theta `$.
* A derivation is called *input-consuming* iff all its derivation steps are input-consuming.

The following lemma states that we are allowed to restrict our attention to input-consuming derivations with relevant mgu’s.

###### Lemma 4

Let $`p(𝐬,𝐭)`$ and $`p(𝐮,𝐯)`$ be two atoms. If there exists an mgu $`\theta `$ of $`p(𝐬,𝐭)`$ and $`p(𝐮,𝐯)`$ such that $`𝐬\theta =𝐬`$, then there exists a *relevant* mgu $`\vartheta `$ of $`p(𝐬,𝐭)`$ and $`p(𝐮,𝐯)`$ such that $`𝐬\vartheta =𝐬`$.

Proof. Since $`p(𝐬,𝐭)`$ and $`p(𝐮,𝐯)`$ are unifiable, there exists a relevant mgu $`\theta _{\mathrm{𝑟𝑒𝑙}}`$ of them (cfr. \[Apt97\], Theorem 2.16). Now, $`\theta _{\mathrm{𝑟𝑒𝑙}}`$ is a renaming of $`\theta `$. Thus $`𝐬\theta _{\mathrm{𝑟𝑒𝑙}}`$ is a variant of $`𝐬`$. Then there exists a renaming $`\rho `$ such that $`\mathrm{𝐷𝑜𝑚}(\rho )\mathrm{𝑉𝑎𝑟}(𝐬,𝐭,𝐮,𝐯)`$ and $`𝐬\theta _{\mathrm{𝑟𝑒𝑙}}\rho =𝐬`$. Now, take $`\vartheta =\theta _{\mathrm{𝑟𝑒𝑙}}\rho `$. $`\mathrm{}`$

From now on, we assume that all mgu’s used in the input-consuming derivation steps are relevant.

###### Example 5

Consider the program REVERSE with accumulator in the modes defined below.

| mode reverse(In, Out). |
| --- |
| mode reverse\_acc(In,Out,In) |
| reverse(Xs,Ys) $``$reverse\_acc(Xs,Ys,\[ \]). |
| reverse\_acc(\[ \],Ys,Ys). |
| reverse\_acc(\[X|Xs\],Ys,Zs) $``$reverse\_acc(Xs,Ys,\[X|Zs\]). |

The derivation $`\delta `$ of $`\mathrm{𝚁𝙴𝚅𝙴𝚁𝚂𝙴}\{\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}([\mathrm{𝚇𝟷},\mathrm{𝚇𝟸}],\mathrm{𝚉𝚜})\}`$ depicted below is input-consuming.

| $`\delta :=`$ | $`\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}([\mathrm{𝚇𝟷},\mathrm{𝚇𝟸}],\mathrm{𝚉𝚜})\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}\mathrm{\_}\mathrm{𝚊𝚌𝚌}([\mathrm{𝚇𝟷},\mathrm{𝚇𝟸}],\mathrm{𝚉𝚜},[])`$ |
| --- | --- |
|  | $`\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}\mathrm{\_}\mathrm{𝚊𝚌𝚌}([\mathrm{𝚇𝟸}],\mathrm{𝚉𝚜},[\mathrm{𝚇𝟷}])\mathrm{𝚛𝚎𝚟𝚎𝚛𝚜𝚎}\mathrm{\_}\mathrm{𝚊𝚌𝚌}([],\mathrm{𝚉𝚜},[\mathrm{𝚇𝟸},\mathrm{𝚇𝟷}])\mathrm{}`$. |

### 3.2 Input-Consuming vs. Delay Declarations

Delay declarations are by far the most popular mechanism for implementing dynamic scheduling. However, being a non-logical mechanism, they are difficult to model and there are few proposals concerning their semantics \[Mar97\] and \[FGMP97\].

An alternative approach to dynamic scheduling, which is much more declarative in nature, has been proposed by Smaus \[Sma99b\]. It consists in the use of input-consuming derivations.

There is a main difference between the concept of delay declaration and the one of input-consuming derivation: While in the first case only the atom selectability is controlled, in the second one both the atom and the clause selectability are affected. In fact, in presence of delay declarations, if an atom is selectable then it can be resolved with respect to any program clause (provided it unifies with its head); on the contrary, in an input-consuming derivation, if an atom is selectable then it is input-consuming resolvable wrt. some, but not necessarily all, program clauses, i.e, only a restricted class of clauses can be used for resolution.

Also the concept of *deadlock* has to be understood in two different ways. For programs using delay declarations a deadlock situation occurs when no atom in a query satisfies the delay declarations (i.e., no atom is selectable), while for input-consuming derivations a deadlock occurs when no atom in a query is resolvable via an input-consuming derivation step and the derivation does not fail, i.e., there is some atom in the query which unifies with a clause head but the unification is not input-consuming.

In spite of these differences, in many situations there is a strict relation between programs using delay declarations and input-consuming derivations. This relation is studied by Smaus in his PhD thesis \[Sma99a\]. More precisely, Smaus proves a result that relates block declarations and input-consuming derivations. A block declaration is a special case of delay declaration and it is used to declare that certain arguments of an atom must be *non-variable* when the atom is selected for resolution. In Chapter 7 of \[Sma99a\], Smaus shows that block declarations can be used to ensure that derivations are input-consuming. In force of this result and of practical experience, we might claim that in most “usual” moded programs using them, delay declarations are employed precisely for ensuring the input-consumedness of the derivations.

In fact, delay declarations are generally employed to guarantee that the interpreter will not use an “inappropriate” clause for resolving an atom (the other, perhaps less prominent, use of delay declarations is to ensure absence of runtime errors, but we do not address this issue in this paper). This is achieved by preventing the selection of an atom until a certain degree of instantiation is reached. This degree of instantiation ensures then that the atom is unifiable only with the heads of the “appropriate” clauses. In presence of modes, we can reasonably assume that this degree of instantiation is the one of the *input* positions, which are the ones carrying the information. Now, it is easy to see that a derivation step involving a clause $`c`$ is input-consuming iff no further instantiation of the input positions of the resolved atom could prevent it from being resolvable with $`c`$. Therefore $`c`$ must belong to the set of “appropriate” clauses for resolving it. Thus, the concepts of input-consuming derivation and of delay declarations are often employed for ensuring the same properties.

### 3.3 Nicely-Moded Programs

In the sequel of the paper we will restrict ourselves to programs and queries which are nicely-moded. In this section we report the definition of this concept together with some basic important properties of nicely-moded programs.

###### Definition 6 (Nicely-Moded)

* A query $`Q:=p_1(𝐬_1,𝐭_1),\mathrm{},p_n(𝐬_n,𝐭_n)`$ is *nicely-moded* if $`𝐭_1,\mathrm{},𝐭_n`$ is a linear sequence of terms and for all $`i\{1,\mathrm{},n\}`$

$$\mathrm{𝑉𝑎𝑟}(𝐬_i)\underset{j=i}{\overset{n}{}}\mathrm{𝑉𝑎𝑟}(𝐭_j)=\mathrm{}.$$
* A clause $`c=p(𝐬_0,𝐭_0)Q`$ is *nicely-moded* if $`Q`$ is nicely-moded and

$$\mathrm{𝑉𝑎𝑟}(𝐬_0)\underset{j=1}{\overset{n}{}}\mathrm{𝑉𝑎𝑟}(𝐭_j)=\mathrm{}.$$

In particular, every unit clause is nicely-moded.
* A program $`P`$ is nicely-moded if all of its clauses are nicely-moded.

Note that a one-atom query $`p(𝐬,𝐭)`$ is nicely-moded if and only if $`𝐭`$ is linear and $`\mathrm{𝑉𝑎𝑟}(𝐬)\mathrm{𝑉𝑎𝑟}(𝐭)=\mathrm{}`$.

###### Example 7

* The program APPEND in the modes app(In,In,Out) is nicely-moded.
* The program REVERSE with accumulator in the modes depicted in Example 5 is nicely-moded.
* The following program MERGE is nicely-moded.

| mode merge(In,In,Out). |
| --- |
| merge(Xs,\[ \],Xs). |
| merge(\[ \],Xs,Xs). |
| merge(\[X|Xs\],\[Y|Ys\],\[Y|Zs\]) $``$Y \< X, merge(\[X|Xs\],Ys,Zs). |
| merge(\[X|Xs\],\[Y|Ys\],\[X|Zs\]) $``$Y \> X, merge(Xs,\[Y|Ys\],Zs). |
| merge(\[X|Xs\],\[X|Ys\],\[X|Zs\]) $``$merge(Xs,\[X|Ys\],Zs). |

The following result is due to Smaus \[Sma99a\], and states that the class of programs and queries we are considering is persistent under resolution.

###### Lemma 8

Every resolvent of a nicely-moded query $`Q`$ and a nicely-moded clause $`c`$, where the derivation step is input-consuming and $`\mathrm{𝑉𝑎𝑟}(Q)\mathrm{𝑉𝑎𝑟}(c)=\mathrm{}`$, is nicely-moded.

The following Remark, also in \[Sma99a\], is an immediate consequence of the definition of input-consuming derivation step and the fact that the mgu’s we consider are relevant.

###### Remark 9

Let the program $`P`$ and the query $`Q:=𝐀,p(𝐬,𝐭),𝐂`$ be nicely-moded.
If $`𝐀,p(𝐬,𝐭),𝐂\stackrel{\theta }{}(𝐀,𝐁,𝐂)\theta `$ is an input-consuming derivation step with selected atom $`p(𝐬,𝐭)`$, then $`𝐀\theta =𝐀`$.

## 4 The Left Switching Lemma

The *switching lemma* (see for instance \[Apt97\], Lemma 3.32) is a well-known result which allows one to prove the independence of the computed answer substitutions from the selection rule.

In the case of logic programs using dynamic scheduling, the switching lemma does not hold any longer. For example, in program APPEND reported in the introduction (together with the delay declaration $`d_1`$) we have that the rightmost atom of $`Q_2`$ is selectable only after the leftmost one has been resolved; i.e., the switching lemma cannot be applied.

Nevertheless we can show that, for input-consuming derivations of nicely-moded programs, a weak version of the switching lemma still holds. Intuitively, we show that we can switch the selection of two atoms whenever this results in a left to right selection. For this reason, we call it *left switching lemma*.

First, we need one technical result, stating that the only variables of a query that can be “affected” in an input-consuming derivation process are those occurring in some output positions. Intuitively, this means that if the input arguments of a call are not “sufficiently instantiated” then it is delayed until it allows for an input-consuming derivation step (if it is not the case then a deadlock situation will arise).

###### Lemma 10

Let the program $`P`$ and the query $`Q`$ be nicely-moded. Let $`\delta :=Q\stackrel{\theta }{}Q^{}`$ be a partial input-consuming derivation of $`P\{Q\}`$. Then, for all $`x\mathrm{𝑉𝑎𝑟}(Q)`$ and $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(Q))`$, $`x\theta =x`$.

Proof. Let us first establish the following claim.

###### Claim 11

Let $`𝐳`$ and $`𝐰`$ be two variable disjoint sequences of terms such that $`𝐰`$ is linear and $`\theta =\mathrm{𝑚𝑔𝑢}(𝐳,𝐰)`$. If $`s_1`$ and $`s_2`$ are two variable disjoint terms occurring in $`𝐳`$ then $`s_1\theta `$ and $`s_2\theta `$ are variable disjoint terms.

Proof. The result follows from Lemmata 11.4 and 11.5 in \[AP94a\]. $`\mathrm{}`$

We proceed with the proof of the lemma by induction on $`\mathrm{𝑙𝑒𝑛}(\delta )`$.

*Base Case*. Let $`\mathrm{𝑙𝑒𝑛}(\delta )=0`$. In this case $`Q=Q^{}`$ and the result follows trivially.

*Induction step*. Let $`\mathrm{𝑙𝑒𝑛}(\delta )>0`$. Suppose that $`Q:=𝐀,p(𝐬,𝐭),𝐂`$ and

$$\delta :=𝐀,p(𝐬,𝐭),𝐂\stackrel{\theta _1}{}(𝐀,𝐁,𝐂)\theta _1\stackrel{\theta _2}{}Q^{}$$

where $`p(𝐬,𝐭)`$ is the selected atom of $`Q`$, $`c:=p(𝐮,𝐯)𝐁`$ is the input clause used in the first derivation step, $`\theta _1`$ is a relevant mgu of $`p(𝐬,𝐭)`$ and $`p(𝐮,𝐯)`$ and $`\theta =\theta _1\theta _2`$.

Let $`x\mathrm{𝑉𝑎𝑟}(𝐀,p(𝐬,𝐭),𝐂)`$ and $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,p(𝐬,𝐭),𝐂))`$. We first show that

$$x\theta _1=x$$
(1)
We distinguish two cases.

$`(a)`$ $`x\mathrm{𝑉𝑎𝑟}(𝐬)`$. In this case, property $`(\text{1})`$ follows from the hypothesis that $`\delta `$ is input-consuming.

$`(b)`$ $`x\mathrm{𝑉𝑎𝑟}(𝐬)`$. Since $`x\mathrm{𝑉𝑎𝑟}(𝐀,p(𝐬,𝐭),𝐂)`$, by standardization apart, we have that $`x\mathrm{𝑉𝑎𝑟}(p(𝐮,𝐯))`$. Moreover, since $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,p(𝐬,𝐭),𝐂))`$, it also holds that $`x\mathrm{𝑉𝑎𝑟}(p(𝐬,𝐭))`$. Then, property $`(\text{1})`$ follows from relevance of $`\theta _1`$.
Now we show that

$$x\theta _2=x$$
(2)
Again, we distinguish two cases:

$`(c)`$ $`x\mathrm{𝑉𝑎𝑟}((𝐀,𝐁,𝐂)\theta _1)`$. In this case, because of the standardization apart condition, $`x`$ will never occur in $`(𝐀,𝐁,𝐂)\theta _1\stackrel{\theta _2}{}Q^{}`$. Hence, $`x\mathrm{𝐷𝑜𝑚}(\theta _2)`$ and $`x\theta _2=x`$.

$`(d)`$ $`x\mathrm{𝑉𝑎𝑟}((𝐀,𝐁,𝐂)\theta _1)`$. In this case, in order to prove $`(\text{2})`$ we show that $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((𝐀,𝐁,𝐂)\theta _1))`$. The result then follows by the inductive hypothesis.

From the standardization apart, relevance of $`\theta _1`$ and the fact that the first derivation step is input-consuming, it follows that $`\mathrm{𝐷𝑜𝑚}(\theta _1)\mathrm{𝑉𝑎𝑟}(Q)\mathrm{𝑉𝑎𝑟}(𝐭)`$.

From the hypothesis that $`Q`$ is nicely-moded, $`\mathrm{𝑉𝑎𝑟}(𝐭)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,𝐂))=\mathrm{}`$. Hence, $`\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,𝐂))\theta _1=\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,𝐂))`$. Since $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀,𝐂))`$, this proves that $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((𝐀,𝐂)\theta _1))`$.

It remains to be proven that $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\theta _1)`$. We distinguish two cases.

$`(d1)`$ $`x\mathrm{𝑉𝑎𝑟}(𝐬)`$. Since $`x\mathrm{𝑉𝑎𝑟}(p(𝐬,𝐭))`$, the fact that $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\theta _1)`$ follows immediately by standardization apart condition and relevance of $`\theta _1`$.

$`(d2)`$ $`x\mathrm{𝑉𝑎𝑟}(𝐬)`$. By known results (see \[Apt97\], Corollary 2.25), there exists two relevant mgu $`\sigma _1`$ and $`\sigma _2`$ such that

* $`\theta _1=\sigma _1\sigma _2`$,
* $`\sigma _1=\mathrm{𝑚𝑔𝑢}(𝐬,𝐮)`$,
* $`\sigma _2=\mathrm{𝑚𝑔𝑢}(𝐭\sigma _1,𝐯\sigma _1)`$.

From relevance of $`\sigma _1`$ and the fact that, by nicely-modedness of $`Q`$, $`\mathrm{𝑉𝑎𝑟}(𝐬)\mathrm{𝑉𝑎𝑟}(𝐭)=\mathrm{}`$, we have that $`𝐭\sigma _1=𝐭`$, and by the standardization apart condition $`\mathrm{𝑉𝑎𝑟}(𝐭)\mathrm{𝑉𝑎𝑟}(𝐯\sigma _1)=\mathrm{}`$. Now by nicely-modedness of $`c`$, $`\mathrm{𝑉𝑎𝑟}(𝐮)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁))=\mathrm{}`$. Since $`\sigma _1`$ is relevant and by the standardization apart condition it follows that

$$\mathrm{𝑉𝑎𝑟}(𝐮\sigma _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\sigma _1))=\mathrm{}$$
(3)
The proof proceeds now by contradiction. Suppose that $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\sigma _1\sigma _2))`$. Since by hypothesis $`x\mathrm{𝑉𝑎𝑟}(𝐬)`$, and $`𝐬=𝐮\sigma _1\sigma _2`$, we have that $`\mathrm{𝑉𝑎𝑟}(𝐮\sigma _1\sigma _2)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\sigma _1\sigma _2))\mathrm{}`$. By $`(\text{3})`$, this means that there exist two distinct variables $`z_1`$ and $`z_2`$ in $`\mathrm{𝑉𝑎𝑟}(\sigma _2)`$ such that $`z_1\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\sigma _1))`$, $`z_2\mathrm{𝑉𝑎𝑟}(𝐮\sigma _1)`$ and

$$\mathrm{𝑉𝑎𝑟}(z_1\sigma _2)\mathrm{𝑉𝑎𝑟}(z_2\sigma _2)\mathrm{}$$
(4)
Since, by the standardization apart condition and relevance of the mgu’s, $`\mathrm{𝑉𝑎𝑟}(\sigma _2)`$ $`\mathrm{𝑉𝑎𝑟}(𝐯\sigma _1)\mathrm{𝑉𝑎𝑟}(𝐭)`$ and $`(\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐁\sigma _1))\mathrm{𝑉𝑎𝑟}(𝐮\sigma _1))\mathrm{𝑉𝑎𝑟}(𝐭)=\mathrm{}`$, we have that $`z_1`$ and $`z_2`$ are two disjoint subterms of $`𝐯\sigma _1`$. Since $`\sigma _2=\mathrm{𝑚𝑔𝑢}(𝐭,𝐯\sigma _1)`$, $`𝐭`$ is linear and disjoint from $`𝐯\sigma _1`$, (4) contradicts Claim 11. $`\mathrm{}`$

The following corollary is an immediate consequence of the above lemma and the definition of nicely-moded program.

###### Corollary 12

Let the program $`P`$ and the one-atom query $`A`$ be nicely-moded. Let $`\delta :=A\stackrel{\theta }{}Q^{}`$ be a partial input-consuming derivation of $`P\{A\}`$. Then, for all $`x\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))`$, $`x\theta =x`$.

Next is the main result of this section, showing that for input-consuming nicely-moded programs one half of the well-known switching lemma holds.

###### Lemma 13 (Left-Switching)

Let the program $`P`$ and the query $`Q_0`$ be nicely-moded. Let $`\delta `$ be a partial input-consuming derivation of $`P\{Q_0\}`$ of the form

$$\delta :=Q_0\underset{c_1}{\overset{\theta _1}{}}Q_1\mathrm{}Q_n\underset{c_{n+1}}{\overset{\theta _{n+1}}{}}Q_{n+1}\underset{c_{n+2}}{\overset{\theta _{n+2}}{}}Q_{n+2}$$

where

* $`Q_n`$ is a query of the form $`𝐀,B,𝐂,D,𝐄`$,
* $`Q_{n+1}`$ is a resolvent of $`Q_n`$ and $`c_{n+1}`$ wrt. $`D`$,
* $`Q_{n+2}`$ is a resolvent of $`Q_{n+1}`$ and $`c_{n+2}`$ wrt. $`B\theta _{n+1}`$.

Then, there exist $`Q_{n+1}^{}`$, $`\theta _{n+1}^{}`$, $`\theta _{n+2}^{}`$ and a derivation $`\delta ^{}`$ such that

$$\theta _{n+1}\theta _{n+2}=\theta _{n+1}^{}\theta _{n+2}^{}$$

and

$$\delta ^{}:=Q_0\underset{c_1}{\overset{\theta _1}{}}Q_1\mathrm{}Q_n\underset{c_{n+2}}{\overset{\theta _{n+1}^{}}{}}Q_{n+1}^{}\underset{c_{n+1}}{\overset{\theta _{n+2}^{}}{}}Q_{n+2}$$

where $`\delta ^{}`$ is input-consuming and

* $`\delta `$ and $`\delta ^{}`$ coincide up to the resolvent $`Q_n`$,
* $`Q_{n+1}^{}`$ is a resolvent of $`Q_n`$ and $`c_{n+2}`$ wrt. $`B`$,
* $`Q_{n+2}`$ is a resolvent of $`Q_{n+1}^{}`$ and $`c_{n+1}`$ wrt. $`D\theta _{n+1}^{}`$,
* $`\delta `$ and $`\delta ^{}`$ coincide after the resolvent $`Q_{n+2}`$.

Proof. Let $`B:=p(𝐬,𝐭)`$, $`D:=q(𝐮,𝐯)`$, $`c_{n+1}:=q(𝐮^{},𝐯^{})𝐃`$ and $`c_{n+2}:=p(𝐬^{},𝐭^{})𝐁`$. Hence, $`\theta _{n+1}=\mathrm{𝑚𝑔𝑢}(q(𝐮,𝐯),q(𝐮^{},𝐯^{}))`$ and

$$𝐮\theta _{n+1}=𝐮,\text{ since }\delta \text{ is input-consuming.}$$
(5)
By $`(\text{5})`$ and the fact that $`Q_n`$ is nicely-moded and $`\theta _{n+1}`$ is relevant, we have that $`p(𝐬,𝐭)\theta _{n+1}=p(𝐬,𝐭)`$. Then, $`\theta _{n+2}=\mathrm{𝑚𝑔𝑢}(p(𝐬,𝐭)\theta _{n+1},p(𝐬^{},𝐭^{}))=\mathrm{𝑚𝑔𝑢}(p(𝐬,𝐭),p(𝐬^{},𝐭^{}))`$ and

$$𝐬\theta _{n+2}=𝐬,\text{ since }\delta \text{ is input-consuming.}$$
(6)
Moreover,222We use the notation $`\mathrm{𝑚𝑔𝑢}(E)`$ to denote the mgu of a set of equations $`E`$, see \[Apt97\].

$$\theta _{n+1}\theta _{n+2}=\mathrm{𝑚𝑔𝑢}\{p(𝐬,𝐭)=p(𝐬^{},𝐭^{}),q(𝐮,𝐯)=q(𝐮^{},𝐯^{})\}=\theta _{n+2}\theta _{n+2}^{}$$
(7)
where

$$\theta _{n+2}^{}=\mathrm{𝑚𝑔𝑢}(q(𝐮,𝐯)\theta _{n+2},q(𝐮^{},𝐯^{})\theta _{n+2})=\mathrm{𝑚𝑔𝑢}(q(𝐮,𝐯)\theta _{n+2},q(𝐮^{},𝐯^{})).$$

We construct the derivation $`\delta ^{}`$ as follows.

$$\delta ^{}:=Q_0\underset{c_1}{\overset{\theta _1}{}}Q_1\mathrm{}Q_n\underset{c_{n+2}}{\overset{\theta _{n+1}^{}}{}}Q_{n+1}^{}\underset{c_{n+1}}{\overset{\theta _{n+2}^{}}{}}Q_{n+2}$$

where

$$\theta _{n+1}^{}=\theta _{n+2}$$
(8)
By $`(\text{6})`$, $`Q_n\underset{c_{n+2}}{\overset{\theta _{n+1}^{}}{}}Q_{n+1}^{}`$ is an input-consuming derivation step. Observe now that

$$\begin{array}{ccccc}𝐮\theta _{n+1}^{}\theta _{n+2}^{}\hfill & =\hfill & 𝐮\theta _{n+2}\theta _{n+2}^{},\hfill & (\text{by }(\text{8}))\hfill & \\ & =\hfill & 𝐮\theta _{n+1}\theta _{n+2},\hfill & (\text{by }(\text{7}))\hfill & \\ & =\hfill & 𝐮\theta _{n+2},\hfill & (\text{by }(\text{5}))\hfill & \\ & =\hfill & 𝐮\theta _{n+1}^{},\hfill & (\text{by }(\text{8})).\hfill & \end{array}$$

This proves that $`Q_{n+1}^{}\underset{c_{n+1}}{\overset{\theta _{n+2}^{}}{}}Q_{n+2}^{}`$ is an input-consuming derivation step. $`\mathrm{}`$

This result shows that it is always possible to proceed left-to-right to resolve the selected atoms. Notice that this is different than saying that the leftmost atom of a query is always resolvable: It can very well be the case that the leftmost atom is suspended and the one next to it is resolvable. However, if the leftmost atom of a query is not resolvable then we can state that the derivation will not succeed, i.e., either it ends by deadlock, or by failure or it is infinite.

It is important to notice that if we drop the nicely-modedness condition the above lemma would not hold any longer. For instance, it does not apply to the query $`Q_1`$ of the introduction which is not nicely-moded. In fact, the leftmost atom of $`Q_1`$ is resolvable only after the rightmost one has been resolved at least once.

The following immediate corollary will be used in the sequel.

###### Corollary 14

Let the program $`P`$ and the query $`Q:=𝐀,𝐁`$ be nicely-moded. Suppose that

$$\delta :=𝐀,𝐁\stackrel{\theta }{}𝐂_1,𝐂_2$$

that is a partial input-consuming derivation of $`P\{Q\}`$ where $`𝐂_1`$ and $`𝐂_2`$ are obtained by partially resolving $`𝐀`$ and $`𝐁`$, respectively. Then there exists a partial input-consuming derivation

$$\delta ^{}:=𝐀,𝐁\stackrel{\theta _1}{}𝐂_1,𝐁\theta _1\stackrel{\theta _2}{}𝐂_1,𝐂_2$$

where all the $`𝐀`$-steps are performed in the prefix $`𝐀,𝐁\stackrel{\theta _1}{}𝐂_1,𝐁\theta _1`$ and $`\theta =\theta _1\theta _2`$.

## 5 Termination

In this section we study the termination of input-consuming derivations. To this end we refine the ideas of Bezem \[Bez93\] and Cavedon \[Cav89\] who studied the termination of logic programs in a very strong sense, namely with respect to all selection rules, and of Smaus \[Sma99b\] who characterized terminating input-consuming derivations of programs which are both well and nicely-moded.

### 5.1 Input Terminating Programs

We first introduce the key notion of this section.

###### Definition 15 (Input Termination)

A program is called *input terminating* iff all its input-consuming derivations started in a nicely-moded query are finite.

The method we use in order to prove that a program is input terminating is based on the following concept of moded level mapping due to Etalle *et al.* \[EBC99\].

###### Definition 16 (Moded Level Mapping)

Let $`P`$ be a program and $`_P^{}`$ be the extended Herbrand base333The extended Herbrand base of $`P`$ is the set of equivalence classes of all (possibly non-ground) atoms, modulo renaming, whose predicate symbol appears in $`P`$. As usual, an atom is identified with its equivalence class. for the language associated with $`P`$. A function $`||`$ is a *moded level mapping for $`P`$* iff:

* it is a function $`||:_P^{}𝐍`$ from atoms to natural numbers;
* for any $`𝐭`$ and $`𝐮`$, $`|p(𝐬,𝐭)|=|p(𝐬,𝐮)|`$.

For $`A_P^{}`$, $`|A|`$ is the *level* of $`A`$.

The condition $`|p(𝐬,𝐭)|=|p(𝐬,𝐮)|`$ states that the level of an atom is independent from the terms in its output positions. There is actually a small yet important difference between this definition and the one in \[EBC99\]: In \[EBC99\] the level mapping is defined on ground atoms only. Indeed, in \[EBC99\] only well-moded atoms are considered, i.e., atoms with ground terms in the input positions. Here, instead, we are considering nicely-moded atoms whose input positions can be filled in by (possibly) non-ground terms.

###### Example 17

Let us denote by $`\mathrm{𝑇𝑆𝑖𝑧𝑒}(t)`$ the term size of a term $`t`$, that is the number of function and constant symbols that occur in $`t`$.

* A moded level mapping for the program APPEND reported in the introduction is as follows:
* A moded level mapping for the program REVERSE with accumulator of Example 5 is the following:

| |reverse($`x_s`$,$`y_s`$)|= *TSize*($`x_s`$) |
| --- |
| |reverse\_acc($`x_s`$,$`y_s`$,$`z_s`$)|=*TSize*($`x_s`$). |

### 5.2 Quasi Recurrency

In order to give a sufficient condition for termination, we are going to employ a generalization of the concept of *recurrent* and of *semi-recurrent* program. The first notion (which in the case of normal programs, i.e., programs with negation, coincides with the one of *acyclic program*) was introduced in \[Bez93, AB91\] and independently in \[Cav91\] in order to prove universal termination for all selection rules together with other properties of logic programs. Later, Apt and Pedreschi \[AP94a\] provided the new definition of semi-recurrent program, which is equivalent to the one of recurrent program, but it is easier to verify in an automatic fashion. In order to proceed, we need a preliminary definition.

###### Definition 18

Let $`P`$ be a program, $`p`$ and $`q`$ be relations. We say that *$`p`$ refers to $`q`$* in $`P`$ iff there is a clause in $`P`$ with $`p`$ in the head and $`q`$ in the body. We say that *$`p`$ depends on $`q`$* and write $`pq`$ in $`P`$ iff $`(p,q)`$ is in the reflexive and transitive closure of the relation *refers to*.

According to the above definition, $`pqpqpq`$ means that $`p`$ and $`q`$ are mutually recursive, and $`pqpqp\simeq ̸q`$ means that $`p`$ calls $`q`$ as a subprogram. Notice that $``$ is a well-founded ordering.

Finally, we can provide the key concept we are going to use in order to prove input termination.

###### Definition 19 (Quasi Recurrency)

Let $`P`$ be a program and $`||:_P^{}𝐍`$ be a moded level mapping.

* A clause of $`P`$ is called *quasi recurrent with respect to $`||`$*  if for every instance of it, $`H𝐀,B,𝐂`$

$$\text{if }\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B)\text{ then }|H|>|B|.$$
(9)
* A program $`P`$ is called *quasi recurrent with respect to $`||`$*  if all its clauses are. $`P`$ is called *quasi recurrent* if it is quasi recurrent wrt. some moded level mapping $`||:_P^{}𝐍`$.

The notion of quasi recurrent program differs from the concepts of recurrent and of semi-recurrent program in two ways. First, we require that $`|H|>|B|`$ only for those body atoms which mutually depend on $`\mathrm{𝑅𝑒𝑙}(H)`$; in contrast, both the concept of recurrent and of semi-recurrent program require that $`|H|>|B|`$ ($`|H||B|`$ in the case of semi-recurrency) also for the atoms for which $`\mathrm{𝑅𝑒𝑙}(H)\simeq ̸\mathrm{𝑅𝑒𝑙}(B)`$. Secondly, every instance of a program clause is considered, not only ground instances as in the case of (semi-)recurrent programs. This allows us to treat directly any nicely-moded query without introducing the concept of *boundedness* \[AP94a\] or *cover* as in \[MT95\].

It is worthwhile noticing that this concept almost coincides with the one of *ICD-acceptable* program introduced and used in \[Sma99b\]. We decided to use a different name because we believe that referring to the word acceptable might lead to confusion: The concept of acceptable program was introduced by Apt and Pedreschi \[AP93, AP94a\] in order to prove termination of logic programs using the left-to-right selection rule. The crucial difference between recurrency and acceptability lies in the fact that the latter relies on a model $`M`$; this allows condition (9) to be checked only for those body atoms which are in a way “reachable” wrt. $`M`$. Hence, every recurrent program is acceptable but not vice-versa. As an aside, Marchiori and Teusink \[MT95\] introduce the notion of *delay recurrent* program although their concept is based on the presence of a model $`M`$. Our definition does not rely on a model, and so it is much more related to the notion of recurrent than the one of acceptable program.

We can now state our first basic result on termination, in the case of non-modular programs.

###### Theorem 20

Let $`P`$ be a nicely-moded program. If $`P`$ is quasi recurrent then $`P`$ is input terminating.

Proof. It will be obtained from the proof of Theorem 24 by setting $`R=\mathrm{}`$. $`\mathrm{}`$

###### Example 21

Consider the program $`\mathrm{𝙼𝙴𝚁𝙶𝙴}`$ defined in Example 7. Let $`||`$ be the moded level mapping for $`\mathrm{𝙼𝙴𝚁𝙶𝙴}`$ defined by

It is easy to prove that MERGE is quasi recurrent wrt. the moded level mapping above. By Theorem 20, all input-consuming derivations of MERGE started with a query $`\mathrm{𝚖𝚎𝚛𝚐𝚎}(s,t,u)`$, where $`u`$ is linear and variable disjoint from $`s`$ and $`t`$, are terminating.

### 5.3 Modular Termination

This section contains a generalization of Theorem 20 to the modular case, as well as the complete proofs for it. The following lemma is a crucial one.

###### Lemma 22

Let the program $`P`$ and the query $`Q:=A_1,\mathrm{},A_n`$ be nicely-moded. Suppose that there exists an infinite input-consuming derivation $`\delta `$ of $`P\{Q\}`$. Then, there exist an index $`i\{1,\mathrm{},n\}`$ and substitution $`\theta `$ such that

1. there exists an input-consuming derivation $`\delta ^{}`$ of $`P\{Q\}`$ of the form

$$\delta ^{}:=A_1,\mathrm{},A_n\stackrel{\theta }{}𝐂,(A_i,\mathrm{},A_n)\theta \mathrm{}$$
2. there exists an infinite input-consuming derivation of $`P\{A_i\theta \}`$.

Proof. Let $`\delta :=A_1,\mathrm{},A_n\mathrm{}`$ be an infinite input-consuming derivation of $`P\{Q\}`$. Then $`\delta `$ contains an infinite number of $`A_k`$-steps for some $`k\{1,\mathrm{},n\}`$. Let $`i`$ be the minimum of such $`k`$. Hence $`\delta `$ contains a finite number of $`A_j`$-steps for $`j\{1,\mathrm{},i1\}`$ and there exists $`𝐂`$ and $`𝐃`$ such that

$$\delta :=A_1,\mathrm{},A_n\stackrel{\vartheta }{}𝐂,𝐃\mathrm{}$$

where $`A_1,\mathrm{},A_n\stackrel{\vartheta }{}𝐂,𝐃`$ is a finite prefix of $`\delta `$ which comprises all the $`A_j`$-steps of $`\delta `$ for $`j\{1,\mathrm{},i1\}`$ and $`𝐂`$ is the subquery of $`𝐂,𝐃`$ consisting of the atoms resulting from some $`A_j`$-step ($`j\{1,\mathrm{},i1\}`$). By Corollary 14, there exists an infinite input-consuming derivation $`\delta ^{}`$ such that

$$\delta ^{}:=A_1,\mathrm{},A_n\stackrel{\theta }{}𝐂,(A_i,\mathrm{},A_n)\theta \stackrel{\theta ^{}}{}𝐂,𝐃\mathrm{}$$

where $`\vartheta =\theta \theta ^{}`$. This proves (i).

Now, let $`\delta ^{\prime \prime }:=𝐂,(A_i,\mathrm{},A_n)\theta \stackrel{\theta ^{}}{}𝐂,𝐃\mathrm{}`$. Note that in $`\delta ^{\prime \prime }`$ the atoms of $`𝐂`$ will never be selected and, by Remark 9, will never be instantiated. Let $`\delta ^{\prime \prime \prime }`$ be obtained from $`\delta ^{\prime \prime }`$ by omitting the prefix $`𝐂`$ in each query. Hence $`\delta ^{\prime \prime \prime }`$ is an infinite input-consuming derivation of $`P\{(A_i,\mathrm{},A_n)\theta \}`$ where an infinite number of $`A_i\theta `$-steps are performed. Again, By Remark 9, for every finite prefix of $`\delta ^{\prime \prime \prime }`$ of the form

$$A_i\theta ,(A_{i+1},\mathrm{},A_n)\theta \stackrel{\sigma _1}{}𝐃_1,𝐃_2\stackrel{\sigma _2}{}𝐃_1^{},𝐃_2^{}$$

where $`𝐃_1`$ and $`𝐃_2`$ are obtained by partially resolving $`A_i\theta `$ and $`(A_{i+1},\mathrm{},A_n)\theta `$, respectively, and $`𝐃_1,𝐃_2\stackrel{\sigma _2}{}𝐃_1^{},𝐃_2^{}`$ is an $`A_j`$-step for some $`j\{i+1,\mathrm{},n\}`$, we have that $`𝐃_1^{}=𝐃_1`$. Hence, from the hypothesis that there is an infinite number of $`A_i\theta `$-steps in $`\delta ^{\prime \prime }`$, it follows that there exists an infinite input-consuming derivation of $`P\{A_i\theta \}`$. This proves (ii). $`\mathrm{}`$

The importance of the above lemma is shown by the following corollary of it, which will allow us to concentrate on queries containing only one atom.

###### Corollary 23

Let $`P`$ be a nicely-moded program. $`P`$ is input terminating iff for each nicely-moded one-atom query $`A`$ all input-consuming derivations of $`P\{A\}`$ are finite.

We can now state the main result of this section. Here and in what follows we say that a relation $`p`$ is *defined in* the program $`P`$ if $`p`$ occurs in a head of a clause of $`P`$, and that $`P`$ *extends* the program $`R`$ if no relation defined in $`P`$ occurs in $`R`$.

###### Theorem 24

Let $`P`$ and $`R`$ be two programs such that $`P`$ extends $`R`$. Suppose that

* $`R`$ is input terminating,
* $`P`$ is nicely-moded and quasi recurrent wrt. a moded level mapping $`||:_P^{}𝐍`$.

Then $`PR`$ is input terminating.

Proof. First, for each predicate symbol $`p`$, we define $`\mathrm{𝑑𝑒𝑝}_P(p)`$ to be the number of predicate symbols it depends on. More formally, $`\mathrm{𝑑𝑒𝑝}_P(p)`$ is defined as the cardinality of the set $`\{q|q\text{ is defined in }P\text{ and }pq\}`$. Clearly, $`\mathrm{𝑑𝑒𝑝}_P(p)`$ is always finite. Further, it is immediate to see that if $`pq`$ then $`\mathrm{𝑑𝑒𝑝}_P(p)=\mathrm{𝑑𝑒𝑝}_P(q)`$ and that if $`pq`$ then $`\mathrm{𝑑𝑒𝑝}_P(p)>\mathrm{𝑑𝑒𝑝}_P(q)`$.

We can now prove our theorem. By Corollary 23, it is sufficient to prove that for any nicely-moded one-atom query $`A`$, all input-consuming derivations of $`P\{A\}`$ are finite.

First notice that if $`A`$ is defined in $`R`$ then the result follows immediately from the hypothesis that $`R`$ is input terminating and that $`P`$ is an extension of $`R`$. So we can assume that $`A`$ is defined in $`P`$.

For the purpose of deriving a contradiction, assume that $`\delta `$ is an infinite input-consuming derivation of $`(PR)\{A\}`$ such that $`A`$ is defined in $`P`$. Then

$$\delta :=A\stackrel{\theta _1}{}(B_1,\mathrm{},B_n)\theta _1\stackrel{\theta _2}{}\mathrm{}$$

where $`HB_1,\mathrm{},B_n`$ is the input clause used in the first derivation step and $`\theta _1=\mathrm{𝑚𝑔𝑢}(A,H)`$. Clearly, $`(B_1,\mathrm{},B_n)\theta _1`$ has an infinite input-consuming derivation in $`PR`$. By Lemma 22, for some $`i\{1,\mathrm{},n\}`$ and for some substitution $`\theta _2`$,

1. there exists an infinite input-consuming derivation of $`(PR)\{A\}`$ of the form

$$A\stackrel{\theta _1}{}(B_1,\mathrm{},B_n)\theta _1\stackrel{\theta _2}{}𝐂,(B_i,\mathrm{},B_n)\theta _1\theta _2\mathrm{};$$
2. there exists an infinite input-consuming derivation of $`P\{B_i\theta _1\theta _2\}.`$

Notice also that $`B_i\theta _1\theta _2`$ is nicely-moded. Let now $`\theta =\theta _1\theta _2`$. Note that $`H\theta (B_1,\mathrm{},B_n)\theta `$ is an instance of a clause of $`P`$.

We show that (2) cannot hold. This is done by induction on $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A)),|A|`$ wrt. the ordering $``$ defined by: $`m,nm^{},n^{}`$ iff either $`m>m^{}`$ or $`m=m^{}`$ and $`n>n^{}`$.

Base. Let $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A))=0`$ ($`|A|`$ is arbitrary). In this case, $`A`$ does not depend on any predicate symbol of $`P`$, thus all the $`B_i`$ as well as all the atoms occurring in its descendents in any input-consuming derivation are defined in $`R`$. The hypothesis that $`R`$ is input terminating contradicts $`(2)`$ above.

*Induction step*. We distinguish two cases:

1. $`\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B_i)`$,
2. $`\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B_i)`$.

In case $`(a)`$ we have that $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A))=\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(H\theta ))>\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(B_i\theta ))`$. So, $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A)),|A|=\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(H\theta )),|H\theta |\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(B_i\theta )),|B_i\theta |`$. In case $`(b)`$, from the hypothesis that $`P`$ is quasi recurrent wrt. $`||`$, it follows that $`|H\theta |>|B_i\theta |`$.

Consider now the partial input-consuming derivation $`A\stackrel{\theta }{}𝐂,(B_i,\mathrm{},B_n)\theta `$. By Corollary 12 and the fact that $`||`$ is a moded level mapping, it follows that $`|A|=|A\theta |=|H\theta |`$. Therefore, $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A)),|A|=\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(H\theta )),|H\theta |\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(B_i\theta )),|B_i\theta |`$. In both cases, the contradiction follows by the inductive hypothesis. $`\mathrm{}`$

###### Example 25

The program FLATTEN using difference-lists is nicely-moded with respect to the modes described below, provided that one replaces “$``$” by “,”, as we have done here.

| mode flatten(In,Out). |
| --- |
| mode flatten\_dl(In,Out,In). |
| mode constant(In). |
| mode $``$(In,In). |
| flatten(Xs,Ys) $``$flatten\_dl(Xs,Ys,\[ \]). |
| flatten\_dl(\[ \],Ys,Ys). |
| flatten\_dl(X,\[X|Xs\],Xs) $``$constant(X), X $``$ \[ \]. |
| flatten\_dl(\[X|Xs\],Ys,Zs) $``$ | flatten\_dl(Xs,Y1s,Zs), |
|  | flatten\_dl(X,Ys,Y1s). |

Consider the moded level mapping for $`\mathrm{𝙵𝙻𝙰𝚃𝚃𝙴𝙽}`$ defined by

| |flatten($`x_s`$,$`y_s`$)| = TSize($`x_s`$) |
| --- |
| |flatten\_dl($`x_s`$,$`y_s`$,$`z_s`$)| = TSize($`x_s`$). |

It is easy to see that the program FLATTEN is quasi recurrent wrt. the moded level mapping above. Hence, all input-consuming derivations of program FLATTEN started with a query flatten($`\mathrm{s}`$,$`\mathrm{t}`$), where $`t`$ is linear and variable disjoint from $`s`$, are terminating.

## 6 Termination: A Necessary Condition

Theorem 20 provides a sufficient condition for termination. The condition is not necessary, as demonstrated by the following simple example.

| mode p(In,Out). |
| --- |
| p(X,a) $``$p(X,b). |
| p(X,b). |

This program is clearly input terminating, however it is not quasi recurrent. If it was, we would have that $`|𝚙(𝚇,𝚊)|>|𝚙(𝚇,𝚋)|`$, for some moded level mapping $`||`$ (otherwise the first clause would not be quasi recurrent). On the other hand, since $`𝚙(𝚇,𝚊)`$ and $`𝚙(𝚇,𝚋)`$ differ only for the terms filling in their output positions, by definition of moded level mapping, $`|𝚙(𝚇,𝚊)|=|𝚙(𝚇,𝚋)|`$. Hence, we have a contradiction.

Nevertheless, as shown by other works, e.g., \[Bez93, AP93, EBC99\], it is important to be able to give a characterization of termination, i.e., a condition which is *necessary* and sufficient to ensure termination. To this purpose is dedicated this section.

### 6.1 Simply-Moded Programs

As demonstrated by the example above, in order to provide a necessary condition for termination we need to further restrict the class of programs we consider. The first problem is that we should rule out those situations in which termination is guaranteed by the instantiation of the output positions of some selected atom, as it happens in the above example. For this we restrict to *simply-moded* programs which are nicely-moded programs with the additional condition that the output arguments of clause bodies are variables.

###### Definition 26 (Simply-Moded)

* A query $`Q`$ (resp., a clause $`c=HQ`$) is *simply-moded* if it is nicely-moded and $`\mathrm{𝑂𝑢𝑡}(Q)`$ is a linear sequence of variables.
* A program $`P`$ is simply-moded iff all of its clauses are simply-moded.

It is important to notice that most programs are simply-moded (see the mini-survey at the end of \[AP93\]) and that often non simply-moded programs can naturally be transformed into simply-moded ones.

###### Example 27

* The programs REVERSE of Example 5, MERGE of Example 7 and FLATTEN of Example 25 are all simply-moded.
* Consider the program LAST which extends REVERSE:

| mode last(In,Out). |
| --- |
| last(Ls,E)$``$reverse(Ls,\[E|\_\]). |

This program is not simply-moded since the argument filling in the output position in the body of the first clause is not a variable. However, it can be transformed into a simply-moded one as follows:

| mode last(In,Out). |
| --- |
| mode selectfirst(In,Out). |
| last(Ls,E)$``$reverse(Ls,Rs), selectfirst(Rs,E). |
| selectfirst(\[E|\_\],E). |

The following lemma, which is an immediate consequence of Lemma 30 in \[AL95\], shows the persistence of the notion of simply-modedness.

###### Lemma 28

Every resolvent of a simply-moded query $`Q`$ and a simply-moded clause $`c`$, where the derivation step is input-consuming and $`\mathrm{𝑉𝑎𝑟}(Q)\mathrm{𝑉𝑎𝑟}(c)=\mathrm{}`$, is simply-moded.

### 6.2 Input-Recursive Programs

Unfortunately, the restriction to simply-moded programs alone is not sufficient to extend Theorem 20 by a necessary condition. Consider for instance the following program QUICKSORT:

|  | mode qs(In,Out). |
| --- | --- |
|  | mode part(In,In,Out,Out). |
|  | mode app(In,In,Out). |
|  | qs(\[ \],\[ \]). |
| $`c_1:=`$ | qs(\[X|Xs\],Ys) $``$part(X,Xs,Littles,Bigs), |
|  |  | qs(Littles,Ls), |
|  |  | qs(Bigs,Bs), |
|  |  | app(Ls,\[X|Bs\],Ys). |
|  | part(X,\[ \],\[ \],\[ \]). |
|  | part(X,\[Y|Xs\],\[Y|Ls\],Bs) $``$X\>Y, part(X,Xs,Ls,Bs). |
|  | part(X,\[Y|Xs\],Ls,\[Y|Bs\]) $``$X\<=Y, part(X,Xs,Ls,Bs). |

This program is simply-moded and input terminating444Provided that one models the built-in predicates \> and \<= as being defined by (an infinite number of) ground facts of the form \>($`m`$,$`n`$) and \<=($`m`$,$`n`$). The problem here is that the definition of input-consuming derivation does not consider the presence of built-ins.. However it is not quasi recurrent. Indeed, there exist no moded level mapping $`||`$ such that, for every variable-instance, $`|\mathrm{𝚚𝚜}([𝚇|\mathrm{𝚇𝚜}],\mathrm{𝚈𝚜})|>|\mathrm{𝚚𝚜}(\mathrm{𝙻𝚒𝚝𝚝𝚕𝚎𝚜},\mathrm{𝙻𝚜})|`$ and $`|\mathrm{𝚚𝚜}([𝚇|\mathrm{𝚇𝚜}],\mathrm{𝚈𝚜})|>|\mathrm{𝚚𝚜}(\mathrm{𝙱𝚒𝚐𝚜},\mathrm{𝙱𝚜})|`$. This is due to the fact that, in clause $`c_1`$ there is no direct link between the input arguments of the recursive calls and those of the clause head. This motivates the following definition of *input-recursive* programs.

###### Definition 29 (Input-Recursive)

Let $`P`$ be a program.

* A clause $`H𝐀,B,𝐂`$ of $`P`$ is called *input-recursive* if

$$\text{if }\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B)\text{ then }\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(B))\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H)).$$
* A program $`P`$ is called *input-recursive* if all its clauses are.

Thus, we say that a clause is input-recursive if the set of variables occurring in the arguments filling in the input positions of each recursive call in the clause body is a subset of the set of variables occurring in the arguments filling in the input positions of the clause head. Input-recursive programs have strong similarities with primitive recursive functions.

###### Example 30

* The programs APPEND of the introduction, REVERSE of Example 5 and MERGE of Example 7 are all input-recursive.
* The program FLATTEN of Example 25 is not input-recursive. This is due to the presence of the fresh variable Y1s in a body atom of the last clause.
* QUICKSORT, is not input-recursive. In particular, clause $`c_1`$ is not input-recursive.

### 6.3 Characterizing Input Terminating Programs

We can now prove that by restricting ourselves to input-recursive and simply-moded programs, the condition of Theorem 20 is also a necessary one.

To prove this, we follow the approach of Apt and Pedreschi when characterizing terminating programs \[AP94a\]. First we introduce the notion of *IC-tree* that corresponds to the notion of *S-tree* in \[AP94a\] and provides us with a representation for all input-consuming derivations of a program $`P`$ with a query $`Q`$, then we define a level mapping which associates to every atom $`A`$ the number of nodes of a given IC-tree and finally we prove that $`P`$ is quasi recurrent wrt. such a level mapping.

###### Definition 31 (IC-tree)

An IC-tree for $`P\{Q\}`$ is a tree whose nodes are labelled with queries such that

* its branches are input-consuming derivations of $`P\{Q\}`$,
* every node $`Q`$ has exactly one descendant for every atom $`A`$ of $`Q`$ and every clause $`c`$ from $`P`$ such that $`A`$ is input-consuming resolvable wrt. $`c`$. This descendant is a resolvent of $`Q`$ and $`c`$ wrt. $`A`$.

In this tree, a node’s children consist of all its resolvents, “modulo renaming”, via an input-consuming derivation step wrt. all the possible choices of a program clause and a selected atom.

###### Lemma 32 (IC-tree 1)

An IC-tree for $`P\{Q\}`$ is finite iff all input-consuming derivations of $`P\{Q\}`$ are finite.

Proof. By definition, the IC-trees are finitely branching. The claim now follows by König’s Lemma. $`\mathrm{}`$

Notice that if an IC-tree for $`P\{Q\}`$ is finite then all the IC-trees for $`P\{Q\}`$ are finite.

For a program $`P`$ and a query $`Q`$, we denote by $`\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(Q)`$ the number of nodes in an IC-tree for $`P\{Q\}`$. The following properties of IC-trees will be needed.

###### Lemma 33 (IC-tree 2)

Let $`P`$ be a program, $`Q`$ be a query and $`T`$ be a finite IC-tree for $`P\{Q\}`$. Then

* for all non-root nodes $`Q^{}`$ in $`T`$, $`\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(Q^{})<\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(Q)`$,
* for all atoms $`A`$ of $`Q`$, $`\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(A)\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(Q)`$.

Proof. Immediate by Definition 31 of IC-tree. $`\mathrm{}`$

We can now prove the desired result.

###### Theorem 34

Let $`P`$ be a simply-moded and input-recursive program. If $`P`$ is input terminating then $`P`$ is quasi recurrent.

Proof. We show that there exists a moded level mapping $`||`$ for $`P`$ such that $`P`$ is quasi recurrent wrt. $`||`$.

Given an atom $`A`$, we denote with $`A^{}`$ an atom obtained from $`A`$ by replacing the terms filling in its output positions with fresh distinct variables. Clearly, we have that $`A^{}`$ is simply-moded. Then we define the following moded level mapping for $`P`$:

$$|A|=\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(A^{}).$$

Notice that, the level $`|A|`$ of an atom $`A`$ is independent from the terms filling in its output positions, i.e., $`||`$ is a moded level mapping. Moreover, since $`P`$ is input terminating and $`A^{}`$ is simply-moded (in particular, it is nicely-moded), all the input-consuming derivations of $`P\{A^{}\}`$ are finite. Therefore, by Lemma 32, $`\mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(A^{})`$ is defined (and finite), and thus $`|A|`$ is defined (and finite) for every atom $`A`$.

We now prove that $`P`$ is quasi recurrent wrt. $`||`$.

Let $`c:H𝐀,B,𝐂`$ be a clause of $`P`$ and $`H\theta 𝐀\theta ,B\theta ,𝐂\theta `$ be an instance of $`c`$ (for some substitution $`\theta `$). We show that $`\text{if }\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B)\text{ then }|H\theta |>|B\theta |`$.

Let $`H=p(𝐬,𝐭)`$. Hence, $`(H\theta )^{}=p(𝐬\theta ,𝐱)`$ where $`𝐱`$ is a sequence of fresh distinct variables. Consider a variant $`c^{}:H^{}𝐀^{},B^{},𝐂^{}`$ of $`c`$ variable disjoint from $`(H\theta )^{}`$. Let $`\rho `$ be a renaming such that $`c^{}=c\rho `$. Clearly, $`(H\theta )^{}`$ and $`H^{}`$ unify. Let $`\mu =\mathrm{𝑚𝑔𝑢}((H\theta )^{},H^{})=\mathrm{𝑚𝑔𝑢}((H\theta )^{},H\rho )=\mathrm{𝑚𝑔𝑢}(p(𝐬\theta ,𝐱),p(𝐬,𝐭)\rho )`$. By properties of substitutions (see \[Apt97\]), since $`𝐱`$ consists of fresh variables, there exists two relevant mgu $`\sigma _1`$ and $`\sigma _2`$ such that

* $`\sigma _1=\text{mgu}(𝐬\theta ,𝐬\rho )`$,
* $`\sigma _2=\text{mgu}(𝐱\sigma _1,𝐭\rho \sigma _1)`$.

Since $`𝐬\rho 𝐬\theta `$, we can assume that $`\mathrm{𝐷𝑜𝑚}(\sigma _1)\mathrm{𝑉𝑎𝑟}(𝐬\rho )`$. Because of standardization apart, since $`𝐱`$ consists of fresh variables, $`𝐱\sigma _1=𝐱`$ and thus $`\sigma _2=\text{mgu}(𝐱,𝐭\rho \sigma _1)`$. Since $`𝐱`$ is a sequence of variables, we can also assume that $`\mathrm{𝐷𝑜𝑚}(\sigma _2)\mathrm{𝑉𝑎𝑟}(𝐱)`$. Therefore $`\mathrm{𝐷𝑜𝑚}(\mu )\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((H\theta )^{}))\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H\rho ))`$. Moreover, since $`(𝐀^{},B^{},𝐂^{})\mu =(𝐀,B,𝐂)\rho \mu `$, we have that

$$(H\theta )^{}\stackrel{\mu }{}(𝐀,B,𝐂)\rho \mu $$

is an input-consuming derivation step, i.e., $`(𝐀,B,𝐂)\rho \mu `$ is a descendant of $`(H\theta )^{}`$ in an IC-tree for $`P\{(H\theta )^{}\}`$.

By definition of $`\mu `$, $`𝐬\theta =𝐬\rho \mu `$; hence

$$(\rho \mu )_{|\mathrm{𝐼𝑛}(H)}=\theta _{|𝐬}.$$
(10)
Let now $`B=p(𝐮,𝐯)`$. By (10) and the hypothesis that $`c`$ is input-recursive, that is $`\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(B))\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H))=\mathrm{𝑉𝑎𝑟}(𝐬)`$, it follows that

$$𝐮\rho \mu =𝐮(\rho \mu )_{|\mathrm{𝐼𝑛}(H)}=𝐮\theta _{|𝐬}=𝐮\theta .$$
(11)
Moreover, since $`c^{}`$ is simply-moded, $`\mathrm{𝐼𝑛}(H\rho )\mathrm{𝑂𝑢𝑡}(B\rho )=\mathrm{}`$. Hence, by definition of $`\mu `$ and standardization apart, $`\mathrm{𝐷𝑜𝑚}(\mu )\mathrm{𝑂𝑢𝑡}(B\rho )=\mathrm{}`$, i.e.,

$$𝐯\rho \mu =𝐯\rho .$$
(12)
Therefore, by (11) and (12), $`B\rho \mu =p(𝐮,𝐯)\rho \mu =p(𝐮\theta ,𝐯\rho )=(B\theta )^{}`$, i.e.,

$$B\rho \mu =(B\theta )^{}.$$
(13)
Hence,
$`\begin{array}{cccc}|H\theta |\hfill & =\hfill & \mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((H\theta )^{})\hfill & \text{by definition of }||\hfill \\ & >\hfill & \mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((𝐀,B,𝐂)\rho \mu )\hfill & \text{by Lemma }\text{33}\text{ (i)}\hfill \\ & \hfill & \mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(B\rho \mu )\hfill & \text{by Lemma }\text{33}\text{ (ii)}\hfill \\ & =\hfill & \mathrm{𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((B\theta )^{})\hfill & \text{by (}\text{13}\text{)}\hfill \\ & =\hfill & |B\theta |\hfill & \text{by definition of }||.\hfill \end{array}`$
$`\mathrm{}`$

## 7 Applicability

This section is intended to show through some examples the applicability of our results. Then, programs from various well-known collections are analyzed.

### 7.1 Examples

It is worth noticing that, since the definition of input-consuming derivation is independent from the textual order of the atoms in the clause bodies, the results we have provided (Theorems 20, 24 and 34) hold also in the case that programs and queries are *permutation* nicely- (or simply-) moded \[SHK98\], that is programs and queries which would be nicely- (or simply-) moded after a permutation of the atoms in the bodies. Therefore, for instance, we can apply Theorems 20 and 24 to the program $`\mathrm{𝙵𝙻𝙰𝚃𝚃𝙴𝙽}`$ as it is presented in \[Apt97\] (except for the replacement of “$``$” with “,”), i.e.,

| flatten(Xs,Ys) $``$flatten\_dl(Xs,Ys,\[ \]). |
| --- |
| flatten\_dl(\[ \],Ys,Ys). |
| flatten\_dl(X,\[X|Xs\],Xs) $``$constant(X), X $``$ \[ \]. |
| flatten\_dl(\[X|Xs\],Ys,Zs) $``$ | flatten\_dl(X,Ys,Y1s), |
|  | flatten\_dl(Xs,Y1s,Zs). |

where the atoms in the body of the last clause are permuted with respect to the version of Example 25.

Let us consider again the program APPEND of the introduction with its natural delay declaration:

| mode app(In,In,Out) |
| --- |
| app(\[ \],Ys,Ys). |
| app(\[H|Xs\],Ys,\[H|Zs\]) $``$app(Xs,Ys,Zs). |

Let $`𝒬`$ be the set of one-atom queries of the form app($`s`$,$`t`$,$`Z`$) where $`s`$ and $`t`$ are any terms and $`Z`$ is a variable disjoint from $`s`$ and $`t`$. Observe that $`𝒬`$ is closed under resolution: Each resolvent in a derivation starting in a query from $`𝒬`$ is still a query from $`𝒬`$. Moreover, because of the presence of the delay declaration, only atoms whose first argument is a non-variable term are allowed to be selected. Thus, selectable atoms have the form app($`s`$,$`t`$,$`Z`$) where

* $`s`$ is a non-variable term,
* $`t`$ is any term and $`Z`$ is a variable disjoint from $`s`$ and $`t`$.

Any derivation of APPEND starting in a query of $`𝒬`$ is similar to an input-consuming one. This follows from the fact that for any selectable atom $`A`$ and clause’s head $`H`$, there exists a mgu $`\theta `$ which does not affect the input arguments of $`A`$. In fact, let $`A`$ be a selectable atom of $`𝒬`$. If $`A`$ unifies with the head of the first clause then, by $`(1)`$, $`s`$ is the empty list \[ \] and $`\theta =\mathrm{𝑚𝑔𝑢}(A,H)=\{\mathrm{𝚈𝚜}/t,Z/t\}`$. Otherwise, If $`A`$ unifies with the head of the second clause then, by $`(1)`$, $`s`$ is a term of the form \[$`s_1`$|$`s_2`$\] and $`\theta =\mathrm{𝑚𝑔𝑢}(A,H)=\{𝙷/s_1,\mathrm{𝚇𝚜}/s_2,\mathrm{𝚈𝚜}/t,Z/[s_1|\mathrm{𝚉𝚜}]\}`$. By $`(2)`$ it follows that, in both cases, $`s\theta =s`$ and $`t\theta =t`$, i.e., $`\theta `$ does not affect the input arguments of $`A`$.

Moreover, it is easy to check that APPEND is quasi recurrent wrt. the moded level mapping depicted in Example 17. Since it is nicely-moded, by applying Theorem 20 it follows that it is input terminating. By the arguments above, we can conclude that all the derivations of $`\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}`$ in presence of the delay declaration $`d_1`$ and starting in a (permutation) nicely-moded query are finite. Hence, in particular, we can state that all the derivations of APPEND starting in the query $`Q_1`$ of the introduction, which is not nicely-moded but it is permutation nicely-moded, are finite.

### 7.2 Benchmarks

In order to assess the applicability of our results, we have looked into four collections of logic programs, and we have checked those programs against the three classes of programs: (permutation) nicely-moded, input terminating and quasi recurrent programs. The results are reported in Tables 1 to 4. These tables clearly show that our results apply to the large majority of the programs considered.

In Table 1 the programs from Apt’s collection are considered, see \[Apt97\]. The programs from the DPPD’s collection, maintained by Leuschel and available at the URL: http://dsse.ecs.soton.ac.uk/$``$mal/systems/dppd.html, are referred to in Table 2. Table 3 considers various programs from Lindenstrauss’s collection (see the URL: http://www.cs.huji.ac.il/$``$naomil). Finally, in Table 4 one finds the (almost complete) list of programs by F. Bueno, M. Garcia de la Banda and M. Hermenegildo that can be found at the URL: http://www.clip.dia.fi.upm.es.

For each program we specify the name and the modes of the main procedure. Then we report whether or not the program is (permutation) nicely-moded (NM), input terminating (IT), and quasi recurrent (QR). Notice that for programs which are not input terminating, because of Theorem 20, it does not make sense to check whether or not they are quasi recurrent. For this reason, we leave blank the cells in the column QR corresponding to non-input terminating programs.

Finally, Table 5 reports the list of programs from previous tables which have been found to be input terminating but not quasi recurrent. For these programs, the notion of quasi recurrency does not provide an exact characterization of input termination. In particular, Theorem 34 does not apply. In order to understand which of the hypothesis of the theorem does not hold, we report in Table 5 whether or not these programs are simply-moded (SM) and input-recursive (IR).

## 8 Conclusion and Related Works

In this paper we studied the properties of input-consuming derivations of nicely-moded programs.

This study is motivated by the widespread use of programs using dynamic scheduling controlled by delay declarations. In fact, as we have motivated in Section 3.2, we believe that in most practical programs employing delay declarations these constructs are used for guaranteeing that the derivation steps are input-consuming.

In the first place, we showed that for nicely-moded programs a weak version of the well-known switching lemma holds: If, given a query $`(𝐀,B,𝐂,D,𝐄)`$, $`D`$ is selected before $`B`$ in an input-consuming derivation, then the two resolution steps can be interchanged while maintaining that the derivation is input-consuming.

Secondly, we presented a method for proving termination of programs and queries which are (permutation) nicely-moded. We also showed a result characterizing a class of input terminating programs.

In the literature, the paper most related to the present one is certainly \[Sma99b\]. Our results strictly generalize those in \[Sma99b\] in the fact that we drop the condition that programs and queries have to be well-moded. This is particularly important in the formulation of the queries. For instance, in the program FLATTEN of Example 25, our results show that every input-consuming derivation starting in a query of the form $`\mathrm{𝚏𝚕𝚊𝚝𝚝𝚎𝚗}(t,s)`$ terminates provided that $`t`$ is linear and disjoint from $`s`$, while the results of \[Sma99b\] apply only if $`t`$ is a ground term. Note that well-moded queries (in well-moded programs) never terminate by deadlock, since the leftmost atom of each resolvent is ground in its input positions and hence selectable. This does not hold for nicely-moded queries which might deadlock. Our method allows us thus to cope also with this more difficult situation: For instance we can prove that all derivations of APPEND starting in $`\mathrm{𝚊𝚙𝚙}(𝚇,𝚈,𝚉)`$ are terminating. In practice the result of \[Sma99b\] identify a class of programs and queries which is both terminating and *deadlock free*. While deadlock is clearly an undesirable situation, there are various reasons why one might want to prove termination independently from the absence of deadlock: In the first place, one might want to prove absence of deadlock using a different tool than by employing well-moded programs. Secondly, in some situations absence of deadlock might be difficult or impossible to prove, like in a modular context in which the code of some module is not known, hence not analyzable: consider for instance the query generator\_1(X1s), generator\_2(X2s), append(X1s,X2s,Zs)., where the generators are defined in different modules; our results allow us to demonstrate that if the generators terminate, then the above query terminates. On the other hand, one cannot determine whether it is deadlock free unless one has a more precise specification of the generators. Thirdly, it is well-known that one of the goals of dynamic scheduling is precisely enforcing termination; in this respect a deadlock can be regarded as the situation in which “all else failed”. Our system allows us to check how effective dynamic scheduling is in enforcing termination.

Concluding our comparison with \[Sma99b\], for the class of (permutation) simply-moded and input-recursive programs, we provide an exact characterization of input termination. A similar result is not present in \[Sma99b\].

Apt and Luitjes \[AL95\] have also tackled the problem of the termination of programs in presence of dynamic scheduling. The techniques employed in it are based on determinacy checks and the presence of successful derivations, thus are completely different from ours. It is nevertheless worth mentioning that \[AL95\] reports a special ad-hoc theorem, in order to prove that, if $`u`$ is linear and disjoint from $`s`$ then the query $`\mathrm{𝚊𝚙𝚙}(s,t,u)`$ terminates. This is reported in order to show the difficulties one encounters in proving termination in presence of dynamic scheduling. Now, under the further (mild) additional condition that $`u`$ be disjoint from $`t`$, the termination of $`\mathrm{𝚊𝚙𝚙}(s,t,u)`$ is a direct consequence of our main result.

Another related paper is the one by Marchiori and Teusink \[MT95\]. However, Marchiori and Teusink make a strong restriction on the selection rule, which has to be *local*; this restriction actually forbids any form of coroutining. Moreover, \[MT95\] allows only *safe* delay declarations; we do not report here the definition of *safe* delay declaration, we just say that it is rather restrictive: For instance, the delay declaration we have used for APPEND is not safe (a safe one would be delay app(X,\_,\_) until list(X)). Actually, their requirements go beyond ensuring that derivations are input-consuming.

Applicability and effectiveness of our results have been demonstrated by matching our main definitions against the programs of four public program lists. These benchmarks showed that most of the considered programs are nicely-moded (for a suitable mode) and quasi recurrent (wrt. a suitable level mapping).


format: text

text:
# I Introduction

## I Introduction

Semileptonic weak hadron decays provide useful information on form factors of the weak current. The lepton pair can then be replaced with a hadron, permitting the calculation of nonleptonic decays. Although this hadron can re-interact with the rest of the system, the effects of this re-interaction sometimes can be neglected or evaluated. In such cases one is employing the factorization hypothesis. An early version of this hypothesis  was recently justified for certain decays of hadrons containing heavy quarks .

In the present paper we update and test some factorization predictions first made a number of years ago . We compare values of the Cabibbo-Kobayashi-Maskawa matrix element $`|V_{cb}|`$ and form factor shapes obtained from (1) the differential distribution $`d\mathrm{\Gamma }(\overline{B}^0D^{()+}l^{}\overline{\nu }_l)/dq^2`$  and (2) the color-favored two-body nonleptonic decays $`\overline{B}^0D^{()+}(\pi ^{},\rho ^{},a_1^{})`$. We find that consistency between nonleptonic and semileptonic determinations is at least as good as that among the semileptonic determinations themselves.

Using a combined fit to semileptonic and nonleptonic decays and the measured value of the $`D_s`$ meson decay constant $`f_{D_s}`$, we then predict the rates for $`\overline{B}^0D^{()+}D_s^{()}`$ and find that they are in accord with experiment. We thus find that factorization holds not only in color-favored cases in which the current produces a light meson, where it has been justified , but also when the current produces a heavy meson, where no such justification has been presented. The importance of such processes has recently been stressed by Lipkin . We also find that new experimental ratios of helicity amplitudes for color-favored processes agree with predictions. We shall ignore small non-factorizable contributions to color-favored $`\overline{B}^0`$ decays as discussed, for example, in Ref. .

In Section II we review factorization predictions for the decays $`\overline{B}^0W^{}D^{()+}`$, where the virtual $`W^{}`$ produces either a lepton pair $`l^{}\overline{\nu }_l`$ or a hadron $`\pi ^{}`$, $`\rho ^{}`$, $`a_1^{}`$, $`D_s^{}`$, or $`D_s^{}`$. These processes are purely color-favored. We do not consider the corresponding $`B^{}`$ decays, for which the nonleptonic processes receive both color-favored and color-suppressed contributions. We then (Section III) discuss the differential distributions $`d\mathrm{\Gamma }(\overline{B}^0D^{()+}l^{}\overline{\nu }_l)/dq^2`$ and the information they can provide regarding the values of $`|V_{cb}|`$ and the form factor slope at the normalization point. Results of fits to $`\overline{B}^0`$ two-body decays to charmed final states are presented and compared with those from semileptonic decays in Section IV. We discuss the predictions of the factorization hypothesis for decays in which the weak current produces a $`D_s^{()}`$ in Section V and for ratios of helicity amplitudes in Section VI. Section VII concludes. An Appendix summarizes parameters of error ellipses used in combining data.

## II Notation and predictions

We review notation which is described in more detail in Ref. . We consider processes in which a semileptonic $`\overline{B}^0`$ decay of the form shown in Fig. 1(a) can be related to the corresponding decay with the lepton pair replaced by a quark pair, illustrated in Fig. 1(b). The matrix element for production of a pseudoscalar meson $`P(q)`$ of 4-momentum $`q`$ from the vacuum by the axial vector current is

$$P(q)|A_\mu |0=if_Pq_\mu ,$$
(1)
while that for production of a vector meson by the vector current is

$$V(q)|V_\mu |0=ϵ_\mu ^{}M_Vf_V,$$
(2)
and that for production of an axial vector meson by the axial vector current is

$$A(q)|A_\mu |0=ϵ_\mu ^{}M_Af_A,$$
(3)
The form factors for the $`\overline{B}^0(v)D^{()}(v^{})`$ transitions are described in the heavy-quark limit by one universal function of the Lorentz-invariant variable $`wvv^{}`$, where $`v`$ and $`v^{}`$ are invariant four-velocities: $`vp_{\overline{B}^0}/m_B`$, $`v^{}p_{D^{()}}/m_{D^{()}}`$. We take $`c=1`$ and note that $`q=pp^{}`$. Another expression for $`w`$ is then

$$w=\frac{p_Bp_{D^{()}}}{m_Bm_{D^{()}}}=\frac{m_B^2+m_{D^{()}}^2q^2}{2m_Bm_{D^{()}}}.$$
(4)
\[A variable $`(vv^{})^2=2(1w)`$ was called $`w`$ in Ref. .\] If $`ϵ`$ denotes the polarization vector of the final $`D^{}`$, we may write

$$D(v^{})|V_\mu |B(v)=\sqrt{m_Dm_B}F_V(w)(v+v^{})_\mu ,$$
(5)
$$D^{}(v^{},ϵ)|A_\mu |B(v)=\sqrt{m_Dm_B}F_A(w)[ϵ_\mu ^{}(1+vv^{})ϵ^{}vv_\mu ^{}],$$
(6)
$$D^{}(v^{},ϵ)|V_\mu |B(v)=i\sqrt{m_Dm_B}F_V(w)ϵ_{\mu \nu \alpha \beta }ϵ^\nu v^\alpha v_{}^{}{}_{}{}^{\beta }.$$
(7)
We take $`m_B=5.28`$ GeV and $`m_D=m_{D^+}=2.01`$ GeV or $`m_{D^+}=1.87`$ GeV depending on the final-state charmed meson. The maximum momentum transfer occurs when the recoiling $`D^{()}`$ is at rest in the $`B`$ rest frame, so $`q_{\mathrm{max}}^2=(m_Bm_{D^{()}})^2`$ and hence $`w1`$. Another useful relation is

$$y\frac{q^2}{m_B^2}=12w\sqrt{\zeta ^{()}}+\zeta ^{()},\zeta ^{()}\frac{m_{D^{()}}^2}{m_B^2}.$$
(8)
The differential decay width as a function of $`w`$ for $`\overline{B}^0D^{()+}l^{}\overline{\nu _l}`$ can then be written as

$$\frac{d\mathrm{\Gamma }}{dw}=\frac{G_F^2}{48\pi ^3}|V_{cb}|^2m_B^2m_{D^{()}}^3\sqrt{w^21}f^{()}(w)|F_{V,A}(w)|^2,$$
(9)
where for $`BDl\overline{\nu _l}`$

$$f(w)=(w^21)(1+\sqrt{\zeta })^2,$$

for $`BD_T^{}l\overline{\nu _l}`$

$$f_T^{}(w)=4wy(w+1),$$

and for $`BD_L^{}l\overline{\nu _l}`$

$$f_L^{}(w)=(1\sqrt{\zeta ^{}})^2(w+1)^2.$$

We shall take the form factors $`F_{V,A}(w)`$ to be parametrized as in Ref. . The form factor $`F_V(w)`$ governing the process $`\overline{B}^0D^+l^{}\overline{\nu }_l`$ can be expressed as

$$F_V(w)=F_V(1)\times \left[18\rho _{F_V}^2z+(51\rho _{F_V}^210)z^2(252\rho _{F_V}^284)z^3\right],$$
(10)
where $`z(\sqrt{w+1}\sqrt{2})/(\sqrt{w+1}+\sqrt{2})`$ (the corresponding variable for elastic $`BB`$ transitions, a natural one for discussing analyticity in dispersion relations, was introduced in ), while the form factor $`F_A(w)`$ governing $`BD^{}l\overline{\nu }_l`$ is related to the axial-vector form factor $`A_1(w)`$ by

$$\left[1+\frac{4w}{w+1}\frac{12w\sqrt{\zeta ^{}}+\zeta ^{}}{(1\sqrt{\zeta ^{}})^2}\right]\left|F_A(w)\right|^2=$$

$$\left\{2\frac{12w\sqrt{\zeta ^{}}+\zeta ^{}}{(1\sqrt{\zeta ^{}})^2}\left[1+\frac{w1}{w+1}R_1(w)^2\right]+\left[1+\frac{w1}{1\sqrt{\zeta ^{}}}\left(1R_2(w)\right)\right]^2\right\}\left|A_1(w)\right|^2.$$
(11)
$`A_1(w)`$ can similarly be parametrized as

$$A_1(w)=A_1(1)\times \left[18\rho _{A_1}^2z+(53\rho _{A_1}^215)z^2(231\rho _{A_1}^291)z^3\right].$$
(12)
These forms are motivated by dispersion relations . $`R_1(w)`$ and $`R_2(w)`$ are given by

$`R_1(w)`$ $`=`$ $`R_1(1)0.12(w1)+0.05(w1)^2,`$
$`R_2(w)`$ $`=`$ $`R_2(1)+0.11(w1)0.06(w1)^2.`$ (13)
In this paper we use the CLEO experimental results for $`R_1(1)`$ and $`R_2(1)`$ :

$`R_1(1)`$ $`=`$ $`1.18\pm 0.30\pm 0.12,`$ (14)
$`R_2(1)`$ $`=`$ $`0.71\pm 0.22\pm 0.07.`$ (15)
As we know, $`\rho _{F_V}^2`$ and $`\rho _{A_1}^2`$ are the slope parameters for the form factors $`F_V(w)`$ and $`A_1(w)`$ at zero recoil, respectively. The difference between $`\rho _{A_1}^2`$ and $`\rho _{F_A}^2`$, the slope parameter for $`F_A(w)`$ at $`w=1`$, is predicted to be $`\rho _{F_A}^2\rho _{A_1}^2=0.21`$ . Recall that $`\rho _{F_V}^2`$ and $`\rho _{F_A}^2`$ are actually the same in the single pole model. To make a connection between $`F_{V,A}(w)`$ and the single pole form factor :

$$_{V,A}(w)=_{V,A}(1)/[12(1w)/w_{0(V,A)}^2],$$
(16)
we assume $`\rho _{F_V}^2=\rho _{A_1}^20.21`$. From now on we will simplify $`\rho _{A_1}^2`$ as $`\rho ^2`$. This parameter describes the slope of the Isgur-Wise  form factor at the zero-recoil point: $`\rho ^2=[dF_{A_1}(w)/dw]|_{w=1}`$ (see, e.g., ).

At $`w=1`$, the vector and axial vector form factors are expected to behave as $`F_V(1)=\eta _V(1+\delta _{1/m_b})`$, $`F_A(1)=\eta _A(1+\delta _{1/m_b^2})`$. Here $`\eta _V=1.022\pm 0.004`$ and $`\eta _A=0.960\pm 0.007`$ are QCD corrections . The terms $`\delta _{1/m_b}`$ and $`\delta _{1/m_b^2}`$ are non-perturbative in origin, and correspond physically to the excitation of states other than $`D`$ and $`D^{}`$. Lacking a reliable method for estimating the term $`\delta _{1/m_b}`$ in $`F_V(1)`$ , we set it equal to zero. The absence of a $`\delta _{1/m_b}`$ term in $`F_A(1)`$ is the subject of Luke’s theorem . We take $`\delta _{1/m_b^2}=0.05\pm 0.035`$ , with the product $`F_A(1)=0.913\pm 0.042`$ as used in Ref. . Eq. (9) can then be integrated with respect to $`w`$ to yield predicted decay rates as functions of the two parameters $`\rho ^2`$ and $`|V_{cb}|`$.

The decay widths of some nonleptonic modes may be obtained under the assumption of factorization. For simplicity we assume all $`\overline{B}^0D^+M^{}`$ transitions to involve $`F_V(w_M)`$ and all $`\overline{B}^0D^+M^{}`$ transitions to involve $`F_A(w_M^{})`$, where

$$w_M(m_B^2+m_D^2m_M^2)/(2m_Bm_D),w_M^{}(m_B^2+m_D^{}^2m_M^2)/(2m_Bm_D^{}).$$
(17)
We then find

$`\mathrm{\Gamma }(\overline{B}^0D^+\pi ^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_\pi ^2|a_1|^2|F_V(w_\pi )|^2(1\sqrt{\zeta })^2`$ (18)
$`\times \lambda ^{1/2}(1,\zeta ,\zeta _\pi ){\displaystyle \frac{[(1+\sqrt{\zeta })^2\zeta _\pi ]^2}{4\sqrt{\zeta }}}`$
$`\mathrm{\Gamma }(\overline{B}^0D_{}^{}{}_{}{}^{+}\pi ^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_\pi ^2|a_1|^2|F_A(w_\pi ^{})|^2(1+\sqrt{\zeta ^{}})^2`$ (19)
$`\times \lambda ^{1/2}(1,\zeta ^{},\zeta _\pi ){\displaystyle \frac{\lambda (1,\zeta ^{},\zeta _\pi )}{4\sqrt{\zeta ^{}}}}`$
$`\mathrm{\Gamma }(\overline{B}^0D^+\rho ^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_\rho ^2|a_1|^2|F_V(w_\rho )|^2(1+\sqrt{\zeta })^2`$ (20)
$`\times \lambda ^{1/2}(1,\zeta ,\zeta _\rho ){\displaystyle \frac{\lambda (1,\zeta ,\zeta _\rho )}{4\sqrt{\zeta }}}`$
$`\mathrm{\Gamma }(\overline{B}^0D_{}^{}{}_{}{}^{+}\rho ^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_\rho ^2|a_1|^2|F_A(w_\rho ^{})|^2N(\zeta ^{},\zeta _\rho )`$ (21)
$`\times \lambda ^{1/2}(1,\zeta ^{},\zeta _\rho ){\displaystyle \frac{(1+\sqrt{\zeta ^{}})^2\zeta _\rho }{4\sqrt{\zeta ^{}}}}`$
$`\mathrm{\Gamma }(\overline{B}^0D^+a_1^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_{a_1}^2|a_1|^2|F_V(w_{a_1})|^2(1+\sqrt{\zeta })^2`$ (22)
$`\times \lambda ^{1/2}(1,\zeta ,\zeta _{a_1}){\displaystyle \frac{\lambda (1,\zeta ,\zeta _{a_1})}{4\sqrt{\zeta }}}`$
$`\mathrm{\Gamma }(\overline{B}^0D_{}^{}{}_{}{}^{+}a_1^{})`$ $`=`$ $`{\displaystyle \frac{G_F^2}{32\pi }}|V_{cb}|^2|V_{ud}|^2m_B^3f_{a_1}^2|a_1|^2|F_A(w_{a_1}^{})|^2N(\zeta ^{},\zeta _{a_1})`$ (23)
$`\times \lambda ^{1/2}(1,\zeta ^{},\zeta _{a_1}){\displaystyle \frac{(1+\sqrt{\zeta ^{}})^2\zeta _{a_1}}{4\sqrt{\zeta ^{}}}}`$
where $`\zeta _M=m_M^2/m_B^2`$ while

$$N(\zeta ^{},\zeta _M)(1\sqrt{\zeta ^{}})^2[(1+\sqrt{\zeta ^{}})^2\zeta _M]+4\zeta _M(1+\zeta ^{}\zeta _M),$$
(24)
$$\lambda (a,b,c)a^2+b^2+c^22ab2ac2bc.$$
(25)
The QCD correction $`|a_1|`$ is taken to be 1.05 for all processes; this is a sufficiently good approximation to the actual situation, in which values differ by less than a percent from process to process . In the limit of small $`m_\pi `$, the results (18) and (19) are special cases of the simple Bjorken relation

$$\mathrm{\Gamma }(\overline{B}^0D^{()+}\pi ^{})=6\pi ^2f_\pi ^2|V_{ud}|^2|a_1|^2\frac{d\mathrm{\Gamma }(\overline{B}^0D^{()+}l^{}\overline{\nu }_l)}{dq^2}|_{q^2=m_\pi ^2}.$$
(26)
## III Semileptonic decays

The CLEO Collaboration  at the Cornell Electron Storage Ring (CESR) and the ALEPH, DELPHI, and OPAL Collaborations  at LEP  have measured the spectra in lepton-pair squared effective mass $`q^2`$ (equivalently, in the Isgur-Wise variable $`w`$) for the decay $`\overline{B}^0D^+l^{}\overline{\nu }_l`$. The spectra may then be fitted for $`F_A(1)|V_{cb}|`$ and $`\rho ^2`$. There is a strong correlation between the two parameters. The results are shown in Fig. 2 and Table I, where we have taken $`F_A(1)=0.913\pm 0.042`$ as in Ref. . Our fitted parameters for the CLEO data differ slightly from those presented by the collaboration itself, since we wished to generate an error ellipse and therefore fitted the spectral points directly without taking account of point-to-point correlations. For comparison, CLEO quotes $`|V_{cb}|=0.0464\pm 0.0020(\mathrm{stat}.)\pm 0.0021(\mathrm{syst}.)\pm 0.0021(\mathrm{theor}.)`$ and $`\rho ^2=1.67\pm 0.11\pm 0.22`$. The combined fit implies $`|V_{cb}|=0.0399\pm 0.0023`$ and $`\rho ^2=1.27\pm 0.26`$.

The CLEO Collaboration has also measured the spectrum for the decay $`\overline{B}^0D^+l^{}\overline{\nu }_l`$ . A fit to this spectrum with the form factor (10) and with $`F_V(1)=1.022`$ yields $`|V_{cb}|=0.0459_{0.0044}^{+0.0053}`$ and $`\rho ^2=1.33_{0.25}^{+0.21}`$.

## IV Nonleptonic two-body decays and combined fit

We fit rates for nonleptonic two-body decays \[Eqs. (1823)\] to experimental averages, allowing (as in the fit to semileptonic spectra) for variation of $`|V_{cb}|`$ and $`\rho ^2`$. We use the averages of Ref.  except for modes for which new values have been presented ; these are summarized and averaged in Table II. For the decays involving $`D_s^{()}`$ (to be discussed in the next Section) the last errors in the second and third columns of Table II refer to a common systematic error in $`D_s`$ branching ratios, which are based on $`(D_s^+\varphi \pi ^+)=(3.6\pm 0.9)\%`$, and are combined accordingly. In our fits we use $`|V_{ud}|=0.974`$, $`\tau _B=1.548\mathrm{ps}`$, and $`f_\pi =131\mathrm{MeV}`$. $`f_\rho `$ and $`f_{a_1}`$ are determined to be $`209\mathrm{MeV}`$ and $`229\mathrm{MeV}`$ , respectively, from the branching ratios for $`\tau \rho \nu `$ and $`\tau a_1\nu `$.

The fit to two-body nonleptonic decays alone gives rise to a different correlation between $`|V_{cb}|`$ and $`\rho ^2`$ than that to the $`\overline{B}^0D^{()+}l^{}\overline{\nu }_l`$ spectra, since the decay rates are dominated by low $`q^2`$ and hence high $`w`$. Contours of $`\mathrm{\Delta }\chi ^2=1(1\sigma `$) for nonleptonic decays are shown along with the $`\mathrm{\Delta }\chi ^2=1`$ contours for $`\overline{B}^0D^{()+}l^{}\overline{\nu }_l`$ spectra in Fig. 3. Also shown are the $`\mathrm{\Delta }\chi ^2=1`$ contours for the combined fit without and with common theoretical errors. We find $`|V_{cb}|=0.0415\pm 0.0022`$ and $`\rho ^2=1.52\pm 0.11`$. The results are summarized in Table III. The error on $`|V_{cb}|`$ is dominated by the theoretical uncertainty on the form factors at $`w=1`$, which we take to have the same fractional value (0.042/0.913) for vector and axial form factors.

The fitted branching ratios are compared with experimental data in Table IV. We also show the predictions of a recent investigation based on a more detailed application of the factorization hypothesis . The quality of the fit is acceptable except for a slight excess in the predicted branching ratio for $`\overline{B}^0D^+\pi ^{}`$.

It is interesting to compare the form factors based on Eqs. (10) and (11) with the simple pole model (16) , where $`m_Bw_{0(V,A)}`$ has the interpretation of the mass of a pole in the weak $`bc`$ (V,A) current. The axial form factor for $`\rho _{A_1}^2=1.52`$ is compared with a pole model with $`w_{0A}=1.17`$ in Fig. 4. Also shown are CLEO  and DELPHI  data points. The pole-model form factor is almost indistinguishable from that  motivated by dispersion relations. The value $`w_{0A}=1.12\pm 0.17`$, found in Ref. , is consistent with the present determination $`w_{0A}=1.17\pm 0.08`$.

The vector form factor (10) is characterized by a slope parameter $`\rho _{F_V}^2=\rho _{A_1}^20.21`$  and hence $`\rho _{F_V}^2=1.31`$. It is compared to a pole form factor with $`w_{0V}=1.14`$ and to the CLEO data  in Fig. 5. Thus, a nearly universal pole position characterizes the vector and axial form factors, as in Ref. . The CLEO data lie slightly above the predicted form factor but have the same $`w`$ dependence, as one can also see in Fig. 3. It should be recalled that, in contrast to the case of the axial-vector form factor, theoretical estimates of the $`𝒪(1/m_b)`$ correction to the vector form factor are lacking . The normalization of the CLEO data may reflect our ignorance of this correction.

## V $`D_s^{()}`$ production by the weak current

When the $`q\overline{q}^{}`$ meson in Fig. 1(b) is a $`D_s^{}`$ or $`D_s^{}`$, Eqs. (1823) can be used for the respective predictions for $`\mathrm{\Gamma }(\overline{B}^0D^+D_s^{})`$, $`\mathrm{\Gamma }(\overline{B}^0D^+D_s^{})`$, $`\mathrm{\Gamma }(\overline{B}^0D^+D_s^{})`$, and $`\mathrm{\Gamma }(\overline{B}^0D^+D_s^{})`$ by replacing $`f_\pi f_{D_s}`$, $`f_\rho f_{D_s^{}}`$, $`\zeta _\pi \zeta _{D_s}m_{D_s}^2/m_B^2`$, $`\zeta _\rho \zeta _{D_s^{}}m_{D_s^{}}^2/m_B^2`$, and other corresponding substitutions of kinematic variables $`w`$ and $`N`$. We shall assume $`f_{D_s^{}}=f_{D_s}=270\pm 16\pm 34`$ MeV based on an experimental average of rates for $`D_s\mu \nu `$ and $`D_s\tau \nu `$ ; the latter error is the common systematic error associated with a 25% uncertainty in the branching ratio for $`D_s^+\varphi \pi ^+`$. (For comparison, the value of $`259\pm 74`$ MeV was found in Ref.  by utilizing the observed branching ratios of processes in which the weak current produced a $`D_s`$ or $`D_s^{}`$.)

We then predict the branching ratios for $`D_s^{()}`$ production by the weak current shown in Table V. Experimental values are from Ref.  ($`D^+D_s^{()}`$) or Table II ($`D^+D_s^{()}`$). The predictions have an overall 25% uncertainty associated with all $`D_s`$ branching ratios. They are as well obeyed as those for the light mesons.

An additional prediction involving heavy meson production by the weak current  is that $`(\overline{B}^0D^+D^{})/(\overline{B}^0D^+D_s^{})=0.13(f_D/f_{D_s})^20.09`$, where $`f_D`$ and $`f_{D_s}`$ are the decay constants for the nonstrange and strange $`D`$ mesons. The experimental value for this ratio  is $`0.06_{0.03}^{+0.04}`$.

## VI Ratios of helicity amplitudes

The decays of spinless particles to two vector mesons are describable  by amplitudes $`A_0`$ (longitudinal polarization), $`A_{}`$ (linear parallel polarization) and $`A_{}`$ (linear perpendicular polarization), normalized such that $`|A_0|^2+|A_{}|^2+|A_{}|^2=1`$. Factorization predicts $`(|A_0|^2,|A_{}|^2,|A_{}|^2)=(88,10,2)\%`$ for $`\overline{B}^0D^+D_s^{}`$ and (55,39,6)% for $`\overline{B}^0D^+\rho ^{}`$. Experimental values are only quoted for $`|A_0|^2`$: $`(87.8\pm 3.4\pm 3.0)\%`$ for $`\overline{B}^0D^+D_s^{}`$  and $`(50.6\pm 13.9\pm 3.6)\%`$ for $`\overline{B}^0D^+\rho ^{}`$ . These agree with the predictions, as does the intermediate case of $`\rho ^{}(1418)`$ production .

## VII Conclusions

New data on $`B`$ meson decays have improved the precision of tests of some early factorization predictions , and yield a value $`|V_{cb}|=0.0415\pm 0.0022`$ when CLEO and LEP data on $`\overline{B}^0D^{()+}l^{}\overline{\nu }_l`$ spectra are combined with two-body nonleptonic decays $`\overline{B}^0D^{()+}(\pi ^{},\rho ^{},a_1^{})`$. The slope of the universal Isgur-Wise form factor at the normalization point $`w=1`$ is found to be described by the parameter $`\rho ^2=1.52\pm 0.11`$. These values are only slightly different from those based on $`\overline{B}^0D^{()+}l^{}\overline{\nu }_l`$ spectra alone, indicating that factorization for color-favored decays and universality of $`\overline{B}D^{()}`$ form factors are reasonable approximations. Consistency between nonleptonic and semileptonic determinations is at least as good as that among the semileptonic processes themselves. Our neglect of $`𝒪(1/m_b)`$ corrections to the vector form factor may underestimate the rate for $`\overline{B}^0D^+l^{}\overline{\nu }_l`$ slightly.

Satisfactory rates for processes involving $`D_s^{()}`$ production by the weak current are obtained when the world average of direct measurements for $`f_{D_s}`$ is used, and when it is assumed that $`f_{D_s^{}}=f_{D_s}`$. Ratios of helicity amplitudes for color-favored processes are also found to be in accord with predictions.

## Acknowledgments

We thank Elisabetta Barberio, Karl Ecklund, Roger Forty, Richard Hawkings, Jon Thaler, and Alan Weinstein for discussions. This work was supported in part by the United States Department of Energy through Grant No. DE FG02 90ER40560, and in part by the U. S. – Israel Binational Science Foundation through Grant No. 98-00237.

## Appendix: Parametrization of error ellipses

In order to combine results of fits to semileptonic decays in the absence of the ALEPH and DELPHI raw spectra, we have parametrized their fits in terms of error ellipses corresponding to $`\mathrm{\Delta }\chi ^2=1`$, and generated corresponding ellipses for our own fits to CLEO and DELPHI data. The equations describing these ellipses are given below. Also shown are the contributions to $`\mathrm{\Delta }\chi ^2`$ for each set of $`\overline{B}^0D^+l^{}\overline{\nu }_l`$ data when $`x\rho ^2`$ and $`y|V_{cb}|`$ are taken to equal their values $`x=1.52`$ and $`y=0.0415`$ in the global fit. The corresponding $`\mathrm{\Delta }\chi ^2`$ value is $`4.02`$ for the sum of the nonleptonic modes listed in Table IV, which, when combined with the $`\mathrm{\Delta }\chi ^2`$ values for the semileptonic spectra, leads to a total of $`\mathrm{\Delta }\chi ^2=23.2`$ for the fit to five semileptonic spectra and six nonleptonic decay rates. The largest source of this $`\mathrm{\Delta }\chi ^2`$ (10.3) is the higher overall scale of the $`\overline{B}^0D^+l^{}\overline{\nu }_l`$ spectrum measured by CLEO, with some contribution also from the disparity between the CLEO and ALEPH fits. In comparison with these disagreements among purely semileptonic processes, the fits to nonleptonic decays do not fare badly at all.

CLEO:

$`41.8814(xx_c)^25174.3(xx_c)(yy_c)+238793(yy_c)^2`$ $`=`$ $`1;`$
$`x_c=1.58;y_c=0.0461;\mathrm{\Delta }\chi ^2`$ $`=`$ $`3.78;`$
ALEPH:

$`9.6816(xx_a)^22554.0(xx_a)(yy_a)+287560(yy_a)^2`$ $`=`$ $`1;`$
$`x_a=0.74;y_a=0.0361;\mathrm{\Delta }\chi ^2`$ $`=`$ $`3.52;`$
OPAL:

$`19.4601(xx_o)^23771.3(xx_o)(yy_o)+379980(yy_o)^2`$ $`=`$ $`1;`$
$`x_o=1.44;y_o=0.0414;\mathrm{\Delta }\chi ^2`$ $`=`$ $`0.10;`$
DELPHI:

$`14.1777(xx_d)^22856.4(xx_d)(yy_d)+246120(yy_d)^2`$ $`=`$ $`1;`$
$`x_d=1.22;y_d=0.0378;\mathrm{\Delta }\chi ^2`$ $`=`$ $`1.47;`$
CLEO+ALEPH+OPAL+DELPHI (without common theoretical normalization error; divide all coefficients by 2.850 for ellipse with this error):

$`85.2008(x\overline{x})^214356(x\overline{x})(y\overline{y})+1152453(y\overline{y})^2`$ $`=`$ $`1;`$
$`\overline{x}=1.27;\overline{y}=0.0399;`$
CLEO+ALEPH+OPAL+DELPHI+DECAYS (without common theoretical normalization error; divide all coefficients by 3.514 for ellipse with this error):

$`1059.7(x\stackrel{~}{x})^286781(x\stackrel{~}{x})(y\stackrel{~}{y})+2524400(y\stackrel{~}{y})^2`$ $`=`$ $`1;`$
$`\stackrel{~}{x}=1.52;\stackrel{~}{y}=0.0415;`$