Oracle Semantics for Prolog

Roberto Barbuti

Dipartimento di Informatica, Università di Pisa

Corso Italia 40, I-56125 Pisa, Italy

          barbuti@di.unipi.it

Michael Codish

Department of Mathematics & Computer Science Ben-Gurion University of the Negev P.O. Box 653, Beer-Sheba, Israel

        codish@bengus.bgu.ac.il

Roberto Giacobazzi

Dipartimento di Informatica, Università di Pisa

Corso Italia 40, I-56125 Pisa, Italy

           giaco@di.unipi.it

and

Michael J. Maher

IBM T.J. Watson Research Center P.O. Box 704, Yorktown Heights NY 10598

           mjm@watson.ibm.com

Abstract

This paper proposes to specify semantic definitions for logic programming languages such as Prolog in terms of an oracle which specifies the control strategy and identifies which clauses are to be applied to resolve a given goal. The approach is quite general. It is applicable to Prolog to specify both operational and declarative semantics as well as other logic programming languages.

Previous semantic definitions for Prolog typically encode the sequential depth-first search of the language into various mathematical frameworks. Such semantics mimic a Prolog interpreter in the sense that following the “leftmost” infinite path in the computation tree excludes computation to the right of this path from being considered by the semantics. The basic idea in this paper is to abstract away from the sequential control of Prolog and to provide a declarative characterization of the clauses to apply to a given goal. The decision whether or not to apply a clause is viewed as a query to an oracle which is specified from within the semantics and reasoned about from outside. This approach results in simple and concise semantic definitions which are more useful for arguing the correctness of program transformations and providing the basis for abstract interpretations than previous proposals.

Contents

1 Introduction 1

2 Preliminaries 4

3 Operational oracle semantics 6 3.1 Transition systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Transition systems for logic programs . . . . . . . . . . . . . . . . . . . . . . . . 6

4 Oracle declarative semantics 11 4.1 Top-down unfolding-based oracle semantics . . . . . . . . . . . . . . . . . . . . . 13 4.2 Relation between fixpoint and operational oracle semantics . . . . . . . . . . . . 15 4.3 Bottom-up oracle semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

5 Applications 19 5.1 The oracle for slp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.2 The oracle for Prolog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.3 Approximations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

6 Conclusions 23

A Appendix: proofs 25

1 Introduction

Logic programming is attractive for its non-algorithmic style and for its clean logical and fixpoint semantics. This leads to a high-level approach to programming, provides for the application of semantic-based techniques, such as abstract interpretation, and eases the justification of program transformations. On the other hand, real logic languages, such as Prolog, sacrifice logical purity to achieve acceptable efficiency. As a consequence the semantic simplicity and its advantages are often lost. Due to this dichotomy, logic programming faces two different paradigms: logic programming, in which the accent is placed on declarative specification of problems, and logic programming, in which the central issue is to write efficient programs to solve problems.

In this paper we weaken this dichotomy by applying the logic programming style to define a semantics for the logic programming language Prolog. The resulting semantics is more declarative than previous proposals. The central idea is perhaps best paraphrased as applying the equation Prolog = Logic + Control at the semantic level. Our semantics is partitioned into two components. The ‘logic’ component which is similar to what is found in classic semantics of logic programs; and the ‘control’ component which specifies when a given clause may be applied to solve a query or sub-query. In many cases both components have a clean specification such as those given for logic programs. As a consequence many of the advantages of logic programming are regained.

Declarative semantics for logic programs specify the set of ground atoms which are implied by the program, often by means of a fixpoint construction. This construction abstracts away from operational aspects of the interpreter, for example answer substitutions, goal dependence and search strategy. Although declarative semantics can be specified in different frameworks, they are typically defined in terms of an immediate consequence operator such as the classic T_{P} operator [van Emden and Kowalski 76]. While this approach captures the logical meaning of a program it does not adequately model one of the fundamental aspects of a logic program, namely its ability to compute substitutions. The work in [Falaschi, Levi, Martelli and Palamidessi 89] and [Falaschi, Levi, Martelli and Palamidessi 93] fills this gap by proposing a declarative semantics for logic programs that makes explicit the correspondence between computed answer substitutions and declarative meaning (model-theoretic and fixpoint) of the programs. The idea is to enhance the semantic domain by introducing variables to the Herbrand Universe. The declarative semantics is defined in terms of an immediate consequence operator as in the ground case. Moreover, the answer substitutions for a query can be obtained by “solving” the goal into the non-ground model of the program. However, the semantics is still not equipped to cope with the control features present in real logic languages such as left-to-right selection rule, depth-first search strategy, cut, etc...

In contrast, operational semantics are much more closely linked to the interpreter. Such semantics generally follow a top-down and goal-dependent approach. Because in these semantics the control is explicit, they are suitable to model real logic languages such as Prolog, in which the set of answers to goals computed by a program strongly depends on the control. For this reason the semantic definition of Prolog is usually given by encoding operational semantics in frameworks such as dynamic algebra [Börger 90], deterministic transition systems [de Bruin and de Vink 89], and denotational semantics [Jones and Mycroft 84], [Arbab and Berry 87], and [Debray and Mishra 87].

In [Barbuti, Codish, Giacobazzi and Levi 92] a new approach to defining the semantics of real logic programs is considered. Prolog control features are modeled in a constraint-based language called τ belonging to the ask/tell paradigm of Saraswat [Saraswat 90]. A transformation from Prolog to τ is defined to describe the meaning of a Prolog program P in terms of the declarative semantics of the corresponding τ-program. Ask constraints are used to specify the conditions for a clause to be chosen for reduction. These constraints “ask” for the termination of the computation with the preceding clauses. The meaning of a Prolog program is then constructed by composing the meaning of the appropriate τ program (the “logic component”) with a corresponding termination theory (the “control component”) which is not specified from within the semantics.

In contrast, this paper adopts a direct and self-contained approach. Instead of ‘asking’ about the control, a standard semantics of logic programs is enhanced by an oracle which at each step specifies from within the semantics the set of applicable clauses. Different notions of control are specified by different choices of oracles. In particular we focus on an oracle for pure Prolog. A pure Prolog program is a logic program in which an order is fixed for both clauses and goals in the body of clauses [Sterling and Shapiro 86]. Its meaning can be obtained by combining leftmost selection rule and sequential search for unifiable clauses. While the selection rule can easily be specified within the semantics, the specification of sequential search is done by an oracle. This oracle is obtained by viewing the Prolog program as a logic program and by reasoning about its meaning. This can be done both in a top-down manner, by means of a transition system, and in a bottom-up manner, using “T_{P} -like” methods. Furthermore, the oracle can be introduced into both transition system and T_{P} -based semantics. We believe that the approach is general and can be applied to extend a wide range of semantic definitions for logic programs to deal with various notions of control.

The oracle approach to the semantics provides the conditions for a generic oracle to ensure that desirable semantic properties of logic programs, such as the existence of a fixpoint semantics and the equivalence between top-down and bottom-up semantics, are satisfied for any oracledriven computations. This is particularly suitable for the definition of semantics as a basis for reasoning about program behavior and constructing abstract interpretations. Previous semantic definitions for Prolog have not been sufficiently useful for these purposes, although they have existed for some time. Instead, work on abstract interpretation, for example, has concentrated on abstracting semantics which ignore the depth-first nature of Prolog computation. Clearly the results of such analyses are inherently less accurate than the results of similar analyses based on truer semantics. We believe that this is largely due to the complexity of previous definitions in which information about control is mimicked but not explicitly specified. In contrast the semantic-based analysis of a program in our approach can be partitioned into the analysis of the logic component and the analysis of the control component. If no information about the control (which amounts to termination) is obtained then the result is equivalent to current commonly used analyses which ignore control. Otherwise, we can only gain in precision.

The following example illustrates the advantage of using a Prolog semantics instead of a logic programming semantics for the analysis of Prolog programs.

Example 1.1. Consider a logic program P in Table 1 which is intended to compute the sum of a list of numbers and check that it is positive (non-zero). There is a fundamental difference between the logic program P and the Prolog program P due to the depth-first strategy of the later. The Prolog program diverges when queried with positive sum list(X,Y) while the same goal has a refutation for the corresponding logic program.

   positive sum list(X,Y) ← list of numbers(X), sum(X,Y), positive(Y).  % (1)
   list of numbers([ ]).                                                % (2)
   list of numbers([X|Xs]) ← number(X), list of numbers(Xs).            % (3)
   number(0).                                                           % (4)
   number(s(X)) ← number(X).                                           % (5)
   sum([ ],0).                                                          % (6)
   sum([X|Xs],Z) ← sum(Xs,Y), add(X,Y,Z).                              % (7)
   add(0,X,X).                                                          % (8)
   add(s(X),Y,s(Z)) ← add(X,Y,Z).                                      % (9)
   positive(s(X)).                                                      % (0)

Table 1: A logic program.

Now, consider a simple semantic-based type analysis of the Prolog program P and query positive sum list(X,Y), like those proposed in [Barbuti and Giacobazzi 92], [Pyo and Reddy 89], and [Kanomori and Horiuchi 88], which ignore Prolog’s search strategy. Current implementations, such as those proposed in [Bruynooghe 91] and [Le Charlier and Van Hentenryck 94], easily detect that any answer for the call list of numbers(X) binds X to a list of numbers. However, a more accurate analysis based on a Prolog semantics could detect that clause (5) in the Prolog program is never applied. Hence X is bound to a list of zeroes. Consequently, for any call pattern of list of numbers, the predicate number in the Prolog program P is deterministic and hence the introduction of cuts is justified:

    number(0) ← !.                % (4′)
    number(s(X)) ← !, number(X).  % (5′)

Moreover, given such an analysis we can determine that the goal positive sum list(X,Y) will never succeed thus justifying the introduction of cuts in the predicate list of numbers:

    list of numbers([ ]) ← !.                                     % (2′)
    list of numbers([X|Xs]) ← !, number(X), list of numbers(Xs).  % (3′)

The transformed Prolog program is equivalent to P in the sense that it gives exactly the same answers for any call to positive sum list. However, the transformed program has a preferable behaviour as it does not diverge. Moreover it is deterministic and can be compiled more efficiently as described in [Debray and Warren 89]. The transformation described in this example can be viewed as transforming infinite failure into finite failure. Observe that similar transformations can be applied to introduce cuts to the predicates defining sum and add. However these can be justified without considering Prolog’s depth-first control strategy because they are called with their first arguments ground.

The rest of this paper is structured as follows: Section 2 presents some preliminary definitions and notations. Section 3 illustrates how a Prolog oracle is operationally specified and introduced into a transition system semantics for logic programs. This is fairly straightforward and the resulting semantics is concise and resembles standard transition system semantics for logic programs. However as a basis for program analysis we wish to obtain a T_{P} -like semantics, namely a fixpoint characterization of the program meaning. This is done in Section 4. In particular we define an unfolding-based oracle semantics which is proved to be equivalent to a corresponding bottom-up fixpoint oracle semantics. These semantics are shown to be sound and complete with respect to the operational one. In Section 5 we introduce a suitable oracle for sequential logic programs and for pure Prolog programs. While the first corresponds to a straightforward oracle, the second, once combined with the oracle-based semantics, provides a concise specification for fixpoint semantics of Prolog. We also discuss some approximations for the Prolog oracle showing how the oracle semantics can be abstracted for semantics-based program analysis. We close with a short conclusion. For continuity and ease of readability, the proofs together with auxiliary lemmata, have been moved to the appendix. This paper is an extended and revised version of [Barbuti, Codish, Giacobazzi and Maher 92]: in particular the ideas of [Barbuti, Codish, Giacobazzi and Maher 92] are reported in Sections 3 and 4.1.

2 Preliminaries

In the following we assume familiarity with the standard definitions and notation for logic programs. The standard reference works by Apt [Apt 90] and Lloyd [Lloyd 87] provide the necessary background material.

Given a possibly infinite set X, we denote by X^{∗} the set of finite sequences of symbols in X. The concatenation of sequences π_{1} and π_{2} is denoted π_{1} :: π_{2}. The sequence of symbols with first element s followed by the sequence S is denoted s | S. The empty sequence is denoted Λ. The length of a sequence π is denoted |π|. We extend this notation to denote set-cardinality. If R ⊆ X × X is a relation on X then R^{∗} denotes the reflexive and transitive closure of R. For any a, b ∈ X we denote a R^{k} b, for k ≥ 2, the relation ∃c ∈ X : a R c ∧ c R^{k−1} b, where R^{1} = R. If ∼ is an equivalence relation on X, we denote by [x]_{∼} the equivalence class of x ∈ X. When clear from the context we abbreviate [x]_{∼} by [x] and often abuse notation by letting the elements of a set denote their corresponding equivalence classes. In the following, Nat will denote the set of natural numbers. Moreover, we denote the power set of a set X by ℘(X). Finally, to specify function parameters, we often make use of Church’s lambda notation.

Let L(⊑, ⊥, ⊤, ⊔, ⊓) be a non empty complete lattice with partial ordering ⊑, least upper bound ⊔, greatest lower bound ⊓, top element ⊤ and bottom element ⊥. Let f : L → L be a function. We say that f is idempotent if f(f(x)) = f(x), reductive if f(x) ⊑ x, and additive if f(x⊔y) = f(x)⊔f(y), for every x and y. Functions are ordered as follows: f ⊑ g iff f(x) ⊑ g(x) for every x. The ordinal power of f is defined as usual: f↑0(x) = x, f↑α(x) = f(f↑(α − 1)(x)) for every successor ordinal α and f ↑α(x) = ⊔_{δ<α} f ↑δ(x) for every limit ordinal α. ω denotes the first limit ordinal. The fundamental theorem of Tarski states that the set of fixpoints of a monotonic function f is a complete lattice. The least fixpoint of a function f is denoted lfp(f). If f is a continuous function then lfp(f) = f↑ω(⊥) and is often denoted f↑ω.

Throughout, Σ, Π and V ar will respectively denote a set of function symbols, a set of predicate symbols and a denumerable set of variables. With each function symbol f ∈ Σ and predicate symbol p ∈ Π is associated a unique natural number called its arity; a (predicate or function) symbol f with arity n is written f/n. The non-ground term algebra over Σ and V ar is denoted T erm(Σ, V ar) or T erm for short. The corresponding Herbrand universe is T erm(Σ, ∅). In the following we will always implicitly consider non trivial Herbrand universes (i.e. containing more than one element). The set of atoms constructed from predicate symbols in Π and terms from T erm is denoted Atom(Π, Σ, V ar) or Atom for short. A goal is a sequence of atoms and we define Goal = Atom^{∗}. The empty atom sequence is denoted by true, and sometimes is omitted. A clause is an object of the form h ← B where h is an atom, called the head, and B is a goal, called the body. The set of clauses constructed from elements of Atom(Π, Σ, V ar) is denoted Clause(Π, Σ, V ar) or Clause for short. Syntactic equivalence for any syntactic object (e.g. terms, atoms, clauses, etc.) is denoted ≡. The set of variables that occur in a syntactic object t is denoted vars(t). A logic program is a (finite) set of clauses P. We sometimes associate with a program an ordering on the clauses of the program. In this case we let P_{ℓ} denote a program P and an injection ℓ : P → Nat. The injection ℓ is intended to reflect the textual ordering of the clauses in P as assumed in Prolog.

