Modelling Prolog Control ^{∗}

Roberto Barbuti, Michael Codish, Roberto Giacobazzi, Giorgio Levi

Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

(barbuti,codish,giaco,levi)@di.unipi.it

Abstract

The goal of this paper is to construct a semantic basis for the abstract interpretation of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of Horn clause logic. While pure logic programming has clean fixpoint, model-theoretic and operational semantics the situation for Prolog is different. Difficulties in capturing the declarative meaning of Prolog programs have led to various semantic definitions which attempt to encode the search strategy in different mathematical frameworks. However semantic based analyses of Prolog are typically achieved by abstracting the more simple but less precise declarative semantics of pure logic Programs.

We propose instead to model Prolog control in a simple constraint logic language which is presented together with its declarative and operational semantics. This enables us to maintain the usual approach to declarative semantics of logic programs while capturing control aspects such as search strategy and selection rule.

1 Introduction

Standard semantics typically associate programs with entities which capture the essence of “what they do” while abstracting away from details related to the text of the program as well as the control of the execution model. For semantics-based program analysis an enhanced or “collecting” semantics which recaptures some of these details is usually required. After all, the purpose of program analysis is to analyse the text of the program with respect to the control of its execution model. In general, the fact that collecting semantics can be viewed as uncovering details which the standard semantics has hidden imposes a restriction on the choice of semantic models upon which program analyses can be based.

∗This work has been 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.

In the case of logic programs, standard semantics traditionally associate programs with the set of ground atoms which they imply. Program analyses, in contrast, are often required to capture: (1) answer substitutions for a query; and (2) call patterns – that is how particular clauses in the program are used in refutations of a query. It is no coincidence that in most cases practical abstract interpretations of logic programs approximate top-down semantics based on SLD resolution (e.g. [10]). The information concerning control and textual details of a program are more naturally recovered (and collected) from such semantics.

An alternative approach is taken in [11] and further pursued in this paper. Instead of enhancing the semantic basis for analysis to capture control — the program itself is enhanced so that its standard meaning reflects the required control. The key idea is to enhance a program P by a transformation M so that the standard meaning of M (P) reflects the control information required for the analysis of P. So for example, the declarative meaning of a logic program P enhanced by a “magic set” transformation [4] is shown to reflect the call patterns of P enabling bottom-up analysis (e.g. [7, 11, 24]). The approach of modelling control has two main advantages: (1) the standard semantics is not required to be extended to a collecting semantics; and (2) any of the alternative semantic definitions for a language are potential choices as a basis for analysis.

In this paper we apply the idea of modelling control to define a declarative semantics for Prolog with the intention of providing a semantic basis for program analysis. The semantics of Prolog is usually specified by encoding its (sequential) control within different frameworks such as dynamic algebras [8], deterministic transition systems [14] or denotational semantics [3, 15, 20]. However, (semantics-based) analyses of Prolog are usually achieved by abstracting the more simple but less precise semantics of pure logic programs. This can lead to problems as illustrated by the following example.

Example 1.1 Consider the parallel execution of the following Prolog program P where the predicate eq models an equality theory and the predicates q and r are defined elsewhere. A similar program is used by Lloyd (page 59 in [22]) to illustrate the incompleteness of Prolog’s search strategy.

p(x, y) ← eq(x, y), q(x), r(y).

eq(a, b).

eq(c, b).

eq(x, y) ← eq(y, x). eq(x, y) ← eq(x, z), eq(z, y).

eq(x, x).

A compiler may designate the calls q(x) and r(y) in the body of the first clause for parallel execution if it is able to detect (at compile-time) that any possible run-time environemnt does not bind x and y to terms which share a variable. Semantics-based program analysis is often able to provide such an information (see for example [25]).

An analysis of P which is based on a semantics that considers Prolog’s left to right computation rule but ignores the depth first search strategy will not enable parallel execution of q(x) and r(y) due to the clause eq(x, x) which introduces sharing to the runtime environment for x and y. However, Prolog execution of P would never consider the clause eq(x, x) due to the infinite branch introduced by the depth first search strategy. Furthermore, an analysis of P which is based on a Prolog semantics could detect that:

1. q(x) and r(y) can be executed in parallel; and

2. the clause eq(x, x) is not reachable, indicating a potential error in the program.

We propose to model Prolog semantics in a constraint logic language τ which is expressive enough to capture Prolog control yet restricted enough to have a simple declarative semantics. 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 P^{τ}. The target language τ is strongly related to the cc class of concurrent constraint languages [27]. Constraints are used to specify that a clause may be chosen for reduction only if the computation with the preceding (Prolog) clauses terminates. We present a semantics for τ which is open with respect to the interpretation of these (termination) constraints. The meaning of a Prolog program is constructed by composing the meaning of the appropriate τ program (the “logic component”) with a corresponding termination theory (the “control component”). This approach supports the analysis of Prolog programs based on the abstract interpretation [13] of τ programs consisting of two corresponding components: (1) a standard analysis for the logic component of the program; and (2) a termination analysis for the control component.

An approximate model for the control component (termination) can be provided either by applying techniques of abstract interpretation, as described in [6], or by applying proof procedures as proposed by [26]. It is interesting to note that a precise model for the control component provides a result which reflects the standard Prolog semantics; while the worst approximation (which specifies that all termination conditions are possibly true) reflects the meaning of P as a pure logic program.

The rest of the paper is organized as follows: Section 2 reviews the model of constraint logic programs and presents some preliminary definitions and notations. Section 3 demonstrates the basic intuition of our approach via an example. Section 4 introduces the τ language together with its operational and declarative semantics. Section 5 describes how to model depth-first control of Prolog using the τ language. Section 6 discusses the interpretation of the termination conditions. Section 7 describes related work and concludes. The Appendix contains the proofs of the equivalence results presented in Section 4. This paper is an extended version of [5].

2 Preliminaries

In the following we assume familiarity with logic programming theory [1, 22].

Let Σ and Var be denumerable sets of function symbols, and variables respectively; T (Σ) and T (Σ, Var) denote the corresponding ground and non-ground term algebras respectively. Likewise, if Π denotes a denumerable set of predicate symbols, A(Σ, Π, Var) denotes the set of atoms of the form p(t_{1}, …, t_{n}) where p ∈ Π and t_{i} ∈ T (Σ, Var) (1 ≤ i ≤ n). When clear from the context we will refer to elements of A(Σ, Π, Var) as Π-atoms or simply as atoms. Note that A(Σ, Π, ∅) is the set of ground Π-atoms. The set of finite sequences of atoms is denoted Atom^{∗}. The sequence of atoms with first element A followed by the sequence B is denoted A | B; the concatenation of two sequences B and B′ is denoted B :: B′. The empty sequence is denoted by Λ. The set of variables that occur in a syntactic object t is denoted vars(t). Tuples of variables and terms are sometimes denoted x̄, ȳ,… and t̄, s̄,… respectively.

Let I ⊆ A(Σ, Π, Var) and V ⊆ Var; A <<_{V} I denotes that A is a renaming of an element of I which contains no variables in V . Moreover, we extend this notation for any syntactic object. An equation is an expression of the form t = s where t, s ∈ T (Σ, Var). A set of equations E is unifiable iff there exists a mapping ϑ from Var into T (Σ, Var) (called a solution) such that ∀(t = s) ∈ E, (tϑ) ≡ (sϑ) where ≡ denotes syntactic equivalence and tϑ is the term obtained by replacing each variable x in t with ϑ(x). Solutions apply in the same way to any syntactic object. The empty set of equations is denoted ϵ. The application of a set of equations σ to a syntactic object A is defined by Aσ = {Aϑ | ϑ is a solution of σ}. Notice that the set Aσ is closed under instantiation and hence under renaming. The standard ordering on atoms (i.e. less general or more instantiated) is captured by defining A ⪯ B iff there is a unifiable set of equations σ such that Aϵ = Bσ.

Constraint logic programming (CLP) is a generalization of the pure logic programming paradigm, having similar model-theoretic, fixpoint and operational semantics [19]. One relevant feature is the distinction between testing for satisfiability and computing a solution of a given constraint formula. In CLP, the set of predicate symbols Π is partitioned into Π_{C} and Π_{P}. The meaning of the predicates symbols in Π_{P} is given by a program in the usual way. Predicate symbols in Π_{C} are used to build constraints and their meaning is given by a separate constraint theory X. Π_{C} contains at least the equality symbol “=”. In the following we will denote as CLP(X) a constraint logic programming paradigm based on the constraint theory X. A constraint logic program is a finite set of clauses of the form H ← c □ B̄ where H is an atom, c is a constraint formula and B̄ is a sequence of atoms in A(Σ, Π_{P}, Var). A constraint formula is a conjunction of atomic formulas in A(Σ, Π_{C}, Var). A goal G has the form c □ B̄. A derivation of a program P for an initial goal G_{0} is a (finite or infinite) sequence of goals. Consecutive goals G_{i} = c_{i} □ B̄_{i} and G_{i+1} = c_{i+1} □ B̄_{i+1} in the sequence are related as follows: (1) c_{i+1} = c_{i} ∧ {B = H } ∧ c where H ← c □ B̄ <<_{vars(Gi )} P, B is an element of B̄_{i} and c_{i} ∧ {B = H } ∧ c is satisfiable; and (2) B̄_{i+1} is obtained from B̄_{i} by replacing the selected occurrence of B with B̄. The replacement of B by B̄ and the formation of c_{i+1} is called a derivation step. A computation rule determines (uniquely) for every goal in a derivation, which atom in that goal is selected. The computation of a solution of a constraint is left to a constraint solver, which does not affect the semantics definition of the language. A derivation for a goal G_{0} is successful if it is finite and ends with a goal c_{n} □ Λ. In this case, c_{n} is called an answer constraint for G_{0}. In the CLP paradigm, at each derivation step for a goal, the constraint part c is checked for satisfiability with respect to a constraint theory X [19], namely X ⊧ (∃)c, where (∃)c denotes the existential closure of c.

