format: text

text:
# Semantics and Termination of Simply-Moded Logic Programs with Dynamic SchedulingThis paper is the long version of [8]. It contains the proofs omitted there for space reasons.

## 1 Introduction

### 1.1 Background

Logic programming is based on giving a computational interpretation to a fragment of first order logic. Kowalski  advocates the separation of the logic and control aspects of a logic program and has coined the famous formula

> Algorithm = Logic + Control.

The programmer should be responsible for the logic part. The control should be taken care of by the logic programming system.

In reality, logic programming is far from this ideal. Without the programmer being aware of the control and writing programs accordingly, logic programs would usually be hopelessly inefficient or even non-terminating.

One aspect of control in logic programs is the selection rule, stating which atom in a query is selected in each derivation step. The standard selection rule in logic programming languages is the fixed left-to-right rule of Prolog. While this rule provides appropriate control for many applications, there are situations, e.g. in the context of parallel execution or the test-and-generate paradigm, that require a more flexible control mechanism, namely, *dynamic scheduling*, where the selectable atoms are determined at runtime. Such a mechanism is provided in modern logic programming languages in the form of *delay declarations* .

To demonstrate that on the one hand, the left-to-right selection rule is sometimes inappropriate, but that on the other hand, the selection mechanism must be controlled in some way, consider the following programs APPEND and IN\_ORDER

| % | append(Xs,Ys,Zs) $``$Zs is the result of concatenating the lists Xs and Ys |
| --- | --- |
|  | append(\[H|Xs\],Ys,\[H|Zs\]) $``$ |
|  |  | append(Xs,Ys,Zs). |
|  | append(\[\],Ys,Ys). |
| % | in\_order(Tree,List) $``$List is an ordered list of the nodes of Tree |
|  | in\_order(tree(Label,Left,Right),Xs) $``$ |
|  |  | in\_order(Left,Ls), |
|  |  | in\_order(Right,Rs), |
|  |  | append(Ls,\[Label|Rs\],Xs). |
|  | in\_order(void,\[\]). |

together with the query (read\_tree and write\_list are defined elsewhere)

$$\text{q}:\text{read\_tree(Tree), in\_order(Tree,List), write\_list(List)}.$$

If read\_tree cannot read the whole tree at once — say, it receives the input from a stream — it would be nice to be able to run the “processes” in\_order and write\_list on the available input. This can only be done if one uses a dynamic selection rule (Prolog’s rule would call in\_order only after read\_tree has finished, while other fixed rules would immediately diverge). In order to avoid nontermination one should adopt appropriate delay declarations, namely

| delay in\_order(T,\_) until nonvar(T). |
| --- |
| delay append(Ls,\_,\_) until nonvar(Ls). |
| delay write\_list(Ls,\_) until nonvar(Ls). |

These declarations avoid that in\_order, append and write\_list are selected “too early”, i.e. when their arguments are not “sufficiently instantiated”. Note that instead of having interleaving “processes”, one can also select several atoms in parallel, as long as the delay declarations are respected. This approach to parallelism has been first proposed in  and “has an important advantage over the ones proposed in the literature in that it allows us to parallelise programs written in a large subset of Prolog by merely adding to them delay declarations, so *without modifying* the original program” .

Compared to other mechanisms for user-defined control, e.g., using the cut operator in connection with built-in predicates that test for the instantiation of a variable (`var` or `ground`), delay declarations are more compatible with the declarative character of logic programming. Nevertheless, many important declarative properties that have been proven for logic programs do not apply to programs with delay declarations. The problem is mainly related to deadlock.

Essentially, for such programs the well-known equivalence between model-theoretic and operational semantics does not hold. For example, the query append(X,Y,Z) does not succeed (it *deadlocks*) and this is in contrast with the fact that (infinitely many) instances of append(X,Y,Z) are contained in the least Herbrand model of APPEND. This shows that a model-theoretic semantics in the classical sense is not achievable, in fact the problem of finding a suitable declarative semantics is still open. Moreover, while for the left-to-right selection rule there are results that allow us to characterise when a program is terminating, these results do not apply any longer in presence of dynamic scheduling.

### 1.2 Contributions

This paper contains essentially four contributions tackling the above problems.

In order to provide a characterisation of dynamic scheduling that is reasonably abstract and hence amenable to semantic analysis, we consider *input-consuming derivations* , a formalism similar to *Moded GHC* . In an input-consuming derivation, only atoms whose input arguments are not instantiated through the unification step may be selected. Moreover, we restrict our attention to the class of *simply-moded* programs, which are programs that are, in a well-defined sense, consistent wrt. the modes. As also shown by the benchmarks in Sec. 7, most practical programs are simply-moded. We analyse the relations between input-consuming derivations and programs with delay declarations. We demonstrate that under some statically verifiable conditions, input-consuming derivations are exactly the ones satisfying the (natural) delay declarations of programs.

We define a denotational semantics which enjoys a model-theoretical reading and has a bottom-up constructive definition. We show that it is compositional, correct and fully abstract wrt. the computed answer substitutions of successful derivations. E.g., it captures the fact that the query append(X,Y,Z) does not succeed.

Since dynamic scheduling also allows for parallelism, it is sometimes important to model the result of *partial* (i.e., incomplete) derivations. For instance, one might have queries (processes) that never terminate, which by definition may never reach the state of *success*, i.e. of successful completion of the computation. Therefore, we define a second semantics which enjoys the same properties as the one above. We demonstrate that it is correct, fully abstract and compositional wrt. the computed substitutions of partial derivations. We then have a uniform (in our opinion elegant) framework allowing us to model both successful and partial computations.

Finally, we study the problem of termination of input-consuming programs. We present a result which characterises termination of simply-moded input-consuming programs. This result is based on the semantics mentioned in the previous paragraph.

The rest of this paper is organised as follows. The next section introduces some preliminaries. Section 4 shows properties of input-consuming derivations that are needed in the proofs. Section 3 defines delay declarations, and formally compares them to input-consuming derivations. Section 5 provides a result on denotational semantics for input-consuming derivations, first for complete derivations, then for incomplete (input-consuming) derivations. Section 6 provides a sufficient and necessary criterion for termination of programs using input-consuming derivations. Section 7 surveys some benchmark programs. Section 8 concludes.

## 2 Preliminaries