A substitution ϑ is a mapping from V ar to T erm which acts as the identity almost everywhere, i.e. such that its domain dom(ϑ) = {x ∈ V ar | ϑ(x) ≠ x} is finite. It extends to apply to any syntactic object in the usual way. The set range(ϑ) is defined as range(ϑ) = ∪_{x∈dom(ϑ)}vars(ϑ(x)). We will often make use of the set theoretic notation {x ↦ t | x ∈ dom(ϑ), ϑ(x) = t} to represent ϑ. The empty substitution is denoted ε. For a syntactic object s, we denote by ϑ_{|s} the restriction of ϑ to the variables of s. The application of a substitution ϑ to a syntactic object s is denoted by sϑ. If Θ is a set of substitutions, then sΘ = {sϑ | ϑ ∈ Θ}. Composition of substitutions ρ and σ is defined as usual and denoted ρσ. A substitution σ is idempotent if σσ = σ (or dom(σ) ∩ range(σ) = ∅). The set of idempotent substitutions is denoted Sub. A variable renaming is a (generally not idempotent) substitution which is a bijection on V ar. Syntactic objects t_{1} and t_{2} are equivalent up to renaming, denoted t_{1} ∼ t_{2}, if, for some variable renaming ρ, t_{1}ρ = t_{2}. We write t_{1} ≤ t_{2} iff there exists a substitution ϑ such that t_{1} = t_{2}ϑ. These notions can be extended on idempotent substitutions in the obvious way. Given an equivalence class (induced by renaming) t̂ of syntactic objects and a finite set of variables V ⊆ V ar, it is always possible to find a representative t of t̂ (i.e., an object t such that [t] = t̂) which contains no variables from V. Let I be a set of (equivalence classes of) syntactic objects and let s be a syntactic object. Then, A <<_{s} I denotes that A is a renaming (representative) of an element of I which does not share variables with s. Furthermore, we extend this to specify tuples of renamed apart syntactic objects:

⟨A_{1}, …, A_{n}⟩ <<_{s} I ⇔ ⋀_{i=1}^{n} (A_{i} <<_{s} I) ∧ ⋀_{i≠j} (vars(A_{i}) ∩ vars(A_{j}) = ∅)

The notion of unification can be given in terms of equations and equation solving. This is because the difference between unification and equation solving is only a matter of representation [Lassez, Maher, and Marriott 88]. An equation has the form t = u where t, u are syntactic objects and = is interpreted as syntactic equality. Given a set E of equations, E is unifiable iff there exists ϑ such that for each (t = u) ∈ E, (tϑ) ≡ (uϑ). We denote by Unif(E) the (possibly empty) set of unifiers of E. We fix a partial function mgu which maps a pair of syntactic objects (or a set of equations) into an idempotent most general unifier of the objects, if such exists. For sequences of syntactic objects (e.g. terms, atoms) ⟨t_{1}, ..., t_{n}⟩ and ⟨u_{1}, ..., u_{n}⟩, n ≥ 1, mgu(⟨t_{1}, ..., t_{n}⟩, ⟨u_{1}, ..., u_{n}⟩) is an equivalent notation for mgu({t_{1} = u_{1}, ..., t_{n} = u_{n}}). For a set of equations E: mgu(E) is an idempotent element in the set {ϑ ∈ Unif(E) | ∀ϑ′ ∈ Unif(E) : ϑ ≤ ϑ′}. mgu(E) = fail means that E is not unifiable. It is well known that the mgu of a set of equations is unique up to renaming (see [Eder 85] and [Lassez, Maher, and Marriott 88]). Let ϑ = {x_{1} ↦ t_{1}, ..., x_{n} ↦ t_{n}} be a substitution. We denote E(ϑ) = {x_{1} = t_{1}, ..., x_{n} = t_{n}}. For non-trivial Herbrand universes, ϑ = mgu(E) iff E has the same solutions as E(ϑ) (denoted E(ϑ) ≈ E) [Lassez, Maher, and Marriott 88].

3 Operational oracle semantics

This section presents an operational semantics for logic programs defined in terms of transition systems. The semantics is standard except for the fact that an oracle is introduced providing a uniform approach to capture different control strategies. In particular, we describe an oracle to capture the depth-first control strategy of Prolog.

3.1 Transition systems

Definition 3.1 (transition system). A transition system is a pair (X, R) consisting of a set X of states and a transition relation R ⊆ X × X on states.

In general, transition systems are applied to describe program meaning in terms of the transitive closure of the transition relation which specifies a basic computation step.

Definition 3.2 (derived states). Let Ψ = (X, R) be a transition system on states X. If s R^{∗} s′ then we say that s′ is derived from s. If s R^{k} s′ we say that s′ is derived from s in k steps.

A transition system can be viewed as associating a computation tree with (initial) states.

Definition 3.3 (computation tree). Let Ψ = (X, R) be a transition system and x ∈ X a state. The computation tree associated with x is the tree T (Ψ, x) with root x and inductively defined so that every state y derived from x is a vertex in the tree and has a child z iff y R z.

The notion of universal termination is formalized by the following:

Definition 3.4 (universal termination). Let Ψ = (X, R) be a transition system and x ∈ X a state. We say that x terminates universally for Ψ iff T (Ψ, x) is of finite height.

3.2 Transition systems for logic programs

The transition system approach is well suited and commonly applied to define semantics of logic languages. States are goals and correspond to resolvents, the transition relation specifies resolution and the transition system captures the computation tree for initial goals.

Definition 3.5 (transition system, Ψ_{P}^{lp}). Let P be a logic program. The transition system Ψ_{P}^{lp} is (Goal, ⟶^{lp}_{P}) where ⟶^{lp}_{P} ⊆ Goal×Goal is the smallest relation such that G⟶^{lp}_{P} G′ iff

1. G = ⟨A_{1}, …, A_{i}, …, A_{k}⟩, 1 ≤ i ≤ k;

2. H ← B_{1}, …, B_{n} <<_{G} P such that φ = mgu(A_{i}, H); and

3. G′ = ⟨A_{1}, …, B_{1}, …, B_{n}, …, A_{k}⟩φ.

The substitution φ is referred to as the associated substitution of the transition G⟶^{lp}_{P} G′.

The standard notion of a computation tree for an initial goal G and a program P is captured by T (Ψ_{P}^{lp}, G). Definition 3.5 is often refined (e.g. [Lloyd 87]) by introducing a selection rule on the atoms in a state. In particular, Prolog assumes a left-to-right selection rule. In addition logic programming languages typically introduce a control strategy to specify which clauses should be applied to the selected atom. Prolog employs a depth-first search strategy, applying the rules in textual order. In the following we introduce the notion of an oracle transition system in which an oracle is used to capture specific control features.

Definition 3.6 (oracle). An oracle is a function f : ℘(Clause) × Goal → ℘(Clause) such that for any logic program P and goal G: f(P, G) ⊆ P (i.e. f is reductive).

The following transition system employs a left-to-right selection rule. Moreover it enhances Definition 3.5, by introducing a generic oracle. A Prolog semantics is then derived as an instance of this definition by specifying an appropriate oracle. By Prolog, we mean pure Prolog in which evaluation is assumed to proceed until all answers are generated and that unification is sound and terminating (i.e. the occur check is performed).

Definition 3.7 (oracle transition system, Ψ_{P}^{f}). Let P be a Prolog program and f be an oracle. The transition system Ψ_{P}^{f} is (Goal, ⟶^{f}_{P}) where ⟶^{f}_{P} ⊆ Goal × Goal is the smallest relation such that G⟶^{f}_{P} G′ iff

1. G = ⟨A_{1}, …, A_{k}⟩;

2. H ← B_{1}, …, B_{n} <<_{G} f(P, G) such that φ = mgu(A_{1}, H); and

3. G′ = ⟨B_{1}, …, B_{n}, A_{2}, …, A_{k}⟩φ.

The substitution φ is referred to as the associated substitution of the transition G⟶^{f}_{P} G′. The substitution associated with a sequence of transitions is the composition of the substitutions associated with the transitions in the sequence.

The transition system Ψ_{P}^{slp} is defined by taking the oracle slp = λP.λG.P in Definition 3.7. This specifies what we call sequential logic programs which are logic programs executed with a left-to-right selection rule.

Intuitively, the computation tree for a Prolog program P and goal G corresponds to a pruning of T (Ψ_{P}^{slp}, G). The children of a node are assumed to be ordered to reflect the textual ordering of

[figure: G; leftmost infinite branch; _{P rolog answers}]

Figure 1: Prolog computation tree.

clauses in P and everything to the right of the left-most infinite path is excluded by the pruning (see Figure 1). Prolog evaluation corresponds to a depth-first, left-to-right traversal of the Prolog computation tree, and is assumed to find all of the alternative answers. This intuition can be applied to define a transition system for Prolog by imposing a condition on Ψ_{P}^{slp}, excluding goals which are to the right of an infinite branch. Consider an oracle prolog which, for a given program P, associates each goal with exactly those clauses in P which are eventually chosen by Prolog’s search strategy. In this case ⟶^{prolog}_{P} specifies (somewhat tautologously) the transition relation for P rolog. A similar argument can be applied to specify transition relations for Prolog with cut, and meta-logical predicates such as var(x) or negation. A less tautologous description of the Prolog oracle is provided as follows. Let P_{ℓ} be a Prolog program (where ℓ is the textual ordering) and let G be a goal. Then the clause C ∈ P is chosen by the oracle iff each path in T (Ψ_{P}^{slp}, G) starting with a transition which applies a clause C′ such that ℓ(C′) < ℓ(C) is finite. It is straightforward to show that the Prolog computation tree for a goal G and program P_{ℓ} terminates universally iff T (Ψ_{P}^{slp}, G) terminates universally [Vasak and Potter 86]. Furthermore, by Konig’s Lemma, T (Ψ_{P}^{slp}, G) terminates universally iff it is finite because ⟶^{slp}_{P} has finite branching. Hence,

Definition 3.8 (Prolog oracle). Let P be a logic program ordered textually by ℓ and G a goal. The Prolog oracle is given by

prolog(P, G) = \{ C ∈ P | \begin{matrix}Q = \{C′ | ℓ(C′) < ℓ(C)\}, \\ G⟶^{slp}_{Q}G′ ⇒ T (Ψ_{P}^{slp}, G′) is finite \end{matrix} \} .

Note that in contrast to ⟶^{lp}_{P} and ⟶^{slp}_{P}, the relation ⟶^{prolog}_{P} is not decidable (it is semidecidable). However, the vertices in T (Ψ_{P}^{prolog}, G) are recursively enumerable just as the vertices of T (Ψ_{P}^{lp}, G) and T (Ψ_{P}^{slp}, G). Moreover, approximations of Prolog semantics are derived by determining that a given clause is not chosen (for a given goal) by the Prolog oracle. This boils down to determining that a corresponding computation tree is infinite. This is similar to the proposal described in [Lever 91] to reason about SLS resolution [Przymusinski 89] applying loop-checking techniques. Some applications in dataflow analysis will be discussed in Section 5.

Example 3.1. Consider the program P from Example 1.1 and the goal positive list sum(X, Y). The Prolog computation tree is illustrated in Figure 2. To see why Prolog does not apply the clause (5) to the goal G (indicated in Figure 2 by a double arrow) it is sufficient to observe that the tree which first applies clause (4) to G is infinite. In this case, clause (5) is not in prolog(P, G).

The notion of the answers and partial answers for a goal G are defined as usual in transition system semantics by considering the substitutions associated with the corresponding sequences of transitions. We do not distinguish partial answers and the corresponding instances of the initial goal as computation proceeds.

Definition 3.9 (answers and partial answers). Let P be a logic program, G a goal and L ∈ {lp, slp, prolog}. We say that G′ is an L-partial answer for G (at depth k) iff G′ ∼ Gϑ where ϑ is the associated substitution of a sequence G⟶^{L}\begin{matrix}k \\ P \end{matrix} G′′ of transitions. If G′′ = true then G′ is a L-answer for G at depth k.

While it is well known ([Apt and van Emden 82]) that the answers for a goal are independent of the selection rule, this property does not extend to partial answers. For example, consider the program:

    p(x) ← q(x), r(x).
    r(s(x)) ← r(x).

The lp-partial answers for p(x) are {p(s^{n}(x))|n > 0}, whereas the slp-partial answers are {p(x)} (up to variable renaming). Furthermore, observe that the tree T (Ψ_{P}^{lp}, p(x)) has an infinite branch while T (Ψ_{P}^{slp}, p(x)) is finite.

We will need the following

Definition 3.10 (derivation paths). Let Ψ_{P}^{f} = (Goal, ⟶^{f}_{P}) be an oracle transition system for program P ordered textually by ℓ and oracle f. A derivation path for Ψ_{P}^{f} and goal G is an element π ∈ Nat^{∗} such that either π = Λ or π = ⟨n⟩ :: π′, where G⟶^{f}_{P} G′ by applying the clause C ∈ P, ℓ(C) = n and π′ is a derivation path for G′. A derivation from G to G′ with path π is denoted G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′.

Derivation paths (paths for short), namely sequences of symbols in Nat^{∗}, are denotations which represent the sequence of clauses applied in the derivation. We extend the notion of slp- and lp-partial answers to include paths in the obvious way. The link between paths and the depth of a computation is a consequence of the following straightforward proposition.

Proposition 3.1. Let L ∈ {lp, slp}. G′ is a L-(partial) answer at depth d for a goal G and program P iff it is a L-(partial) answer with path π for G and P and d = |π|.

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; positive list sum(X, Y); list of numbers(X), sum(X, Y), positive(Y); (1); (3); number(X′), list of numbers(Xs′), sum([X′ | Xs′], Y), positive(Y); (4); list of numbers(Xs′), sum([0 | Xs′], Y), positive(Y); (3); (2); sum([], Y), positive(Y); fail; (2); sum([0], Y), positive(Y); fail; G]

Figure 2: An example Prolog computation tree.

We adopt the convention that branches in a computation tree are labeled by the number of the clause applied. A finite subtree which does not contain a “true” leaf is indicated as fail.

4 Oracle declarative semantics