The Herbrand constraint theory, H, is obtained by choosing Π_{C} = {=} interpreted as Clark’s equality theory. Herbrand constraints are (systems of) equations between terms in the non-ground term algebra. It is well known that logic programs can be characterised as corresponding CLP(H) programs (e.g., [12]). In this case the satisfiability of a Herbrand constraint is determined by computing a solution (a set of equations in solved form or most general unifier).

An extension of constraint logic programming is provided by the ask-tell paradigm [23, 27]. In addition to satisfiability, validation (or entailment) is introduced. A possibly existentially quantified constraint a is entailed by a constraint c iff X ⊧ (∀)(c ⇒ a) (denoted X ⊧ (c ⇒ a)) where (∀)c denotes the universal closure of c.

An ask-tell clause has the form

H ← ⟨a : c⟩ □ B̄

where a and c are constraints (called ask and tell constraints respectively). In each derivation step ask constraints are checked for entailment, while tell constraints are checked for satisfiability.

Goals have the form c_{i} □ B̄_{i} (as before). A derivation in the ask-tell paradigm is a sequence of goals G_{i} for i = 0, 1... such that G_{i+1} is obtained from G_{i} by means of a renamed program clause H ← ⟨a : c⟩ □ B̄ provided that c ∧ {H = B} ∧ c_{i} is satisfiable and a is entailed by c_{i} ∧ {H = B} where B is the selected atom in B̄_{i}. Notice that if X ⊧ (c ⇒ a) then X ⊧ (c ∧ c′ ⇒ a) holds for any constraint c′. Tell constraints are then monotonically refined during the derivation, at each step of the computation, the set of possible solutions of the constraint is contained in the set of possible solutions at any prior step. Thus, an ask constraint, entailed at a given step in a computation, will be entailed at all the subsequent steps. For this reason, ask constraints are not collected in the derivation.

This different view of constraint programming, based on ask and tell constraints, leads to a powerful paradigm for concurrent computations (cc languages) in a shared store [27]. A store is a constraint representing the global state of the computation. The evaluation of an ask constraint in a given store can have three possible results:

(1) the ask constraint is entailed by the store; (2) the negation of the ask constraint is entailed by the store; or (3) neither the ask constraint nor its negation are entailed by the store. Synchronization is achieved through suspending ask, namely the process is suspended when the store entails neither the ask constraint nor its negation. A process remains suspended until the store becomes sufficiently updated to either entail the ask constraint or its negation.

In the following we will consider the ask-tell paradigm in a sequential framework. Namely, we do not allow suspension, i.e. if an ask constraint is not entailed by a store, the computation fails. Moreover we will consider a slighty different notion of ask constraints and entailment.

3 The Approach

This section demonstrates the basic idea of our approach via an intuitive example.

Example 3.1 Consider a Prolog program consisting of two clauses written in a CLP style.

C_{1} = p(x̄) ← x̄ = t̄_{1} □ q(t̄_{2}).

C_{2} = p(x̄) ← x̄ = t̄_{3} □ r(t̄_{4}).

and the goal

G = ȳ = t̄ □ p(ȳ), r(s̄).

The intended operational semantics can be described by:

1. The first clause is applied to p(x̄) if the constraint c ≡ ȳ = t̄ ∧ p(ȳ) = p(x̄) ∧ x̄ = t̄_{1} is satisfiable. The success of G then depends on the success of the goal c □ q(t̄_{2}), r(s̄).

2. The second clause is applied if

(a) the computation of G starting with a derivation applying the first clause for p terminates (e.g. finitely fails or succeeds); and

(b) the constraint ȳ = t̄ ∧ p(ȳ) = p(x̄) ∧ x̄ = t̄_{3} is satisfiable.

Informally, the above program could be translated to the following (constrained) one, where the search strategy is coded in an ask-like constraint.

C_{1}^{τ} = p(x̄) ← ⟨true : x̄ = t̄_{1}⟩ □ q(t̄_{2}).

C_{2}^{τ} = p(x̄) ← ⟨term_{p}^{2}(p(x̄)) : x̄ = t̄_{3}⟩ □ r(t̄_{4}).

The ask constraint true of C_{1}^{τ} denotes that C_{1}^{τ} is applicable to any goal, while the ask constraint term_{p}^{2}(p(x̄)) of C_{2}^{τ} expresses the fact that the application of C_{2}^{τ} depends on termination of the computations for the goal p(x̄) starting from clauses C_{i}^{τ} with i < 2.

Checking for the termination of the atom p(x̄) is not sufficient if this atom is part of a non-atomic goal. In such a case, the applicability of a clause to a goal depends on the termination of the computation for the whole goal, starting from the preceding clauses. Thus, the applicability condition for clauses is not limited to the termination of one atom, but it must be extended to the whole goal. When dealing with non-atomic goals, the termination condition has to consider the whole computation, thus, the argument of term_{p}^{2} must be extended at execution time. For instance, with the goal ȳ = t̄ □ p(ȳ), r(s̄), the ask constraint of clause C_{2}^{τ} must become term_{p}^{2}(ȳ = t̄, p(ȳ) = p(x̄) □ p(x̄), r(s̄)), asking for the termination of the goal p(x̄), r(s̄) in a store containing the binding x̄ = t̄.

To better understand the behaviour of applicability conditions, consider the following:

Example 3.2 Consider the Prolog program:

p(0).
p(s(x)).
r(x) ← r(x).

The second clause can be applied to the goal p(x) because the computation for this goal terminates applying the first clause. However, the second clause is not applicable to the goal p(x), r(x) as the computation starting with the first clause does not terminate for this goal (because of the divergence for r(0)).

The computational model of the constraint language introduced in the next section is suitabe to model such a behaviour.

4 The τ language

This section introduces a constraint logic language τ which is applied in the next section to model Prolog control. We present and prove equivalent two semantic definitions for τ. An operational semantics defined in terms of a simple transition system is later used to justify the proposed modelling of Prolog. A declarative semantics is given in terms of an immediate consequence operator and in combination with the transformation proposed in the next section provides a basis for bottom-up abstract interpretations of Prolog programs.

A τ program consists of ask-tell constrained clauses as in the cc paradigm. However in contrast with the cc framework, ask and tell constraints will be interpreted over different algebraic structures:

• Tell constraints are interpreted over the usual Herbrand system, H [19].

• Ask constraints correspond to semi-decidable tests which are intended to specify termination conditions (applied below to model termination of Prolog goals). These tests are interpreted by an associated termination theory, T .

4.1 Syntax

Let Σ, Π and Var be given as above and let Π_{H} = {=}, Π_{T} and Π_{P} be a partition of Π. We assume an element true ∈ Π_{T}. A finite sequence of Π_{P}-atoms is called a Π_{P}-resolvent or a resolvent for short.

Definition 4.1 (goals and constraints) A tell constraint or a store is a finite set of Π_{H}-atoms. The set of stores is denoted by Store. An ask constraint is an element of the form t(g) where t ∈ Π_{T} and g is a Π_{P}-resolvent. Ask constraints of the form t(Λ) are denoted t. A constraint is a pair ⟨ask : tell⟩ consisting of an ask and a tell constraint.

A goal is a pair c □ B consisting of a constraint c and a resolvent B. The set of goals is denoted by Goal. The empty tell constraint is denoted by “true”.

In the following we will often omit Λ in empty goals.

Definition 4.2 (programs) A τ program consists of a finite set of clauses of the form H ← c □ B where H is a Π_{P}-atom and c □ B is a goal.

Ask and tell constraints are interpreted over corresponding T and H theories. T is a downward closed (i.e. closed under instantiation) set of ask constraints called a termination theory. We assume that true(g) ∈ T for every resolvent g.

Constraint consistency is defined for a given “environment” specified by a resolvent and a store.

Definition 4.3 (ask and tell consistency) Let ρ be a resolvent, σ a store and ⟨ask : tell⟩ a constraint with ask = t(g), we write:

• H ⊧_{σ} tell iff σ ∪ tell has a solution,

• T ⊧_{σ}^{ρ} ask iff t(g :: ρ)σ ⊆ T ,

• ⟨H, T ⟩ ⊧_{σ}^{ρ} ⟨ask : tell⟩ iff H ⊧_{σ} tell and T ⊧_{σ}^{ρ} ask

and say that ask and tell are respectively H and T consistent for σ and ρ.

Example 4.1 Consider a store σ = {y = s(z)}, a resolvent ρ = p(0) and a termination theory T = {t(g) | g ∈ A(Σ, Π_{P}, Var)^{∗}} with Σ = {0, s}, Π_{P} = {p} and a constraint c = ⟨t(p(y)) : y = s(0)⟩. Since σ ∪ {y = s(0)} has a solution and t(p(y), p(0))σ ⊆ T , therefore ⟨H, T ⟩ ⊧_{σ}^{ρ} c.

Intuitively, T consistency will be used to model the dynamic extension of applicability conditions for clauses. Given a store σ and a resolvent ρ, T ⊧_{σ}^{ρ} t(g) guarantees that the atomic goal g extended with the atoms in the resolvent ρ, terminates in the store σ.

4.2 Operational Semantics

An operational semantics for τ is formalised in terms of a transition relation on goals. A pair in the relation corresponds to the reduction of a goal with a renamed clause from the program. The conditions on the tell parts of the goal and clause are the standard ones reviewed in Section 2 (e.g. CLP(H) [19]). At each step the ask conditions of the chosen clause are tested with respect to a “current” store and resolvent. Ask constraints are not collected since downward closure of T implies that any test satisfied in a store will be continuously satisfied in subsequent (updated) stores.