The reader is assumed to be familiar with the terminology and the basic results of the semantics of logic programs . Following , we use boldface characters to denote sequences of objects: $`𝐭`$ denotes a sequence of terms, $`𝐁`$ is a query (i.e., a possibly empty sequence of atoms). The empty query is denoted by $`\mathrm{}`$. The relation symbol of an atom $`A`$ is denoted $`Rel(A)`$. The set of variables occurring in a syntactic object $`o`$ is denoted $`\mathrm{𝑉𝑎𝑟}(o)`$. We say that $`o`$ is *linear* if every variable occurs in it at most once. Given a *substitution* $`\sigma =\{x_1/t_1,\mathrm{},x_n/t_n\}`$, we say that $`\{x_1,\mathrm{},x_n\}`$ is its *domain* (denoted by $`\mathrm{𝐷𝑜𝑚}(\sigma )`$), and $`\mathrm{𝑉𝑎𝑟}(\{t_1,\mathrm{},t_n\})`$ is its *range* (denoted by $`\mathrm{𝑅𝑎𝑛}(\sigma )`$). Note that $`\mathrm{𝑉𝑎𝑟}(\sigma )=\mathrm{𝐷𝑜𝑚}(\sigma )\mathrm{𝑅𝑎𝑛}(\sigma )`$. If $`t_1,\mathrm{},t_n`$ is a permutation of $`x_1,\mathrm{},x_n`$ then we say that $`\sigma `$ is a *renaming*. The *composition* of substitutions is denoted by juxtaposition ($`x\theta \sigma =(x\theta )\sigma `$). We say that a term $`t`$ is an *instance* of $`t^{}`$ iff for some $`\sigma `$, $`t=t^{}\sigma `$; further, $`t`$ is a *variant* of $`t^{}`$, written $`tt^{}`$, iff $`t`$ and $`t^{}`$ are instances of each other. 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^{}`$. A query $`Q:𝐀,B,𝐂`$ and a clause $`c:H𝐁`$ (variable disjoint with $`Q`$) yield the resolvent $`(𝐀,𝐁,𝐂)\theta `$ with $`\theta =mgu(B,H)`$. We say that $`𝐀,B,𝐂\stackrel{\theta }{}(𝐀,𝐁,𝐂)\theta `$ is a *derivation step (using $`c`$)*, and call $`B`$ the *selected atom*. A *derivation of* $`P\{Q\}`$ is a sequence of derivation steps $`Q\stackrel{\theta _1}{}Q_1\stackrel{\theta _2}{}\mathrm{}`$ using (variants of) clauses in the program $`P`$. A finite derivation $`Q\stackrel{\theta _1}{}\mathrm{}\stackrel{\theta _n}{}Q_n`$ is also denoted $`Q\underset{P}{\overset{\vartheta }{}}Q_n`$, where $`\vartheta =\theta _1\mathrm{}\theta _n`$. The restriction of $`\vartheta `$ to $`Q`$ is a *computed answer substitution* (*c.a.s.*). If $`Q_n=\mathrm{}`$, the derivation is *successful*.

### 2.1 Delay Declarations

Logic programs with delay declarations consist of two parts: a set of clauses and a set of delay declarations, one for each of its predicate symbols. A delay declaration associated with an $`n`$-ary predicate symbol $`p`$ has the form

$$\mathrm{𝚍𝚎𝚕𝚊𝚢}p(t_1,\mathrm{},t_n)\mathrm{𝚞𝚗𝚝𝚒𝚕}\mathrm{𝐶𝑜𝑛𝑑}(t_1,\mathrm{},t_n)$$

where $`\mathrm{𝐶𝑜𝑛𝑑}(t_1,\mathrm{},t_n)`$ is a formula in some assertion language . A derivation is *delay-respecting* if an atom $`p(t_1,\mathrm{},t_n)`$ is selected only if $`\mathrm{𝐶𝑜𝑛𝑑}(t_1,\mathrm{},t_n)`$ is satisfied. In this case, we also say that the atom $`p(t_1,\mathrm{},t_n)`$ is selectable. In particular, we consider delay declarations of the form

$$\mathrm{𝚍𝚎𝚕𝚊𝚢}p(𝚇_1,\mathrm{},𝚇_n)\mathrm{𝚞𝚗𝚝𝚒𝚕}\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(𝚇_{i_1})\mathrm{}\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(𝚇_{i_k}).$$

where $`1i_1<\mathrm{}<i_kn`$.111For the case that $`k=0`$, the empty conjunction might be denoted as $`\mathrm{𝚝𝚛𝚞𝚎}`$, or the delay declaration might simply be omitted. The condition $`\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(t_{i_1})\mathrm{}\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(t_{i_k})`$ is satisfied if and only if $`t_{i_1},\mathrm{},t_{i_k}`$ are non-variable terms. Such delay declarations are equivalent to the block declarations of SICStus Prolog .

### 2.2 Moded Programs

A *mode* indicates how a predicate should be used.

###### Definition 2.1

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

If $`m_p(i)=\mathrm{𝐼𝑛}`$ (resp. *Out*), we say that $`i`$ is an $`\mathrm{𝑖𝑛𝑝𝑢𝑡}`$ (resp. *output*) *position of* $`p`$. 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 that $`𝐬`$ is the sequence of terms filling in its input positions and $`𝐭`$ is the sequence of terms filling in its output positions.

The notion of simply-moded program is due to Apt and Etalle .

###### Definition 2.2

A clause $`p(𝐭_0,𝐬_{n+1})p_1(𝐬_1,𝐭_1),\mathrm{},p_n(𝐬_n,𝐭_n)`$ is *simply-moded* iff $`𝐭_1,\mathrm{},𝐭_n`$ is a linear vector of variables and for all $`i[1,n]`$

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

A query $`𝐁`$ is *simply-moded* iff the clause $`q𝐁`$ is simply-moded, where $`q`$ is any variable-free atom. A program is simply-moded iff all of its clauses are. $`\mathrm{}`$

Thus, a clause is simply-moded if the output positions of body atoms are filled in by distinct variables, and every variable occurring in an output position of a body atom does not occur in an earlier input position. In particular, every unit clause is simply-moded. Notice also that programs APPEND and IN\_ORDER are simply-moded wrt. the modes append(In,In,Out) and in\_order(In,Out).

### 2.3 Input-Consuming Derivations

Input-consuming derivations are a formalism for describing dynamic scheduling in an abstract way .

###### Definition 2.3

A derivation step $`𝐀,B,𝐂\stackrel{\theta }{}`$ $`(𝐀,𝐁,𝐂)\theta `$ is *input-consuming* if and only if $`\mathrm{𝐼𝑛}(B)\theta =\mathrm{𝐼𝑛}(B)`$. A derivation is *input-consuming* iff all its derivation steps are input-consuming. $`\mathrm{}`$

Thus, allowing only input-consuming derivations is a form of dynamic scheduling, since whether or not an atom can be selected depends on its degree of instantiation at runtime. If no atom is resolvable via an input-consuming derivation step, the query *deadlocks*.222 Notice that there is a difference between this notion of deadlock and the one used for programs with delay declarations; see  for a detailed discussion.

It has been shown that the input-consuming333The notion of input-consuming is not used, but it is said that the input of the selected atom must be an instance of the input of the head, which is in fact a necessary condition for a derivation step to be input-consuming. resolvent of a simply-moded query using a simply-moded clause is simply-moded \[4, Lemma 30\].

## 3 Input-Consuming Derivations and Delay Declarations

In this section, we show a correspondence between input-consuming derivations and delay declarations.

###### Example 3.1

Consider again the delay declaration

It is easy to check that *every* derivation starting in a query append($`\mathrm{t}`$,$`\mathrm{s}`$,X), where X is a variable disjoint from $`s`$ and $`t`$, is input-consuming wrt. append(In,In,Out) iff it respects the delay declaration.

To show the correspondence between delay declarations and input-consuming derivations suggested by this example, we need some further definitions. We call a term $`t`$ *flat* if $`t`$ has the form $`f(x_1,\mathrm{},x_n)`$ where the $`x_i`$ are distinct variables. Note that constants are flat terms. The significance of flat term arises from the following observation: if $`s`$ and $`t`$ are unifiable, $`s`$ is non-variable and $`t`$ is flat, then $`s`$ is an instance of $`t`$. Think here of $`s`$ being a term in an input position of a selected atom, and $`t`$ being the term in that position of a clause head.

###### Definition 3.2

A program $`P`$ is *input-consistent* iff for each clause $`H𝐁`$ of it, the family of terms filling in the input positions of $`H`$ is linear, and consists of variables and flat terms. $`\mathrm{}`$

We also consider here delay declarations of a restricted type.

###### Definition 3.3

A program with delay declarations is *simple* if every delay declaration is of the form

$$\mathrm{𝚍𝚎𝚕𝚊𝚢}p(𝚇_1,\mathrm{},𝚇_n)\mathrm{𝚞𝚗𝚝𝚒𝚕}\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(𝚇_{i_1})\mathrm{}\mathrm{𝚗𝚘𝚗𝚟𝚊𝚛}(𝚇_{i_k}).$$

where $`i_1,\mathrm{},i_k`$ is a subset of the input positions of $`p`$.

Moreover, we say that the positions $`i_1,\mathrm{},i_k`$ of $`p`$ are *controlled*, while the other input positions of $`p`$ are *free*. $`\mathrm{}`$

Thus the controlled positions are those “guarded” by a delay declaration. The main result of this section shows that, under some circumstances, using delay declarations is equivalent to restricting to input-consuming derivations. The first statement of the theorem has been shown previously \[18, Theorem 7.9\], although not exactly for the same class of programs. We prefer to give a proof here.

###### Lemma 3.4

Let $`P`$ be simply-moded, input-consistent and simple. Let $`Q`$ be a simply-moded query.

* If for every clause $`H𝐁`$ of $`P`$, $`H`$ contains variables in its free positions, then every derivation of $`P\{Q\}`$ respecting the delay declarations is input-consuming (modulo renaming).
* If in addition for every clause $`H𝐁`$ of $`P`$, the head $`H`$ contains flat terms in its controlled positions, then every input-consuming derivation of $`P\{Q\}`$ respects the delay declarations.

Proof. It is sufficient to show the result for the first step. The general result follows from the persistence of simply-modedness under input-consuming derivation steps \[4, Lemma 30\]. Let $`A=p(𝐬,𝐭)`$ be the atom in $`Q`$ selected in the step and $`H=p(𝐯,𝐮)`$.

We prove the first statement. Clearly $`A`$ and $`H`$ are unifiable. Since $`P`$ is input-consistent and by hypothesis, $`𝐯`$ is linear and has variables in the free positions, and variables or flat terms in the controlled positions. Moreover, since $`P`$ is simple and $`A`$ is selectable, $`𝐬`$ is non-variable in the controlled positions. Considering in addition that the clause is a fresh copy renamed apart from $`Q`$, it follows that $`𝐬`$ is an instance of $`𝐯`$. Let $`\theta _1`$ be the substitution with $`\mathrm{𝐷𝑜𝑚}(\theta _1)\mathrm{𝑉𝑎𝑟}(𝐯)`$ such that $`𝐯\theta _1=𝐬`$.

Since $`𝐭`$ is a linear vector of variables, there is a substitution $`\theta _2`$ such that $`\mathrm{𝐷𝑜𝑚}(\theta _2)\mathrm{𝑉𝑎𝑟}(𝐭)`$ and $`𝐭\theta _2=𝐮\theta _1`$.

Since $`Q`$ is simply moded, we have $`\mathrm{𝑉𝑎𝑟}(𝐭)\mathrm{𝑉𝑎𝑟}(𝐬)=\mathrm{}`$, and therefore $`\mathrm{𝑉𝑎𝑟}(𝐭)\mathrm{𝑉𝑎𝑟}(𝐯\theta _1)=\mathrm{}`$. Thus it follows by the previous paragraph that $`\theta =\theta _1\theta _2`$ is an MGU of $`p(𝐬,𝐭)`$ and $`p(𝐯,𝐮)`$. More precisely, we have $`𝐬\theta _1\theta _2=𝐬`$, $`𝐯\theta _1\theta _2=𝐯\theta _1`$, $`𝐮\theta _1\theta _2=𝐮\theta _1`$, and $`𝐭\theta _1\theta _2=𝐭\theta _2`$, and so in particular, the derivation step using $`\theta `$ is input-consuming. Since mgu’s are unique modulo renaming, the first statement follows.

We now show the second statement. If $`H`$ contains flat (i.e., non-variable) terms in all controlled positions, then clearly $`A`$ must be non-variable in those positions for the derivation step using the clause to be input-consuming. But then $`A`$ is also selectable. Since the same holds for every clause, the statement follows. $`\mathrm{}`$

In order to assess how realistic these conditions are, we have checked them against a number of programs from various collections. (The results can be found in Sec. 7). Concerning the statement that all delay-respecting derivations are input-consuming, we are convinced that this is the case in the overwhelming majority of practical cases. Concerning the converse, that is, that all input-consuming derivations are delay-respecting, we could find different examples in which this was not the case. In many of them this could be fixed by a simple transformation of the programs444To give an intuitive idea, the transformation would, e.g., replace the clause even(s(s(X))):- even(X). with even(s(Y)):- s\_decomp(Y,X), even(X)., where we define s\_decomp(s(X),X). and the mode is s\_decomp(In,Out)., in other cases it could not (e.g., flatten, ). Nevertheless, we strongly believe that the latter form a small minority.

The delay declarations for the considered programs were either given or derived based on the presumed mode. Note that delay declarations as in Def. 3.3 can be more efficiently implemented than, e.g., delay declarations testing for groundness. Usually, the derivations permitted by the latter delay declarations are a strict subset of the input-consuming derivations.

## 4 Properties of Input-Consuming Derivations

This section contains some technical results about input-consuming derivations that are needed in the proofs. Moreover, it defines simply-local substitutions, which are crucial for our semantics.

### 4.1 Switching and Pushing

The material in this subsection is not contained in the conference version , and is needed in the proofs but not for understanding the main results of this paper.

We recall the following results . Notice that they have been proven for nicely-moded programs and queries. However, since simply-modedness is a special case of nicely-modedness, the properties stated below also apply to the class of programs and queries considered in this paper.

The following lemma states that the only variables of a nicely-moded query that can be “affected” through the computation of an input-consuming derivation with a nicely-moded program are those occurring in some output positions.

###### Lemma 4.1

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

The following definition is due to Smaus .

###### Definition 4.2

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 $`A`$ in $`(𝐀,𝐂)`$, $`A\theta `$ is a *direct descendant of A*. We say that $`A`$ is a descendant of $`B`$ if the pair $`(A,B)`$ is in the reflexive, transitive closure of the relation *is a direct descendant*. 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 $`𝐁`$. $`\mathrm{}`$

The next corollary is an immediate consequence of the Left-Switching Lemma .

###### Corollary 4.3

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

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

is a partial input-consuming derivation of $`P\{𝐀,𝐁\}`$. Then there exist $`𝐂_1`$ and $`𝐂_2`$ and a partial input-consuming derivation

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

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

###### Lemma 4.4

(Input Pushing Lemma) Let the program $`P`$ and the query $`𝐀`$ be nicely-moded. Let $`\theta `$ be a substitution such that $`\mathrm{𝑉𝑎𝑟}(\theta )\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀))=\mathrm{}`$. Then for every (partial) input-consuming derivation $`\delta :𝐀\stackrel{\sigma }{}𝐁`$, there exists a (partial) input-consuming derivation $`\delta ^{}:𝐀\theta \stackrel{\sigma ^{}}{}𝐁^{}`$ such that

* they have the same length,
* for every derivation step, atoms in the same positions are selected and the input clauses employed are variants of each other.

Moreover, $`𝐀\theta \sigma ^{}`$ is an instance of $`𝐀\sigma `$ and $`𝐁^{}`$ is an instance of $`𝐁`$.

Proof. Notice that since $`\mathrm{𝑉𝑎𝑟}(\theta )\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(𝐀))=\mathrm{}`$ by hypothesis, $`𝐀\theta `$ is nicely-moded as well. Since, by Lemma 4.1, input-consuming derivations only affect variables occurring in the output positions of a query, one only has to appropriately instantiate every resolvent in the derivation. Clearly, every resolution step remains input-consuming (the selected atom is just instantiated a bit further). $`\mathrm{}`$

### 4.2 Simply-Local Substitutions

We now define *simply-local* substitutions, which reflect the way clauses become instantiated in input-consuming derivations. A simply-local substitution can be decomposed into several substitutions, corresponding to the instantiation of the *output* of each *body atom*, as well as the *input* of the *head*.

###### Definition 4.5

Let $`\theta `$ be a substitution. We say that $`\theta `$ is *simply-local* wrt. the clause $`c:p(𝐭_0,𝐬_{n+1})p_1(𝐬_1,𝐭_1),\mathrm{},p_n(𝐬_n,𝐭_n)`$ iff there exist substitutions $`\sigma _0,\sigma _1\mathrm{},\sigma _n`$ and disjoint sets of fresh (wrt. $`c`$) variables $`v_0,v_1,\mathrm{},v_n`$ such that $`\theta =\sigma _0\sigma _1\mathrm{}\sigma _n`$ where for $`i\{0,\mathrm{},n\}`$,

* $`\mathrm{𝐷𝑜𝑚}(\sigma _i)\mathrm{𝑉𝑎𝑟}(𝐭_i)`$,
* $`\mathrm{𝑅𝑎𝑛}(\sigma _i)\mathrm{𝑉𝑎𝑟}(𝐬_i\sigma _0\sigma _1\mathrm{}\sigma _{i1})v_i`$.

$`\theta `$ is *simply-local* wrt. a query $`𝐁`$ iff $`\theta `$ is simply-local wrt. the clause $`q𝐁`$ where $`q`$ is any variable-free atom. $`\mathrm{}`$

We make two remarks about this definition.

###### Remark 4.6

1. Concerning the case $`i=0`$, the term vector $`𝐬_0`$ does not exist, but by abuse of notation, we postulate $`\mathrm{𝑉𝑎𝑟}(𝐬_0\mathrm{})=\mathrm{}`$.
2. In the case of a simply-local substitution wrt. a query, $`\sigma _0`$ is the empty substitution, since $`\mathrm{𝐷𝑜𝑚}(\sigma _0)\mathrm{𝑉𝑎𝑟}(q)`$ where $`q`$ is an (imaginary) variable-free atom.

###### Example 4.7

Consider APPEND in mode append(In,In,Out), and its recursive clause $`c:\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}([𝙷|\mathrm{𝚇𝚜}],\mathrm{𝚈𝚜},[𝙷|\mathrm{𝚉𝚜}])\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}(\mathrm{𝚇𝚜},\mathrm{𝚈𝚜},\mathrm{𝚉𝚜})`$. The substitution $`\theta =\{𝙷/𝚅,\mathrm{𝚇𝚜}/[],`$ $`\mathrm{𝚈𝚜}/[𝚆],\mathrm{𝚉𝚜}/[𝚆]\}`$ is simply-local wrt. $`c`$: let $`\sigma _0=\{𝙷/𝚅,\mathrm{𝚇𝚜}/[],\mathrm{𝚈𝚜}/[𝚆]\}`$ and $`\sigma _1=\{\mathrm{𝚉𝚜}/[𝚆]\}`$; then $`\mathrm{𝐷𝑜𝑚}(\sigma _0)\{𝙷,\mathrm{𝚇𝚜},\mathrm{𝚈𝚜}\}`$, and $`\mathrm{𝑅𝑎𝑛}(\sigma _0)v_0`$ where $`v_0=\{𝚅,𝚆\}`$, and $`\mathrm{𝐷𝑜𝑚}(\sigma _1)\{\mathrm{𝚉𝚜}\}`$, and $`\mathrm{𝑅𝑎𝑛}(\sigma _1)\mathrm{𝑉𝑎𝑟}((\mathrm{𝚇𝚜},\mathrm{𝚈𝚜})\sigma _0)`$.

From the next lemma, we will be able to conclude that if $`𝐀,B,𝐂\stackrel{\theta }{}(𝐀,𝐁,𝐂)\theta `$ is an input-consuming derivation step using clause $`c:H𝐁`$, then without loss of generality, $`\theta `$ can be decomposed into two substitutions that are simply-local wrt. the clause $`H`$ and the query $`B`$, respectively.

###### Lemma 4.8

(Simply-Local MGU) Let the atoms $`A`$ and $`H`$ be variable disjoint and $`A`$ be simply-moded. Suppose that there exists $`\vartheta =\mathrm{𝑚𝑔𝑢}(A,H)`$ such that $`\mathrm{𝐼𝑛}(A\vartheta )=\mathrm{𝐼𝑛}(A)`$. Then there exist two substitutions $`\sigma _0^H`$ and $`\sigma _1^A`$ such that $`\sigma _0^H\sigma _1^A=\mathrm{𝑚𝑔𝑢}(A,H)`$, and $`\sigma _0^H`$ is simply-local wrt. the clause $`H`$, and $`\sigma _1^A`$ is simply-local wrt. the query $`A`$.

Proof. Let $`A=p(𝐬,𝐭)`$ and $`H=p(𝐯,𝐮)`$. By properties of mgu’s (see \[2, Corollary 2.25\]), there exist substitutions $`\sigma _0^H`$ and $`\sigma _1^A`$ (the names have been chosen to correspond closely to Def. 4.5) such that

$$\sigma _0^H=\mathrm{𝑚𝑔𝑢}(𝐬,𝐯),\sigma _1^A=\mathrm{𝑚𝑔𝑢}(𝐭\sigma _0^H,𝐮\sigma _0^H)\text{and}\sigma _0^H\sigma _1^A=\mathrm{𝑚𝑔𝑢}(A,H),$$

and all those mgu’s are relevant. Since, by hypothesis, $`𝐯\vartheta =𝐬\vartheta =𝐬`$, it follows that $`𝐬`$ is an instance of $`𝐯`$. Hence, we can assume without loss of generality that $`\sigma _0^H`$ is such that $`𝐯\sigma _0^H=𝐬`$ and thus

* $`\mathrm{𝐷𝑜𝑚}(\sigma _0^H)\mathrm{𝑉𝑎𝑟}(𝐯)`$, and
* $`\mathrm{𝑅𝑎𝑛}(\sigma _0^H)\mathrm{𝑉𝑎𝑟}(𝐬)`$.

Since $`\mathrm{𝑉𝑎𝑟}(𝐬)`$ is fresh wrt. $`H`$, this means that $`\sigma _0^H`$ is simply-local wrt. the clause $`H`$.

By relevance of $`\sigma _0^H`$, simply-modedness of $`A`$ and the fact that $`A`$ and $`H`$ are variable disjoint, it follows that $`\mathrm{𝐷𝑜𝑚}(\sigma _0^H)\mathrm{𝑉𝑎𝑟}(𝐭)=\mathrm{}`$. Hence, $`\sigma _1^A=\mathrm{𝑚𝑔𝑢}(𝐭,𝐮\sigma _0^H)`$. Since, by simply-modedness of $`A`$, $`𝐭`$ is sequence of distinct variables, we can assume without loss of generality that $`\sigma _1^A`$ is such that $`𝐭\sigma _1^A=𝐮\sigma _0^H`$ and thus

* $`\mathrm{𝐷𝑜𝑚}(\sigma _1^A)\mathrm{𝑉𝑎𝑟}(𝐭)`$, and
* $`\mathrm{𝑅𝑎𝑛}(\sigma _1^A)\mathrm{𝑉𝑎𝑟}(𝐮\sigma _0^H)\mathrm{𝑅𝑎𝑛}(\sigma _0^H)\mathrm{𝑉𝑎𝑟}(𝐮)\mathrm{𝑉𝑎𝑟}(𝐬)\mathrm{𝑉𝑎𝑟}(𝐮)`$.

Since $`\mathrm{𝑉𝑎𝑟}(𝐮)`$ is fresh wrt. $`A`$ and noting Remark 4.6 (2), this means that $`\sigma _1^A`$ is simply-local wrt. the query $`A`$. $`\mathrm{}`$

###### Remark 4.9

From now on we assume that all the mgu’s used in input-consuming derivations are composed of two simply-local substitutions as in Lemma 4.8.

The following lemma shows how the accumulated substitution of a derivation starting in a query $`A_1,\mathrm{},A_n`$ can be decomposed into $`n`$ substitutions each corresponding to one atom $`A_i`$.

###### Lemma 4.10

Let the program $`P`$ and the query $`A_1,\mathrm{},A_n`$ be simply-moded. Suppose that $`\delta :A_1,\mathrm{},A_n\stackrel{\vartheta }{}𝐀`$ is an input-consuming partial derivation of $`P\{A_1,\mathrm{},A_n\}`$. Then, there exist $`\sigma _1,\mathrm{},\sigma _n`$ substitutions and $`v_1,\mathrm{},v_n`$ disjoint sets of fresh variables (wrt. $`A_1,\mathrm{},A_n`$) such that $`\vartheta =\sigma _1\mathrm{}\sigma _n`$ and

* for $`i\{1,\mathrm{},n\}`$, $`\mathrm{𝐷𝑜𝑚}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_i))v_i`$,
* for $`i\{1,\mathrm{},n\}`$, $`\mathrm{𝑅𝑎𝑛}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A_i\sigma _1\mathrm{}\sigma _{i1}))v_i`$.

Proof. By induction on $`n`$.

*Base*. Let $`n=1`$. In this case, $`\delta :A\stackrel{\vartheta }{}𝐀.`$ By Lemma 4.1, there exists a set of variables $`v`$ such that $`\mathrm{𝑉𝑎𝑟}(c)v`$ and $`v\mathrm{𝑉𝑎𝑟}(A)=\mathrm{}`$ (i.e. $`v`$ is fresh w.r.t. $`A`$), and $`\mathrm{𝐷𝑜𝑚}(\vartheta )\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A))v`$.

Suppose that $`\delta `$ is of the form

$$A\stackrel{\vartheta _1}{}(B_1,\mathrm{},B_m)\vartheta _1\stackrel{\vartheta _2}{}𝐀$$

where $`c:HB_1,\mathrm{},B_m`$ is the input clause used in the first derivation step, $`\vartheta _1=\mathrm{𝑚𝑔𝑢}(A,H)`$ such that $`\mathrm{𝐼𝑛}(A\vartheta _1)=\mathrm{𝐼𝑛}(A)`$ and $`\vartheta =\vartheta _1\vartheta _2`$. Since $`\vartheta _1`$ is simply-local wrt. $`A`$ and $`H`$, we have that $`\vartheta _1=\sigma _1\sigma _2`$ where

* $`\mathrm{𝐷𝑜𝑚}(\sigma _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H))`$,
* $`\mathrm{𝑅𝑎𝑛}(\sigma _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))`$,
* $`\mathrm{𝐷𝑜𝑚}(\sigma _2)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A))`$,
* $`\mathrm{𝑅𝑎𝑛}(\sigma _2)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(H))`$.

Now $`\mathrm{𝑉𝑎𝑟}(\vartheta _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))v`$. By standardisation apart and simply-modedness of $`A`$, it follows that $`H\sigma _1\sigma _2=H\sigma _1`$, and so $`(B_1,\mathrm{},B_m)\vartheta _1=(B_1,\mathrm{},B_m)\sigma _1`$. Consider the derivation $`(B_1,\mathrm{},B_m)\sigma _1\stackrel{\vartheta _2}{}𝐀`$. We have that $`\mathrm{𝑉𝑎𝑟}(\vartheta _2)\mathrm{𝑉𝑎𝑟}(\sigma _1)v`$. Since $`\mathrm{𝑉𝑎𝑟}(\sigma _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))\mathrm{𝐼𝑛}(H))`$, we have that $`\mathrm{𝑉𝑎𝑟}(\vartheta _2)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))v`$.

Thus, $`\mathrm{𝑅𝑎𝑛}(\vartheta )=\mathrm{𝑅𝑎𝑛}(\vartheta _1\vartheta _2)\mathrm{𝑉𝑎𝑟}(\vartheta _1)\mathrm{𝑉𝑎𝑟}(\vartheta _2)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A))v`$.

*Induction step*. Let $`n>1`$. By Corollary 4.3, there exist $`\sigma _1,\mathrm{},\sigma _n`$ substitutions such that

$$\begin{array}{cc}\delta :A_1,\mathrm{},A_n\stackrel{\sigma _1}{}𝐂_1,(A_2,\mathrm{},A_n)\sigma _1\hfill & \stackrel{\sigma _2}{}\mathrm{}(𝐂_1,\mathrm{},𝐂_{n1}),A_n\sigma _1\mathrm{}\sigma _{n1}\hfill \\ & \stackrel{\sigma _n}{}𝐂_1,\mathrm{},𝐂_n\hfill \end{array}$$

such that $`𝐀=𝐂_1,\mathrm{},𝐂_n`$, and $`\vartheta =\sigma _1\mathrm{},\sigma _n`$, and all the $`A_i`$-steps are performed in the sub-derivation

$$𝐂_1,\mathrm{},𝐂_{i1},(A_i,\mathrm{},A_n)\sigma _1\mathrm{}\sigma _{i1}\stackrel{\sigma _i}{}𝐂_1,\mathrm{},𝐂_i,(A_{i+1},\mathrm{},A_n)\sigma _1\mathrm{}\sigma _i.$$

By the induction hypothesis and standardisation apart, there exist $`v_1,\mathrm{},v_n`$ disjoint sets of fresh variables (wrt. $`A_1,\mathrm{},A_n`$) such that for all $`i\{1,\mathrm{},n\}`$,

* $`\mathrm{𝐷𝑜𝑚}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_i))v_i`$,
* $`\mathrm{𝑅𝑎𝑛}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(A_i\sigma _1\mathrm{}\sigma _{i1}))v_i`$.

$`\mathrm{}`$

## 5 A Denotational Semantics

Previous declarative semantics for logic programs cannot correctly model dynamic scheduling. E.g., none of them reflects the fact that append(X,Y,Z) deadlocks. We define a model-theoretic semantics that models computed answer substitutions of input-consuming derivations of simply-moded programs and queries.

In predicate logic, an interpretation states which formulas are true and which ones are not. For our purposes, it is convenient to formalise this by defining an interpretation $`I`$ as a set of atoms closed under variance. Based on this notion and simply-local substitutions, we now define a restricted notion of model.

###### Definition 5.1

Let $`M`$ be an interpretation. We say that $`M`$ is a *simply-local model* of $`c:HB_1,\mathrm{},B_n`$ iff for every substitution $`\theta `$ simply-local wrt. $`c`$,

if $`B_1\theta ,\mathrm{},B_n\theta M`$ then $`H\theta M`$. (1)
$`M`$ is a *simply-local model* of a program $`P`$ iff it is a simply-local model of each clause of it. $`\mathrm{}`$

Note that a simply-local model is not necessarily a model in the classical sense, since the substitution in (1) is required to be simply-local. For example, given the program $`\{𝚚(\mathrm{𝟷}).,𝚙(𝚇)𝚚(𝚇).\}`$ with modes $`𝚚(\mathrm{𝙸𝚗}),𝚙(\mathrm{𝙾𝚞𝚝})`$, a model must contain the atom $`𝚙(\mathrm{𝟷})`$, whereas a simply-local model does not necessarily contain $`𝚙(\mathrm{𝟷})`$, since $`\{𝚇/\mathrm{𝟷}\}`$ is not simply-local wrt. $`𝚙(𝚇)𝚚(𝚇).`$

We now show that there exists a minimal simply-local model and that it is bottom-up computable. For this we need the following operator $`T_P^{\mathrm{𝑆𝐿}}`$ on interpretations: Given a program $`P`$ and an interpretation $`I`$, define

$$\begin{array}{cc}T_P^{\mathrm{𝑆𝐿}}(I)=\{H\theta \hfill & c:HB_1,\mathrm{},B_nP,\hfill \\ & \theta \text{simply-local wrt.}c,\hfill \\ & B_1,\mathrm{},B_n\theta I\}.\hfill \end{array}$$

Operator’s powers are defined in the standard way: $`T_P^{\mathrm{𝑆𝐿}}0(I)=I`$, $`T_P^{\mathrm{𝑆𝐿}}(i+1)(I)=T_P^{\mathrm{𝑆𝐿}}(T_P^{\mathrm{𝑆𝐿}}i(I))`$, and $`T_P^{\mathrm{𝑆𝐿}}\omega (I)=_{i=0}^{\mathrm{}}T_P^{\mathrm{𝑆𝐿}}i(I)`$. It is easy to show that $`T_P^{\mathrm{𝑆𝐿}}`$ is continuous on the lattice where interpretations are ordered by set inclusion. Hence, by well-known results , $`T_P^{\mathrm{𝑆𝐿}}\omega `$ exists and is the least fixpoint of $`T_P^{\mathrm{𝑆𝐿}}`$.

### 5.1 Modelling Complete Derivations

In this subsection, we use least simply-local models for describing the usual complete derivations. As suggested above, $`T_P^{\mathrm{𝑆𝐿}}`$ can be used to compute the least simply-local model of a program.

###### Proposition 5.2

Let $`P`$ be simply-moded. Then $`T_P^{\mathrm{𝑆𝐿}}\omega (\mathrm{})`$ is the least simply-local model of $`P`$. $`\mathrm{}`$

We denote the least simply-local model of $`P`$ by $`M_P^{\mathrm{𝑆𝐿}}`$.

The following lemma is a special case of the statement that our semantics is correct, fully abstract and compositional. It is needed in the proof of the subsequent theorem, and is not included in .

###### Lemma 5.3

Let the program $`P`$ and the atom $`A`$ be simply-moded. The following statements are equivalent:

* there exists an input-consuming successful derivation $`A\underset{P}{\overset{\vartheta }{}}\mathrm{}`$,
* there exists a substitution $`\theta `$ such that $`A\theta M_P^{\mathrm{𝑆𝐿}}`$ and $`\mathrm{𝐼𝑛}(A\theta )=\mathrm{𝐼𝑛}(A)`$,

where $`A\vartheta `$ and $`A\theta `$ are variant.

Proof.

$`(\mathrm{i})(\mathrm{ii}).`$ By induction on the length of $`\delta `$.

*Base*. Let $`\mathrm{𝑙𝑒𝑛}(\delta )=1`$. In this case $`\delta `$ has the form

$$A\underset{P}{\overset{\vartheta }{}}\mathrm{}$$

where $`c:H`$ is the input clause and $`\vartheta =\mathrm{𝑚𝑔𝑢}(A,H)`$ satisfies $`\mathrm{𝐼𝑛}(A\vartheta )=\mathrm{𝐼𝑛}(A)`$. Since $`\vartheta `$ is simply-local wrt. $`A`$ and $`H`$, by Remark 4.9, $`\vartheta _{|H}`$ is simply-local wrt. $`H`$. Hence, by definition of $`T_P^{\mathrm{𝑆𝐿}}`$,

$$H\vartheta _{|H}=H\vartheta =A\vartheta T_P^{\mathrm{𝑆𝐿}}1(\mathrm{})M_P^{\mathrm{𝑆𝐿}}.$$

*Induction step*. Let $`\mathrm{𝑙𝑒𝑛}(\delta )>1`$. In this case, $`\delta `$ has the form

$$A\stackrel{\vartheta _1}{}(B_1,\mathrm{},B_n)\vartheta _1\stackrel{\vartheta _2}{}\mathrm{}$$

where $`c:HB_1,\mathrm{},B_n`$ is the input clause used in the first derivation step, $`\vartheta _1=\mathrm{𝑚𝑔𝑢}(A,H)`$ satisfies $`\mathrm{𝐼𝑛}(A\vartheta _1)=\mathrm{𝐼𝑛}(A)`$ and $`\vartheta =\vartheta _1\vartheta _2`$. Since $`\vartheta _1`$ is simply-local wrt. $`A`$ and $`H`$, by Remark 4.9, $`\vartheta _{1|H}`$ is simply-local wrt. $`H`$. Let $`\vartheta _{1|H}=\sigma _0`$. By Definition 4.5 of simply-local substitution, there exists a set $`v_0`$ of fresh variables (wrt. $`c`$) such that

$$\mathrm{𝐷𝑜𝑚}(\sigma _0)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H))$$
(2)
and

$$\mathrm{𝑅𝑎𝑛}(\sigma _0)v_0.$$
(3)
By standardisation apart,

$$(B_1,\mathrm{},B_n)\vartheta _1=(B_1,\mathrm{},B_n)\sigma _0.$$
(4)
By (4) and the Left-Switching Lemma, there exist $`\sigma _1^{},\mathrm{},\sigma _n^{}`$ and a derivation $`\delta ^{}`$ isomorphic to $`\delta `$ (modulo the Left-Switching Lemma), and $`\delta ^{}`$ has the form

$$A\stackrel{\vartheta _1}{}(B_1,\mathrm{},B_n)\sigma _0\stackrel{\sigma _1^{}}{}(B_2,\mathrm{},B_n)\sigma _0\sigma _1^{}\mathrm{}B_n\sigma _0\sigma _1^{}\mathrm{}\sigma _{n1}^{}\stackrel{\sigma _n^{}}{}\mathrm{}$$

where $`\vartheta _2=\sigma _1^{}\mathrm{}\sigma _n^{}`$. In particular, for all $`i\{1,\mathrm{},n\}`$, $`\delta _i:B_i\sigma _0\sigma _1^{}\mathrm{}\sigma _{i1}^{}\stackrel{\sigma _i^{}}{}\mathrm{}`$ is an input-consuming successful derivation which is strictly shorter than $`\delta `$.

Hence, by the inductive hypothesis, for all $`i\{1,\mathrm{},n\}`$,

$$B_i\sigma _0\sigma _1^{}\mathrm{}\sigma _i^{}M_P^{\mathrm{𝑆𝐿}}.$$
(5)
By simply-modedness of $`c`$, $`\mathrm{𝑂𝑢𝑡}((B_1,\mathrm{},B_n)\sigma _0)=\mathrm{𝑂𝑢𝑡}(B_1,\mathrm{},B_n)`$.

By Lemma 4.10, there exist distinct sets of fresh variables $`v_1,\mathrm{},v_n`$, such that $`\mathrm{𝐷𝑜𝑚}(\sigma _i^{})\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_i\sigma _1^{}\mathrm{}\sigma _{i1}^{}))v_i`$. By induction on $`i`$, one can prove that, for all $`i\{1,\mathrm{},n\}`$,

$$\mathrm{𝐷𝑜𝑚}(\sigma _i^{})\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_i))v_i.$$
(6)
The base case is trivial. The induction step, follows from the inductive hypothesis (i.e., $`\mathrm{𝐷𝑜𝑚}(\sigma _j^{})\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_j))v_j`$ for $`j\{1,\mathrm{},i1\}`$), standardisation apart and simply-modedness of $`c`$.

For all $`i\{1,\mathrm{},n\}`$, let $`\sigma _i=\sigma _{i|\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_i))}^{}`$. Hence, by (6),

$$\mathrm{𝐷𝑜𝑚}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_i)).$$
(7)
By standardisation apart, for all $`i\{1,\mathrm{},n\}`$,

$$B_i\sigma _0\sigma _1^{}\mathrm{}\sigma _i^{}=B_i\sigma _0\sigma _1\mathrm{}\sigma _i.$$
(8)
By Lemma 4.10 and (8), for all $`i\{1,\mathrm{},n\}`$,

$$\mathrm{𝑅𝑎𝑛}(\sigma _i)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(B_i\sigma _0\sigma _1\mathrm{}\sigma _{i1}))v_i.$$
(9)
By standardisation apart and simply-modedness of $`c`$, it follows that for all $`j\{i+1,\mathrm{},n\}`$, $`\mathrm{𝑉𝑎𝑟}(B_i\sigma _0\sigma _1\mathrm{}\sigma _i)\mathrm{𝐷𝑜𝑚}(\sigma _j^{})=\mathrm{}`$. Hence, by (8), it follows that

$$B_i\sigma _0\sigma _1^{}\mathrm{}\sigma _i^{}=B_i\sigma _0\sigma _1\mathrm{}\sigma _n.$$
(10)
By (2), (3), (7), (9) and the fact that $`v_0,v_1,\mathrm{},v_n`$ are disjoint sets of variables, it follows that

$$\sigma _0\sigma _1\mathrm{}\sigma _n\text{ is simply local wrt. }c.$$
(11)
Moreover, by (5) and (10),

$$B_i\sigma _0\sigma _1\mathrm{}\sigma _nM_P^{\mathrm{𝑆𝐿}}.$$
(12)
By definition of $`T_P^{\mathrm{𝑆𝐿}}`$, $`H\sigma _0\sigma _1\mathrm{}\sigma _nM_P^{\mathrm{𝑆𝐿}}`$. Since $`A\vartheta =A\vartheta _1\vartheta _2=H\vartheta _1\vartheta _2=H\sigma _0\vartheta _2=H\sigma _0\sigma _1^{}\mathrm{}\sigma _n^{}=H\sigma _0\sigma _1\mathrm{}\sigma _n`$, we have proven that

$$A\vartheta M_P^{\mathrm{𝑆𝐿}}.$$
(13)
Since by Lemma 4.1, $`\mathrm{𝐼𝑛}(A\vartheta )=\mathrm{𝐼𝑛}(A)`$, this completes the proof of the “$`(\mathrm{i})(\mathrm{ii})`$” direction.

$`(\mathrm{ii})(\mathrm{i}).`$ We first need to establish the following fact.

###### Fact 1

Let the atom $`A`$ and the clause $`c:HB_1,\mathrm{},B_n`$ be simply-moded. Suppose that there exist two substitutions $`\sigma `$ and $`\theta `$ such that

* $`\sigma `$ is simply-local wrt. $`c`$,
* $`A\theta =H\sigma `$,
* $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\theta )`$.