The objective of this section is to provide a semantic basis for the analysis of Prolog programs which maintains the simplicity of the T_{P} -based semantics for logic programs. We are motivated by the relative simplicity in constructing program analyses as abstractions of T_{P} semantics, as proposed in [Barbuti, Giacobazzi and Levi 93] and [Codish, Dams and Yardeni 94]. We aim to provide a semantics basis for more precise program analyses by introducing specific control issues into the semantics, following the approach illustrated above for transition systems. The reader is reminded that proofs have been deferred to the appendix.

The semantics we develop provides a success set from which Prolog answers can be determined. In order to specify the oracle from within the semantics we enhance the semantic objects to capture also partial computations and derivation paths. Our approach is based on the observation that both top-down and bottom-up semantics of logic programs can be expressed in terms of program unfolding [Levi 88]. Section 4.1 introduces a top-down unfolding semantics for logic programs with oracles. Later, in Section 4.3, a bottom-up unfolding semantics is introduced by allowing the same oracle to be applied in the process of unfolding, in a “reversed way”. In Sections 5.1 and 5.2 we consider two instances of the oracle semantics by specifying the declarative oracles slp and prolog.

The semantics we consider is that of partial computations, which includes the computed answer semantics as a special case. This facilitates the specification of both logic and control in a similar approach. As partial computations are dependent on the selection rule, we assume a leftto-right selection rule in what follows. Declarative semantics with selection rules for logic programs are independently proposed also in [Gabbrielli and Meo 92], by considering the more general family of local selection rules. We follow the approach of [Bossi, Gabbrielli, Levi and Meo 94] which defines a bottom-up semantics in which interpretations consist of clauses instead of atoms. Each clause in an interpretation represents a partial computation from its head to its body. We further enhance interpretations so that each clause is associated with a path indicating its position in a corresponding computation tree. The length of the paths in an interpretation provides a handle on the finiteness of computations, as needed for the oracle specification in the case of Prolog. Paths are ordered by the lexicographical ordering ⪯. The lexicographic ordering ⪯ on paths is defined by π ⪯ π′ iff π = p_{1}...p_{n}, π′ = p′_{1}...p′_{m} for p_{i}, p′_{i} ∈ Nat and either there exists an integer j such that p_{j} ≤ p′_{j} and for all i < j, p_{i} = p′_{j}, or n ≤ m and p_{i} = p′_{i} for 1 ≤ i ≤ n. This enables us to reason about such concepts as the “leftmost” infinite path in a computation tree.

Definition 4.1 (interpretations). Let H = Clause(Π, Σ, V ar)/_{∼} × Nat^{∗}. The domain of interpretations is Int = (℘(H), ⊆).

In order to view programs as interpretations, we let P_{ℓ} denote the interpretation associated with the program P ordered textually by ℓ, namely the set of clauses { (C; ℓ(C)) | C ∈ P_{ℓ} } . In what follows we will implicitly assume the existence of ℓ and, when clear from the context, we denote the interpretation P_{ℓ} by P.

The following definition extends the notion of an oracle (Definition 3.6) for interpretations. This provides suitable oracles for the declarative semantics. Their meaning is different from those defined in Definition 3.6. We associate an oracle with each program, specifying which clauses in an interpretation are applicable to a goal.

Definition 4.2 (declarative oracle). Let P be a program. An oracle for P is a function: f_{P} : Int × Goal → Int which is idempotent, additive and reductive in its first argument. When clear from the context the subscript P is omitted.

Idempotence specifies that the reduction to obtain the set of “applicable clauses” is all at once. Additivity specifies that a clause may be “applicable” independently from the other clauses in the current interpretation. As we will see later, the applicability of a clause in a Prolog computation depends only on its textual order in the program.

A difference between oracles according to Definition 3.6 (we will call them operational oracles) and declarative oracles is that the latter are defined over interpretations incorporating paths, whereas the former are not. For simplicity, in the following we refer to declarative oracles only. However, it is straightforward to extend the operational oracle semantics and related notions in Section 3 with declarative oracles, by interpreting programs P as corresponding interpretations P_{ℓ}. In particular, if f is a declarative oracle, we denote by G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ the sequence of transitions G⟶_{π}^{f′}\begin{matrix}∗ \\ P \end{matrix} G′, where f′ is the operational oracle defined by f′(P, G) = f(P_{ℓ}, G).

In general an oracle f(I, G) for a program P specifies the set of clauses in an interpretation I for P which are applicable to the goal G. In the following we will focus on the class of downward closed and sound oracles which include in particular the Prolog oracle.

Downward closure is specified on both of the oracle arguments. It specifies the reduction implemented by the oracle in terms of the instantiation of its arguments. In particular we require that the applicability of a clause will not depend on its degree of instantiation, as in Prolog, where the applicability condition for a clause depends upon the preceding clauses in the textual order. In the following, for an oracle f, the applicability of a clause C to a goal G is expressed by f({C}, G) ≠ ∅. Note that the applicability condition for a clause C to a goal G does not imply that C and G unify.

Definition 4.3 (downward closed oracles). An oracle f is downward closed iff for each interpretation I, goals G and G′, clause C and substitution ϑ:

• f(I, G) ⊆ f(I, Gϑ);

• f(I, G :: G′) ⊆ f(I, G);

• f({C}, G) ≠ ∅ ⇔ f({Cϑ}, G) ≠ ∅.

Note that the second condition is related with the left-to-right selection rule of Prolog. Downward closure of the oracle implies the following propositions. The first shows that variable names are not significant.

Proposition 4.1 (∼-congruence). Let f be a downward closed oracle for a program. Then, for any interpretation I and goals G, G′: G ∼ G′ ⇒ f(I, G) = f(I, G′).

The following property is similar to properties of stability [Gaifman, Maher and Shapiro 91] and monotonicity [Saraswat, Weinbaum, Kahn and Shapiro 88] in relation to concurrent languages.

Proposition 4.2. Let P be a program and f be a downward closed oracle for P. If G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ with associated substitution ϑ, then Gϑ⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′′ and G′′ ∼ G′.

The converse (i.e. Lifting Lemma 8.2 in [Lloyd 87]) may not hold (e.g. for the Prolog oracle), as shown in the following example:

Example 4.1. Consider the following Prolog program P:

    \begin{matrix}p(s(x)) ← p(x). \\ p(x). \end{matrix}

While the goal p(0) succeeds in a Prolog transition system semantics, p(x) does not.

We now generalize the notion of partial answers for declarative oracles and interpretations.

Definition 4.4 (f-answers and f-partial answers). Let f : Int × Goal → Int be an oracle for a program P, I ∈ Int an interpretation and G = ⟨a_{1}, …, a_{n}⟩ a goal. We say that G′ is an f-partial answer for G with path π in I iff there exists k ∈ {1, ..., n} such that for each 1 ≤ i ≤ k: (h_{i} ← B_{i}, π_{i}) <<_{Gϑ_{i−1}} f(I, (a_{i}, ..., a_{n})ϑ_{i−1}) where ϑ_{0} = ε, B_{i} = true for i < k, ϑ_{i} = ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}), Gϑ_{k} ∼ G′ and π = π_{1} :: ⋯:: π_{k}. The corresponding resolvent in I with path π is (B_{k} :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ_{k}. If k = n and B_{k} = true then G′ is a f-answer for G in I with path π. The set of f-partial answers with paths for G in I is denoted

P^{f}(I, G) = \{ (G′, π) | \begin{matrix}G′is an f-partial answer \\ of G with path π in I \end{matrix} \} .

In the following we denote by Φ the interpretation { ([p(x̄) ← p(x̄)]_{∼}; Λ) | p ∈ Π } where each clause is a tautology and each path is empty. This interpretation associates any goal G with the corresponding empty partial computations. As in [Bossi, Gabbrielli, Levi and Meo 94], it is used to simplify the presentation of the semantics of partial computations given below.

4.1 Top-down unfolding-based oracle semantics

The unfolding semantics mimics the operational semantics by a top-down construction in which a clause (h ← B; π) represents a partial computation from h to B and π indicates the position of the partial computation in the proof-tree. This results in a natural extension of the oracle-based operational semantics to the unfolding semantics construction.

Definition 4.5 (unfolding oracle semantics). Let P be a logic program, f a declarative oracle for P and I an interpretation.

Unf_{P}^{f} (I) = \{ ([(h ← B)σ]_{∼}; π :: ⟨l⟩) | \begin{matrix}C ≡ (h ← b_{1}, …, b_{n}; π) ∈ I, \\ (h′ ← B′; l) <<_{C} f(P, (b_{1}, …, b_{n})), \\ σ = mgu(b_{1}, h′), \\ B = B′ :: ⟨b_{2}, …, b_{n}⟩ \end{matrix} \}

The following proposition is an immediate consequence of the definition..

Proposition 4.3. λI.Unf_{P}^{f} (I) is additive.

The unfolding process is intended to capture all partial computations for arbitrary initial goals. In the case of logic programs it is sufficient to consider answers (or partial answers) for goals of the form p(x_{1}, ..., x_{n}). However as illustrated by Example 4.1 this is not the case for our oracle-based semantics due to the lack of the lifting lemma. Therefore, we initiate the unfolding process with any instance of a tautological clause i.e. an element of lwr(Φ), where

lwr(I) = \{ (h ← B; π)ϑ | \begin{matrix}(h ← B; π) ∈ I \\ dom(ϑ) ⊆ vars(h) \end{matrix} \}

for any interpretation I.

Definition 4.6 (unfolding-based fixpoint semantics). Let P be a program, f be a corresponding oracle and U_{P}^{f} = λI.Unf_{P}^{f} (I ∪lwr(Φ)). The unfolding semantics of P is lfp(U_{P}^{f}).

Note that the unfolding of a clause in Φ with any clause C is the clause C itself; thus in the first step U_{P}^{f} (∅) collects all the clauses in lwr(P) which are applicable to an atomic goal:

U_{P}^{f} (∅) = \{ (h ← B; l)σ | \begin{matrix}(h ← B; l) ∈ f(P, h′) \\ σ = mgu(h, h′), h′ ∈ Atom \end{matrix} \} .

More generally we can state the following lemma which is a straightforward consequence of the definition and of the downward closure of the oracle.

Lemma 4.4. Let P be a program and f be an oracle. If [C]_{∼} ∈ lfp(U_{P}^{f}) then lwr({[C]_{∼}}) ⊆ lfp(U_{P}^{f}).

By Unf_{P}^{f} additivity, lfp(U_{P}^{f}) can be obtained as the limit of the sequence:

U_{P}^{f}↑1 = Unf_{P}^{f} (lwr(Φ)),

U_{P}^{f}↑n = Unf_{P}^{f} (U_{P}^{f}↑(n − 1)) ∪ Unf_{P}^{f} (lwr(Φ)) for n > 1.

According to the structure of this sequence, by a straightforward induction on n we can prove the following

Lemma 4.5. Let P be a program, f be an oracle and (c; π) ∈ U_{P}^{f}↑ω. Then |π| = n iff (c; π) ∈ Unf_{P}^{f}↑n(lwr(Φ)).

Thus, by definition: (c; π) ∈ U_{P}^{f}↑ω, |π| ≤ n iff (c; π) ∈ U_{P}^{f}↑n.

The following result specifies how the oracle based semantics preserves the ordering among arbitrary oracles.

Theorem 4.6. Let P be a program and f, g be oracles for P. If for each interpretation I and goal G: f(I, G) ⊆ g(I, G) then lfp(U_{P}^{f}) ⊆ lfp(U_{P}^{g}).

Among the set of oracles, we can distinguish the identity oracle, slp = λIλG.I (see Section 5.1 for a semantic interpretation of slp) and the empty oracle, ⊥ = λIλG.∅. They are, respectively, the greatest and least oracles. Consequently, for any oracle f, ∅ = lfp(U_{P}^{⊥}) ⊆ lfp(U_{P}^{f}) ⊆ lfp(U_{P}^{slp}).

4.2 Relation between fixpoint and operational oracle semantics

The relation between unfolding-based oracle semantics and the transition-system semantics with oracles is provided by soundness and completeness results. We need to restrict the class of oracles to obtain these desirable results.

Definition 4.7 (oracle soundness). Let P be a program. An oracle f for P is sound with respect to unfolding iff for each goal g | G,

g | G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} (B :: G)ϑ with substitution ϑ ⇒ f (\{(g ← B; π)ϑ\}, g | G) ≠ ∅.

By the soundness condition, the sequential applicability of clauses to a goal implies the applicability to the same goal of a modified clause corresponding to their sequential application. This property allows us to merge the sequential applicability of different clauses into a single applicable clause, and plays a central role in proving soundness and completeness of the declarative oracle semantics.

Example 4.2. Consider the program P in Example 1.1. The soundness condition is clearly verified by the typical Prolog’s search strategy. For instance (see Figure 2), if clause (1) is applicable to the goal positive list sum(X,Y) and clause (3) is applicable to the resulting goal:

                     list of numbers(X), sum(X, Y), positive(Y),

resulting in the state B = number(X′), list of numbers(Xs′), sum([X′ | Xs′], Y), positive(Y), then the clause obtained by combining the application of (1) and (3):

                       (positive list sum(X, Y) ← B; ⟨1⟩ :: ⟨3⟩)

is applicable to the initial goal positive list sum(X,Y). The soundness of the prolog oracle will be formally discussed in Section 5.

Example 4.3. Consider the program P

                                 \begin{matrix}p ← q. & % (1) \\ q ← r. & % (2) \end{matrix}

Define an oracle f for P as follows. For singleton interpretations we define

f({(p ← q; π)}, G) = {(p ← q; π)}
f({(q ← r; π)}, G) = {(q ← r; π)}
f({(c; π)}, G) = ∅

for every goal G and path π, and every clause c except the clauses in P. For other interpretations we define f(∪_{j}I_{j}, G) = ∪_{j}f(I_{j}, G) for every goal G.

f is a downward closed oracle for P (we leave verification of this fact to the reader) but it is not sound with respect to unfolding. Clearly p ⟶_{⟨1⟩::⟨2⟩}^{f}\begin{matrix}∗ \\ P \end{matrix} r. However f(\{(p ← r; ⟨1⟩ :: ⟨2⟩)\}, p) = ∅.

In the following we restrict our attention to downward closed and sound oracles only.

The following theorem states the soundness of the unfolding-based fixpoint semantics with respect to the operational one. In the following we will implicitly assume partial answers with non empty paths. It is worth noticing that empty partial answers can be obtained from any goal by applying clauses in Φ.

Theorem 4.7 (soundness). Let P be a program, f an oracle for P, G a goal and ϑ the substitution associated with G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′. Then, Gϑ is an f-partial answer of G with path π in the interpretation lfp(U_{P}^{f}) and G′ ∼ G′′, where G′′ is the corresponding resolvent with path π in lfp(U_{P}^{f}).

To prove a completeness result for the fixpoint semantics with respect to the operational one, we need an additional property for the oracles. For this purpose we introduce the notion of U-derivable clauses. This allows us to consider only clauses which may be part of a computation for the program.