Definition 4.4 (transition system) Let P be a τ program and let T be a termination theory. Define ⟶^{T}_{P} ⊆ Goal × Goal to be the smallest relation such that:

⟨true : tell⟩ □ A | B ⟶^{T}_{P} ⟨true : tell ∪ {H = A} ∪ tell′⟩ □ B′ :: B

if C = H ← ⟨ask′ : tell′⟩ □ B′ <<_{V} P, where V = vars(⟨true : tell⟩ □ A | B), H ⊧_{tell} {H = A} ∪ tell′ and T ⊧_{tell∪{H =A}}^{B} ask′.

The (non-ground) success set of a τ-program is specified (similar to the case of logic programs, e.g. [17]) in terms of the atomic goals of the form ⟨true : tell⟩ □ p(x̄) which have successful computations as specified by the transitive closure of the transition relation (given a termination theory T ).

Definition 4.5 (success set) Let P be a τ program and let T be a termination theory. The success set of P with respect to T is:

S_{T} (P) = \{ p(x̄)σ | ⟨true : tell⟩ □ p(x̄) ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ⟩ □ \} .

Notice that the success set of a program P is a set of atoms closed under instantiation. The operational semantics of a τ program is defined in terms of the successful computations for (consistent) initial goals:

Definition 4.6 (operational semantics) Let P be a τ program and let T be a termination theory. Define O_{T} (P) : Goal → 2^{Store} by:

O_{T} (P) = λ⟨ask : tell⟩ □ G. \{ σ | \begin{matrix}⟨true : tell⟩ □ G ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ⟩ □ \\ H ⊧_{∅} tell and T ⊧_{∅}^{Λ} ask \end{matrix} \} .

Note that the operational semantics is parametric with respect to a choice of termination theory T . In the following we refer to such semantic definitions as open with respect to T .

Example 4.2 Let T = {t(g) | g ∈ A(Σ, Π_{P}, ∅)^{∗}} be a termination theory Π_{P} = {p}, Σ = {0, s}, and let P be the following τ-program:

p(x) ← ⟨true : x = 0⟩ □.

p(x) ← ⟨t(p(x)) : x = s(y)⟩ □ p(y).

The goal ⟨true : true⟩ □ p(s(x)) cannot be reduced since reduction with the first clause would result in an inconsistent tell constraint while reduction with the second clause is not ask consistent (the termination theory contains only ground atoms). The goal ⟨true : true⟩ □ p(s(0)) has a successful computation:

⟨true : true⟩ □ p(s(0)) ⟶^{T}_{P} ⟨true : y = 0⟩ □ p(y) ⟶^{T}_{P} ⟨true : y = 0⟩ □.

The success set of P with respect to T is

{p(0), p(s(0)), p(s(s(0))), …}.

4.3 Declarative Semantics

We now define a declarative semantics for τ programs which is open with respect to the interpretation of ask constraints. It is defined in terms of unfoldings of clauses [21] which contain uninterpreted ask conditions. This approach facilitates separation of termination from computation when applied to modelling Prolog control. Unfoldings of clauses with ask and tell constraints result in sequences of constraints [18] which we term constrained atoms.

Definition 4.7 (constrained atoms) A constrained atom, π, is a formula of the form

H ← ⟨ask_{1} : tell_{1}⟩ ← ⋯ ← ⟨ask_{n} : tell_{n}⟩

where H is an atom and ⟨ask_{1} : tell_{1}⟩, …, ⟨ask_{n} : tell_{n}⟩ are constraints. We often denote π = H ← ⟨ask_{i} : tell_{i}⟩_{i=1}^{n} and tell(π) = ∪_{i=1}^{n} tell_{i}.

The notion of consistency extends naturally to constrained atoms:

Definition 4.8 (consistent constrained atom) Let σ_{0} be a store, ρ a resolvent, T a termination theory and π = p(x̄) ← ⟨ask_{i} : tell_{i}⟩_{i=1}^{n} a constrained atom. We write:

• H ⊧_{σ_{0}} π iff H ⊧_{σ_{0}} tell(π),

• T ⊧_{σ_{0}}^{ρ} π iff for i = 1..n, T ⊧_{σ_{i−1}}^{ρ} ask_{i} where σ_{i} = σ_{i−1} ∪ tell_{i},

• ⟨H, T ⟩ ⊧_{σ_{0}}^{ρ} π iff H ⊧_{σ_{0}} π and T ⊧_{σ_{0}}^{ρ} π.

Example 4.3 Let π = p(x) ← ⟨t(p(x)) : x = s(y)⟩ ← ⟨t(p(y)) : y = s(z)⟩ ← ⟨t(p(z)) : z = s(w)⟩, σ = {x = sss(0)} and T = {t(p(0)), t(p(s(0))), t(p(ss(0))), …}. Then ⟨H, T ⟩ ⊧_{σ}^{Λ} π because H ⊧_{σ} {x = s(y), y = s(z), z = s(w)} and

T ⊧_{σ}^{Λ} t(p(x)),

T ⊧_{σ∪{x=s(y)}}^{Λ} t(p(y)) and T ⊧_{σ∪{x=s(y),y=s(z)}}^{Λ} t(p(z)).

The following example demonstrates that consistency of constrained atoms is order dependent:

Example 4.4 Let T = {t(p(f (a)))}, σ = ∅ and

π_{1} = p(x) ← ⟨true : x = f (a)⟩ ← ⟨t(p(x)) : true⟩,
π_{2} = p(x) ← ⟨t(p(x)) : true⟩ ← ⟨true : x = f (a)⟩;

then ⟨H, T ⟩ ⊧_{σ}^{Λ} π_{1} but ⟨H, T ⟩ |̸=_{σ}^{Λ} π_{2}.

The semantic objects will consist of (equivalence classes) of consistent constrained atoms. In the following we will often denote by η a sequence of constraints ⟨t_{i}(g_{i}) : tell_{i}⟩_{i=1}^{n}. Intuitively, a constrained atom, p ← η, represents a sequence of ask and tell constraints corresponding to a possible computation for p. A computed answer constraint is returned for that atom only if all the constraints in the sequence are consistent with respect to the current store. As the atom can be used in a more complex goal all the ask constraints in η must be augmented to be sensitive to the context in which they are used. This motivates the following notation: let η be the sequence ⟨t_{i}(g_{i}) : tell_{i}⟩_{i=1}^{n}, for any resolvent ρ, we denote by η[ρ] the (augmented) sequence ⟨t_{i}(g_{i} :: ρ) : tell_{i}⟩_{i=1}^{n}.

Definition 4.9 (equivalence of constrained atoms) Let π_{1} and π_{2} be constrained atoms; π_{1} ∼ π_{2} iff for every termination theory T , store σ and resolvent ρ there are renamings π′_{1} = p(t̄_{1}) ← η_{1}, π′_{2} = p(t̄_{2}) ← η_{2} of π_{1} and π_{2} such that vars(σ)∩vars(π′_{i}) ⊆ vars(t̄_{i}), for i = 1, 2 and ⟨H, T ⟩ ⊧_{σ}^{ρ} π′_{1} ⇔ ⟨H, T ⟩ ⊧_{σ}^{ρ} π′_{2}.

The equivalence of constrained atoms, π′_{1} = p(t̄_{1}) ← η_{1} and π′_{2} = p(t̄_{2}) ← η_{2} is specified with respect to stores which do not affect the local variables of η_{1} and η_{2} (that is the local variables of possible computations for p(t̄_{1}) and p(t̄_{2})).

Note that for any constrained atom π = p(t̄) ← η there is an equivalent constrained atom of the form π′ = p(x̄) ← η′ (in which x̄ are distinct variables not occurring in π) defined by taking new variables x̄ and η′ = ⟨true : x̄ = t̄⟩ ← η. So in the following, any constrained atom may be denoted as p(x̄) ← η.

Definition 4.10 (B_{P}^{τ} base) Let P be a τ-program. The base of interpretations for P, denoted B_{P}^{τ}, is the set of equivalence classes of constrained atoms over the alphabet of P.

Definition 4.11 (interpretation) An interpretation is any subset of B_{P}^{τ}.

In the following we give a fixpoint characterization of the semantics in terms of a continuous immediate consequence operator T_{P}^{τ}.

Definition 4.12 Let P be a τ-program. The mapping T_{P}^{τ} : 2^{BP^{τ}} → 2^{BP^{τ}} is defined by:

T_{P}^{τ}(I ) = \{ [H ← η̄]_{∼} | \begin{matrix}C = H ← c □ B_{1}, …, B_{n} ∈ P, \\ for i = 1..n \\ ρ_{i} = B_{i+1}, …, B_{n}, \\ π_{i} = H_{i} ← η_{i}, [π_{i}]_{∼} ∈ I , \\ η̄_{i} = ⟨true : H_{i} = B_{i}⟩ ← η_{i}[ρ_{i}], \\ C , π_{1}, …, π_{n} are renamed apart, \\ η̄ = c ← η̄_{1} ← ... ← η̄_{n}, H ⊧_{∅} H ← η̄ \end{matrix} \} .

Note that the unfolding of an atom B_{i} in the body of the clause C with respect to a constrained atom H_{i} ← η_{i} keeps track of the current resolvent. Thus, the resulting constrained atom H ← η̄ represents a computation for the atomic goal H obtained by applying to a clause the computations for the atoms in the body. To construct the new applicability tests, all the termination tests in each computation are enhanced with the resolvent corresponding to the remaining part of the goal to be evaluated. The ask constraints in the sequence η_{i}, in fact, are enhanced with the current resolvent ρ_{i} = B_{i+1}, ..., B_{n} (η_{i}[ρ_{i}]).

Proposition 4.1 T_{P}^{τ} is well defined and continuous.