Then, for each variant $`c^{}:H^{}B_1^{},\mathrm{},B_n^{}`$ of $`c`$ variable disjoint with $`A`$, there exists $`\vartheta =\mathrm{𝑚𝑔𝑢}(A,H^{})`$ such that $`A\vartheta =A\theta `$ and $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\vartheta )`$.

Proof of Fact. Since $`A\theta =H\sigma `$, it follows that (since $`A`$ and $`H^{}`$ are variable-disjoint) $`A`$ and $`H^{}`$ are unifiable, and $`A\theta `$ ($`=H\sigma `$) is an instance of the most general common instance of $`A`$ and $`H^{}`$. Now, since by assumption $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\theta )`$ and $`\sigma `$ is simply-local wrt. $`c`$, we can choose $`\vartheta =\mathrm{𝑚𝑔𝑢}(A,H^{})`$ such that

$`\mathrm{𝐼𝑛}(A)`$ $`=`$ $`\mathrm{𝐼𝑛}(A\vartheta ).`$ (14)
$`\mathrm{𝑂𝑢𝑡}(H^{}\vartheta )`$ $`=`$ $`\mathrm{𝑂𝑢𝑡}(H\sigma ).`$ (15)
Using that $`\vartheta `$ is an mgu, the assumptions in the statement, and (14), we have $`\mathrm{𝐼𝑛}(H^{}\vartheta )=\mathrm{𝐼𝑛}(A\vartheta )=\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\theta )=\mathrm{𝐼𝑛}(H\sigma )`$, i.e.,