Definition 4.8 (U-derivable clauses). A clause (c; π) is U-derivable (in a program P) iff (c; π) ∈ lfp(U_{P}^{slp}).

Because interpretations and programs have the same structure, in the following we abuse by letting I be a generic interpretation in Unf_{I}^{f}.

Definition 4.9 (oracle completeness). Let P be a program. An oracle f for P is complete with respect to unfolding iff for each goal g | G and U-derivable clauses (h ← B; π) and (c; π′) sharing no variables with g | G and with each other, if f(Unf_{{(c;π′)}}^{slp}({(h ← B; π)}), g | G) ≠ ∅ and mgu(h, g) ≠ fail then

• f({(h ← B; π)}, g | G) ≠ ∅, and

• f({(c; π′)}, (B :: G)mgu(h, g)) ≠ ∅.

By completeness we can decompose the applicability condition for the unfolding of clauses in terms of the sequential applicability of each clause involved in the process. Therefore, if a U-derivable clause is applicable to a goal, each clause in the derivation is sequentially applicable to the same goal. This corresponds precisely to the reverse case of the soundness condition for U-derivable clauses.

Example 4.4. Consider the program P in Example 1.1. The completeness condition is clearly verified by the typical Prolog’s search strategy. For instance (see Figure 2 and Example 4.2), if clause

                       (positive list sum(X, Y) ← B; ⟨1⟩ :: ⟨3⟩)

where B = number(X′), list of numbers(Xs′), sum([X′ | Xs′], Y), positive(Y), is applicable to the goal positive list sum(X, Y), then both clause (1) and (3) are applicable to the goals

positive list sum(X, Y) and list of numbers(X), sum(X, Y), positive(Y) respectively. The com-

pleteness of the prolog oracle will be formally discussed in Section 5.

Example 4.5. Consider the program P from Example 4.3, and define an oracle f for P as follows. For singleton interpretations we define

f({(p ← r; π)}, G) = (p ← r; π)
f({(c; π)}, G) = ∅

for every goal G and path π, and every clause c except p ← r. For other interpretations we define f(∪_{j}I_{j}, G) = ∪_{j}f(I_{j}, G) for every goal G.

f is a downward closed oracle for P and is sound, but it is not complete with respect to unfolding. First note that (p ← q; ⟨1⟩) and (q ← r; ⟨2⟩) are U-derivable clauses. Taking (p ← q; ⟨1⟩) for (h ← B; π) and (q ← r; ⟨2⟩) for (c; π′) in the definition of oracle completeness, we find that Unf_{{(c;π′)}}^{slp}({(h ← B; π)}) contains (p ← r; ⟨1⟩ :: ⟨2⟩). Thus, considering the goal p (corresponding to g | G), f(Unf_{{(c;π′)}}^{slp}({(h ← B; π)}), p) ≠ ∅. However both f({(p ← q; ⟨1⟩)}, p) and f({(q ← r; ⟨2⟩)}, q) are empty. Hence f is not complete.

In the following we will assume sound and complete oracles when not specified otherwise.

While for soundness we require the introduction of lwr(Φ) to the semantics, for completeness we must consider, for each path, only the most general partial answers. It is precisely because of the presence of paths that we are able to provide in this way the completeness result. The following lemma shows that any clause in lfp(U_{P}^{f}) can be viewed as an instance of a clause obtained by iterating unfolding on a tautological clause in Φ.

Lemma 4.8. Let P be a program, f be a corresponding oracle and (c; π) ∈ Unf_{P}^{f}↑n(lwr(Φ)). Then (c; π) ∈ lwr({(c′; π)}) for some (c′; π) ∈ Unf_{P}^{slp}↑n(Φ).

The following lemma ensures that for any atomic goal h and path π there exists a most general partial answer with path π in P^{f}(lfp(U_{P}^{f}), h).

Lemma 4.9. Let h be an atomic goal, π be a path such that |π| = n and D = { h′ | (h′; π) ∈ P^{f}(lfp(U_{P}^{f}), h) }. If D ≠ ∅ then lub_{≤}D ∈ D and lub_{≤}D = hϑ where ϑ = mgu(h, h′) for (h′ ← B′; π) ∈ Unf_{P}^{f}↑n({h ← h; Λ}).

It is straightforward to extend the previous lemma to possibly non atomic goals, as stated in the following corollary

Corollary 4.10. Let G be a goal, π be a path and D = { G′ | (G′; π) ∈ P^{f}(lfp(U_{P}^{f}), G) }. If D ≠ ∅ then lub_{≤}D ∈ D.

Let P be a program and f be a corresponding oracle. We denote by mgp^{f}(P, G) the set of most general f-partial answers (with paths) for G in lfp(U_{P}^{f}). Notice that mgp^{f}(P, G) ⊆ P^{f}(lfp(U_{P}^{f}), G).

We can now prove the following completeness result for the oracle semantics.

Theorem 4.11 (completeness). Let P be a program, f an oracle for P, and G a goal. If Gϑ is the most general f-partial answer of G with path π in lfp(U_{P}^{f}) and G′′ is the corresponding resolvent then G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ with associated substitution ϑ′, Gϑ ∼ Gϑ′ and G′′ ∼ G′.

Combining this theorem with Theorem 4.7 and Corollary 4.10 we have the following characterization of answers and partial answers computed with the oracle f in terms of U_{P}^{f}. Recall that we assume f is downward-closed, and sound and complete with respect to unfolding.

Theorem 4.12. Let P be a program and f an oracle for P. Let G, G′, G′′ be goals and ϑ, ψ be substitutions. Suppose G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ with associated substitution ϑ and suppose Gψ is the most general f-partial answer of G with path π in lfp(U_{P}^{f}) and G′′ is the corresponding resolvent. Then Gϑ ∼ Gψ and G′ ∼ G′′.

4.3 Bottom-up oracle semantics

Top-down constructions typically unfold clauses from an interpretation (a set of partial computations) with program clauses. In contrast, bottom-up constructions involve the unfolding of program clauses with clauses from an interpretation ([Levi 88]). The two approaches correspond to top-down and bottom-up constructions of the computation trees. A bottom-up oracle semantics is derived by switching the role of the program and the interpretation in Definition 4.5. In this case we are able to specify directly a semantics for successful computations. Hence, in the bottom-up construction each step proceeds by unfolding the atoms in the body of a program clause h ← b_{1}, ..., b_{n} with a successful computation (unit clauses from an interpretation) for each b_{i}. The oracle, in this case, has two different functionalities: (1) to specify which program clauses should be unfolded; and (2) to specify which computations it should be unfolded with. In addition, left-to-right selection of atoms is modeled by performing the unfolding in a sequence from left-to-right. The following definition introduces the oracle-based bottom-up immediate consequence operator. The operator T_{P}^{f} constructs the success set in a bottom-up way by applying applicable successful computations in I to the bodies of program clauses. Notice that not all the clauses can contribute to the semantics; there are clauses never chosen by the oracle, and clauses which can be chosen only under further instantiation of the variables in the head. To model this behaviour, we consider clauses in lwr(P).

Definition 4.10 (bottom-up oracle semantics). Let P be a logic program ordered textually by ℓ, let f be an oracle for P and I an interpretation. We define

T_{P}^{f} (I) = \{ [(h ← true; π̄_{n})σ_{n}]_{∼} | \begin{matrix}C ≡ (h ← b_{1}, …, b_{n}; l) ∈ f(lwr(P), h), \\ σ_{0} = ε, π̄_{0} = ⟨l⟩ and for each 1 ≤ i ≤ n: \\ (h_{i} ← true; π_{i}) <<_{Cσ_{i−1}} f(I, (b_{i}, ..., b_{n})σ_{i−1}), \\ σ_{i} = σ_{i−1}mgu(b_{i}σ_{i−1}, h_{i}), π̄_{i} = π̄_{i−1} :: π_{i} \end{matrix} \} .

Proposition 4.13. T_{P}^{f} is continuous.

The next result provides the equivalence of top-down and bottom-up oracle semantics for successful computations. To prove the claim we need the following lemmata.

Lemma 4.14 (AND-compositionality). Let P be a program, G = b_{1}, ..., b_{n} be a goal and f be an oracle for P. ⟨b_{1}, ..., b_{n}⟩⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} true is a refutation for G with substitution ϑ iff

1. for each 1 ≤ i ≤ n: ϑ_{i} and π_{i} are the substitution and path associated with the refutation

(b_{i})ϑ_{1}...ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} true for the goal (b_{i})ϑ_{1}...ϑ_{i−1};

2. π = π_{1} :: ⋯:: π_{n};

3. f({(b_{i} ← true)ϑ_{1}...ϑ_{i}; π_{i})}, (b_{i}, ..., b_{n})ϑ_{1}...ϑ_{i−1}) ≠ ∅; and

4. (b_{1}, ..., b_{n})ϑ ∼ (b_{1}, ..., b_{n})ϑ_{1}...ϑ_{n}.

The following lemma is a consequence of the oracle completeness.

Lemma 4.15. Let P be a program, f be an oracle for P, h ∈ Atom and a | G be a goal. If h⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} B with

substitution ϑ, f(\{(h ← B; π)ϑ\}, a | G) ≠ ∅ and mgu(hϑ, a) ≠ fail then a | G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} (B ::

G)ϑmgu(hϑ, a).

Theorem 4.16. Let P be a program and f an oracle for P. Then,

lfp(T_{P}^{f}) = \{ (hϑ ← true; π) | \begin{matrix}h⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} true \\ with substitution ϑ \end{matrix} \} .

Using the previous theorem and the soundness and completeness of the top-down fixpoint semantics (Theorem 4.12) we can show that the top-down and bottom-up fixpoint semantics are compatible.

Corollary 4.17. Let P be a program and f an oracle for P. Then,

lfp(T_{P}^{f}) = { (h ← true; π) | (h ← true; π) ∈ lfp(U_{P}^{f}) } .

Consequently, oracle based-computations can be characterized by means of both a top-down and bottom-up semantic constructions.

Corollary 4.18. Let P be a program, f an oracle for P and G a goal. G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} true with associated substitution ϑ iff Gϑ is the most general f-answer of G with path π in lfp(T_{P}^{f}).

5 Applications

In this section we introduce two examples of oracles: one for slp-programs and one for Prolog programs.

5.1 The oracle for slp

For slp-programs the order of clauses does not affect the computation. Thus any clause can be applied to a given goal provided that unification succeeds. This behaviour is captured by the oracle slp = λI.λG.I returning the whole set of clauses. It is easy to see that slp is downwardclosed and sound and complete with respect to unfolding. The declarative semantics defined as the set of most general answers in α(lfp(T_{P}^{slp})) corresponds precisely to the semantics in [Falaschi, Levi, Martelli and Palamidessi 89] of computed answer substitutions. This equivalence is based on the observation that in slp-computations the Lifting Lemma holds [Lloyd 87]; i.e. it cannot be the case that a clause is not applicable while some of its instantiations are. Thus, applying all the instances (by lwr) of a clause and taking the most general computations corresponds to simply applying the clause itself. Similarly, the multiset semantics of [Maher and Ramakrishnan 89] computed by NSN evaluation can be extracted from lfp(T_{P}^{slp}).

5.2 The oracle for Prolog

The Prolog oracle is defined, as in the operational case, in terms of the logic programming semantics with left-to-right selection. Namely, the declarative Prolog oracle is defined in terms of the set of partial computations with paths as given by lfp(U_{P}^{slp}). Each interpretation is totally ordered with respect to the lexicographic ordering ⪯ on paths. This ordering is adequate to declaratively specify a depth-first search strategy on the proof tree. In the following examples a sequence of n elements is denoted a_{1} · a_{2} · . . . · a_{n}, and a^{n} denotes a · a · . . . · a with n occurrences of a.

Example 5.1. Consider the Prolog program P:

                            q(x,y) ← p(x,y).  % (1)
                            p(a,b).            % (2)
                            p(x,y) ← p(x,y).  % (3)
                            p(x,x).            % (4)

lfp(U_{P}^{slp}) = lwr (\{ \begin{matrix}(p(x, y) ← p(x, y); 3^{n+1}), \\ (p(a, b); 3^{n} · 2); (p(x, x); 3^{n} · 4); \\ (q(x, y) ← p(x, y); 1 · 3^{n}), \\ (q(a, b); 1 · 3^{n} · 2); (q(x, x); 1 · 3^{n} · 4) \end{matrix} | n ≥ 0 \}) .

The corresponding partial answers (for an arbitrary goal) are totally ordered by the lexicographical ordering on paths. Consider the successful computation for the goal q(x, y): (q(x, x); 1·3·4). The partial computations to the “left” include for instance: (q(a, b); 1 · 3^{n} · 2) for n ≥ 0. The only computation “to the the right” of (q(x, x); 1 · 3 · 4) is (q(x, x); 1 · 4). By the soundness and completeness of the semantics, this behaviour is modeled by the most general partial answers in lfp(U_{P}^{slp}).

Intuitively, if P is a Prolog program and C ≡ (h ← b_{1}, ..., b_{n}; π) represents a partial computation with path π from the goal h to the resolvent b_{1}, ..., b_{n}; then the declarative Prolog oracle for P should specify that the clause C′ ≡ (h′ ← B′; l′) can be applied to the goal b_{1}, ..., b_{n} iff the computation which applies any of the previous clauses universally terminates. This is formalized by introducing the notion of most general partial answers (mgp) which characterizes the set of most general slp-partial answers for a goal G in lfp(U_{P}^{slp}) that have paths to the left of a path π

mgp_{π}^{slp}(P, G) = \{ ([G′]_{∼}; π′) | \begin{matrix}([G′]_{∼}; π′) ∈ mgp^{slp}(P, G) \\ π′ ≺ π \end{matrix} \} .

We can use slp-partial answers instead of prolog-partial answers because the universal termination behaviour of Prolog programs is identical to the universal termination behaviour of sequential logic programs. Thus, we can give the following

Definition 5.1 (declarative Prolog oracle). Let P be a program, I ∈ Int and G be a goal. Then,

prolog_{P} (I, G) = { (c, π) ∈ I | mgp_{π}^{slp}(P, G) is finite }

As usual, when clear from the context the subscript P is omitted.

Example 5.2. Consider the Prolog program P in Example 5.1. The fourth clause cannot be applied to the goal p(x, y) because:

∀n ≥ 0 : (p(a, b); 3^{n} · 2), (p(x, x); 3^{n+1} · 4) ∈ mgp_{⟨4⟩}^{slp}(P, q(x, y)).

We now prove that prolog is an oracle in its declarative meaning (i.e. an additive lower closure which is downward closed, sound and complete). It is straightforward to prove that λI.prolog(I, G) is idempotent, additive and reductive. Moreover

Proposition 5.1. The function prolog is a downward closed oracle.

Proposition 5.2. The oracle prolog is sound and complete with respect to unfolding.

The equivalence between the declarative and the operational definitions of the Prolog oracle is a consequence of the following theorem.