Proof. The proof is standard [17, 22]. □

Definition 4.13 (fixpoint semantics) The fixpoint semantics for a τ-program P is defined by F(P) = lfp(T_{P}^{τ}) = T_{P}^{τ} ↑ ω.

Example 4.5 Consider the following τ programs P_{1}^{τ} and P_{2}^{τ} where Π_{T} = {t, true}:

P_{1}^{τ}: p(x) ← ⟨true : true⟩ □.

p(x) ← ⟨t(p(x)) : x = s(y)⟩ □ p(y).

P_{2}^{τ}: p(x) ← ⟨t(p(x)) : true⟩ □.

p(x) ← ⟨true : x = s(y)⟩ □ p(y).

The fixpoint semantics of P_{1}^{τ} and P_{2}^{τ} are:

F(P_{1}^{τ}) = \{ \begin{matrix}p(x) ← ⟨true : true⟩, \\ p(x) ← ⟨t(p(x)) : x = s(y)⟩, \\ p(x) ← ⟨t(p(x)) : x = s(y)⟩ ← ⟨t(p(y)) : y = s(z)⟩, \\ p(x) ← ⟨t(p(x)) : x = s(y)⟩ ← ⟨t(p(y)) : y = s(z)⟩ \\ ← ⟨t(p(z)) : z = s(w)⟩, \\ … \end{matrix} \}

F(P_{2}^{τ}) = \{ \begin{matrix}p(x) ← ⟨t(p(x)) : true⟩, \\ p(x) ← ⟨true : x = s(y)⟩ ← ⟨t(p(y)) : true⟩, \\ p(x) ← ⟨true : x = s(y)⟩ ← ⟨true : y = s(z)⟩ ← ⟨t(p(z)) : true⟩, \\ … \end{matrix} \}

Observe that for the previous example, in the evaluation of the lfp(T_{P}^{τ}), the resolvents ρ_{i} are always empty as the clauses of P have unit or empty bodies. Example 5.3 illustrates the more general case.

In Example 4.6 (below) we show how to compose an interpretation for the ask predicate t with F(P_{1}^{τ}) and F(P_{2}^{τ}) to provide success sets for P_{1}^{τ} and P_{2}^{τ}. The choice of P_{1}^{τ} and P_{2}^{τ} is further motivated by Example 5.3.

4.4 Equivalence of Operational and Declarative Semantics

By composing the open declarative semantics F(P) of a program P with a termination theory T we can derive the corresponding success set S_{T} (P).

Definition 4.14 Let I be an interpretation, ρ a resolvent and T a termination theory. The composition I [T ] of I and T with respect to ρ is defined by:

I [T ](ρ) = \{ p(x̄)σ | \begin{matrix}[π]_{∼} = [p(x̄) ← η]_{∼} ∈ I , \\ ∃θ : vars(θ) ∩ vars(π) ⊆ x̄, \\ T ⊧_{θ}^{ρ} π, σ = tell(π) ∪ θ \end{matrix} \} .

Note that I [T ](ρ) contains the atoms obtained by the composition of the constrained atoms in I with a termination theory T and a resolvent ρ. Given π = p(x̄) ← η ∈ I , if the sequence η is consistent in a store θ with respect to T and ρ and σ = tell(π) ∪ θ then π contributes p(x̄)σ to this composition.

Proposition 4.2 (monotonicity of composition) Let I be an interpretation. If T_{1} ⊆ T_{2} then for each resolvent ρ, I [T_{1}](ρ) ⊆ I [T_{2}](ρ).

Proof. The proof is a straightforward application of the definitions. □

Example 4.6 Consider the programs P_{1}^{τ} and P_{2}^{τ} from Example 4.5 and let

T_{1} = {t(g) | g ∈ A(Σ, Π_{P}, Var)^{∗}} and T_{2} = {t(g) | g ∈ A(Σ, Π_{P}, ∅)^{∗}}

where Σ = {0, s} and Π_{P} = {p}. Then

F(P_{1}^{τ})[T_{1}](Λ) = {p(t) | t ∈ T (Σ, Var)} and

F(P_{2}^{τ})[T_{2}](Λ) = {p(t) | t ∈ T (Σ)}.

The following theorem states the soundness and completeness of the fixpoint semantics with respect to the operational notion of success set.

Theorem 4.3 (soundness and completeness) Let P be τ-program and T be a termination theory. Then S_{T} (P) = F(P)[T ](Λ).

Proof. See the Appendix. □

Strong equivalence shows the equivalence between the operational semantics of a program and the answers which can be computed from its fixpoint semantics for arbitrary goals:

Definition 4.15 (answers for generic goals) Let I be an interpretation and let T be a termination theory. The set of answers for a goal

G = ⟨ask : tell⟩ □p_{1}(t̄_{1}), ..., p_{n}(t̄_{n})

in I for T is defined by:

ans_{I}^{T} (G) = \{ σ | \begin{matrix}T ⊧_{∅}^{Λ} ask and for i = 1..n : \\ [π_{i}]_{∼} = [p_{i}(x̄_{i}) ← η_{i}]_{∼} ∈ I , \\ π_{1}, ..., π_{n}, G are renamed apart, \\ ρ_{i} = p_{i+1}(t̄_{i+1}), ..., p_{n}(t̄_{n}), \\ σ_{0} = tell and σ_{i} = σ_{i−1} ∪ \{x̄_{i} = t̄_{i}\} ∪ tell(π_{i}), \\ T ⊧_{σ_{i−1}∪\{x̄i =t̄i \}}^{ρi} π_{i}, H ⊧_{∅} σ_{n}, \\ σ = σ_{n} \end{matrix} \} .

Informally, the answers for G = ⟨ask : tell⟩ □p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) with respect to I and T are obtained in the following way: for each atom p_{i}(t̄_{i}) in G a constrained atom, π_{i} = p_{i}(x̄_{i}) ← η_{i}, is extracted from I . Each η_{i} is checked for consistency with respect to the termination theory T , the store resulting from processing the atoms in positions 1, ..., i − 1 enhanced with the bindings x̄_{i} = t̄_{i} and the resolvent given by the sequence of atoms in positions i + 1, ..., n. If a η_{i} is found consistent then {x̄_{i} = t̄_{i}} ∪ tell(π_{i}) is added to the current store to continue the process until p_{n}(t̄_{n}).

The following theorem states the equivalence between the concept of answers for a goal and the oparational semantics.

Theorem 4.4 (strong equivalence) Let P be τ-program, T a termination theory and G = ⟨ask : tell⟩ □ B_{1}, ..., B_{n} be a goal. Then σ′ ∈ ans_{F(P)}^{T}(G) iff σ ∈ O_{T} (P)(G) and Gσ = Gσ′.

Proof. See the Appendix. □

For a given a termination theory, F(P) may contain possibly inconsistent sequences (i.e. constrained atoms which cannot be satisfied). The “pruning” is operated by interpreting F(P) in the termination theory.

5 Modelling Prolog in τ

The basic idea applied in this section is to specify in a “declarative” way the condition upon which a Prolog clause might eventually be chosen under a depth-first strategy. Namely, that there is no infinite path to the left in the corresponding SLD tree. This idea is first applied to model Prolog control in τ. A transformation which associates a Prolog program P with a corresponding τ program P^{τ} is introduced. The same idea is then applied to define an operational semantics for Prolog which is used to argue the correctness of this transformation.

We assume that Prolog evaluation proceeds until all answers are generated and that Prolog evaluation is sound. A Prolog program is viewed as a set of predicates, each predicate consisting of an ordered set of clauses. Prolog goals are sequences of atoms. Let us return to Example 3.1 where the operational semantics of the Prolog program P:

p(t̄_{1}) ← q(t̄_{2}).
p(t̄_{3}) ← r(t̄_{4}).

is informally captured by the τ program P^{τ}

p(x̄) ← ⟨true : x̄ = t̄_{1}⟩ □ q(t̄_{2}).
p(x̄) ← ⟨term_{p}^{2}(p(x̄)) : x̄ = t̄_{3}⟩ □ r(t̄_{4}).

The claim is that given the intended termination theory of P, the τ-program P^{τ} has the same meaning as the Prolog program P. The following definitions specify the transformation from Prolog to τ and what we mean by the intended termination theory.

Definition 5.1 (transformation) Let P be a Prolog program. For each predicate {C_{1}, …, C_{m}} in P we generate from the clause C_{i} = p(t̄) ← Body a corresponding τ clause:

C_{i}^{τ} = p(x̄) ← ⟨term_{p}^{i}(p(x̄)) : x̄ = t̄⟩ □ Body.

The corresponding τ program P^{τ} is then defined by collecting the respective C_{i}^{τ} clauses for all the predicates in P:

P^{τ} = \{ C_{i}^{τ} | \begin{matrix}\{C_{1}, …, C_{n}\} ∈ P, \\ i ∈ \{1, …, n\} \end{matrix} \} .

The Π_{T} predicates term_{p}^{i}(p(x̄)) in the above definition correspond to tests which are intended to enable τ reduction of a goal with a clause C_{i}^{τ} only in case Prolog computation of the corresponding goal starting with the preceding clauses for that predicate (i.e. {C_{1}, …, C_{i−1}}) terminates. Note that under this interpretation term_{p}^{1} is vacuously true.

By SLD reduction we mean usual resolution with a left-to-right selection rule [22]. An SLD reduction is captured by:

Definition 5.2 (resolve) Let Clause denote the set of Horn clauses. Define: resolve : Atom^{∗} ×Clause → 2^{Atom^{∗}} by:

resolve(G, H ← Body) = \{ \begin{matrix}(Body :: B)\{H = A\} & if G = A | B, \\ ∅ & otherwise. \end{matrix}

The following definition is motivated by the observation (e.g. [2]) that when reasoning about termination of all solutions for a goal with a Prolog program, it is possible to ignore depth-first search and hence to consider the corresponding SLD tree (with a left-to-right selection rule). The proof of this observation is straightforward [28].

Definition 5.3 (intended termination theory) Let P be a Prolog program. The intended termination theory for P is defined by:

T_{Prolog}(P) = \{ term_{p}^{i}(g) | \begin{matrix}\{C_{1}, …, C_{n}\} defines p in P and \\ for 1 ≤ i ≤ n : \\ if g′ ∈ ⋃_{j <i}resolve(g, C_{j} ) then \\ the SLD tree for P and g′ is finite \end{matrix} \} .

Theorem 5.1 The intended termination theory for a Prolog program P is a termination theory (i.e. closed under instantiation).

Proof. The proof follows straightforwardly from the results in [28]. □

In the next section we discuss how to approximate the intended termination theory for a Prolog program. Meanwhile, we claim that given the intended termination theory for a Prolog program, the corresponding τ program captures the operational meaning of P. To formalise this we introduce an operational semantics for Prolog. We will need the following:

Definition 5.4 (finite-transitive) A relation R ⊆ X × X on a set X is finite-transitive for x ∈ X iff the multi-set {x′ | xR^{∗}x′} is finite.

The following definition specifies a transition relation for logic programs with a leftto-right selection rule (but ignores the depth-first search of Prolog). This definition is then applied to specify the transition relation for Prolog. The implicit use of stores instead of substitutions is not essential.

Definition 5.5 (transition relation for SLD) Let P be a logic program; ⟶^{sld}_{P} ⊆ Atom^{∗} × Atom^{∗} is the relation defined by:

g ⟶^{sld}_{p} g′ ⇔ g′ ∈ ⋃_{C ∈P}resolve(g, C ).

We denote by pred_{P}(A) the predicate (i.e. ordered set of clauses) for atom A in a Prolog program P.

Definition 5.6 (transition relation for Prolog)

Let P be a Prolog program; ⟶^{prolog}_{P} ⊆ Atom^{∗} × Atom^{∗} is the smallest relation such that

A | B ⟶^{prolog}_{P} G

if pred_{P}(A) = {C_{1}, …, C_{n}}; 1 ≤ i ≤ n; G ∈ resolve(A | B, C_{i}); and

∀G′ ∈ ⋃_{j <i}resolve(A | B, C_{j} ) the relation ⟶^{sld}_{P} is finite-transitive for G′.

The success set of a Prolog program P is captured in terms of the transitive closure

of ⟶^{prolog}_{P}.

Definition 5.7 (Prolog success set) The Prolog success set is S_{Prolog} : Prolog → 2^{Atom} such that:

S_{Prolog}(P) = { A ∈ Atom | A ⟶^{prolog}_{P}^{∗} Λ } .

Theorem 5.2 Let P be a Prolog program and P^{τ} the corresponding τ program. Then:

S_{Prolog}(P) = F(P^{τ})[T_{Prolog}(P)](Λ).

Proof. By Theorem 4.3, F(P^{τ})[T_{Prolog}(P)](Λ) = S_{TProlog (P)}(P^{τ}). We have to prove that:

S_{Prolog}(P) = S_{TProlog (P)}(P^{τ}).

The proof argues the correspondence between the respective operational behaviours of P and of P^{τ} given the corresponding intended termination theory. Let G = p(t̄) | B̄ be a Prolog goal.

G ⟶^{prolog}_{P} G′; iff

∃C_{i} ∈ pred_{P}(p(t̄)) = {C_{1}, ..., C_{m}} such that G′ ∈ resolve(G, C_{i})

and ∀G′′ ∈ ∪_{j <i} resolve(G, C_{j} ), G′′ has a finite SLD tree; iff

∃C_{i} ∈ pred_{P}(p(t̄)) = {C_{1}, ..., C_{m}}, C_{i} = p(s̄) : − Body,

such that G′ ∈ resolve(G, C_{i}) and term_{p}^{i}(G) ∈ T_{Prolog}(P); iff

∃C_{i}^{τ} = p(x̄) : − ⟨term_{p}^{i}(p(x̄)) : x̄ = s̄⟩ □ Body ∈ P^{τ},

term_{p}^{i}(p(t̄) | B̄) ∈ T_{Prolog}(P); iff

∃C_{i}^{τ} = p(x̄) : − ⟨term_{p}^{i}(p(x̄)) : x̄ = s̄⟩ □ Body ∈ P^{τ},

T_{Prolog}(P) ⊧B̄ x̄=t̄ term_{p}^{i}(p(x̄)); iff

⟨true : true⟩ □ p(t̄) | B̄ ⟶^{T}_{P^{τ}} ⟨true : {x̄ = t̄, x̄ = s̄}⟩ □ Body :: B̄.

Notice that ⟨true : σ⟩ □ G ⟶^{T}_{P^{τ}} ⟨true : σ′⟩ □ G′ iff for each G′′ ∈ Gσ: ⟨true : true⟩ □ G′′ ⟶^{T}_{P^{τ}} ⟨true : σ′′⟩ □ G′′′ and G′σ′ = G′′′σ′′. The theorem follows by a straightforward inductive argument. □

In the following we consider the success set of pure logic programs as defined in [17], where the standard approach is enhanced by introducing variables into the semantics objects.

Proposition 5.3 Let P be a Prolog program and T_{lp} denote a termination theory which for every predicate p and corresponding i^{th} clause contains term_{p}^{i}(g) for every resolvent g. F(P^{τ})[T_{lp}](Λ) is the success set of P interpreted as a logic program, closed under instantiation.

Proof. By the definition

S_{Tlp} (P^{τ}) = \{ p(x̄)σ | ⟨true : θ⟩ □ p(x̄) →^{Tlp} \begin{matrix}∗ \\ P^{τ} \end{matrix} ⟨true : σ⟩ □. \} .

Let

P^{′τ} = \{ p(x̄) ← ⟨true : σ′⟩ □ Body | \begin{matrix}pred_{P}(p(x̄)) = \{C_{1}, ..., C_{m}\} ∈ P^{τ} , \\ 1 ≤ i ≤ m, \\ C_{i} = p(x̄) ← ⟨term_{p}^{i}(p(x̄)) : σ′⟩ □ Body \end{matrix} \}.

Notice that ∀g ∈ Atom^{∗}: T ⊧_{∅}^{Λ} t(g), thus S_{Tlp} (P^{τ}) = S_{Tlp} (P^{′τ}). It is easy to prove

[19] that S_{Tlp} (P^{′τ}) corresponds to the success set of a CLP(H) program, closed under instantation.

□

In the following examples we write true instead of the corresponding termination conditions for the first clause. Furthermore we do not specify these atoms in the respective termination theories. This simplifies somewhat the presentation.

Example 5.1 Consider the following two Prolog programs with Σ = {0, s} and Π_{P} = {p}:

P_{1}: p(x).

p(s(y)) ← p(y).

P_{2}: p(s(y)) ← p(y).

p(x).

The transformed programs are respectively

P_{1}^{τ}: p(x) ← ⟨true : true⟩ □.

p(x) ← ⟨term_{p}^{2}(p(x)) : x = s(y)⟩ □ p(y).

P_{2}^{τ}: p(x) ← ⟨true : x = s(y)⟩ □ p(y). p(x) ← ⟨term_{p}^{2}(p(x)) : true⟩ □.

The intended termination theories for P_{1} and P_{2} consist respectively of the nonground and ground sets of goals:

T_{Prolog}(P_{1}) = {term_{p}^{2}(g) | g ∈ A(Σ, Π_{P}, Var)^{∗}} and

T_{Prolog}(P_{2}) = {term_{p}^{2}(g) | g ∈ A(Σ, Π_{P}, ∅)^{∗}}.

The open declarative meanings of P_{1}^{τ} and P_{2}^{τ} correspond to those given in Example 4.5; the success sets correspond to those given in Example 4.6:

S_{Prolog}(P_{1}) = F(P_{1}^{τ})[T_{Prolog}(P_{1})](Λ) = {p(t) | t ∈ T (Σ, Var)}
S_{Prolog}(P_{2}) = F(P_{2}^{τ})[T_{Prolog}(P_{2})](Λ) = {p(t) | t ∈ T (Σ)},

which express the computational behaviour of the original Prolog programs.

In particular, F(P_{2}^{τ})[T_{Prolog}(P_{2})](Λ) does not include p(x) which corresponds to the fact the the Prolog computation does not succeed for that goal (because it diverges).

Example 5.2 Consider the following Prolog program P with Σ = {a, b} and Π_{P} = {p}:

p(a, b).
p(x, y) ← p(x, y).
p(x, x).

The corresponding transformed τ-program P^{τ} is:

p(x, y) ← ⟨true : x = a, y = b⟩ □.
p(x, y) ← ⟨term_{p}^{2}(p(x, y)) : true⟩ □ p(x, y).
p(x, y) ← ⟨term_{p}^{3}(p(x, y)) : x = y⟩ □.

Note that there are no goals g ∈ A(Σ, Π_{P}, Var)^{∗} such that for all

g′ ∈ resolve(g, p(a, b).) ∪ resolve(g, p(x, y) ← p(x, y).),

the SLD tree for P and g′ is finite. The Prolog termination theory for P is then:

T_{Prolog}(P) = { term_{p}^{2}(p(t_{1}, t_{2})) | t_{1}, t_{2} ∈ T (Σ, Var) } ∪

\{ term_{p}^{2}(p(t_{1}, t_{2}) | g) | \begin{matrix}t_{1}, t_{2} ∈ T (Σ, Var), \\ g ∈ A(Σ, Π_{P}, Var)^{n}, n ≥ 1, \\ H |̸= \{t_{1} = a, t_{2} = b\} \end{matrix} \} .

The success set of P as a Prolog program is

F(P^{τ})[T_{Prolog}(P)](Λ) = {p(a, b)};

while the success set of P interpreted as a pure logic program is

F(P^{τ})[T_{lp}](Λ) = {p(a, b)} ∪ { p(t, t) | t ∈ T (Σ, Var) }.

Note that while the depth-first search strategy is captured by the transformation and the corresponding termination conditions, the left-to-right selection rule is modelled by the sequential composition of atoms in the bodies in τ-clauses.

In the following example we show how the order of the atoms in the body of a Prolog clause leads to different solutions and how the declarative semantics of the transformed program captures this fact.

Example 5.3 The Prolog program Q:

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

is transformed in a τ-program Q^{τ}:

q(x) ← ⟨true : true⟩ □ p(x), r(x).

p(x) ← ⟨true : x = s(y)⟩ □ p(y).

p(x) ← ⟨term_{p}^{2}(p(x)) : true⟩ □.

r(x) ← ⟨true : x = 0⟩ □.

The declarative meaning of Q^{τ} is

F(Q^{τ}) = \{ \begin{matrix}r(x) ← ⟨true : x = 0⟩, \\ q(x) ← ⟨term_{p}^{2}(p(x), r(x)) : true⟩ ← ⟨true : x = 0⟩ \end{matrix} \} ⋃ F(P_{2}^{τ})

where F(P_{2}^{τ}) is defined in Example 4.5. Note that the solutions x = s^{n}(0) are inconsistent with the only solution for r (i.e. x = 0).

The intended termination theory T_{Prolog}(Q) contains

{term_{p}^{2}(p(t), r(t′)) | t ∈ T (Σ), t′ ∈ T (Σ, Var)}.

By considering the intended termination theory, the goal q(x) does not succeed because

T_{Prolog}(Q) |̸=_{∅}^{Λ} term_{p}^{2}(p(x), r(x)),

while q(0) succeeds. Changing the order of the atoms in the body of the first Prolog clause (and in the corresponding τ one) leads to the model

F(Q^{τ}) = \{ \begin{matrix}r(x) ← ⟨true : x = 0⟩ \\ q(x) ← ⟨true(p(x)) : x = 0⟩ ← ⟨term_{p}^{2}(p(x)) : true⟩ \end{matrix} \} ⋃ F(P_{2}^{τ}).

In this case q(x) succeeds with answer x = 0.

Example 5.4 Consider the Prolog program from Example 1.1. Let P_{1} denote the clauses for the predicate eq/2 and let P_{2} denote the same program in which the order of the third and fourth clauses is switched. Lloyd [22] observes (see Example 1.1) that there is no way to order the clauses of this program so that a Prolog system will find a refutation for a goal eq(a, c). We illustrate how this is reflected in our semantics. The corresponding τ-programs P_{1}^{τ} and P_{2}^{τ} are:

P_{1}^{τ} : eq(x, y) ← ⟨true : x = a, y = b⟩ □.
eq(x, y) ← ⟨term_{eq}^{2}(eq(x, y)) : x = c, y = b⟩ □.
eq(x, z) ← ⟨term_{eq}^{3}(eq(x, z)) : true⟩ □ eq(x, y), eq(y, z).
eq(x, y) ← ⟨term_{eq}^{4}(eq(x, y)) : true⟩ □ eq(y, x).
eq(x, y) ← ⟨term_{eq}^{5}(eq(x, y)) : x = y⟩ □.

P_{2}^{τ} : eq(x, y) ← ⟨true : x = a, y = b⟩ □.
eq(x, y) ← ⟨term_{eq}^{2}(eq(x, y)) : x = c, y = b⟩ □.
eq(x, y) ← ⟨term_{eq}^{3}(eq(x, y)) : true⟩ □ eq(y, x).
eq(x, z) ← ⟨term_{eq}^{4}(eq(x, z)) : true⟩ □ eq(x, y), eq(y, z).
eq(x, y) ← ⟨term_{eq}^{5}(eq(x, y)) : x = y⟩ □.

It follows (informally) from the argument in [22] that the respective intended termination theories T_{Prolog}(P_{1}) and T_{Prolog}(P_{2}) do not contain ask constraints of the form term_{eq}^{4}(eq(t_{1}, t_{2})) for any terms t_{1}, t_{2} ∈ T (Σ, Var). Furthermore, any of the constrained atoms eq(x_{1}, x_{2}) ← η in F(P_{1}^{τ}) and F(P_{2}^{τ}) which are tell consistent with the initial store {x_{1} = a, x_{2} = c}, contain an ask constraint of that form. For instance, the following elements are in F(P_{1}^{τ}) and F(P_{2}^{τ}) respectively:

eq(x_{1}, x_{2}) ← ⟨term_{p}^{3}(p(x_{1}, y)) : true⟩ ← ⟨true : x_{1} = a, y = b⟩ ← ⟨term_{p}^{4}(p(y, x_{2})) : true⟩ ← ⟨term_{p}^{2}(p(x_{2}, y)) : x_{2} = c, y = b⟩.

eq(x_{1}, x_{2}) ← ⟨term_{eq}^{4}(eq(x_{1}, y)) : true⟩ ← ⟨true : x_{1} = a, y = b⟩ ← ⟨term_{eq}^{3}(eq(y, x_{2})) : true⟩ ← ⟨term_{eq}^{2}(eq(x_{2}, y)) : x_{2} = c, y = b⟩.

Thus, for i ∈ {1, 2}:

eq(a, c) ∉ S_{Prolog}(P_{i}) = F(P_{i}^{τ})[T_{Prolog}(P_{i})](Λ)

which reflects Lloyd’s claim.

6 Modelling Termination

In the previous section we have shown how to capture declaratively the success set of a Prolog program P by composing an interpretation for a corresponding τ program P^{τ} with the intended termination theory T_{Prolog}(P). Of course T_{Prolog}(P) cannot be effectively computed. However, the goal of this paper is to provide a semantic basis for the analysis of Prolog programs and for this purpose approximations of T_{Prolog}(P) both from above and from below can be useful:

\underline{from above:} T_{a} ⊇ T_{Prolog}(P) ⇒ F(P^{τ})[T_{a}](Λ) ⊇ F(P^{τ})[T_{Prolog}(P)](Λ) 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. In particular because by Proposition 5.3 the success set of the logic program P is F(P^{τ})[T_{lp}](Λ) and taking T_{a} ⊂ T_{lp}, gives F(P^{τ})[T_{a}](Λ) ⊂ F(P^{τ})[T_{lp}](Λ).

\underline{from below:} T_{b} ⊆ T_{Prolog}(P) ⇒ F(P^{τ})[T_{b}](Λ) ⊆ F(P^{τ})[T_{Prolog}(P)](Λ) 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 [16]; or to estimate a lower bound to the number of solutions.

Figure 1 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. Let P^{τ} denote the corresponding τ program. The solutions for G correspond to the success branches of the entire tree. These can be derived by composing F(P^{τ}) with T_{lp}. 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 by composing F(P^{τ}) with the intended

[figure: G; _{TProlog}; _{Tb}; _{Ta}; _{Tlp}; leftmost infinite branch]

Figure 1: SLD-tree for G with P

termination theory T_{Prolog}(P). Approximations of the Prolog solutions for G from above and below can be derived by composing F(P^{τ}) respectively with T_{a} and T_{b} which approximate T from above and from below.

We would like to capture the intended termination theory for a Prolog program P as the declarative meaning of some corresponding τ program. This would provide a precise declarative specification of T_{Prolog}(P) by applying the τ semantics. Furthermore it would enable approximations to be derived by abstract interpretation. In general to model intended termination theories as τ-programs we need to introduce a notion of user defined predicates in the ask parts of clauses and to interpret them as local tests which do not affect the global bindings of variables.

In the following example the intended termination theory for the Prolog program P_{2} in Example 4.5 and 5.1 is defined in terms of a well known downward closed theory.

Example 6.1 Consider the τ-program P_{2}^{τ} in Example 5.1:

p(x) ← ⟨true : x = s(x′)⟩ □ p(x′).
p(x) ← ⟨term_{p}^{2}(p(x)) : true⟩ □.

and let us define a termination theory for atomic goals T_{≠} such that

term_{p}^{2}(p(x))σ ∈ T_{≠} iff (x ≠ s( ))σ

where ≠ means “not unifiable”. In this hypothesis P_{2}^{τ} is equivalent to the following τ-program R:

p(x) ← ⟨true : x = s(x′)⟩ □ p(x′).

p(x) ← ⟨x ≠ s( ) : true⟩ □.

where ask constraints are disequations on T (Σ, Var). The declarative meaning of R is:

F(R) = \{ \begin{matrix}p(x) ← ⟨x ≠ s( ) : true⟩, \\ p(x) ← ⟨true : x = s(x′)⟩ ← ⟨x′ ≠ s( ) : true⟩, \\ … \end{matrix} \} .

If T′_{≠} is the (downward closed) theory corresponding to “not-unifiable” on T (Σ, Var) then F(R)[T_{≠}](Λ) gives the set {p(0), p(s(0)), p(ss(0)), …} which corresponds to the success set for the Prolog program P_{2} in Example 4.5 and 5.1.

7 Conclusions

We have presented a simple constraint logic language τ together with its operational and declarative semantics. The operational semantics is used to justify a transformation which captures the control of a Prolog program given a suitable termination theory. The declarative semantics is parametric with respect to this theory enabling the specification of Prolog meaning by composition of a “logic part” with a “control part”. Because the declarative semantics of τ is both simple and in the usual T_{P} style it provides a suitable basis for abstract interpretation of Prolog via the defined transformation.

The required termination theory can be approximated either by integrating results on Prolog termination (e.g. [2, 9, 26, 29]) or by extending the τ language so as to model termination from within and applying abstract interpretation.

The basic idea of defining semantics for Prolog without considering notions such as depth-first search and backtracking, which are more (sequential) implementation oriented is an important contribution of this paper. In particular, this idea can be applied to define a simple and concise operational semantics. We are currently in the process of applying this idea to other semantic definitions and extending our results to model full Prolog.

A Appendix

The proof of soundness and completeness is facilitated by the following basic observations:

Observation A.1 ((left-to-right) composition of operational semantics) Let T be termination theory, B_{1}, …, B_{k} atoms and σ_{0}, …, σ_{k} sets of tell constraints. For a goal ⟨true : σ_{0}⟩ □ B_{1}, …, B_{k} we have

⟨true : σ_{0}⟩ □ B_{1}, …, B_{k} ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ_{k}⟩ □ iff

⋀_{i=1}^{k} ⟨true : σ_{i−1}⟩ □ B_{i}, …, B_{k} ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ_{i}⟩ □B_{i+1}, …, B_{k}

Observation A.2 Let T be a termination theory, ρ a resolvent and π_{i} = p(x̄) ← η_{i} (i = 1..2) equivalent constrained atoms. If T ⊧_{∅}^{ρ} π_{i} (i = 1..2), then p(x̄)tell(π_{1}) = p(x̄)tell(π_{2}).

Observation A.3 Let G = ⟨true : σ⟩ □ p(t̄) | B̄ be a goal and x̄ be a tuple of distinct variables not occurring in G. Then ⟨true : σ⟩ □ p(t̄) | B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ′⟩ □ B̄ iff

⟨true : σ ∪ \{x̄ = t̄\}⟩ □ p(x̄) | B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ′′⟩ □ B̄

and p(t̄)σ′ = p(x̄)σ′′.

Proof of Theorem 4.3. Let x̄ = x_{1}, ..., x_{h} be a tuple of distinct variables, θ a constraint and B̄ a resolvent. In the following, with an abuse of notation, we denote x̄ both the tuple of variables x_{1}, ..., x_{h} and the corresponding set of variables {x_{1}, ..., x_{h}}. We prove by induction that

(∗) [π]_{∼} = [p(x̄) ← η]_{∼} ∈ T_{P}^{τ} ↑ ω iff ⟨true : θ⟩ □ p(x̄) | B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ′⟩ □ B̄

where π is a representative of [π]_{∼} such that vars(θ) ∩ vars(π) ⊆ x̄, ⟨H, T ⟩ ⊧B̄ ; θ π, σ = tell(π) ∪ θ and p(x̄)σ = p(x̄)σ′.

(⇒) Induction on the power n of T_{P}^{τ}:

• base step: (n = 1) is straightforward by definition of T_{P}^{τ}.

• inductive step: assume the theorem for (n > 1) and take [π]_{∼} = [p(x̄) ← η]_{∼} ∈ T_{P}^{τ} ↑ (n + 1) such that vars(θ) ∩ vars(π) ⊆ x̄, T ⊧B̄ ; θ π, and let σ = tell(π) ∪ θ.

By the definition of T_{P}^{τ}:

– ∃C = p(s̄) ← ⟨ask_{0} : tell_{0}⟩ □ b_{1}(s̄_{1}), …, b_{k}(s̄_{k}) ∈ P; – for j = 1, ..., k,

∃[π_{j} ]_{∼} = [b_{j} (x̄_{j} ) ← η_{j} ]_{∼} ∈ T_{P}^{τ} ↑ n

(renamed apart from each other and from C ) and

– η̄_{j} = ⟨true : x̄_{j} = s̄_{j} ⟩ ← η_{j} [b_{j +1}(s̄_{j +1}), …, b_{k}(s̄_{k}) :: B̄];

such that π′ = p(s̄) ← ⟨ask_{0}[B̄] : tell_{0}⟩ ← η̄_{1} ← ⋯ ← η̄_{k} and π ∼ π′.

Assume w.l.o.g. that x̄ do not occur in π′ (otherwise take an equivalent renaming of π′) and take

π′′ = p(x̄) ← ⟨true : x̄ = s̄⟩ ← ⟨ask_{0}[B̄] : tell_{0}⟩ ← η̄_{1} ← ⋯ ← η̄_{k}.

Clearly π′ ∼ π′′ and hence T ⊧B̄ ; θ π′′. Furthermore, by Observation A.2, p(x̄)σ = p(x̄)(θ ∪ tell(π′′)).

By definition of T -consistency of π′′, assuming:

σ_{0} = θ ∪ {x̄ = s̄} ∪ tell_{0} and
σ_{j} = σ_{j −1} ∪ {x̄_{j} = s̄_{j} } ∪ tell(π_{j} ), for each j ∈ {1, ..., k};

we have:

∀j ∈ {1, ..., k} : T ⊧_{σ_{j −1}∪{x̄j =s̄j }}^{ρj} π_{j} , where ρ_{j} = b_{j +1}(s̄_{j +1}), …, b_{k}(s̄_{k}) :: B̄.

Since π_{j} are renamed apart from C and from each other: vars(σ_{j −1} ∪ {x̄_{j} = s̄_{j} }) ∩ vars(π_{j} ) = x̄_{j} , and p(x̄)σ = p(x̄)σ_{k}.

Thus, ∀j ∈ {1, ..., k} :

∃[π_{j} ]_{∼} = [b_{j} (x̄_{j} ) ← η_{j} ]_{∼} ∈ T_{P}^{τ} ↑ n,
vars(σ_{j −1} ∪ {x̄_{j} = s̄_{j} }) ∩ vars(π_{j} ) = x̄_{j} , T ⊧_{σ_{j −1}∪{x̄j =s̄j }}^{ρj} π_{j} , and
σ_{j} = σ_{j −1} ∪ {x̄_{j} = s̄_{j} } ∪ tell(π_{j} ).

By the inductive hypothesis: ∀j ∈ {1, ..., k}

⟨true : σ′_{j −1} ∪ \{x̄_{j} = s̄_{j} \}⟩ □ b_{j} (x̄_{j} ), b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix}