$$\mathrm{𝐼𝑛}(H^{}\vartheta )=\mathrm{𝐼𝑛}(H\sigma ).$$
(16)
By (15) and (16),

$$A\vartheta =H^{}\vartheta =H\sigma =A\theta .$$
(17)
By (14) and (17), $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\theta )`$. This completes the proof of the Fact. $`\mathrm{}`$

We now continue the proof of the main statement. We show by induction on $`i`$ that if $`A\theta T_P^{\mathrm{𝑆𝐿}}i(\mathrm{})`$ for some $`i>0`$ and substitution $`\theta `$ such that $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\theta )`$, then there exists an input-consuming successful derivation

$$A\underset{P}{\overset{\vartheta }{}}\mathrm{}$$

and $`A\vartheta =A\theta `$.

Base. Let $`i=1`$. In this case, $`A\theta T_P^{\mathrm{𝑆𝐿}}1(\mathrm{})`$. By Definition of $`T_P^{\mathrm{𝑆𝐿}}`$, there exists a clause $`c:H`$ of $`P`$ and a substitution $`\sigma `$ such that $`\sigma `$ is simply-local wrt. $`c`$ and $`A\theta =H\sigma `$. Let $`H^{}`$ be a variant of $`c`$ variable disjoint from $`A`$. By Fact 1, there exists an mgu $`\vartheta `$ of $`A`$ and $`H`$ such that $`A\theta =A\vartheta `$ and $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\vartheta )`$, i.e., there exists an input-consuming successful derivation $`A\underset{P}{\overset{\vartheta }{}}\mathrm{}`$.

*Induction step*. Let $`i>1`$ and $`A\theta T_P^{\mathrm{𝑆𝐿}}i(\mathrm{})`$. By definition of $`T_P^{\mathrm{𝑆𝐿}}`$, there exists a clause $`c:HB_1,\mathrm{},B_n`$ of $`P`$ and a substitution $`\sigma `$ such that $`\sigma `$ is simply-local wrt. $`c`$, $`(B_1,\mathrm{},B_n)\sigma T_P^{\mathrm{𝑆𝐿}}(i1)`$ and $`A\theta =H\sigma `$.

By Definition 4.5 of simply-local substitution, there exist $`\sigma _0,\sigma _1,\mathrm{},\sigma _n`$ substitutions and $`v_0,v_1,\mathrm{},v_n`$ disjoint sets of fresh variables (wrt. $`c`$) such that $`\sigma =\sigma _0\sigma _1\mathrm{}\sigma _n`$ where

* $`\mathrm{𝐷𝑜𝑚}(\sigma _0)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H))`$,
* $`\mathrm{𝑅𝑎𝑛}(\sigma _0)v_0`$,
* for $`j\{1,\mathrm{},n\}`$, $`\mathrm{𝐷𝑜𝑚}(\sigma _j)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(B_j))`$,
* for $`j\{1,\mathrm{},n\}`$, $`\mathrm{𝑅𝑎𝑛}(\sigma _j)\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}))v_j`$.

By simply-modedness of $`c`$, we have that for all $`j\{1,\mathrm{},n\}`$, $`B_j\sigma _0\sigma _1\mathrm{}\sigma _j=B_j\sigma _0\sigma _1\mathrm{}\sigma _n`$.

So we have $`(B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1})\sigma _jT_P^{\mathrm{𝑆𝐿}}(i1)`$ and

$$\mathrm{𝐼𝑛}(B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1})=\mathrm{𝐼𝑛}((B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1})\sigma _j),$$

and hence, by the inductive hypothesis, for all $`j\{1,\mathrm{},n\}`$, there is an input-consuming derivation $`B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\underset{P}{\overset{\sigma _j^{}}{}}\mathrm{}`$ such that

$$B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\sigma _j^{}=B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\sigma _j.$$

Let $`c^{}:H^{}B_1^{},\mathrm{},B_n^{}`$ be a variant of $`c`$ variable disjoint from $`A`$ such that $`c^{}=c\rho `$ for some renaming $`\rho `$. By Fact 1, there exists an mgu $`\vartheta _1`$ of $`A`$ and $`H^{}`$ such that $`\mathrm{𝐼𝑛}(A)=\mathrm{𝐼𝑛}(A\vartheta _1)`$ and $`H^{}\vartheta _1=H\rho \vartheta _1=H\sigma _0`$. Thus, $`(B_1^{},\mathrm{},B_n^{})\vartheta _1=(B_1,\mathrm{},B_n)\sigma _0.`$ By the inductive hypothesis, for all $`j1,\mathrm{},n`$, there exists an input-consuming successful derivation $`B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\underset{P}{\overset{\sigma _j^{}}{}}\mathrm{}`$ such that $`B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\sigma _j^{}=B_j\sigma _0\sigma _1\mathrm{}\sigma _{j1}\sigma _j`$.

Hence, there exists an input-consuming successful derivation

$$(B_1,\mathrm{},B_n)\sigma _0\underset{P}{\overset{\vartheta _2}{}}\mathrm{}$$

such that $`(B_1,\mathrm{},B_n)\sigma _0\vartheta _2=(B_1,\mathrm{},B_n)\sigma _0\sigma _1\mathrm{}\sigma _n`$.

Hence, there exists an input-consuming successful derivation

$$A\underset{P}{\overset{\vartheta _1}{}}(B_1,\mathrm{},B_n)\vartheta _1\underset{P}{\overset{\vartheta _2}{}}\mathrm{}$$

with $`\vartheta =\vartheta _1\vartheta _2`$ and $`A\vartheta _1\vartheta _2=H\sigma _0\vartheta _2=H\sigma _0\sigma _1\mathrm{}\sigma _n=H\sigma =A\theta `$, i.e., $`A\vartheta =A\theta `$. $`\mathrm{}`$

We now state that our semantics is correct, fully abstract and compositional for complete derivations.

###### Theorem 5.4

Let the program $`P`$ and the query $`𝐀`$ be simply-moded. The following statements are equivalent:

* there exists an input-consuming successful derivation $`𝐀\underset{P}{\overset{\vartheta }{}}\mathrm{}`$,
* there exists a substitution $`\theta `$, simply-local wrt. $`𝐀`$, such that $`𝐀\theta M_P^{\mathrm{𝑆𝐿}}`$,

where $`𝐀\theta `$ is a variant of $`𝐀\vartheta `$.

Proof. Let $`𝐀:=A_1,\mathrm{},A_n`$. The proof is by induction on $`n`$.

Base. Let $`n=1`$. In this case the thesis follows from Lemma 5.3.

Induction step. Let $`n>1`$.

$`(\mathrm{i})(\mathrm{ii}).`$ Let $`\theta =\vartheta _{|𝐀}`$. By Lemma 4.10, $`\theta `$ is simply-local wrt. $`𝐀`$. By Corollary 4.3, there exists a successful input-consuming derivation of the form

$$A_1,\mathrm{},A_n\underset{P}{\overset{\vartheta _1}{}}(A_2,\mathrm{},A_n)\vartheta _1\underset{P}{\overset{\vartheta _2}{}}\mathrm{}$$

where $`\vartheta =\vartheta _1\vartheta _2`$.

By Lemma 4.10 and standardisation apart, $`\mathrm{𝐷𝑜𝑚}(\vartheta _1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_1))v_1`$ where $`v_1`$ is a set of fresh variables (wrt. $`A_1,\mathrm{},A_n`$), and $`\mathrm{𝐷𝑜𝑚}(\vartheta _2)`$ $`\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((A_2,\mathrm{},A_n)\vartheta _1))v,`$ where $`v`$ is a set of fresh variables (wrt. $`A_1,\mathrm{},A_n`$ and $`\vartheta _1`$). By simply-modedness of $`c`$ and standardisation apart, $`\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((A_2,\mathrm{},A_n)\vartheta _1))=\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_2,\mathrm{},A_n))`$, and so $`\mathrm{𝐷𝑜𝑚}(\vartheta _2)`$ $`\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_2,\mathrm{},A_n))v`$.

By simply-modedness of $`c`$, $`\mathrm{𝑉𝑎𝑟}(A_1)\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}(A_2,\mathrm{},A_n))=\mathrm{}`$. Hence, by standardisation apart, $`\mathrm{𝑉𝑎𝑟}(A_1\vartheta _1)\mathrm{𝐷𝑜𝑚}(\vartheta _2)=\mathrm{}`$, i.e., $`A_1\vartheta _1\vartheta _2=A_1\vartheta _1`$.

By the inductive hypothesis, $`A_1\vartheta _1=A_1\vartheta _1\vartheta _2M_P^{\mathrm{𝑆𝐿}}`$ and $`(A_2,\mathrm{},A_n)\vartheta _1\vartheta _2M_P^{\mathrm{𝑆𝐿}}`$, i.e., $`𝐀\theta M_P^{\mathrm{𝑆𝐿}}`$.

$`(\mathrm{ii})(\mathrm{i}).`$ By the inductive hypothesis, there exists an input-consuming successful derivation $`A_1\underset{P}{\overset{\vartheta _1}{}}\mathrm{}`$ where $`A_1\vartheta _1=A_1\theta `$. Again by the inductive hypothesis, there exists an input-consuming successful derivation $`(A_2,\mathrm{},A_n)\theta _{|A_1}\underset{P}{\overset{\vartheta _2}{}}\mathrm{}`$such that $`(A_2,\mathrm{},A_n)\theta _{|A_1}\vartheta _2=(A_2,\mathrm{},A_n)\theta `$. Since, by standardisation apart,$`(A_2,\mathrm{},A_n)\theta _{|A_1}=(A_2,\mathrm{},A_n)\vartheta _1`$, it follows that there is an input-consuming successful derivation

$$A_2,\mathrm{},A_n\underset{P}{\overset{\vartheta _1}{}}(A_2,\mathrm{},A_n)\vartheta _1\underset{P}{\overset{\vartheta _2}{}}\mathrm{}.$$

$`\mathrm{}`$

###### Example 5.5

Considering again APPEND, we have that

$$M_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}=\underset{n=0}{\overset{\mathrm{}}{}}\{\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}([t_1,\mathrm{},t_n],s,[t_1,\mathrm{},t_n|s])|t_1,\mathrm{},t_n,s\text{ are any terms }\}.$$

Using Theorem 5.4, we can conclude that the query append(\[a,b\],X,Y) succeeds with computed answer $`\theta =\{𝚈/[𝚊,𝚋|𝚇]\}`$. In fact, append(\[a,b\],X,\[a,b|X\])$`\mathrm{M}_{\mathrm{APPEND}}^{\mathrm{SL}}`$, and $`\theta `$ is simply-local wrt. the query above.

On the other hand, we can also say that the query append(X,\[a,b\],Y) has *no successful input-consuming derivations*. In fact, for every $`AM_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}`$ we have that the first input position of $`A`$ is filled in by a non-variable term. Therefore there is no simply-local $`\theta `$ such that append(X,\[a,b\],Y)$`\mathrm{\theta }\mathrm{M}_{\mathrm{APPEND}}^{\mathrm{SL}}`$. This shows that this semantics allows us to model correctly deadlocking derivations.

However, if one considers derivations that are not input-consuming, then the query append(X,\[a,b\],Y) has successful derivations. Likewise, if one considers substitution that are not simply-local, append(X,\[a,b\],Y) has instances in $`M_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}`$.

### 5.2 Modelling Partial Derivations

Dynamic scheduling also allows for parallelism. In this context it is important to be able to model the result of partial derivations. That is to say, instead of considering computed answer substitutions for complete derivations, we now consider computed answer substitutions for partial derivations. As we will see, this will be essential in order to prove termination of the programs.

Let $`\mathrm{𝑆𝑀}_P`$ be the set of all simply-moded atoms of the extended Herbrand universe of $`P`$. In analogy to Prop. 5.2, we have the following proposition.

###### Proposition 5.6

Let $`P`$ be simply-moded. Then $`T_P^{\mathrm{𝑆𝐿}}\omega (\mathrm{𝑆𝑀}_P)`$ is the least simply-local model of $`P`$ containing $`\mathrm{𝑆𝑀}_P`$. $`\mathrm{}`$

We denote the least simply-local model of $`P`$ containing $`\mathrm{𝑆𝑀}_P`$ by $`\mathrm{𝑃𝑀}_P^{SL}`$, for *partial model*.

We now proceed in the same way as in the previous subsection: We first show a special case of the statement that our semantics is correct, fully abstract and compositional (for partial derivations). Based on this, we show the theorem itself.

###### Lemma 5.7

Let the program $`P`$ and the atom $`A`$ be simply-moded. The following statements are equivalent:

* there exists an input-consuming partial derivation $`A\underset{P}{\overset{\vartheta }{}}𝐀`$,
* there exists a substitution $`\theta `$ such that $`A\theta \mathrm{𝑃𝑀}_P^{SL}`$ and $`\mathrm{𝐼𝑛}(A\theta )=\mathrm{𝐼𝑛}(A)`$,

where $`A\vartheta `$ and $`A\theta `$ are variant.

Proof. The proof is almost identical to the one of Lemma 5.3. The basic difference is that now, in the base cases, we have to consider derivations of length zero.

$`(\mathrm{i})(\mathrm{ii}).`$ If $`\mathrm{𝑙𝑒𝑛}(\delta )=0`$, then $`𝐀=A`$ and $`\vartheta =ϵ`$ (the empty substitution). The thesis follows from the fact that $`A`$ is simply-moded and $`\mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}`$ contains the set of all simply-moded atoms.

$`(\mathrm{ii})(\mathrm{i}).`$ If $`A\theta T_P^{\mathrm{𝑆𝐿}}0(\mathrm{𝑆𝑀}_P)=\mathrm{𝑆𝑀}_P`$ then $`\theta `$ is just a renaming of the output variables of $`A`$. The thesis follows by taking $`\vartheta `$ to be the empty substitution and $`\delta `$ to be the derivation of length zero. $`\mathrm{}`$

We now state that our semantics is correct, fully abstract and compositional for partial derivations.

###### Theorem 5.8

Let the program $`P`$ and the query $`𝐀`$ be simply-moded. The following statements are equivalent:

* there exists an input-consuming derivation $`𝐀\underset{P}{\overset{\vartheta }{}}𝐀^{}`$,
* there exists a substitution $`\theta `$, simply-local wrt. $`𝐀`$, such that $`𝐀\theta \mathrm{𝑃𝑀}_P^{SL}`$,

where $`𝐀\theta `$ is a variant of $`𝐀\vartheta `$.

Proof. The proof is analogous to the one of Theorem 5.4, but using Lemma 5.7 instead of 5.3. $`\mathrm{}`$

Note that the derivation in point (i) ends in $`𝐀^{}`$, which might be non-empty.

###### Example 5.9

Consider again APPEND. First, $`\mathrm{𝑃𝑀}_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{SL}`$ contains $`M_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}`$ as a subset (see Ex. 5.5). Note that $`M_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}`$ is obtained by starting from the fact clause `append([],Ys,Ys)` and repeatedly applying the $`T_P^{\mathrm{𝑆𝐿}}`$ operator using the recursive clause of APPEND. Now to obtain the remaining atoms in $`\mathrm{𝑃𝑀}_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{SL}`$, we must repeatedly apply the $`T_P^{\mathrm{𝑆𝐿}}`$ operator, starting from any simply moded atom, i.e., an atom of the form $`\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}(s,t,x)`$ where $`s`$ and $`t`$ are arbitrary terms but $`x`$ does not occur in $`s`$ or $`t`$. It is easy to see that we thus have to add $`\mathrm{𝑆𝑀}_P`$ together with

$$\begin{array}{cc}\{\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}([t_1,\mathrm{},t_n|s],t,[t_1,\mathrm{},t_n|x])|\hfill & t_1,\mathrm{},t_n,s,t\text{ are arbitrary terms,}\hfill \\ & x\text{ is a fresh variable}\}.\hfill \end{array}$$

Consider the query $`\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}([𝚊,𝚋|𝚇],𝚈,𝚉)`$. The substitution $`\theta =\{𝚉/[𝚊,𝚋|𝚉^{}]\}`$ is simply-local wrt. the query, and $`\mathrm{𝚊𝚙𝚙𝚎𝚗𝚍}([𝚊,𝚋|𝚇],𝚈,[𝚊,𝚋|𝚉^{}])\mathrm{𝑃𝑀}_{\mathrm{𝙰𝙿𝙿𝙴𝙽𝙳}}^{\mathrm{𝑆𝐿}}`$. Using Theorem 5.8, we can conclude that the query has a partial derivation with computed answer $`\theta `$. Following the same reasoning, one can also conclude that the query has a partial derivation with computed answer $`\theta =\{𝚉/[𝚊|𝚉^{}]\}`$.

## 6 Termination

Input-consuming derivations were originally conceived as an abstract and “reasonably strong” assumption about the selection rule in order to prove termination . The first result in this area was a sufficient criterion applicable to well- and nicely-moded programs. This was improved upon by dropping the requirement of well-modedness, which means that one also captures termination by deadlock . In this section, we only consider simply moded programs and queries (simply-moded and well-moded programs form two largely overlapping, but distinct classes), and we provide a criterion for termination which is sufficient and necessary, and hence an exact characterisation of termination. We first define our notion of termination.

###### Definition 6.1

A program is called *input terminating* iff all its input-consuming derivations started in a simply-moded query are finite. $`\mathrm{}`$

In order to prove that a program is input terminating, we need the concept of moded level mapping .

###### Definition 6.2

A function $`||`$ is a *moded level mapping* iff it maps atoms into $``$ and such that for any $`𝐬`$, $`𝐭`$ and $`𝐮`$, $`|p(𝐬,𝐭)|=|p(𝐬,𝐮)|`$. $`\mathrm{}`$

The condition $`|p(𝐬,𝐭)|=|p(𝐬,𝐮)|`$ states that the *level* of an atom is independent from the terms in its output positions.

Note that programs without recursion terminate trivially. In this context, we need the following standard definitions .

###### Definition 6.3

Let $`P`$ be a program, $`p`$ and $`q`$ be relations. We say that

* *p refers to q* iff there is a clause in $`P`$ with $`p`$ in the head and $`q`$ in the body.
* *p depends on q* iff $`(p,q)`$ is in the reflexive and transitive closure of the relation *refers to*.
* *p* and *q* are *mutually recursive*, written $`pq`$, iff $`p`$ and $`q`$ depend on each other. $`\mathrm{}`$

We now define simply-acceptability, which is in analogy to acceptability , but defined to deal with simply-moded and input-consuming programs.

###### Definition 6.4

Let $`P`$ be a program and $`M`$ a simply-local model of $`P`$ containing $`\mathrm{𝑆𝑀}_P`$. A clause $`H𝐀,B,𝐂`$ is *simply-acceptable wrt. the moded level mapping $`||`$ and $`M`$* iff for every substitution $`\theta `$ simply-local wrt. it,

$$\text{if }𝐀\theta M\text{ and }\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B)\text{ then }|H\theta |>|B\theta |.$$

The program $`P`$ is *simply-acceptable wrt. $`M`$* iff there exists a moded level mapping $`||`$ such that each clause of $`P`$ is simply-acceptable wrt. $`||`$ and $`M`$.

We also say that $`P`$ is *simply-acceptable* if it is simply acceptable wrt. some $`M`$.

Let us compare simply-acceptability to acceptability, used to prove left-termination . Acceptability is based on a (classical) model $`M`$ of the program, and for a clause $`HA_1,\mathrm{},A_n`$, one requires $`|H\theta |>|A_i\theta |`$ only if $`M(A_1,\mathrm{},A_{i1})\theta `$. The reason is that for LD-derivations, $`A_1,\mathrm{},A_{i1}`$ must be completely resolved before $`A_i`$ is selected. By the correctness of LD resolution , it turns out that the c.a.s. $`\theta `$, just before $`A_i`$ is selected, is such that $`M(A_1,\mathrm{},A_{i1})\theta `$. It has been argued previously that it is difficult to use a similar argument for input-consuming derivations . Using the results of the previous section, we have overcome this problem. We exploited that provided that programs and queries are simply-moded, we know that even though $`A_1,\mathrm{},A_{i1}`$ may not be resolved completely, $`A_1,\mathrm{},A_{i1}\theta `$ will be in any “partial model” of the program.

In the next two subsections, we prove that simply-acceptability is a sufficient and necessary criterion for termination. The sections can be skipped by the reader who is not interested in the proofs.

### 6.1 Sufficiency of Simply-Acceptability

The following corollary of \[6, Lemma 5.8\] allows us to restrict our attention to queries containing only one atom.

###### Corollary 6.5

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

From now on, 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`$ iff no relation defined in $`P`$ occurs in $`R`$.