Theorem 5.3. Let P be a program textually ordered by ℓ, C ∈ P, Q = { C′ | ℓ(C′) < ℓ(C) }, and G be a

goal. Then, G⟶^{slp}_{Q}G′ ⇒ T (Ψ_{P}^{slp}, G′) is finite iff mgp_{⟨ℓ(C)⟩}^{slp}(P, G) is finite.

Example 5.3. Consider the Prolog program P in Example 5.1. The only goal G such that T (Ψ_{P}^{slp}, G) is finite is G = true. Thus the evaluation of lfp(U_{P}^{prolog}) proceeds as follows, for each n ≥ 0:

(T_{P}^{prolog})^{n}(∅) = \{ \begin{matrix}(p(a, b); 3^{m} · 2) \\ ((p(x, y) ← p(x, y))σ; 3^{m}), \\ (q(a, b); 1 · 3^{m} · 2), \\ ((q(x, y) ← p(x, y))σ; 1 · 3^{m}) \end{matrix} | \begin{matrix}m ≤ n, \\ σ substitution \end{matrix} \} .

Since the only clause for p with an empty body in lfp(U_{P}^{prolog}) is p(a, b), we can argue that the (Prolog) success set for p in P is {p(a, b)}.

Example 5.4. Consider the Prolog program P:

                        p(a,b).                   % (1)
                        p(c,b).                   % (2)
                        p(x,y) ← p(y,x).         % (3)
                        p(x,y) ← p(x,z),p(z,y).  % (4)

This program is used by Lloyd [Lloyd 87] to illustrate the incompleteness of Prolog’s search strategy. The claim is that: “no matter how the clauses of P are ordered and no matter what the computation rule, a depth-first search with fixed order of program clauses will never find a solution for p(a, c)”. The Prolog semantics is:

lfp(U_{P}^{prolog}) = \{ \begin{matrix}(p(a, b); 3^{2n} · 1), (p(c, b); 3^{2n} · 2) \\ (p(b, a); 3^{2n+1} · 1), (p(b, c); 3^{2n+1} · 2) \end{matrix} | n ≥ 0 \} ,

with a corresponding success set for P: {p(a, b), p(c, b), p(b, a), p(b, c)}. Because clauses (3) and (4) have completely general heads, they match with any partial computation. Thus if (3) is before (4) in the program, the system will never consider (4) and viceversa [Lloyd 87]. This behaviour is captured in our semantics construction. In particular, for each partial computation G = p(t_{1}, t′_{1}), ..., p(t_{n}, t′_{n}), the clause (p(x, y) ← p(x, z), p(z, y); 4) ∉ prolog(P, G) because, ∀n ≥ 0 we have (p(x, y) ← p(x, y); 3^{2n}), (p(x, y) ← p(y, x); 3^{2n+1}) ∈ lfp(U_{P}^{slp}). Thus ∀n ≥ 0

(p(t_{1}, t′_{1}), ..., p(t_{n}, t′_{n}); 3^{2n}), (p(t′_{1}, t_{1}), ..., p(t_{n}, t′_{n}); 3^{2n+1}) ∈ mgp_{⟨4⟩}^{slp}(P, G).

A similar behaviour can be verified by changing the order of clauses 3 and 4:

                        p(a,b).                   % (1)
                        p(c,b).                   % (2)
                        p(x,y) ← p(x,z),p(z,y).  % (3)
                        p(x,y) ← p(y,x).         % (4)

where ∀n ≥ 1: (p(x, y) ← p(x, z_{n}), ..p(z_{n}, z_{n−1}).., p(z_{1}, y)); 3^{n}) ∈ lfp(U_{P}^{slp}). As before, the clause (p(x, y) ← p(y, x); 4) cannot be applied to any partial computation.

5.3 Approximations

In the previous section we have shown how to capture declaratively the semantics of a Prolog program P by enhancing the standard semantics for pure logic programs with an oracle. Of course it is not possible in general to provide an oracle which corresponds precisely to prolog. However, since we are interested to provide a semantic basis for the analysis of Prolog programs, for this purpose approximations of prolog both from above and from below can be useful. A similar argument has been considered in [Barbuti, Codish, Giacobazzi and Levi 92] and [Barbuti, Codish, Giacobazzi and Levi 93], which also provides a semantic basis for Prolog program analysis. By Theorem 4.6 we can distinguish between two possible approximations for the prolog oracle:

• \underline{from above:} let f_{a} be an oracle such that for each goal G: λI.f_{a}(I, G) ⊇ λI.prolog(I, G). In this case we have lfp(U_{P}^{prolog}) ⊆ lfp(U_{P}^{f_{a}}), hence providing an approximation from above of the (Prolog) success set for P. This may provide better approximations than can be achieved when abstracting the meaning of P as a logic program (i.e. with the oracle slp).

• \underline{from below:} let f_{b} be an oracle such that for each goal G: λI.f_{b}(I, G) ⊆ λI.prolog(I, G). In this case we have lfp(U_{P}^{f_{b}}) ⊆ lfp(U_{P}^{prolog}), hence providing an approximation from below of the (Prolog) success set for P which can be useful for example in the context of the complexity analysis described in [Debray and Lin 91]; or to estimate a lower bound to the number of solutions of P.

Figure 3 illustrates the computation tree for a logic program P and a goal G for a left-to-right selection rule in which the left most infinite branch is indicated. The solutions for G correspond to the success branches of the entire tree. These can be derived by considering the trivial oracle slp. The solutions for G assuming Prolog’s depth-first strategy are those which are to the left of the infinite branch. These can be derived with prolog. Approximations of the Prolog solutions for G from above and below can be derived by any oracles f_{a} and f_{b} which, respectively, approximate prolog from above and from below.

Approximation from below corresponds to the use of knowledge concerning definite (universal) termination of subgoals, whereas approximation from above corresponds to the use of knowledge concerning definite non-termination of subgoals. A survey of techniques for establishing termination and non-termination is given in [De Schreye and Decorte 94].

Example 5.5. In this example we consider approximations from below and above in the dataflow analysis of variable aliasing for a simple logic program. Consider the following fragment of a Prolog program

                          p(a,b) ← q(b).        % (1)
                          p(X,f(Y)) ← q(f(Y)).  % (2)
                          p(X,X).                % (3)

with the hypothesis that goal q(b) definitely terminates (terminates universally), while goal q(f(Y)) may have some solutions but it is not definitely terminating. It is easy to see that an approximation from below, which collects computations from definitely terminating goals only, concludes that ground substitutions are computed for the goal p(X,Y). By approximating from above, namely by discarding inapplicable computations, we can observe variable independence between X and Y. This because clause (3) cannot be applied to the goal. With the straightforward oracle slp instead, we lose precision by observing also a variable aliasing between X and Y, which is introduced by clause (3). The latter aliasing is not computed by a Prolog interpreter.

6 Conclusions

We have presented an oracle approach for specifying the semantics of pure Prolog programs. The key idea is to separate the notions of logic and control in the semantic definition. This approach results in simple and concise semantic definitions which are useful in proving properties of programs and in the context of semantic based techniques for analysis and debugging. By factoring the semantics into two components, we provide a semantic foundation to combine results on termination analysis (e.g. see [Apt, Bol and Klop 89], [Apt and Pedreschi 93], [Smith, Genesereth and Ginsberg 86], [Verschaetse and De Schreye 91], and

[figure: G; _{prolog}; _{f_{b}}; _{f_{a}}; _{slp}; leftmost infinite branch]

Figure 3: SLD-tree for G with P

[De Schreye and Decorte 94]) with semantics-based analysis (e.g. abstract interpretation, type inference).

We believe that the oracle approach is of general value in specifying the semantics of nondeterministic languages which are implemented in terms of a specific control strategy. In such cases, our technique can produce a semantics for the implementation in terms of the more natural semantics of the nondeterministic language. For example, the approach could be applied to depth-first implementations of such well-known models of computation as nondeterministic automata and nondeterministic Turing machines. Similarly, the technique applies to grammar formalisms, where the top-down and bottom-up semantics correspond to parsing and sentence generation respectively. Of greater practical interest are current implemented languages to which this technique applies. They include constraint logic programming languages [Jaffar and Lassez 87, Jaffar and Maher 94], set-based languages [Jayaraman 92], and equational languages [Jayaraman 89], among others. The technique also applies to a subset of the string processing languages SNOBOL [Griswold, Poage and Polonsky 71] and Icon [Griswold 93]. However it does not apply to the full languages, nor to full Prolog, because of the existence of constructs which allow the execution of one branch to affect another (nonbacktrackable assignment in SNOBOL and Icon, assert and retract in full Prolog).

There remain open questions whether and/or how the oracle approach can be applied to other aspects of control in logic programming languages such as negation-as-failure, once and cut in Prolog; dynamic scheduling as in MU-Prolog [Naish 86] and languages based on the Andorra principle [Haridi and Janson 90]); and extra-logical predicates such as var and nonvar in various logic languages.

Finally, we note that our approach may contribute to the derivation of parallel implementations (e.g. of Prolog). To see this consider that an implementation can be viewed as a strategy for constructing a corresponding computation tree and that information about an oracle’s decisions may be applied to identify subtrees which can be fruitfully constructed in parallel and subtrees which need not be constructed.

Acknowledgment

This work has been partly supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo” of C.N.R. under grant n. 9100880.PF69 and by the Esprit Basic Research Action 3012 - Compulog I. The stimulating discussion with E. Börger, G. Levi and D. Rosenzweig are gratefully acknowledged. This work was done while M. Codish and M. J. Maher were visiting the Università di Pisa. They thank the Dipartimento di Informatica for its hospitality.

A Appendix: proofs

Proposition 4.1. [∼-congruence] Let f be a downward closed oracle for a program. Then, for any interpretation I and goals G, G′: G ∼ G′ ⇒ f(I, G) = f(I, G′).

Proof. The proof is straightforward by downward closure of the oracle.

Proposition 4.2. Let P be a program and f be a downward closed oracle for P. If G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ with associated substitution ϑ, then Gϑ⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′′ and G′′ ∼ G′.

Proof. By downward closure of the oracle, the proof boils down into the standard one for logic programs (e.g. see [Apt 90]).

Lemma 4.4. Let P be a program and f be an oracle. If [C]_{∼} ∈ lfp(U_{P}^{f}) then lwr({[C]_{∼}}) ⊆ lfp(U_{P}^{f}).

Proof. It is a straightforward consequence of the definition and of the downward closure of the oracle.

Lemma 4.5. Let P be a program, f be an oracle and (c; π) ∈ U_{P}^{f} ↑ω. Then |π| = n iff (c; π) ∈ Unf_{P}^{f} ↑ n(lwr(Φ)).

Proof. The proof is a straightforward induction on n.

Theorem 4.6. Let P be a program and f, g be oracles for P. If for each goal G: λI.f(I, G) ⊆ λI.g(I, G) then lfp(U_{P}^{f}) ⊆ lfp(U_{P}^{g}).

Proof. Let G be a goal and I be an interpretation. Let also f(I, G) ⊆ g(I, G). We prove that Unf_{P}^{f} (I) ⊆ Unf_{P}^{g} (I). If (k ← B′′; π :: ⟨l⟩) ∈ Unf_{P}^{f} (I) then there exists C = (h ← b | B; π) ∈ I and (h′ ← B′; l) <<_{C} f(P, b | B) such that k = hσ, B′′ = (B′ :: B)σ and σ = mgu(b, h′). By the hypothesis: (h′ ← B′; l) <<_{C} g(P, b | B), from which follows the thesis. Thus, by definition: U_{P}^{f} (I) ⊆ U_{P}^{g} (I). The rest of this proof follows by a straightforward inductive argument.

Theorem 4.7. (soundness) Let P be a program, f an oracle for P, G a goal and ϑ the substitution associated with G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′. Then, Gϑ is an f-partial answer of G with path π in the interpretation lfp(U_{P}^{f}) and G′ ∼ G′′, where G′′ is the corresponding resolvent with path π in lfp(U_{P}^{f}).

Proof. The proof is by induction on the length m of the computation. Let G = a_{1}, ..., a_{n}.

\underline{Base case:} by definition:

G⟶_{l}^{f}_{P} (B :: ⟨a_{2}, ..., a_{n}⟩)ϑ

where (h ← B; l) ∈ f(P, G) and ϑ = mgu(h, a_{1}).

By downward closure (h ← B; l) ∈ f(P, a_{1}). (a_{1} ← a_{1}; Λ) ∈ lwr(Φ) and so, by U_{P}^{f} definition, ((h ← B)ϑ; l) ∈ U_{P}^{f} (∅) ⊆ lfp(U_{P}^{f}). By downward closure we have: (h ← B; l) ∈ f(P, G) ⇒ ((h ← B)ϑ; l) ∈ f(P ϑ, G). By additivity (notice that ((h ← B)ϑ; l) ∈ P ϑ ∩ lfp(U_{P}^{f})) we have:

((h ← B)ϑ; l) ∈ f(lfp(U_{P}^{f}), G).

\underline{Inductive case:} assume the inductive hypothesis for lengths ≤ m and let k ∈ \{1, ..., n\} such that

G⟶_{π}^{f}\begin{matrix}m_{1} \\ P \end{matrix} (⟨a_{k}, a_{k+1}, ..., a_{n}⟩)ψ⟶_{π}^{f}\begin{matrix}m_{2} \\ P \end{matrix} (b|B :: ⟨a_{k+1}, ..., a_{n}⟩)ψα⟶_{l}^{f}_{P} (W :: B :: ⟨a_{k+1}, ..., a_{n}⟩)ϑσ

where m ≥ 1, m = m_{1} + m_{2}, ϑ = ψα, (h ← W; l) ∈ f(P, (b | B :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ) and σ = mgu(h, bϑ). By the inductive hypothesis, for 1 ≤ i ≤ k − 1 there exist

(h_{i} ← true; π_{i}) <<_{Gϑ_{i−1}} f(lfp(U_{P}^{f}), (a_{i}, ..., a_{n})ϑ_{i−1})

where ϑ_{i} = ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}), π = π_{1} :: ⋯:: π_{k} and

(h_{k} ← b′ | B′; π_{k}) <<_{Gϑ_{k−1}} f(lfp(U_{P}^{f}), (a_{k}, ..., a_{n})ϑ_{k−1})