⟨true : σ′_{j} ⟩ □ b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄

where σ′_{0} = σ_{0}, for each j = 1, ..., k : b_{j} (x̄_{j} )σ′_{j} = b_{j} (x̄_{j} )σ_{j} and p(x̄)σ′_{k} = p(x̄)σ_{k}. Thus

⟨true : σ′_{j −1}⟩ □ b_{j} (s̄_{j} ), b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix}

⟨true : σ′_{j} ⟩ □ b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄.

Applying Observation A.1 we have:

⟨true : σ_{0}⟩ □ b_{1}(s̄_{1}), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ′_{k}⟩ □ B̄,

and p(x̄)σ′_{k} = p(x̄)σ_{k}.

Since by hypothesis: σ_{0} = θ ∪ {x̄ = s̄} ∪ tell_{0}, H ⊧_{∅} θ ∪ tell(π′′), then H ⊧_{∅} σ_{0}. Moreover since T ⊧B̄ ; θ π′′ then T ⊧B̄ ; θ∪{x̄=s̄} ask_{0}. Thus:

⟨true : θ⟩ □ p(x̄) | B̄ ⟶^{T}_{P} ⟨true : σ_{0}⟩ □ b_{1}(s̄_{1}), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} \begin{matrix}∗ \\ P \end{matrix}