The following theorem is actually even more general than the one in . It shows that simply-acceptability is a sufficient criterion for termination, and can be used in a modular way.

###### Theorem 6.6

Let $`P`$ and $`R`$ be two simply-moded programs such that $`P`$ extends $`R`$. Let $`M`$ be a simply-local model of $`PR`$ containing $`\mathrm{𝑆𝑀}_P`$. Suppose that

* $`R`$ is input terminating,
* $`P`$ is simply acceptable wrt. $`M`$ (and a moded level mapping $`||`$).

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: $`\mathrm{𝑑𝑒𝑝}_P(p)=\mathrm{\#}\{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 6.5, it is sufficient to prove that for any simply-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 $`\delta `$ is an infinite input-consuming derivation of $`(PR)\{A\}`$ such that $`A`$ is defined in $`P`$. Then

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

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

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

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

Let $`\theta =(\vartheta _1\vartheta _2^{})_{|c}`$. By Lemma 4.10, $`\theta `$ is simply-local wrt. $`c`$. Consider the instance $`H\theta (B_1,\mathrm{},B_n)\theta `$ of $`c`$. By Theorem 5.8, $`(B_1,\mathrm{},B_{i1})\theta M`$.

We show that (2) cannot hold, by induction on $`\mathrm{𝑑𝑒𝑝}_P(\mathrm{𝑅𝑒𝑙}(A)),|A|`$ with respect to 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 )).`$. Therefore,