such that (b|B :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ ∼ (b′|B′ :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ_{k}, (a_{k}, ..., a_{n})ψ ∼ (a_{k}, ..., a_{n})ϑ_{k−1} and Gϑ ∼ Gϑ_{k}. Thus, by downward closure (∼-congruence):

(h ← W; l) ∈ f(P, (b′ | B′ :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ_{k}).

Moreover, by Lemma 4.4 and by part 3 of downward closure:

(h_{k} ← b′ | B′; π_{k})ϑ_{k} << f(lfp(U_{P}^{f}), (a_{k}, ..., a_{n})ϑ_{k−1}).

Let σ′ = mgu(h, b′ϑ_{k}). Thus, by U_{P}^{f} definition:

(h_{k} ← W :: B′; π_{k} :: ⟨l⟩)ϑ_{k}σ′ <<_{Gϑ_{k−1}} lfp(U_{P}^{f}).

We have now to prove that the clause (h_{k} ← W :: B′; π_{k} :: ⟨l⟩)ϑ_{k}σ is also applicable to the goal (a_{k}, ..., a_{n})ϑ_{k−1}. From the last m_{2} + 1 transitions in the given derivation and the soundness of the oracle we have

f ({(a_{k}ψ ← W :: B; π_{k} :: ⟨l⟩)ασ}, (a_{k}, ..., a_{n})ψ) ≠ ∅.

By manipulation of substitutions and ∼-congruence of f

f ({(h_{k} ← W :: B′; π_{k} :: ⟨l⟩)ϑ_{k}σ′}, (a_{k}, ..., a_{n})ϑ_{k−1}) ≠ ∅.

Thus, by additivity:

(h_{k} ← W :: B′; π_{k} :: ⟨l⟩)ϑ_{k}σ′ << f(lfp(U_{P}^{f}), (a_{k}, ..., a_{n})ϑ_{k−1}).

Through further manipulation of substitutions, using equivalences given by the inductive hypothesis, we can show that

Gϑ_{k−1}mgu(h_{k}ϑ_{k}σ′, a_{k}) ∼ Gϑ_{k}σ′ ∼ Gϑσ

and

(W :: B :: ⟨a_{k+1}, ..., a_{n}⟩)ϑσ ∼ (W :: B′ :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ_{k}σ′

This concludes the proof.

We now introduce a property of substitutions that will be used in the following.

Lemma A.1. ([Palamidessi 90]) Let ϑ_{1}, ϑ_{2} ∈ Sub. Then mgu(E(ϑ_{1}) ∪ E(ϑ_{2})) = ϑ_{1}mgu(E(ϑ_{2})ϑ_{1}) = ϑ_{2}mgu(E(ϑ_{1})ϑ_{2}).

Lemma 4.8. Let P be a program, f be a corresponding oracle and (c; π) ∈ Unf_{P}^{f}↑n(lwr(Φ)). Then (c; π) ∈ lwr({(c′; π)}) for some (c′; π) ∈ Unf_{P}^{slp}↑n(Φ).

Proof. The proof is by induction on the power of Unf_{P}^{f}.

\underline{Base case:} is straightforward by lwr definition.

\underline{Inductive case:} let (c; π) ∈ Unf_{P}^{f}↑n + 1(lwr(Φ)), then, by definition:

(c; π) = (h ← B′ :: B; π′ :: ⟨l⟩)ϑ
(h ← b | B; π′) ∈ Unf_{P}^{f}↑n(lwr(Φ))
(h′ ← B′; l) ∈ f(P, b | B) and ϑ = mgu(h′, b)

Thus, by the inductive hypothesis (h ← b|B; π′) = (h̃ ← b̃|B̃; π′)σ for some substitution σ such that dom(σ) ⊆ vars(h̃) and (h̃ ← b̃|B̃; π′) ∈ Unf_{P}^{slp}↑n(Φ). Because mgu(h′, b) ≠ fail there exists γ = mgu(h′, b̃) such that (h̃ ← B′ :: B̃; π′ :: ⟨l⟩)γ ∈ Unf_{P}^{slp}↑n + 1(Φ). Moreover, by Lemma A.1 and because E(mgu(E(σ))) ≈ E(σ):

(h ← B′ :: B; π′ :: ⟨l⟩)ϑ = (h ← B′ :: B; π′ :: ⟨l⟩)mgu(b̃σ, h′)
= (h̃ ← B′ :: B̃; π′ :: ⟨l⟩)σmgu(b̃σ, h′)
= (h̃ ← B′ :: B̃; π′ :: ⟨l⟩)mgu(E(σ) ∪ {b̃ = h′})
= (h̃ ← B′ :: B̃; π′ :: ⟨l⟩)mgu(b̃, h′)mgu(E(σ)mgu(b̃, h′))
= (h̃ ← B′ :: B̃; π′ :: ⟨l⟩)γmgu(E(σ)γ)

Notice that dom(mgu(E(σ)γ)) ⊆ vars(h̃γ).

Lemma 4.9. Let h be an atomic goal, π be a path and D = { h′ | (h′; π) ∈ P^{f}(lfp(U_{P}^{f}), h) }. If D ≠ ∅ then lub_{≤}D ∈ D; and lub_{≤}D = h mgu(h, h′) where (h′ ← B′; π) ∈ Unf_{P}^{f}↑|π | ({h ← h; Λ}).

Proof. Let |π| = n and D = { h′ | (h′; π) ∈ P^{f}(lfp(U_{P}^{f}), h) }.

By Lemma 4.5 D = D_{n} = { h′ | (h′; π) ∈ P^{f}(Unf_{P}^{f}↑n(lwr(Φ)), h) }. The proof is by induction on the length n of π.

\underline{Base case:} let us assume D_{1} ≠ ∅. Then there exists a program clause (h′ ← B′, l) ∈ f(P, h) such that π = ⟨l⟩ and

D_{1} = \{ h′′′ | \begin{matrix}h′′′ = h mgu(h, h′ mgu(h′, h′′)) \\ h′′ ∈ Atom \end{matrix} \}

Thus, by definition h mgu(h, h′ mgu(h′, h)) ∈ D_{1}. Moreover, for any substitution ϑ

h mgu(h, h′ mgu(h′, h)) = h mgu(h, h mgu(h′, h))
= h mgu(h′, h)
≥ h mgu(h′ϑ, h)

therefore h mgu(h′, h) ∈ D_{1}, and for each h′′′ ∈ D_{1}: h mgu(h′, h) ≥ h′′′.

\underline{Inductive case:} assume the inductive hypothesis for D_{n} and consider h′′′ ∈ D_{n+1} (D_{n+1} ≠ ∅). Then, by definition there exist:

• C = (h′ ← b′ | B′; π′) <<_{h} Unf_{P}^{f}↑n(lwr(Φ)) and

• (k ← B; l) <<_{h,C} f(P, b′ | B′) such that

π = π′ :: ⟨l⟩, f({(h′ ← B :: B′; π)mgu(b′, k)}, h) ≠ ∅ and h′′′ = h mgu(h, h′ mgu(b′, k)). By the oracle completeness: f({(h′ ← b′ | B′; π′)}, h) ≠ ∅, therefore D_{n} ≠ ∅. By combining the inductive hypothesis and Lemma 4.8, there exists:

(h̃ ← b̃ | B̃; π′)ϑ <<_{h} Unf_{P}^{f}↑n({h ← h; Λ})

where (h̃ ← b̃ | B̃; π′) ∈ Unf_{P}^{slp} ↑ (Φ) and dom(ϑ) ⊆ vars(h̃), such that f({(h̃ ← b̃ | B̃′; π′)ϑ}, h) ≠ ∅ and, for any substitution σ such that dom(σ) ⊆ vars(h̃) and (h̃ ← b̃ | B̃; π′)σ <<_{h} Unf_{P}^{f}↑n(lwr(Φ)): h mgu(h, h̃ϑ) ≥ h mgu(h, h̃σ). Therefore: h′ ← b′ | B′ ≤ (h̃ ← b̃ | B̃)ϑ. In particular, (because of Lemma 4.8) there exists σ′ such that h mgu(h, h̃ϑ) ≥ h mgu(h, h̃σ′) and (h̃ ← b̃ | B̃; π′)σ′ = (h′ ← b′ | B′; π′). Thus, because mgu(b̃σ′, k) ≠ fail then also mgu(b̃ϑ, k) ≠ fail. Therefore:

(h̃ ← B :: B̃; π)ϑmgu(b̃ϑ, k) <<_{h} Unf_{P}^{slp}↑n + 1({(h ← h; Λ)})

and, by the downward closure: f({(h̃ ← B :: B̃; π)ϑmgu(b̃ϑ, k)}, h) ≠ ∅. By the oracle completeness: (k ← B; l) <<_{h,C} f(P, (b̃ | B̃)ϑ) and by definition:

(h̃ ← B :: B̃; π)ϑmgu(b̃ϑ, k) <<_{h} Unf_{P}^{f}↑n + 1({(h ← h; Λ)})

which is also applicable to h.

Consider h̃′′′ = h mgu(h, h̃ϑmgu(b̃_{1}ϑ, k)). Then because h (k) and h̃ (b̃_{1}) are renamed apart from each other, and by Lemma A.1:

h mgu(h, h̃ϑmgu(b̃_{1}ϑ, k)) = h mgu(h, h̃mgu({b̃_{1} = k} ∪ E(ϑ)))
= h mgu({b̃_{1} = k} ∪ E(ϑ))mgu((h = h̃)mgu({b̃_{1} = k} ∪ E(ϑ)))
= h mgu({h = h̃, b̃_{1} = k} ∪ E(ϑ)).

By the inductive hypothesis it follows that: h̃′′′ ≥ h mgu(h, h̃σ′mgu(b̃_{1}σ′, k)) = h′′′, i.e. there exists a most general partial answer for h in U_{P}^{f}↑n + 1 with path π′ :: ⟨l⟩.

Theorem 4.11. (completeness) Let P be a program, f an oracle for P and G a goal. If Gϑ is the most general f-partial answer of G with path π in lfp(U_{P}^{f}) and G′′ is the corresponding resolvent then G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} G′ with associated substitution ϑ′ and Gϑ ∼ Gϑ′ and G′′ ∼ G′.

Proof. The proof is by induction on the power m of U_{P}^{f}. Assume the hypothesis and let G = a_{1}, ..., a_{n}.

\underline{Base case:} let k ∈ \{1, ..., n\} such that for 1 ≤ i ≤ k:

(h_{i} ← B_{i}; l_{i})σ_{i} ∈ f(Unf_{P}^{f} (lwr(Φ)), (a_{i}, ..., a_{n})ϑ_{i−1})
(h_{i} ← B_{i}; l_{i}) ∈ P and B_{i} = true for i < k
ϑ_{0} = ε, ϑ_{i} = ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}σ_{i})
(a_{i}, ..., a_{n})ϑ_{i} is the most general f-partial answer with path ⟨l_{1}...l_{i}⟩
for (a_{i}, ..., a_{n})ϑ_{i−1} in U_{P}^{f}↑1

By definition and by Lemma 4.9: σ_{i} = mgu(a_{i}ϑ_{i−1}, h_{i}). We prove by induction on i that for any i ≥ 1:

ϑ_{i} = mgu( ∪_{j=1}^{i} {a_{i} = h_{i}}).

\underline{i = 1}: because ϑ_{0} = ε then ϑ_{1} = σ_{1} = mgu(\{a_{1} = h_{1}\}) \underline{i > 1}: assume the hypothesis for i − 1. By the inductive hypothesis and by Lemma A.1:

ϑ_{i} = ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}σ_{i})
= ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}mgu(a_{i}ϑ_{i−1}, h_{i}))
= ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, a_{i}ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i}))
= ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i})
= mgu(E(ϑ_{i−1}) ∪ {a_{i} = h_{i}})
= mgu( ∪_{j=1}^{i} {a_{i} = h_{i}}).

Thus, ϑ_{i} = ϑ′_{i} for 1 ≤ i ≤ k, and by the downward closure: (h_{i} ← B_{i}; l_{i}) ∈ f(P, (a_{i}, ..., a_{n})ϑ′_{i−1}) where ϑ′_{i} = ϑ′_{i−1}mgu(a_{i}ϑ′_{i−1}, h_{i}), ϑ′_{0} = ε. Thus, for 1 ≤ i ≤ k:

(a_{i}, ..., a_{n})ϑ′_{i−1}⟶_{l_{i}}^{f}_{P} (B_{i} :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ′_{i}

and, since B_{i} = true for i < k, we have:

(a_{1}, ..., a_{n})⟶_{l_{i}}^{f}\begin{matrix}k \\ P \end{matrix} (B_{k} :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ′_{k}

and ϑ′_{k} = ϑ′_{k−1}mgu(a_{k}ϑ′_{k−1}, h_{k}). Of course, Gϑ′_{k} ∼ Gϑ_{k} and (B_{k} :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ′_{k} ∼ (B_{k} :: ⟨a_{k+1}, ..., a_{n}⟩)ϑ_{k}.

\underline{Inductive case:} let Gϑ be the most general partial answer in U_{P}^{f} ↑m + 1 with path π. Thus, by definition: U_{P}^{f} ↑m + 1 = U_{P}^{f} (U_{P}^{f} ↑m), and there exists k ∈ {1, ..., n} such that for each 1 ≤ i ≤ k:

(h_{i} ← B_{i}; π_{i}) ∈ f(U_{P}^{f} (U_{P}^{f}↑m), (a_{i}, ..., a_{n})ϑ_{i−1})
B_{i} = true for i < k
ϑ_{0} = ε, ϑ_{i} = ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h_{i})
π = π_{1} :: ⋯:: π_{k}
(a_{i}, ..., a_{n})ϑ_{i} is the most general f-partial answer with path π_{i}
for (a_{i}, ..., a_{n})ϑ_{i−1} in U_{P}^{f}↑m + 1.

By definition, for 1 ≤ i ≤ k, we can have two cases:

1. if |π_{i}| ≤ m then, by Lemma 4.5: (h_{i} ← B_{i}; π_{i}) ∈ f(U_{P}^{f}↑m, (a_{i}, ..., a_{n})ϑ_{i−1}) and by the inductive hypothesis:

(a_{i}, ..., a_{n})ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} (B_{i} :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i}

2. if |π_{i}| = m+1 then, by definition there exists (h̃ ← b̃|B̃; π̃) ∈ U_{P}^{f}↑m and (w ← Q; l) ∈ f(P, b̃ | B̃) such that (h_{i} ← B_{i}; π_{i}) ∼ (h̃ ← Q | B̃; π̃ :: ⟨l⟩)σ, where σ = mgu(b̃, w). Moreover: f(Unf_{{(w←Q;l)}}^{f}({(h̃ ← b̃ | B̃; π̃)}), (a_{i}, ..., a_{n})ϑ_{i−1}) ≠ ∅ and since h_{i} ≤ h̃, f is reductive and mgu(h_{i}, a_{i}) ≠ fail, then by the oracle completeness:

(a) f({(h̃ ← b̃ | B̃; π̃)}, (a_{i}, ..., a_{n})ϑ_{i−1}) ≠ ∅

(b) f({(w ← Q; l)}, (b̃ | B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i−1}σ) ≠ ∅. It is straightforward to extend Lemma 4.9 and prove that because (h_{i} ← B_{i}; π_{i}) provides the most general partial answer for (a_{i}, ..., a_{n})ϑ_{i−1} with path π_{i}, then (h̃ ← b̃ | B̃; π̃) provides the most general partial answer with path π̃ for (a_{i}, ..., a_{n})ϑ_{i−1}. Therefore, because of (a) and by the inductive hypothesis:

(a_{i}, ..., a_{n})ϑ_{i−1}⟶_{π̃}^{f}\begin{matrix}∗ \\ P \end{matrix} (b̃ | B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i−1}σ̃

where σ̃ = mgu(a_{i}ϑ_{i−1}, h̃). Because of (b)

(b̃ | B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i−1}σ̃⟶_{l}^{f}_{P} (Q :: B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i−1}σ̃mgu(b̃ϑ_{i−1}σ̃, w).

Since σ = mgu(b̃, w) and σ̃ = mgu(a_{i}ϑ_{i−1}, h̃), we prove that:

(Q :: B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃)mgu(b̃ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃), w) ∼