⟨true : σ′_{k}⟩ □ B̄.

and p(x̄)σ′_{k} = p(x̄)σ.

(⇐) Induction on the length of the computation, m.

• base step: (m = 1) is straightforward.

• inductive step: Let us assume the theorem holds for m > 1 and let us consider

⟨true : θ⟩ □ p(x̄) | B̄ ⟶^{T}_{P}

⟨true : θ ∪ \{x̄ = s̄\} ∪ tell_{0}⟩ □ b_{1}(s̄_{1}), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} \begin{matrix}m \\ P \end{matrix} ⟨true : σ⟩ □ B̄;

where the first reduction step is obtained by reducing the unit goal ⟨true : θ⟩ □ p(x̄) with respect to the clause C = p(s̄) ← ⟨ask_{0} : tell_{0}⟩ □ b_{1}(s̄_{1}), ..., b_{k}(s̄_{k}), where T ⊧B̄ ; θ∪{x̄=s̄} ask_{0} and H ⊧_{∅} θ ∪ {x̄ = s̄} ∪ tell_{0}.

By Observation A.1:

∀j = 1, ..., k : ⟨true : σ_{j −1}⟩ □ b_{j} (s̄_{j} ), ..., b_{k}(s̄_{k}) :: B̄ ⟶^{T} {mj \atop P}

⟨true : σ_{j} ⟩ □ b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄

where σ_{0} = θ ∪ {x̄ = s̄} ∪ tell_{0}, p(x̄)σ_{k} = p(x̄)σ and m_{j} ≤ m. Assume w.l.o.g. that for each j ∈ {1, ..., k}: x̄_{j} do not occur in C , ⟨true : θ⟩ □ p(x̄) | B̄, and {x̄_{1}, ..., x̄_{j −1}}, thus ∀j = 1, ..., k : ⟨true : σ′_{j −1} ∪ \{x̄_{j} = s̄_{j} \}⟩ □ b_{j} (x̄_{j} ), b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄ →^{T} {mj \atop P}

⟨true : σ′_{j} ⟩ □ b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄;

where σ′_{0} = σ_{0}, for each j ∈ {1, ..., k} : b_{j} (x̄_{j} )σ′_{j} = b_{j} (s̄_{j} )σ_{j} and p(x̄)σ′_{k} = p(x̄)σ_{k}. By the inductive hypothesis:

∀j = 1, ..., k, ∃[π_{j} ]_{∼} = [b_{j} (x̄_{j} ) ← η_{j} ]_{∼} ∈ T_{P}^{τ} ↑ ω, T ⊧_{σ′′_{j −1}∪{x̄j =s̄j }}^{ρj} π_{j}

where ρ_{j} = b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k}) :: B̄, σ′′_{j} = σ′′_{j −1} ∪ {x̄_{j} = s̄_{j} } ∪ tell(π_{j} ), σ′′_{0} = σ′_{0}, for each j = 1, ..., k : b_{j} (x̄_{j} )σ′′_{j} = b_{j} (x̄_{j} )σ′_{j} and p(x̄)σ′′_{k} = p(x̄)σ′_{k}. By T_{P}^{τ} definition: [π]_{∼} = [p(x̄) ← η̄]_{∼} ∈ T_{P}^{τ} ↑ ω where

η̄ = ⟨true : x̄ = s̄⟩ ← ⟨ask_{0}[B̄] : tell_{0}⟩ ← η̄_{1} ← ... ← η̄_{k},

and for each j ∈ {1, ..., k} : η̄_{j} = ⟨true : x̄_{j} = s̄_{j} ⟩ ← η_{j} [ρ_{j} ].

Since H ⊧_{∅} σ′′_{k} and σ′′_{k} = θ ∪ {x̄ = s̄} ∪ tell_{0}∪ ∪_{i=1}^{k} (tell(π_{i}) ∪ {x̄_{i} = s̄_{i}}) then

H ⊧_{θ} π.

Moreover since T ⊧B̄ ; θ∪{x̄=s̄} ask_{0} and for each j ∈ {1, ..., k} : T ⊧_{σ′′_{j −1}∪{x̄j =s̄j }}^{ρj} π_{j}

where σ′′_{0} = θ ∪ {x̄ = s̄} ∪ tell_{0}, then j ∈ {1, ..., k} : T ⊧B̄ ; σ′′_{j −1}∪{x̄j =s̄j } b_{j} (x̄_{j} ) ← η_{j} [b_{j +1}(s̄_{j +1}), ..., b_{k}(s̄_{k})].

By definition T ⊧B̄ ; θ π and if σ′′′ = tell(π) ∪ θ then p(x̄)σ′′′ = p(x̄)σ′′_{k} and then p(x̄)σ′′′ = p(x̄)σ.

The theorem follows by considering B̄ = Λ.

□

Proof of Theorem 4.4. The proof follows by Theorem 4.3 and Observation A.1. Let G = ⟨ask : σ_{0}⟩ □ p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}), then

σ ∈ O_{T} (P)(G); iff

T ⊧_{∅}^{Λ} ask and ⟨true : σ_{0}⟩ □ p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ⟩ □, where H ⊧_{∅} σ_{0}; iff

(by Observation A.1) T ⊧_{∅}^{Λ} ask and ∀j ∈ {1, ..., n}:

⟨true : σ_{j −1}⟩ □ p_{j} (t̄_{j} ), ..., p_{n}(t̄_{n}) ⟶^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ_{j} ⟩ □ p_{j +1}(t̄_{j +1}), ..., p_{n}(t̄_{n}), H ⊧_{∅} σ_{0}, and σ = σ_{n}; iff (by Observation A.3) T ⊧_{∅}^{Λ} ask and ∀j ∈ {1, ..., n} : assume x̄_{j} do not occur in G and in {x̄_{1}, ..., x̄_{j −1}}, then

⟨true : σ′_{j −1} ∪ \{x̄_{j} = t̄_{j} \}⟩ □ p_{j} (x̄_{j} ), p_{j +1}(t̄_{j +1})..., p_{n}(t̄_{n}) ⟶^{T} \begin{matrix}∗ \\ P \end{matrix}

⟨true : σ′_{j} ⟩ □ p_{j +1}(t̄_{j +1}), ..., p_{n}(t̄_{n}),

where σ′_{0} = σ_{0}, H ⊧_{∅} σ′_{0}, p_{j} (t̄_{j} )σ_{j} = p_{j} (x̄_{j} )σ′_{j} and (p_{1}(x̄_{1}), ..., p_{n}(x̄_{n}))σ′_{n} = (p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}))σ_{n}; iff

(by the same argument applied to prove (∗) in Theorem 4.3) T ⊧_{∅}^{Λ} ask and ∀j ∈ {1, ..., n}: ∃[π_{j} ]_{∼} = [p_{j} (x̄_{j} ) ← η_{j} ]_{∼} ∈ F(P), ⟨H, T ⟩ ⊧_{σ′′_{j −1}∪{x̄j =t̄j }}^{ρj} π_{j} where

ρ_{j} = p_{j +1}(t̄_{j +1}), ..., p_{n}(t̄_{n}),
σ′′_{0} = σ_{0}, σ′′_{j} = σ′′_{j −1} ∪ {x̄_{j} = t̄_{j} } ∪ tell(π_{j} ),

(p_{1}(x̄_{1}), ..., p_{n}(x̄_{n}))σ′′_{n} = (p_{1}(x̄_{1}), ..., p_{n}(x̄_{n}))σ′_{n} and vars(σ′′_{j}) ∩ vars(π_{j} ) = x̄_{j} .

We can assume w.l.o.g. that π_{j} are renamed apart from G and from each other; iff

σ′′_{n} ∈ ans_{F(P)}^{T}(G) and, since π_{j} are renamed apart from G and from each other, (p_{1}(x̄_{1}), ..., p_{n}(x̄_{n}))σ′′_{n} = (p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}))σ′′_{n}. Thus, Gσ′′_{n} = Gσ.

□

References

[1] 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.

[2] K. R. Apt and D. Pedreschi. Proving Termination of General Prolog Programs. In T. Ito and A.R. Meyer, editors, Proc. of Int. Conf. on Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 265–289. Springer-Verlag, Berlin, 1991.

[3] B. Arbab and D.M. Berry. Operational and Denotational Semantics of Prolog. Journal of Logic Programming, 4:309–330, 1987.

[4] F. Bancilhon, D. Maier, Y. Sagiv, and J.D. Ullman. Magic Sets and Other Strange Ways to Implement Logic Programs. In Proceedings of the ACM Symposium on Principles of Database Systems, pages 1–15, 1986.

[5] R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modelling Prolog Control. In Proc. Nineteenth Annual ACM Symp. on Principles of Programming Languages, pages 95–104. ACM Press, 1992.

[6] R. Barbuti, M. Codish, R. Giacobazzi, and M. Maher. Oracle Semantics for PROLOG. In H. Kirchner and G. Levi, editors, Algebraic and Logic Programming, Proceedings of the Third International Conference, volume 632 of Lecture Notes in Computer Science, pages 100–114. Springer-Verlag, Berlin, 1992.

[7] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semanticsbased Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 15, 1993.

[8] 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.

[9] A. Bossi, N. Cocco, and M. Fabris. Proving Termination of Logic Programs by Exploiting Term Properties. In S. Abramsky and T.S.E. Maibaum, editors, Proc. TAPSOFT’91, volume 494 of Lecture Notes in Computer Science, pages 153–180. Springer-Verlag, Berlin, 1991.

[10] M. Bruynooghe, G. Janssens, B. Demoen, and A. Callebaut. Abstract Interpretation: Towards the Global Optimization of Prolog Programs. In Proc. Fourth IEEE Int’l Symp. on Logic Programming, pages 192–204. IEEE Comp. Soc. Press, 1987.

[11] M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990. To appear in Theoretical Computer Science.

[12] J. Cohen. Constraint Logic Programming Languages. Communications of the ACM, 33:43–70, 1990.

[13] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238–252, 1977.

[14] 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.

[15] 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.

[16] S.K. Debray and N.W. Lin. Automatic Complexity Analysis of Logic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 599–613. The MIT Press, Cambridge, Mass., 1991.

[17] 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.

[18] M. Gabbrielli and G. Levi. Unfolding and fixpoint semantics of concurrent constraint programs. Theoretical Computer Science, 105:85–128, 1992.

[19] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, pages 111–119. ACM, 1987.

[20] N. D. Jones and A. Mycroft. Stepwise Development of Operational and Denotational Semantics for Prolog. In Sten-Åke Tärnlund, editor, Proc. Second Int’l Conf. on Logic Programming, pages 281–288, 1984.

[21] G. Levi. Models, Unfolding Rules and Fixpoint Semantics. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 1649–1665. The MIT Press, Cambridge, Mass., 1988.

[22] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[23] M. J. Maher. Logic semantics for a class of committed-choice programs. In J.-L. Lassez, editor, Proc. Fourth Int’l Conf. on Logic Programming, pages 858–876. The MIT Press, Cambridge, Mass., 1987.

[24] K. Marriott and H. Søndergaard. Bottom-up Abstract Interpretation of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 733–748. The MIT Press, Cambridge, Mass., 1988.

[25] K. Muthukumar and M. Hermenegildo. Determination of Variable Dependence Information through Abstract Interpretation. In E. Lusk and R. Overbeek, editors, Proc. North American Conf. on Logic Programming’89, pages 166–185. The MIT Press, Cambridge, Mass., 1989.

[26] L. Plümer. Termination Proofs for Logic Programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1990.

[27] V.A. Saraswat and M. Rinard. Concurrent constraint programming. In Proc. of the Seventeenth ACM Symposium on Principles of Programming Languages, pages 232–245. ACM, New York, 1990.

[28] T. Vasak and J. Potter. Characterization of Terminating Logic Programs. In Proc. Third IEEE Int’l Symp. on Logic Programming, pages 140–147. IEEE Comp. Soc. Press, 1986.

[29] K. Vershaetse and D. De Shreye. Deriving Termination Proofs for Logic Programs, Using Abstract Procedures. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 301–315. The MIT Press, Cambridge, Mass., 1991.