$$\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 simply-acceptable wrt. $`||`$ and $`M`$, $`\theta `$ is simply-local wrt. $`c`$ and $`(B_1,\mathrm{},B_{i1})\theta M`$, it follows that $`|H\theta |>|B_i\theta |`$. Consider the partial input-consuming derivation $`A\stackrel{\theta }{}𝐂,(B_i,\mathrm{},B_n)\theta `$. By Lemma 4.1 and the fact that $`||`$ is a moded level mapping, we have that $`|A|=|A\theta |=|H\theta |`$. Hence, $`\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{}`$

The above theorem suggests proving termination in a modular way, i.e., extending a program that is already known to be input-terminating by a program that is simply-acceptable. Of course, this theorem holds in particular if the former program is empty.

###### Theorem 6.7

Let $`P`$ be a simply-moded program. If $`P`$ is simply-acceptable then it is input terminating.

Proof. The proof follows from Theorem 6.6, by setting $`R=\mathrm{}`$. $`\mathrm{}`$

### 6.2 Necessity of Simply-Acceptability

We now prove the converse of Theorem 6.7. The results of the previous and this subsection together provide an exact characterisation of input termination.

###### Definition 6.8

An IC-tree for $`P\{Q\}`$ via a dynamic selection rule $``$ is a tree such that