(Q :: B̃ :: ⟨a_{i+1}, ..., a_{n}⟩)mgu(b̃, w)ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃mgu(b̃, w)).

By Lemma A.1 and because dom(ϑ_{i−1}) ∩ vars(h̃) = ∅, dom(ϑ_{i−1}) ∩ vars(w) = ∅ and w is renamed apart from a_{i} and h̃:

ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃)mgu(b̃ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃), w) =
mgu(E(ϑ_{i−1}) ∪ {a_{i} = h̃})mgu(b̃mgu(E(ϑ_{i−1}) ∪ {a_{i} = h̃}), w) =
mgu(E(ϑ_{i−1}) ∪ {a_{i} = h̃} ∪ {b̃ = w})

and

mgu(b̃, w)ϑ_{i−1}mgu(a_{i}ϑ_{i−1}, h̃mgu(b̃, w)) =
mgu(b̃, w)mgu((E(ϑ_{i−1}) ∪ {a_{i} = h̃})mgu(b̃, w)) =
mgu(E(ϑ_{i−1}) ∪ {a_{i} = h̃} ∪ {b̃ = w}).

Therefore, for 1 ≤ i ≤ k: (a_{i}, ..., a_{n})ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} (B_{i} :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ_{i}. Because B_{i} = true

for i < k then: G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} (B_{k} :: ⟨a_{i+1}, ..., a_{n}⟩)ϑ′ where Gϑ_{k} ∼ Gϑ′ and the corresponding resolvents are ∼-equivalent. This concludes the proof.

Proposition 4.13. T_{P}^{f} is continuous.

Proof. It follows by the oracle additivity.

To prove equivalence of top-down and bottom-up oracle semantics for successful computations we need the following lemmata.

Lemma 4.14. (AND-compositionality) Let P be a program, G = b_{1}, ..., b_{n} be a goal and f be an oracle for P. ⟨b_{1}, ..., b_{n}⟩⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} true is a refutation for G with substitution ϑ iff

1. for each 1 ≤ i ≤ n: ϑ_{i} and π_{i} are the substitution and path associated with the refutation

(b_{i})ϑ_{1}...ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} true for the goal (b_{i})ϑ_{1}...ϑ_{i−1};

2. π = π_{1} :: ⋯:: π_{n};

3. f({(b_{i} ← true)ϑ_{1}...ϑ_{i}; π_{i})}, (b_{i}, ..., b_{n})ϑ_{1}...ϑ_{i−1}) ≠ ∅; and

4. (b_{1}, ..., b_{n})ϑ ∼ (b_{1}, ..., b_{n})ϑ_{1}...ϑ_{n}.

Proof. The proof is straightforward by the oracle downward closure and soundness.

Lemma 4.15. Let P be a program, f be an oracle for P, h ∈ Atom and a | G be a goal. If h⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} B with

substitution ϑ, f(\{(h ← B; π)ϑ\}, a | G) ≠ ∅ and mgu(hϑ, a) ≠ fail then a | G⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} (B ::

G)ϑmgu(hϑ, a).

Proof. The proof is by induction on the length n of the computation.

\underline{Base case:} is straightforward by definition.

\underline{Inductive case:} assume

h⟶_{π}^{f}\begin{matrix}n \\ P \end{matrix} (b | B)ϑ⟶_{l}^{f}_{P} (B′ :: B)ϑmgu(h′, bϑ)

where (h′ ← B′; l) ∈ f(P, (b | B)ϑ), f({(h ← B′ :: B; π :: ⟨l⟩)ϑmgu(h′, bϑ)}, a | G) ≠ ∅ and mgu(hϑmgu(h′, bϑ), a) ≠ fail.

By the soundness of the unfolding-based semantics, (h ← b | B; π)ϑ ∈ lfp(U_{P}^{f}) ⊆ lfp(U_{P}^{slp}) (i.e. (h ← b | B; π) is U-derivable), moreover, by definition:

(h ← B′ :: B; π :: ⟨l⟩)ϑmgu(h′, bϑ) = Unf_{{(h′←B′;l)}}^{slp}({(h ← b | B; π)ϑ})

and

f((h ← B′ :: B; π :: ⟨l⟩)ϑmgu(h′, bϑ), a | G)) ≠ ∅

Thus, by the oracle completeness:

1. f({(h ← b | B; π)ϑ}, a | G) ≠ ∅, from which we obtain by the inductive hypothesis:

a | G⟶_{π}^{f}\begin{matrix}n \\ P \end{matrix} (b | B :: G)ϑmgu(hϑ, a)

2. f({(h′ ← B′; l)}, (b | B :: G)ϑmgu(hϑ, a)) ≠ ∅

Therefore:

a | G⟶_{π::⟨l⟩}^{f}\begin{matrix}n + 1 \\ P \end{matrix}(B′ :: B :: G)ϑmgu(hϑ, a)mgu(h′, bϑmgu(hϑ, a))

Because all the clauses are considered to be renamed apart form each other, by Lemma A.1 we have:

\begin{aligned}ϑmgu(hϑ, a)mgu(h′, bϑmgu(hϑ, a)) & = & mgu(\{h′ = b\} ∪ E(mgu(\{h = a\} ∪ E(ϑ)))) \\ & = & mgu(\{h = a, h′ = b\} ∪ E(ϑ)) \end{aligned}

and

\begin{aligned}ϑmgu(h′, bϑ)mgu(a, hϑmgu(h′, bϑ)) & = & mgu(\{h = a\} ∪ E(mgu(\{h′ = b\} ∪ E(ϑ)))) \\ & = & mgu(\{h = a, h′ = b\} ∪ E(ϑ)) \end{aligned}

thus both leading to the same resolvent (B′ :: B :: G)mgu({h = a, h′ = b} ∪ E(ϑ)) (up to variable renaming).

Theorem 4.16. Let P be a program and f an oracle for P. Then,

lfp(T_{P}^{f}) = \{ (hϑ ← true; π) | \begin{matrix}h⟶_{π}^{f}\begin{matrix}∗ \\ P \end{matrix} true \\ with substitution ϑ \end{matrix} \} .

Proof. ⊇. The proof is by induction on the length m of the refutation:

\underline{Base case}: let a be an atom. Assume a has a refutation of length 1 with substitution ϑ, i.e. there exists (h ← true; l) ∈ f(P, a) and ϑ = mgu(a, h). By the downward closure and additivity,

(h ← true; l)ϑ ∈ f(P ϑ, a) ⇒ (h ← true; l)ϑ ∈ f(lwr(P), a).

The thesis follows by T_{P}^{f} definition; i.e. (hϑ ← true; l) ∈ T_{P}^{f} (∅).

\underline{Inductive case}: assume the hypothesis for any atomic goal h and k ≤ m, i.e.

h⟶_{π}^{f}\begin{matrix}k \\ P \end{matrix} true with substitution ϑ ⇒ [(h ← true; π)ϑ]_{∼} ∈ lfp(T_{P}^{f}).

Let

a⟶_{l}^{f}_{P} (b_{1}, ..., b_{n})ϑ_{0}⟶_{π′}^{f}\begin{matrix}m \\ P \end{matrix}true.

be a refutation of length m+1 for the atomic goal a with computed answer substitution ϑ_{0}ϑ and let π be the corresponding sequence of program clauses applied in the computation, i.e. π = ⟨l⟩ :: π′, where (h ← b_{1}, ..., b_{n}; l) is the first clause applied in the refutation and ϑ_{0} = mgu(a, h).

By definition: (h ← b_{1}, ..., b_{n}; l) ∈ f(P, a). Moreover, by Lemma 4.14, for each i = 1, ..., n:

b_{i}ϑ_{0}ϑ_{1}..ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}m_{i} \\ P \end{matrix} true

with computed substitution ϑ_{i}, where m_{i} ≤ n, π′ = π_{1} :: ⋯:: π_{n}, (b_{1}, ..., b_{n})ϑ_{0}ϑ ∼ (b_{1}, ..., b_{n})ϑ_{0}ϑ_{1}..ϑ_{n} and f({(b_{i} ← true; π_{i})ϑ_{0}..ϑ_{i}}, (b_{i}, ..., b_{n})ϑ_{0}..ϑ_{i−1}) ≠ ∅.

By the inductive hypothesis, for i = 1, ..., n:

[(b_{i} ← true; π_{i})ϑ_{0}..ϑ_{i}]_{∼} ∈ lfp(T_{P}^{f}).

Thus, by additivity, for i = 1, ..., n:

[(b_{i} ← true; π_{i})ϑ_{0}..ϑ_{i}]_{∼} ∈ f(lfp(T_{P}^{f}), (b_{i}, ..., b_{n})ϑ_{0}..ϑ_{i−1}).

Since (h ← b_{1}, ..., b_{n}; l) is the first clause applied to the refutation of a and aϑ_{0} = hϑ_{0}, by downward closure we have: (h ← b_{1}, ..., b_{n}; l)ϑ_{0} ∈ f(lwr(P), aϑ_{0}) which implies that (h ← b_{1}, ..., b_{n}; l)ϑ_{0} ∈ f(lwr(P), hϑ_{0}). The thesis follows by T_{P}^{f} definition; i.e. [(h ← true)ϑ_{0}ϑ′′; π]_{∼} ∈ lfp(T_{P}^{f}) where, for i = 1, ..., n by denoting ρ_{i} suitable renaming substitutions:

ϑ′′ = mgu(⟨b_{1}, ..., b_{n}⟩ϑ_{0}, ⟨b_{1}ϑ_{0}ϑ_{1}ρ_{1}, ...b_{n}ϑ_{0}..ϑ_{n}ρ_{n}⟩)

we have ⟨b_{1}, ..., b_{n}⟩ϑ_{0}ϑ′′ ∼ ⟨b_{1}, ..., b_{n}⟩ϑ_{0}..ϑ_{n}, which completes the proof.

⊆. The proof is by induction on the power n of T_{P}^{f}.

\underline{Base case}: is straightforward by definition.

\underline{Inductive case}: let (h ← b_{1}, ..., b_{m}; l) ∈ f(lwr(P), h) and for 1 ≤ i ≤ m: (h_{i} ← true; π_{i}) ∈ f(T_{P}^{f}↑n, (b_{i}, ..., b_{m})ϑ_{i−1}) where ϑ_{0} = ε and ϑ_{i} = ϑ_{i−1}mgu(b_{i}ϑ_{i−1}, h_{i});

(i.e. (h ← true; ⟨l⟩ :: π_{1} :: ⋯:: π_{m})ϑ_{m} ∈ T_{P}^{f}↑n + 1).

By the inductive hypothesis, h̃_{i}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} true with substitution ϑ̃_{i} such that h_{i} = h̃_{i}ϑ̃_{i}.

Since f({(h̃_{i} ← true; π_{i})ϑ̃_{i}}, (b_{i}, ..., b_{m})ϑ_{i−1}) ≠ ∅ and mgu(b_{i}ϑ_{i−1}, h̃_{i}ϑ̃_{i}) ≠ fail, by Lemma 4.15 we have for 1 ≤ i ≤ m:

(b_{i}, ..., b_{m})ϑ_{i−1}⟶_{π_{i}}^{f}\begin{matrix}∗ \\ P \end{matrix} (b_{i+1}, ..., b_{m})ϑ_{i−1}ϑ̃_{i}mgu(b_{i}ϑ_{i−1}, h̃_{i}ϑ̃_{i}).

Note that: (b_{i+1}, ..., b_{m})ϑ_{i−1}ϑ̃_{i}mgu(b_{i}ϑ_{i−1}, h̃_{i}ϑ̃_{i}) ∼ (b_{i+1}, ..., b_{m})ϑ_{i−1}mgu(b_{i}ϑ_{i−1}, h_{i}).

Moreover, because (h ← b_{1}, ..., b_{m}; l) ∈ f(lwr(P), h), there exists (h̃ ← b̃_{1}, ..., b̃_{m}; l) ∈ f(P, h) where σ_{0} = mgu(h, h̃) and (h ← b_{1}, ..., b_{m}; l) ∼ (h̃ ← b̃_{1}, ..., b̃_{m}; l)σ_{0}. Therefore:

h⟶_{l}^{f}_{P} (b̃_{1}, ..., b̃_{m})σ_{0}

Thus, by definition:

h ⟶_{⟨l⟩::π_{1}::···::π_{m}}^{f} \begin{matrix}∗ \\ P \end{matrix} true

with substitution ϑ_{m}, which concludes the proof.

Proposition 5.1. prolog is a downward closed oracle.

Proof. The proof is by contradiction. Let I be an interpretation, P be a program, G = a_{1}, ..., a_{n} and B be goals and [(c; π)]_{∼} ∈ prolog(I, G :: B). By definition mgp_{π}^{slp}(P, G :: B) is finite. Assume mgp_{π}^{slp}(P, Gϑ) be an infinite set, for a substitution ϑ. Let G′ be the most general slp-partial answer for Gϑ in lfp(U_{P}^{slp}) with path π′ ⪯ π. Thus, by definition there exists a most general slp-partial answer G′′ for G in lfp(U_{P}^{slp}) with path π′. (G :: B)mgu(G, G′′) is also a most general partial answer for G :: B in lfp(U_{P}^{slp}) with the same path π′. Thus |mgp_{π}^{slp}(P, Gϑ)| ≤ |mgp_{π}^{slp}(P, G :: B)| which is a contradiction. Moreover, because the set mgp_{π}^{slp} does not depend on the clause c, the applicability of any clause does not depend on the clause instantiation.

To prove soundness and completeness of the prolog oracle we need the following

Lemma A.2. Let P be a program, G be a goal and π, π′ be paths. Then

mgp_{π::π′}^{slp}(P, G) = mgp_{π}^{slp}(P, G) ∪ \{ (G′, π′) | \begin{matrix}(G′, π′) ∈ mgp^{slp}(P, G) \\ π ⪯ π′ ≺ π :: π′ \end{matrix} \}

Proof. The proof is straightforward by lexicographic ordering and by definition.

