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)@dipisa.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.

In proceedings of ACM POPL'92.

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.

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. [9]). 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 [10] 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.[5, 10, 20]). 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.

∗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 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 [6], deterministic transition systems [12] or denotational semantics [17, 3, 13]. However, (semantics-based) analyses of Prolog are usually achieved by abstracting the more simple but less precise semantics of pure logic programs.

Unfortunately, it is not straightforward to encode Prolog control directly in terms of pure logic programs. Instead, we propose to model Prolog control 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 an instance of the cc class of concurrent constraint languages [22]. Constraints are used to specify that a clause may be chosen for reduction only if 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 [11] 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 termination can be provided either by applying techniques of abstract interpretation or by applying proof procedures. It is interesting to note that a precise model for termination provides a result which reflects the standard Prolog control; 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 presents briefly some preliminary definitions and notations. Section 3 introduces the τ language together with operational and declarative semantics. Section 4 describes how to model depth first control of Prolog using the τ language. Section 5 discusses the interpretation of the termination conditions. Section 6 describes related work and concludes.

Full proofs, not included due to space limitations, are present in the full version of this paper.

2 Preliminaries

In the following we assume familiarity with constraint logic programming (CLP) [16] and logic programming theory [1, 19].

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. The set of all 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). 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. Let H denote the standard Herbrand constraint system of equations on terms. 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 renamings. 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σ.

3 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 the basis for bottom-up abstract interpretations of Prolog programs.

A τ program consists of ask-tell constrained clauses as in the cc paradigm [22]. 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 [16].

• 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 .

3.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 3.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”.

Definition 3.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 3.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 3.1

Consider a store σ = {y = s(z)}, a resolvent Λ 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))σ ⊆ T , therefore ⟨H, T ⟩ ⊧_{σ}^{Λ} c.

3.2 Operational Semantics

An operational semantics for τ is given 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 (e.g. CLP(H) [16]). 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 3.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. [15]) in terms of the atomic goals of the form ⟨true : true⟩ □ p(x̄) which have successful computations as specified by the transitive closure of the transition relation (given a termination theory T ).

Definition 3.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(t̄)σ | ⟨true : true⟩ □ p(t̄) →^{T} \begin{matrix}∗ \\ P \end{matrix} ⟨true : σ⟩ □ \}.

The operational semantics of a τ program is defined in terms of the successful computations for (consistent) initial goals:

Definition 3.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} \}.

Example 3.2

Let T be a termination theory {t(g) | g ∈ A(Σ, Π_{P}, ∅)^{∗}}, Π_{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 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))), …}.

3.3 Declarative semantics

We now define a declarative semantics for τ programs which is open [8] with respect to the interpretation of ask constraints. It is defined in terms of unfoldings of clauses [18] 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 which we term constrained atoms.

Definition 3.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 3.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 3.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 3.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 η any sequence of constraints ⟨t_{i}(g_{i}) : tell_{i}⟩_{i=1}^{n} and by η[ρ] the sequence ⟨t_{i}(g_{i} :: ρ) : tell_{i}⟩_{i=1}^{n}.

Definition 3.9 (equiv. of constrained atoms) Let π_{1} and π_{2} be constrained atoms; π_{1} ∼ π_{2} iff for every termination theory T , store σ and resolvent ρ there is a renaming π′_{2} of π_{2} such that

⟨H, T ⟩ ⊧_{σ}^{ρ} π_{1} ⇔ ⟨H, 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 3.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 3.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 3.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} \} .

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

Definition 3.13 (Fixpoint semantics)

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

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

P_{1}^{τ}: p(x) ← 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}^{τ}) =

p(x) ← 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)⟩, …

F(P_{2}^{τ}) =

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⟩, …

In Example 3.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 4.3.

3.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 3.14 (composition)

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 , \\ t̄ ∈ T (Σ, Var)^{∗}, \\ T ⊧_{x̄=t̄}^{ρ} π, \\ σ = tell(π) ∪ \{x̄ = t̄\} \end{matrix} \} .

Proposition 3.2 (monotonicity of composition)

Let I be an interpretation. If T_{1} ⊆ T_{2} then for each resolvent ρ I [T_{1}](ρ) ⊆ I [T_{2}](ρ).

Example 3.6 Consider the programs P_{1}^{τ} and P_{2}^{τ} from Example 3.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 3.3 (soundness and completeness)

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

Proof. [(comment)]

The proof of (⊆) is by induction on the length of the refutation while the proof of (⊇) is by induction on the power of T_{P}^{τ}. Both apply the sequential (left-to-right) composition of the operational semantics:

for a goal ⟨true : σ_{0}⟩ □ B_{1}, …, B_{k}

⟨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}

to the induction hypothesis. □

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 3.15 (answers of an atomic goal)

Let I be an interpretation and let T be a termination theory. The set of answers for a goal

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

in I for T is defined by:

ans_{I}^{T} (G) =

\{ σ | \begin{matrix}for i = 1..n \\ p_{i}(s̄_{i}) ∈ I [T ](p_{i+1}(t̄_{i+1}), ..., p_{n}(t̄_{n})), \\ p_{1}(s̄_{1}), …, p_{n}(s̄_{n}), G are renamed apart, \\ σ = ∪_{i=1}^{n} \{s̄_{i} = t̄_{i}\} ∪ tell, H ⊧_{∅} σ \end{matrix} \}

Theorem 3.4 (strong equivalence)

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

4 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. The basic idea is demonstrated by an example:

Example 4.1

Consider the following Prolog program with the initial goal G = p(t̄), r(s̄):

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

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

The intended operational semantics can be described by:

1. The first clause is applied to p(t̄) if t̄ unifies with t̄_{1}. The success of G then depends on the success of the goal q(t̄_{2}), r(s̄), under the unification substitution.

2. The second clause is applied if (a) starting the computation of G with the first clause for p, it terminates (e.g. finitely fails or succeeds); and

(b) t̄ unifies with t̄_{3}.

The success of the goal then depends on the success of r(t̄_{4}), r(s̄) under the unification substitution.

This behaviour is naturally captured by the following τ program:

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

The ask term_{p}^{2}(p(x̄)) is intended to test if a Prolog goal can be resolved with the second clause for p. Namely, that the computation which applies the first clause to that goal terminates. In fact, the operational semantics of τ will test term_{p}^{2}(p(x̄) :: ρ) where ρ corresponds to the rest of the Prolog goal. The claim is that given the intended termination theory for term_{p}^{2} (i.e. the one which corresponds to the Prolog program) the operational semantics of the above τ program captures the intuitive meaning of the original Prolog program. This argument is justified below.

The following definitions specify the transformation from Prolog to τ and what we mean by the intended termination theory.

Definition 4.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 [19]. An SLD reduction is captured by:

Definition 4.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.

Definition 4.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 4.1 The intended termination theory for a Prolog program P is a termination theory (i.e. closed under instantiation).

Proof. [(comment)] The proof follows from properties of SLD trees. □

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 4.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 left-to-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 4.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 Prolog program P.

Definition 4.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 4.7 (Prolog success set)

S_{prolog} : Prolog → 2^{Atom}

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

Theorem 4.2 Let P be a Prolog program and P^{τ} the corresponding τ program. The Prolog success set S_{Prolog}(P) = F(P^{τ})[T_{Prolog}(P)](Λ).

Proof. [(comment)]

The proof argues the correspondence between the respective operational behaviours of P and of P^{τ} given the corresponding intended termination theory. The ask conditions for termination in a computation of P^{τ} correspond precisely to the conditions for a Prolog transition.

□

Note that:

Proposition 4.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.

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 4.2 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 non-ground 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 3.5; the success sets correspond to those given in Example 3.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).

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 4.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 3.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.

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

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

Figure 5 SLD-tree for G with P

Figure 5 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 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. Consider the following example:

Example 5.1

Let Π_{T_{≠}} = {≠} (i.e. “not unifiable”) and consider the following τ program R:

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

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

The declarative meaning of R is

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

If T_{≠} is the (downward closed) theory corresponding to “not-unifiable” and Σ = {0, s} then F(R)[T_{≠}](Λ) gives the set {t(0), t(s(0)), t(ss(0)), …} which corresponds to the intended termination theory for the Prolog program P_{2} in Example 3.5.

However, 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.

6 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, 7, 21, 23]) 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.

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. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

[2] K. R. Apt and D. Pedreschi. Proving Termination of General Prolog Programs. In Proc. of Int. Conf. on Theoretical Aspects of Computer Software, Sendai, Japan, 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, J. D, Ullman. Magic Sets and Other Strange Ways to Implement Logic Programs. Proccedings of the ACM Symposium on Principles of Database Systems, pages 1–15, Cambridge, Massachusetts, 1986.

[5] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. Technical Report TR 12/91, Dipartimento di Informatica, Università di Pisa, 1991. Submitted for publication.

[6] 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. Springer-Verlag, Berlin, 1990.

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

[8] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. Contributions to the Semantics of Open Logic Programs. Technical report, Dipartimento di Informatica, Università di Pisa, 1991.

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

[10] M. Codish, D. Dams, and E. Yardeni. Bottomup Abstract Interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990. Submitted for publication.

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

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

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

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

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

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

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

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

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

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

[21] L. Plümer. Termination Proofs for Logic Programs, volume 446 of Lecture Notes in Artificial Intelligence - subseries of LNCS. Springer-Verlag, Berlin, 1990. Ph.D. Thesis.

[22] V. A. Saraswat and M. Rinard. Concurrent constraint programming. In Proc. Seventeenth Annual ACM Symp. on Principles of Programming Languages. ACM, 1990.

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