* its root is $`Q`$,
* every node $`Q^{}`$ with a selected atom $`A`$ has exactly one descendant $`Q^{\prime \prime }`$ for each clause $`c`$ such that $`Q^{\prime \prime }`$ is an input-consuming resolvent of $`Q^{}`$ wrt. $`A`$ and $`c`$.

Notice that, since we are considering dynamic selection rules, it can happen that there is no atom selectable (i.e., meeting the condition about input-consuming resolvents above) in a node of an IC-tree.

###### Definition 6.9

An *LIC-derivation* is an input-consuming derivation in which at each step the selected atom is the leftmost atom which can be resolved via an input-consuming derivation step.

Similarly, we define the notion of LIC-tree.

###### Definition 6.10

An *LIC-tree* is an IC-tree in which at each node the selected atom is the leftmost atom which can be resolved via an input-consuming derivation step.

Branches of LIC-trees are LIC-derivations.

###### Lemma 6.11

(\[LIC-tree 1) An LIC-tree for $`P\{Q\}`$ is finite iff all LIC-consuming derivations of $`P\{Q\}`$ are finite.

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

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

###### Lemma 6.12

Let the program $`P`$ and the query $`𝐀,B`$ be simply-moded. Suppose that $`P`$ is input terminating and $`𝐀\theta \mathrm{𝑃𝑀}_P^{SL}`$, where $`\theta `$ is a simply-local substitution wrt. $`𝐀`$. Then $`\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(𝐀,B)\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(B\theta )`$.

Proof. Consider an LIC-tree $`T`$ for $`P\{𝐀,B\}`$. By the hypothesis that $`𝐀\theta \mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}`$, it follows that there exists a substitution $`\sigma `$ (possibly the empty substitution) such that $`\theta `$ is more general than $`\sigma `$, and $`\sigma `$ is a partial c.a.s. for $`P\{𝐀\}`$, such that either no atom is selectable or $`B\sigma `$ is the selected atom.

Clearly, $`\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(𝐀,B)\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(B\sigma )`$. By Lemma 4.4 we have $`\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(B\sigma )\mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}(B\theta )`$. Hence the thesis. $`\mathrm{}`$

We are now in position to prove necessity of simply-acceptability.

###### Theorem 6.13

Let $`P`$ be a simply-moded program. If $`P`$ is input terminating then $`P`$ is simply-acceptable.

Proof. We show that there exists a moded level mapping $`||`$ for $`P`$ such that $`P`$ is simply-acceptable wrt. $`||`$ and $`\mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}`$, the latter being the least simply-local model of $`P`$ containing $`\mathrm{𝑆𝑀}_P`$.

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, all the input-consuming derivations of $`P\{A^{}\}`$ are finite. Therefore, by Lemma 6.11, $`\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 simply-acceptable wrt. $`||`$ and $`\mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}`$.

Let $`c:H𝐀,B,𝐂`$ be a clause of $`P`$ and $`H\theta 𝐀\theta ,B\theta ,𝐂\theta `$ be an instance of $`c`$ where $`\theta `$ is a simply-local substitution wrt. $`c`$. We show that

$$\text{if }\mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}𝐀\theta \text{ and }\mathrm{𝑅𝑒𝑙}(H)\mathrm{𝑅𝑒𝑙}(B)\text{ then }|H\theta |>|B\theta |.$$

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 )`$. Since $`\mu `$ is simply-local wrt $`(H\theta )^{}`$ and $`H^{}`$, we have $`\mathrm{𝐷𝑜𝑚}(\mu )\mathrm{𝑉𝑎𝑟}(\mathrm{𝑂𝑢𝑡}((H\theta )^{}))\mathrm{𝑉𝑎𝑟}(\mathrm{𝐼𝑛}(H\rho ))`$. Hence $`(𝐀^{},B^{},𝐂^{})\mu =(𝐀,B,𝐂)\rho \mu `$, and