Proposition 5.2. prolog is sound and complete.

Proof. Let a | G be a goal and P be a program ordered textually by ℓ. \underline{Soundness} The proof is by induction on the length n of the computation.

\underline{Base case:} is straightforward by definition;

\underline{Inductive case:} assume the inductive hypothesis for n ≥ 1 and let us consider:

a | G⟶_{π}^{prolog}\begin{matrix}n \\ P \end{matrix} (b | B :: G)ϑ⟶_{l}^{prolog}_{P} (Q :: B :: G)ϑσ

where (k ← Q; l) ∈ prolog(P, (b | B :: G)ϑ) and σ = mgu(k, bϑ). By the inductive hypothesis and by definition: |mgp_{π}^{slp}(P, a | G)| < ω and |mgp_{l}^{slp}(P, (b | B :: G)ϑ)| < ω.

Assume (as a contradiction) that mgp_{π::⟨l⟩}^{slp}(P, a | G) is infinite. By Lemma A.2 we have:

mgp_{π::⟨l⟩}^{slp}(P, a | G) = mgp_{π}^{slp}(P, a | G) ∪ \{ (G′, π′) | \begin{matrix}(G′, π′) ∈ mgp^{slp}(P, a | G) \\ π ⪯ π′ ≺ π :: ⟨l⟩ \end{matrix} \} .

Thus the assumption is true iff the set:

D = \{ (G′, π′) | \begin{matrix}(G′, π′) ∈ mgp^{slp}(P, a | G) \\ π ⪯ π′ ≺ π :: ⟨l⟩ \end{matrix} \}

is infinite. This is a contradiction because |mgp_{l}^{slp}(P, (b | B :: G)ϑ)| < ω and since slp is an oracle, by the soundness and completeness of the slp-semantics:

D = \{ (G′, π′) | \begin{matrix}(G′, π) ∈ mgp^{slp}(P, a | G) \\ (G′′, π′′) ∈ mgp^{slp}(P, (b | B :: G)ϑ) \\ π′ = π :: π′′ and π′′ ≺ ⟨l⟩ \end{matrix} \}

is finite.

Completeness Let n < ω and C <<_{a|G} P, (h ← b | B; π) <<_{C,a|G} U_{P}^{prolog}↑n.

Assume prolog(Unf_{{C}}^{prolog}({(h ← b | B; π)}), a | G) ≠ ∅ and mgu(h, a) ≠ fail.

1. By definition |mgp_{π::⟨ℓ(C)⟩}^{slp}(P, a | G)| < ω, and, since by Lemma A.2

mgp_{π}^{slp}(P, a | G) ⊆ mgp_{π::⟨ℓ(C)⟩}^{slp}(P, a | G)

then |mgp_{π}^{slp}(P, a | G)| < ω, i.e. prolog({(h ← b | B; π)}, a | G) ≠ ∅.

2. By Lemma A.2

|\{ (G′, π′) | \begin{matrix}(G′, π′) ∈ mgp^{slp}(P, a | G) \\ π ⪯ π′ ≺ π :: ⟨ℓ(C)⟩ \end{matrix} \}| < ω

Let us assume the set mgp_{⟨ℓ(C)⟩}^{slp}(P, (b|B :: G)mgu(h, a)) is infinite. Because prolog is reductive, there exists (h̃ ← b̃ | B̃; π) ∈ lfp(U_{P}^{slp}) such that (a | G)mgu(h̃, a) ≥ (a | G)mgu(h, a) and (b̃ | B̃ :: G)mgu(h̃, a) ≥ (b | B :: G)mgu(h, a). Thus, if (b | B :: G)mgu(h, a)ϑ ∈ mgp_{⟨ℓ(C)⟩}^{slp}(P, (b | B :: G)mgu(h, a)) with ϑ = mgu(b mgu(h, a), h′) and C = (h′ ← B′; ℓ(C)) ∈ P, then (a|G)mgu(h̃, a)mgu(b̃ mgu(h̃, a), h′) is the most general partial answer for a | G with path π :: ⟨ℓ(C)⟩ in lfp(U_{P}^{slp}). Therefore

|mgp_{⟨ℓ(C)⟩}^{slp}(P, (b | B :: G)mgu(h, a))| ≤ |\{ (G′, π′) | \begin{matrix}(G′, π′) ∈ mgp^{slp}(P, a | G) \\ π ⪯ π′ ≺ π :: ⟨ℓ(C)⟩ \end{matrix} \}|

which is a contradiction. Thus f({C}, (b | B :: G)mgu(h, a)) ≠ ∅.

Theorem 5.3. Let P be a program textually ordered by ℓ, C ∈ P, Q = { C′ | ℓ(C′) < ℓ(C) }, and G be a

goal. Then, G⟶^{slp}_{Q}G′ ⇒ T (Ψ_{P}^{slp}, G′) is finite iff mgp_{⟨ℓ(C)⟩}^{slp}(P, G) is finite.

Proof. Assume the hypothesis: G⟶^{slp}_{Q}G′ ⇒ T (Ψ_{P}^{slp}, G′) is finite. By Theorems 4.7 and 4.11 and Definition 3.4 this is equivalent to

G⟶^{slp}_{Q}G′ ⇒ mgp^{slp}(P, G′) is finite.

The set of most general slp-partial answers for G starting with any of the clauses in Q is then finite; namely the set

\{ (G′′; ⟨ℓ(C′)⟩ :: π) | \begin{matrix}ℓ(C′) < ℓ(C) \\ (G′′; ⟨ℓ(C′)⟩ :: π) ∈ mgp^{slp}(P, G) \end{matrix} \}

is finite. By definition, the assumption is true iff mgp_{⟨ℓ(C)⟩}^{slp}(P, G) is finite.

References

[Apt 90] K. R. Apt. Introduction to logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 495–574. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

[Apt, Bol and Klop 89] K. R. Apt, R. N. Bol, and J. W. Klop. On the safe termination of Prolog programs. In G. Levi and M. Martelli, editors, Proceedings of the Sixth International Conference on Logic Programming, pages 353–368, Lisbon, 1989. The MIT Press.

[Apt and van Emden 82] K. R. Apt and M. H. van Emden. Contributions to the theory of logic programming. Journal of the ACM, 29(3):841–862, July 1982.

[Apt and Pedreschi 93] K. R. Apt and D. Pedreschi. Reasoning about termination of pure Prolog programs. Information and Computation, 106(1):109–157, September 1993.

[Arbab and Berry 87] B. Arbab and D. M. Berry. Operational and denotational semantics of Prolog. The Journal of Logic Programming, 4(4):309–330, December 1987.

[Barbuti, Codish, Giacobazzi and Levi 92] R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modeling Prolog control. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 95–104, January 1992.

[Barbuti, Codish, Giacobazzi and Levi 93] R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modeling Prolog control. Journal of Logic and Computation, 3(6):579–603, 1993.

[Barbuti, Codish, Giacobazzi and Maher 92] R. Barbuti, M. Codish, R. Giacobazzi, and M. J. Maher. Oracle semantics for Prolog. In [Levi and Kirchner 92], pages 100–114.

[Barbuti and Giacobazzi 92] R. Barbuti and R. Giacobazzi. A bottom-up polymorphic type inference in logic programming. Science of Computer Programming, 19(3):281–313, 1992.

[Barbuti, Giacobazzi and Levi 93] R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems, 15(1):133–181, 1993.

[Börger 90] E. Börger. A logical operational semantics of full Prolog. In E.Börger, H. Kleine, H. Büning, and M. Richter, editors, CSL 89. 3rd workshop on Computer Science Logic, volume 440 of Lecture Notes in Computer Science, pages 36–64. Springer-Verlag, Berlin, 1990.

[Bossi, Gabbrielli, Levi and Meo 94] A. Bossi, M. Gabbrielli, G. Levi, and M. Meo. A compositional semantics for logic programs. Theoretical Computer Science, 122(1–2):3–47, 1994.

[de Bruin and de Vink 89] A. de Bruin and E. de Vink. Continuation semantics for Prolog with cut. In J. Diaz and F. Orejas, editors, Proc. CAAP 89, volume 351 of Lecture Notes in Computer Science, pages 178–192. Springer-Verlag, Berlin, 1989.

[Bruynooghe 91] M. Bruynooghe. A practical framework for the abstract interpretation of logic programs. The Journal of Logic Programming, 10(1,2,3 and 4):91–124, 1991.

[Le Charlier and Van Hentenryck 94] B. Le Charlier and P. Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. ACM Transactions on Programming Languages and Systems, 16(1):35–101, January 1994.

[Codish, Dams and Yardeni 94] M. Codish, D. Dams, and E. Yardeni. Bottom-up abstract interpretation of logic programs. Theoretical Computer Science, 124(1):93–126, 1994.

[Debray and Lin 91] S. K. Debray and N.-W. Lin. Automatic complexity analysis of logic programs. In [Furukawa 91], pages 599–613.

[Debray and Mishra 87] S. K. Debray and P. Mishra. Denotational and operational semantics for Prolog. In M. Wirsing, editor, Formal Description of Programming Concepts III, pages 245–269. North-Holland, Amsterdam, 1987.

[Debray and Warren 89] S. K. Debray and D. S. Warren. Functional computations in logic programs. ACM Transactions on Programming Languages and Systems, 11(3):451–481, July 1989.

[De Schreye and Decorte 94] D. De Schreye and S. Decorte. Termination of Logic Programs: the Never-Ending Story, Journal of Logic Programming, 19 & 20:199–260, 1994.

[Eder 85] E. Eder. Properties of substitutions and unifications. Journal of Symbolic Computation, 1:31–46, 1985.

[van Emden and Kowalski 76] M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

[Falaschi, Levi, Martelli and Palamidessi 89] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative modeling of the operational behavior of logic languages. Theoretical Computer Science, 69(3):289–318, 1989.

[Falaschi, Levi, Martelli and Palamidessi 93] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A model-theoretic reconstruction of the operational semantics of logic programs. Information and Computation, 102(1):86–113, 1993.

[Furukawa 91] K. Furukawa, editor. Proceedings of the Eighth International Conference on Logic Programming, Paris, France, 1991. The MIT Press.

[Gabbrielli and Meo 92] M. Gabbrielli and M. C. Meo. Fixpoint semantics for partial computed answer substitutions and call patterns. In Levi and Kirchner [Levi and Kirchner 92], pages 84–99.

[Gaifman, Maher and Shapiro 91] H. Gaifman, M. J. Maher and E. Shapiro. Replay, Recovery, Replication and Snapshots of Nondeterministic Concurrent Programs, Proceedings of the ACM Symposium on Principles of Distributed Computation, 1991.

[Griswold 93] R. E. Griswold. The evaluation of expressions in Icon, ACM Transactions on Programming Languages and Systems, 4(4):563–584, 1993.

[Griswold, Poage and Polonsky 71] R. E. Griswold, J. F. Poage and I. P. Polonsky. The SNOBOL4 Programming Language, Prentice-Hall, 1971.

[Haridi and Janson 90] S. Haridi and S. Janson. Kernel Andorra Prolog and its computation model. In David H. D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 31–46, Jerusalem, 1990. The MIT Press.

[Jaffar and Lassez 87] J. Jaffar and J-L. Lassez. Constraint Logic Programming, Proc. 14th ACM Symposium on Principles of Programming Languages, Munich (January 1987), 111– 119.

[Jaffar and Maher 94] J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey, Journal of Logic Programming, 19 & 20:503–581, 1994.

[Jayaraman 89] B. Jayaraman. Eql: The Language and Its Implementation, IEEE Transactions on Software Engineering 15(6):771–779, 1989.

[Jayaraman 92] B. Jayaraman. Implementation of Subset-Equational Programs, Journal of Logic Programming 12(4):299–324, 1992.

[Jones and Mycroft 84] N. D. Jones and A. Mycroft. Stepwise development of operational and denotational semantics for Prolog. In Proceedings of the International Symposium on Logic Programming, pages 281–288, Atlantic City, 1984. IEEE, Computer Society Press.

[Kanomori and Horiuchi 88] T. Kanomori and K. Horiuchi. Polymorphic type inference in prolog by abstract interpretation. In Logic Programming 87- Tokyo, volume 315 of Lecture Notes in Computer Science, pages 195–214. Springer-Verlag, Berlin, 1988.

[Lassez, Maher, and Marriott 88] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[Lever 91] J. M. Lever. Proving program properties by means of SLS-resolution. In Furukawa [Furukawa 91], pages 614–628.

[Levi 88] G. Levi. Models, unfolding rules and fixpoint semantics. In Robert A. Kowalski and Kenneth A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 1649–1665, Seattle, 1988. The MIT Press.

[Levi and Kirchner 92] G. Levi and H. Kirchner, editors. Algebraic and Logic Programming, Third International Conference, LNCS 632, Volterra, Italy, September 2–4, 1992. Springer-Verlag.

[Lloyd 87] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 2^{nd} edition, 1987.

[Maher and Ramakrishnan 89] M. J. Maher and R. Ramakrishnan. Déjà Vu in Fixpoints of Logic Programs, Proc. North American Conference on Logic Programming, Cleveland, October, 1989, pages 963–980.

[Naish 86] L. Naish. Negation and Control in Prolog, volume 238 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1986.

[Palamidessi 90] C. Palamidessi. Algebraic properties of idempotent substitutions. In M. S. Paterson, editor, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 386–399. Springer-Verlag, Berlin, 1990.

[Przymusinski 89] T. Przymusinski. On the declarative and procedural semantics of logic programs. Journal of Automated Reasoning, 5(2):201–228, 1989.

[Pyo and Reddy 89] C. Pyo and U. S. Reddy. Inference of Polymorphic Types for Logic Programs. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 1115–1134, Cleveland, Ohio, USA, 1989.

[Saraswat 90] V. A. Saraswat. Concurrent constraint programming. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 232–245, January 1990.

[Saraswat, Weinbaum, Kahn and Shapiro 88] V. A. Saraswat, D. Weinbaum, K. Kahn and E. Shapiro. Detecting stable properties of networks in concurrent logic programming languages. Proceedings of the ACM Symposium PODC , 1988.

[Smith, Genesereth and Ginsberg 86] D. E. Smith, M. R. Genesereth, and M. L. Ginsberg. Controlling recursive inference. Artificial Intellingence, 30:343–389, 1986.

[Sterling and Shapiro 86] L. Sterling and E. Shapiro. The Art of Prolog. The MIT Press, Cambridge, Massachusetts, 1986.

[Vasak and Potter 86] T. Vasak and J. Potter. Characterisation of terminating logic programs. In Symposium on Logic Programming, pages 140–147. IEEE Computer Society, The Computer Society Press, September 1986.

[Verschaetse and De Schreye 91] K. Verschaetse and D. De Schreye. Deriving termination proofs for logic programs, using abstract procedures. In [Furukawa 91], pages 301–315.