$$(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 LIC-tree for $`P\{(H\theta )^{}\}`$.

Moreover, $`(𝐀,B,𝐂)\rho \mu (𝐀,B,𝐂)(\rho \mu )_{|\mathrm{𝐼𝑛}(H)}=(𝐀,B,𝐂)\theta _{|\mathrm{𝐼𝑛}(H)}`$.

Let $`\theta =\theta _{|\mathrm{𝐼𝑛}(H)}\theta _{|\mathrm{𝑂𝑢𝑡}(𝐀)}\theta _{|\mathrm{𝑂𝑢𝑡}(B,𝐂)}`$. Hence, $`\theta _{|\mathrm{𝑂𝑢𝑡}(𝐀)}`$ is simply-local wrt. $`A\theta _{|\mathrm{𝐼𝑛}(H)}`$. Then, we have that

$$\begin{array}{ccccc}|H\theta |\hfill & =& \mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((H\theta )^{})\hfill & (\text{by definition of }||)\hfill & \\ & >& \mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((𝐀,B,𝐂)\theta _{|\mathrm{𝐼𝑛}(H)})\hfill & (\text{by definition of LIC-tree})\hfill & \\ & & \mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((𝐀,B)\theta _{|\mathrm{𝐼𝑛}(H)})\hfill & (\text{by definition of LIC-tree})\hfill & \\ & & \mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((B\theta _{|\mathrm{𝐼𝑛}(H)}\theta _{|\mathrm{𝑂𝑢𝑡}(𝐀)})\hfill & (\text{by Lemma }\text{6.12})\hfill & \\ & =& \mathrm{𝑙𝑛𝑜𝑑𝑒𝑠}_P^{\mathrm{𝑖𝑐}}((B\theta )^{})\hfill & (\text{since }\theta \text{ is simply-local wrt. c})\hfill & \\ & =& |B\theta |\hfill & (\text{by definition of }||).\hfill & \end{array}$$

$`\mathrm{}`$

### 6.3 A Characterisation

Summarising, we have characterised input termination by simply-acceptability.

###### Theorem 6.14

A simply-moded program $`P`$ is simply-acceptable iff it is input terminating. In particular, if $`P`$ is input terminating, then it is simply-acceptable wrt. $`\mathrm{𝑃𝑀}_P^{\mathrm{𝑆𝐿}}`$.

Proof. By Theorem 6.7 and Theorem 6.13. $`\mathrm{}`$

###### Example 6.15

Figure 1 shows program 15.3 from : quicksort using a form of difference lists (we permuted two body atoms for the sake of clarity). This program is simply-moded, and when used in combination with dynamic scheduling, the standard delay declarations for it are the following:

| delay quicksort(Xs, \_) until nonvar(Xs). |
| --- |
| delay quicksort\_dl(Xs, \_, \_) until nonvar(Xs). |
| delay partition(Xs, \_, \_, \_) until nonvar(Xs). |
| delay =\<(X,Y) until ground(X) and ground(Y). |
| delay \>(X,Y) until ground(X) and ground.(Y) |

The last two declarations fall out of the scope of Lemma 3.4. Nevertheless, if we think of the built-ins \> and =\< as being conceptually defined by a program containing infinitely many ground facts of the form \>($`\mathrm{n}`$,$`\mathrm{m}`$), with $`n`$ and $`m`$ being two appropriate integers, the derivations respecting the above delay declarations are exactly the input-consuming ones. We can prove that the program is input terminating. Define *len* as

$$\begin{array}{ccccc}\hfill len([h|t])& =& 1+len(t),\hfill & & \\ \hfill len(a)& =& 0\hfill & \text{ if }a\text{ is not of the form }[h|t].\hfill & \end{array}$$

We use the following moded level mapping (positions with $`\mathrm{\_}`$ are irrelevant)

$`|\mathrm{𝚚𝚞𝚒𝚌𝚔𝚜𝚘𝚛𝚝}\mathrm{\_}\mathrm{𝚍𝚕}(l,\mathrm{\_},\mathrm{\_})|`$ $`=`$ $`len(l),`$
$`|\mathrm{𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗}(l,\mathrm{\_},\mathrm{\_},\mathrm{\_})|`$ $`=`$ $`len(l).`$
The level mapping of all other atoms can be set to 0. Concerning the model, the simplest solution is to use the model that expresses the dependency between the list lengths of the arguments of $`\mathrm{𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗}`$, i.e., $`M`$ should contain all atoms of the form $`\mathrm{𝚙𝚊𝚛𝚝𝚒𝚝𝚒𝚘𝚗}(l_1,x,l_2,l_3)`$ where $`len(l_1)>len(l_2)`$ and $`len(l_1)>len(l_3)`$.

## 7 Benchmarks

In order to assess how realistic the conditions of Lemma 3.4 are, we have looked into three collections of logic programs, and we have checked whether those programs were simply moded (SM), input-consistent (IC) and whether they satisfied both sides of Lemma 3.4 (L). Notice that programs which are not input-consistent do not satisfy the conditions of Lemma 3.4. For this reason, some L columns are left blank. The results, reported in Tables 1 to 3, show that our results apply to the majority of the programs considered. Table 1 shows the programs from Apt’s collection , Table 2 those of the DPPD collection (http://dsse.ecs.soton.ac.uk/$``$mal/systems/dppd.html), and Table 3 some programs from Lindenstrauss’s collection (http://www.cs.huji.ac.il/$``$naomil).

## 8 Conclusion

In this paper, we have proven a result that *demonstrates* — for a large class of programs — the equivalence between delay declarations and input-consuming derivations. This was only speculated in . In fact, even though the class of programs we are considering here (simply-moded programs) is only slightly smaller than the one of nicely-moded programs considered in , for the latter a result such as Lemma 3.4 does not hold.

We have provided a denotational semantics for input-consuming derivations using a variant of the well-known $`T_P`$-operator. Our semantics follows the $`s`$-semantics approach  and thus enjoys the typical properties of semantics in this class. This semantics improves on the one introduced in  in two respects: The semantics of this paper models (within a uniform framework) both complete and incomplete derivations, and there is no requirement that the program must be well-moded.

Falaschi et al.  have defined a denotational semantics for CLP programs with dynamic scheduling of a somewhat different kind: the semantics of a query is given by a set of closure operators; each operator is a function modelling a possible effect of resolving the query on a program state (i.e., constraint on the program variables). However, we believe that our approach is more suited to termination proofs.

As mentioned in Subsec. 5.2, in the context of parallelism and concurrency , one can have derivations that never succeed, and yet compute substitutions. Moreover, input-consuming derivations essentially correspond to the execution mechanism of (Moded) FGHC . Thus we have provided a model-theoretic semantics for such programs/programming languages, which go beyond the usual success-based SLD resolution mechanism of logic programming.

On a more practical level, our semantics for partial derivations is used in order to prove termination. We have provided a necessary and sufficient criterion for termination, applicable to a wide class of programs, namely the class of simply-moded programs. For instance, we can now prove the termination of QUICKSORT, which is not possible with the tools of  (which provided only a sufficient condition). In the termination proofs, we exploit that any selected atom in an input-consuming derivation is in a model for partial derivations, in a similar way as this is done for proving left-termination. It is only on the basis of the semantics that we could present a characterisation of input-consuming termination for simply-moded programs.