A Declarative Semantics for the Prolog Cut Operator

Karl Stroetmann^{⋆} and Thomas Glaß

Siemens AG, Corporate Research and Development, D–81730 München, Germany

Abstract. In practice, a large part of most Prolog programs is in fact functional, the search facilities of Prolog are only rarely needed. In order to arrive at efficient implementations it is then convenient to make use of the cut operator provided by Prolog. Up to now, this operator has been regarded as an extra–logical control operator that destroys the declarative semantics of Prolog. In this paper we will show that this is not true. If the cut is used to implement functional predicates and if, furthermore, a certain discipline in its use is adhered to, then programs using the cut operator do possess a declarative semantics.

1 Introduction

It has been observed by others that in practice the main differences between programs written using the paradigm of functional programming and programs written using the paradigm of logic programming is often mainly syntactical. The reason is that a large number of predicates implemented in logic programming are but codings of the graph of a function. However, while an implementation of a function in a functional programming language has a declarative semantics, this is usually not the case for the implementation of a function in Prolog. This is due to the fact that in order to arrive at an efficient implementation it is convenient to make use of the cut operator. In general, the operational semantics of this operator is quite complicated, cf. [PS95, And95]. Nevertheless, if the use of the cut operator satisfies certain restrictions, then it is possible to give a simple declarative semantics to programs using the cut.

The basic idea can best be understood in the propositional case. If

p ← l_{1} ∧ ⋯ ∧ l_{m} ∧! ∧ h_{1} ∧ ⋯ ∧ h_{n} (1) is a propositional Prolog clause, i.e. p is a null–ary relation symbol and l_{i} and h_{j} are propositional literals, that is null–ary relation symbols or negated null– ary relation symbols, then the declarative semantics of this clause is given by the formula

l_{1} ∧ ⋯ ∧ l_{m} → (p ↔ h_{1} ∧ ⋯ ∧ h_{n}). (2) The intuitive reason that (2) correctly represents (1) is that

– provided the clause (1) is selected to resolve a goal of the form p, and

⋆ Address correspondence to Karl.Stroetmann@zfe.siemens.de.

– the resolution of its conditional part l_{1} ∧ ⋯ ∧ l_{m} is successful,

then p is recognized as true if and only if the resolution of h_{1} ∧ ⋯ ∧ h_{n} is successful.

Since this declarative semantics does not reflect the ordering of clauses it is only correct if the operational semantics of the program under consideration is invariant under arbitrary reordering of its clauses. Another condition that has to be satisfied for our semantics to be correct is that the definitions of predicates are complete. In the propositional case this means that there must exist a clause in the definition of p such that the resolution of the conditional part of this clause is successful. The notion of completeness will be defined formally after we have made the operational semantics precise.

1.1 Comparison with Other Work

The cut operator has long been recognized as a problematic feature of Prolog, cf. the book of Lloyd [Llo87]. Previous work was mainly concerned with the formalization of the operational semantics and the development of a denotational semantics cf., among others, the works of Jones and Mycroft [JM84] and de Bruin and de Vink [dBdV89]. Another approach was followed by Börger who used the notion of dynamic algebras to give a mathematical description of the control facilities of Prolog [Bör89].

To our knowledge, the only attempts to give a declarative semantics to the cut operator were the works by Voda [Vod88] and Andrews [And95]. Both works clearly show that, in the general case, the formulas describing a program using the cut operator are very complicated. This is reflected in the fact that in the declarative semantics given by Andrews the resulting formulas are not even computable!

We can do much better because we do not cover the general case. In order to still have a theory that is applicable to real programs we have strived to define a subclass of full Prolog satisfying the following requirements:

– The subclass should be large enough to cover the programming style used in practice.

– The resulting declarative semantics should be simple.

Concerning the first requirement we have identified a functional programming style as the main source of the use of cuts. After all, when coding functions the resulting predicates have to be deterministic and that can most easily by achieved through the use of cuts. Fortunately, it is this functional programming style that has a simple declarative semantics! As a matter of fact, the declarative semantics is not only simple from a conceptual point of view but, furthermore, offers the possibility of applying formal methods to the process of validation. Since this process can be automated to a large extend it makes the application of formal methods economically viable. We will discuss this in more detail in the last section of this paper.

Overview: In the next section we will introduce the necessary notions and notations used in the rest of this paper. In particular, we introduce modes and types. These are necessary prerequisites for introducing our version of an operational semantics for Prolog. This operational semantics will be introduced in Section 3. In Section 4 we give the declarative semantics of Prolog clauses containing the cut operator and, furthermore, prove this semantics to be consistent by constructing a model. In Section 5, this semantics is then shown to be sound and complete with respect to the operational semantics introduced previously. Finally, Section 6 discusses applications of this semantics.

2 Preliminaries

All notions and notations not defined in this paper are assumed to be the same as in Apt [Apt90]. We will only deviate in a small number of points from [Apt90], the most important being that we use modes and types which will be defined below. Another deviation is the fact that we do not use goals but rather find it more convenient to work with queries. A query is taken to be a conjunction of literals. The letters B, C, and G, possibly indexed, will range over queries. Furthermore, we will use the following meta rule for denoting sequences of items: If the items from a class are denoted by a fixed group of letters, then sequences of these items will be denoted by the same letters in boldface. For example, since s and t denote terms, s and t will be used to denote sequences of terms.

2.1 Modes and Types

As already noted by others, compare e. g. [Apt93], in order to develop a declarative semantics that is applicable to the programming style used in the practice of Prolog programming, one has to introduce the concept of modes [DM85] and types [MO84]. We find it convenient to use the notion of a well–typed program as given in Apt and Etalle [AE93], which is based on [BLR92].

We start with the notion of a mode used to define input and output positions of a relation.

Definition 1 (mode) A mode for an n–ary relation symbol p is a function m_{p} from the set {1, ⋯, n} to the set {+, −}. If m_{p}(i) = “+”, we call i an input position of p and if m_{p}(i) = “−”, we call i an output position of p. A moding is a collection of modes, each for a different relation symbol. □

We proceed to define types. Since we do not intend to present a new type system here, the only assumption we make is that a type is a set of ground Prolog terms. The set of all types will be denoted by 𝔗. Individual types will be written as σ and τ.

Definition 2 (type) A type for an n–ary relation symbol p is a function t_{p} from the set {1, ⋯, n} to the set 𝔗. If t_{p}(i) = τ, we call τ the type associated with the position i of p. A typing is a collection of types, each for a different relation symbol. □

The mode and the type of a relation are the components of the signature of the relation.

Definition 3 (signature) A signature for an n–ary relation symbol p is a function s_{p} from the set {1, ⋯, n} to the set {+, −} × 𝔗 such that s_{p}(i) is the pair ⟨m_{p}(i), t_{p}(i)⟩, where m_{p} and t_{p} are the mode and the type of the relation p. Instead of the clumsy ⟨m_{p}(i), t_{p}(i)⟩ we will write s_{p}(i) as the string m_{p}(i)t_{p}(i). A signature for a Prolog program ℙ is a collection of signatures for the relation symbols of ℙ. □

If p is an n–ary relation with mode m_{p} and type t_{p}, the signature of p will be written as

p( m_{p}(1) t_{p}(1), ⋯, m_{p}(n) t_{p}(n) ). For example, the signature of the predicate sort/2 that takes a list of integers as first argument and produces a sorted version of this list in its second argument is written as

      sort( + int*, - int* ).

Here int* denotes the type of all lists of integers.

To be able to define the concept of a well–typed program we need the notion of a typed term. This is a construct of the form s:σ where s is a term and σ is a type. Given a sequence s_{1} : σ_{1}, ⋯, s_{n}: σ_{n} of typed terms we write s ∈ σ where s abbreviates the sequence s_{1}, ⋯, s_{n} and σ abbreviates the sequence σ_{1}, ⋯, σ_{n} iff for all i = 1, ⋯, n we have s_{i} ∈ σ_{i}. A type judgment is a statement of the form s:σ ⇒ t:τ. It is considered to be true (notation ⊧ s:σ ⇒ t:τ) iff for all substitutions ϑ, sϑ ∈ σ implies tϑ ∈ τ.

In the definitions below we will write l to denote either a predicate symbol p or a negated predicate symbol ¬p. We will assume that if a relation p is used negatively, i.e. as ¬p(s), then p has only input positions, i.e. its signature has the form p(+σ_{1}, ⋯, +σ_{m}). For notational convenience we make the following agreement: If an atom is written as p(s, t), then the terms s are at input positions while the terms t are at output positions, i.e. without loss of generality we make the assumption that the input positions always precede the output positions.

Definition 4 (well–signed) In the following, assume that for i = 1, ⋯, n the signature of the relation symbol p_{i} is given by p_{i}( +σ_{i}, −τ_{i} ) while the signature of p_{0} is p_{0}( +τ_{0}, −σ_{n+1} ).

– A clause p_{0}(t_{0}, s_{n+1}) ← l_{1}(s_{1}, t_{1}) ∧ ⋯ ∧ l_{n}(s_{n}, t_{n}) is well–signed iff for all i ∈ {1, ⋯, n + 1} the following conditions are satisfied :

1. var(s_{i}) ⊆ ⋃_{j=0}^{i−1} var(t_{j}).

2. ⊧ t_{0} :τ_{0}, ⋯, t_{i−1} :τ_{i−1} ⇒ s_{i}:σ_{i}.

– A query l_{1}(s_{1}, t_{1}) ∧ ⋯ ∧ l_{n}(s_{n}, t_{n}) is well–signed iff the clause

true ← l_{1}(s_{1}, t_{1}) ∧ ⋯ ∧ l_{n}(s_{n}, t_{n}) is well–signed.

– Finally, a program is called well–signed iff every clause of it is. □

We need one further definition.

Definition 5 (functional) A clause is called functional iff its body contains exactly one occurrence of the cut operator !, i.e. a clause is functional if it has the form

P ← B_{1} ∧! ∧ B_{2}

where B_{1} and B_{2} are queries such that the cut operator ! does not occur in them.

A predicate p is functional iff every clause of its definition is functional. □

Important: In the following we will only be interested in the functional part of a program, i.e. in that part that defines the functional predicates. Our experience has shown that this part makes up the bulk of most programs. In the following, we will use the letter ℙ to always denote a functional program, i.e. a program consisting solely of functional predicates.

3 An Operational Semantics for Prolog

In this section we give a simple operational semantics for Prolog that captures the meaning of the cut operator. In order to prevent this semantics from getting to complicated, it will neither reflect the depth first search strategy nor the selection of clauses in Prolog. It will, however, reflect the left first selection rule of Prolog. Therefore, this semantics is only applicable for programs that are universally terminating, complete, and confluent. These notions will be defined formally after we have defined the auxiliary relation →_{ℙ}.

Informally, a program is universally terminating iff even after arbitrary reordering of the clauses there are no infinite computations.

We will define the notion of completeness in a way that failure is always explicit failure, i.e. if a well–signed query of the form p(s, t) fails, then this is due to the fact that a clause

p(l, r) ← B_{1} ∧! ∧ B_{2} has been selected such that μ = mgu(s, l) exists, the Prolog resolution of B_{1}μ has succeeded with answer ϑ, but the Prolog resolution of the query

B_{2}μϑ ∧ tμϑ = rμϑ has failed. Therefore, explicit failure is always due to the fact that during the Prolog resolution of a query a cut–fail combination has been encountered.

The notion of confluence will be defined so that it is ensured that an arbitrary reordering of the clauses of a program does not change its operational semantics.

To start with we define the notion of a frame. A frame is a pair ⟨G, ϑ⟩ where G is a query and ϑ is a substitution. A frame ⟨G, ϑ⟩ is called well–signed iff the query Gϑ is well–signed.

Given a program ℙ, we proceed to define a rewrite relation →_{ℙ} on well–signed frames as follows:

1. Assume that ⟨p(s, t), ϑ⟩ is a frame where the relation symbol p is different

from the equality symbol =. Then, if ℙ contains a (suitably renamed) clause

p(l, r) ← B_{1} ∧! ∧ B_{2} such that

⟨l = sϑ ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨true, η⟩ holds, then we have

⟨p(s, t), ϑ⟩ →_{ℙ} ⟨B_{2}η ∧ t = rη, ϑ⟩. Here, id denotes the identity substitution and t = rη is short for the formula t_{1} = r_{1}η ∧ ⋯ ∧ t_{n} = r_{n}η, where the assumption is made that r = r_{1}, ⋯, r_{n} and t = t_{1}, ⋯, t_{n}. Of course, a similar remark holds for l = sϑ.

2. If sϑ and tϑ are unifiable with most general unifier μ such that μ is idempo-

tent and relevant in the sense of Lassez and Maher [LM87], then

⟨s = t, ϑ⟩ →_{ℙ} ⟨true, ϑμ⟩.

3. If sϑ and tϑ are not unifiable, then ⟨s = t, ϑ⟩ →_{ℙ} ⟨false, ϑ⟩.

4. If ⟨Q, ϑ⟩ →_{ℙ}^{∗} ⟨false, ϑη⟩, then ⟨¬Q, ϑ⟩ →_{ℙ} ⟨true, ϑ⟩.

5. If ⟨Q, ϑ⟩ →_{ℙ}^{∗} ⟨true, ϑη⟩, then ⟨¬Q, ϑ⟩ →_{ℙ} ⟨false, ϑ⟩.

6. We have ⟨true ∧ G, ϑ⟩ →_{ℙ} ⟨G, ϑ⟩.

7. We have ⟨false ∧ G, ϑ⟩ →_{ℙ} ⟨false, ϑ⟩.

8. If L is a literal and ⟨L, ϑ⟩ →_{ℙ}^{∗} ⟨G_{1}, ϑη⟩ where G_{1} ∈ {true, false}, then ⟨L ∧ G_{2}, ϑ⟩ →_{ℙ} ⟨G_{1} ∧ G_{2}, ϑη⟩.

For the following we need the fact that well–signedness is an invariant of the relation →_{ℙ}, i.e. if the frame F_{1} is well–signed and F_{1} →_{ℙ} F_{2}, then F_{2} is well– signed,^{2} too. This fact can be proven in the same way as the persistence of well–

2 The attentive reader might have noticed that in order for this statement to make sense, the equality predicate =/2 has to be equipped with a signature. This can be done by defining the signature of =/2 as

'='( -T, +T )

where T is a type parameter. This is correct since for every frame of the form ⟨s = t, ϑ⟩ that is encountered, tϑ is a ground term.

typedness under Prolog resolution in [BLR92]. Furthermore, we can prove that if ⟨G_{1}, ϑ_{1}⟩ is well–signed, then ⟨G_{1}, ϑ_{1}⟩ →_{ℙ} ⟨true, ϑ_{1}ϑ_{2}⟩ implies that ϑ_{2} has the form {x_{1}/s_{1}, ⋯, x_{n}/s_{n}} where s_{i} is ground for i = 1, ⋯, n and var(Gϑ_{1}) ⊆ {x_{1}, ⋯, x_{n}}. Therefore, if ⟨G_{1}, ϑ_{1}⟩ →_{ℙ} ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ holds, then the substitution ϑ_{2} is ground.

We proceed to make the notion of universal termination precise. We call a program ℙ universally terminating iff there are no infinite sequences

⟨G_{1}, ϑ_{1}⟩ →_{ℙ} ⟨G_{2}, ϑ_{2}⟩ →_{ℙ} ⋯ →_{ℙ} ⟨G_{n}, ϑ_{n}⟩ →_{ℙ} ⟨G_{n+1}, ϑ_{n+1}⟩ →_{ℙ} ⋯ starting with a well–signed frame ⟨G_{1}, ϑ_{1}⟩. The fact that a given program ℙ is universally terminating implies that every well–signed query has a normal form. Here a frame F is in normal form iff there is no frame F_{1} such that F →_{ℙ} F_{1} holds. A frame F̂ is a normal form of a frame F iff F̂ is in normal form and, furthermore, F →_{ℙ}^{∗} F̂.

We call the program ℙ confluent iff the rewrite relation does not fork, i.e. if

⟨G, ϑ⟩ →_{ℙ} ⟨G_{1}, ϑ_{1}⟩ and ⟨G, ϑ⟩ →_{ℙ} ⟨G_{2}, ϑ_{2}⟩ is only possible if G_{1} = G_{2} and ϑ_{1} = ϑ_{2}. Since there are no clauses defining true or false this is equivalent to the fact that for a given well–signed atom p(s, t) there exists at most one clause p(l, r) ← B_{1} ∧! ∧ B_{2} such that

⟨l = s ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨true, η⟩ holds for a suitable substitution η.

If a program ℙ is confluent, then normal forms are unique. Therefore, in this case we are allowed to speak of the normal form of a frame. Furthermore, the confluence of a program ensures that an arbitrary reordering of its clauses does not change its operational semantics: After all, although there might be different clauses that can be selected to resolve a given atom, there is at most one clause such that the control will reach the cut operator of this clause. Thus, in the case of confluent programs, reordering the clauses is merely a matter of efficiency.

Finally, a program ℙ is called complete iff for every well–signed atom of the form p(s, t) there exists a clause p(l, r) ← B_{1} ∧! ∧ B_{2} such that

⟨l = s ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨true, η⟩ holds for a suitable substitution η.

If a program ℙ is complete, then it is easy to see that the normal form of a well–signed frame F has either the form ⟨true, ϑ⟩ or ⟨false, ϑ⟩ for a suitable substitution ϑ. We define a function nf(F) that returns true in the first case and false in the second, i.e.

nf(F) = \{ \begin{matrix}true & if F →_{ℙ}^{∗} ⟨true, ⟩; \\ false & otherwise. \end{matrix}

For the rest of this paper we make the assumption that all programs are universally terminating, complete, and confluent. It is not too hard to see that the computed answer of a well–signed query G can be computed by computing the normal form of the frame ⟨G, id⟩. If this normal form is ⟨true, ϑ⟩, then the computed answer is ϑ|_{var(G)}, where ϑ|_{var(G)} denotes the restriction of the substitution ϑ to the variables of G. If the normal form is ⟨false, ϑ⟩, then the Prolog resolution of G fails.

In order to show the declarative semantics defined later to be consistent, we need a Lifting Lemma for the relation →_{ℙ}^{∗}. To formulate this lemma we introduce the notion of a substitution being more general than another substitution. Formally we define ϑ to be more general than φ iff there exists a substitution η such that ϑη = φ. If ϑ is more general than φ, then this is written as φ ≤ ϑ.

Lemma 6 (Lifting Lemma) Assume that the frames ⟨B_{1}, σ_{1}⟩ and ⟨B_{1}, ϑ_{1}⟩ are well–signed and that, furthermore, the following holds:

1. ⟨B_{1}, σ_{1}⟩ →_{ℙ}^{∗} ⟨B_{2}, σ_{1}σ_{2}⟩.

2. σ_{1} ≤ ϑ_{1}, i.e. ϑ_{1} is more general than σ_{1}.

Then there exists a substitution ϑ_{2} such that the following holds:

1. ⟨B_{1}, ϑ_{1}⟩ →_{ℙ}^{∗} ⟨B_{2}, ϑ_{1}ϑ_{2}⟩.

2. σ_{1}σ_{2}|_{var(B_{1})} ≤ ϑ_{1}ϑ_{2}|_{var(B_{2})}.

A proof of this lemma can be given by a straightforward induction along the definition of the relation →_{ℙ}.

4 A Declarative Semantics for Functional Programs

In this section we define the declarative semantics for functional programs that are well-signed.

Assume a clause of the form

p(s, t) ← B_{1} ∧! ∧ B_{2} is given. In order to give the declarative semantics of this clause we introduce a sequence of new variables y that has the same length as the sequence t. Furthermore, assume that z is the tuple of all those variables that occur in t or in B_{2}, but do not occur in s nor in B_{1}, i.e.

{z} = (var(t) ∪ var(B_{2}))\(var(s) ∪ var(B_{1})). Then the declarative semantics of the clause given above is defined to be the formula

B_{1} → (p(s, y) ↔ ∃z.B_{2} ∧ t = y).

Of course, t = y is short for t_{1} = y_{1} ∧ ⋯ ∧ t_{n} = y_{n}. The declarative semantics of a program ℙ is then defined to be the collection of the declarative semantics of all of its clauses together with the axioms of CET (Clark’s equational theory) [Cla78]. It will be denoted as decl(ℙ).

Note that if the declarative semantics decl(ℙ) of a program ℙ is defined in this way then the semantics is local in the sense that every single clause is translated into a single formula. This is in contrast to the completion semantics comp(ℙ) since there a definition, i.e. the set of all clauses defining a predicate, is translated into a formula. Therefore the completion semantics is considerably more complex than our semantics. Another important difference between our approach and the completion semantics is the fact that we interpret decl(ℙ) as a set of typed formulas, whereas comp(ℙ) is regarded as a set of plain, i.e. untyped, first order formulas.

To proceed, we consider the predicate remove/3 as an example. The call remove( L, X, S ) removes the first occurrence of X in the list L. The result is the list S. The predicate fails if X is not a member of L. The signature and implementation of this predicate are given as follows:

  %# signature: remove( +list(T), +T, -list(T) ).
  remove( [ X | Xs ], Y, Xs ) :-
          X = Y,
          !.
  remove( [ X | Xs ], Y, [ X | Rs ] ) :-
          not X = Y,
          !,
          remove( Xs, Y, Rs ).
  remove( [], Y, Rs ) :-
          !,
          fail.

Note that the last clause is necessary in order for the implementation to be complete in the sense defined in the last section. The declarative semantics of these clauses is given by the following formulas:

X = Y → (remove([X|Xs], Y, Zs) ↔ true ∧ Xs = Zs).

X ≠ Y → (remove([X|Xs], Y, Zs) ↔ ∃Rs.remove(Xs, Y, Rs) ∧ [X|Rs] = Zs).

true → (remove([], Y, Zs) ↔ ∃Rs.false ∧ Rs = Zs). It should be obvious that these formulas are much more handy than the corresponding formulas resulting from the completion semantics.

4.1 Constructing a Model of decl(𝔓)

As yet, we have not shown the declarative semantics to be consistent. We will do this now by constructing a model 𝔓 of decl(ℙ). 𝔓 will be defined as a Herbrand interpretation [Apt90], i.e. the domain of 𝔓 is the set of all well–typed ground terms and the interpretation f_{𝔓} of an n–ary function symbol f is defined via

f_{𝔓}(t_{1}, ⋯, t_{n}) = f(t_{1}, ⋯, t_{n}). Furthermore, if p is an n–ary predicate symbol, then this predicate symbol is interpreted as the set of tuples of ground terms t_{1}, ⋯, t_{n} such that

⟨p(t_{1}, ⋯, t_{n}), id⟩ →_{ℙ}^{∗} ⟨true, ⟩, i.e. we define

p_{𝔓} = {⟨t_{1}, ⋯, t_{n}⟩ : nf(⟨p(t_{1}, ⋯, t_{n}), id⟩) = true}. The fact that decl(ℙ) is consistent follows from the following theorem.

Theorem 7 If ℙ is universally terminating, confluent, and complete, then 𝔓 ⊧ decl(ℙ).

Proof (sketch): It follows from [Cla78] that 𝔓 is a model of CET. Furthermore, we have to show that

𝔓 ⊧ B_{1} → (p(l, y) ↔ ∃z.B_{2} ∧ y = r) (1) holds for all clauses p(l, r) ← B_{1}∧!∧B_{2} in ℙ, where z is the tuple of variables that are local to r and B_{2}. In order to show (1) we assume that a ground substitution σ is given such that

(a) (B_{1} → (p(l, y) ↔ ∃z.B_{2}∧y = r))σ is a formula containing no free variables, and

(b) 𝔓 ⊧ B_{1}σ

holds true. Now from 𝔓 ⊧ B_{1}σ and the definition of 𝔓 it follows that

nf(⟨B_{1}σ, id⟩) = true. Since B_{1}σ is ground this implies

⟨B_{1}, σ⟩ →_{ℙ}^{∗} ⟨true, τ⟩, (2) where τ ≤ σ and τ|_{var(B_{1})} = σ|_{var(B_{1})}. To proceed, we show that

⟨l = lσ ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨true, ϱ⟩ (3) for a suitable substitution ϱ. The definition of →_{ℙ} shows

⟨l = lσ ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨B_{1}, μ⟩ with μ = mgu(l, lσ). (4) Obviously, σ ≤ μ. Therefore (2) and the Lifting Lemma show that there is a substitution ϱ such that σ|_{var(B_{1})} ≤ ϱ|_{var(B_{1})} and

⟨B_{1}, μ⟩ →_{ℙ}^{∗} ⟨true, ϱ⟩, (5)

(4) and (5) yield (3). Using (3) it follows that ⟨p(lσ, yσ), id⟩ →_{ℙ} ⟨B_{2}ϱ ∧ yσ = rϱ, id⟩

Therefore, we have

nf(⟨p(lσ, yσ), id⟩) = nf(⟨B_{2}ϱ ∧ yσ = rϱ, id⟩). (6) There are two cases.

1. Case: nf(⟨p(lσ, yσ), id⟩) = true.

In this case there is a substitution γ such that ⟨B_{2}ϱ ∧ yσ = rϱ, id⟩ →_{ℙ}^{∗} ⟨true, γ⟩.

Then it is easy to see that

nf(⟨B_{2}ϱγ ∧ yσ = rϱγ, id⟩) = true. The definition of 𝔓 shows therefore that (1) is valid.

2. Case: nf(⟨p(lσ, yσ), id⟩) = false.

We have to show

𝔓 |̸= ∃z.B_{2}σ ∧ yσ = rσ. Let us assume the contrary. Then there is a substitution η such that

nf(⟨B_{2}ση ∧ yσ = rση, id⟩) = true

The Lifting Lemma shows then

nf(⟨B_{2}ϱ ∧ yσ = rϱ, id⟩) = true which, because of our assumption for this case, contradicts (6). □

5 Soundness and Completeness

In this section we show the semantics decl(ℙ) to be correct and complete for programs that are universally terminating, confluent, and complete.

In the following we need to be able to interpret substitutions as formulas. If ϑ = {x_{1}/t_{1}, ⋯, x_{n}/s_{n}} is a substitution, then ϑ is interpreted as the formula x_{1} = t_{1} ∧ ⋯ ∧ x_{n} = t_{n}. The identity substitution id is interpreted as true.

The key lemma is the following:

Lemma 8 Assume ⟨G_{1}, ϑ_{1}⟩ is a well–signed frame. Then, if

⟨G_{1}, ϑ_{1}⟩ →_{ℙ} ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ holds, then the following equivalence is valid:

decl(ℙ) ⊧ G_{1}ϑ_{1} ↔ ∃z.G_{2}ϑ_{1}ϑ_{2} ∧ ϑ_{2}, where z is the tuple of all those variables occurring in the formula G_{2}ϑ_{1}ϑ_{2} ∧ ϑ_{2} but not in G_{1}ϑ_{1}, i.e.

{z} = var(G_{2}ϑ_{1}ϑ_{2} ∧ ϑ_{2})\var(G_{1}ϑ_{1}).

Proof: The claim is shown by induction following the definition of the rewrite relation →_{ℙ}. There are eight cases.

1. ⟨G_{1}, ϑ_{1}⟩ = ⟨p(s, t), ϑ⟩, ℙ contains a clause p(l, r) ← B_{1} ∧! ∧ B_{2}, we have

⟨l = sϑ ∧ B_{1}, id⟩ →_{ℙ}^{∗} ⟨true, η⟩, (1) and therefore we have

⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨B_{2}η ∧ t = rη, ϑ⟩, i.e. ϑ_{1} = ϑ and ϑ_{2} = id. By induction hypothesis (and a trivial side induction along the definition of the transitive closure →_{ℙ}^{∗} of →_{ℙ}), (1) yields

decl(ℙ) ⊧ l = sϑ ∧ B_{1} ↔ ∃u.true ∧ η, where {u} = var(η)\var(l = sϑ ∧ B_{1}). We instantiate this formula with η and use the fact that, since η is ground, we have ⊧ ηη ↔ true. ^{3} Since sϑ is ground we get

decl(ℙ) ⊧ lη = sϑ ∧ B_{1}η. (2)

3 Remember that, if η is the substitution {x_{1}/s_{1}, ⋯, x_{n}/s_{n}}, then the first occurrence of η in the expression ηη is interpreted as the formula x_{1} = s_{1} ∧· · · · · · x_{n} = s_{n}, while the second η is interpreted as the substitution applied to this formula. Since η is ground we have s_{i}η = s_{i} for all i = 1, ⋯, n. Furthermore, by the definition of η we have x_{i}η = s_{i} Therefore ηη is the formula s_{1} = s_{1} ∧ ⋯ ∧ s_{n} = s_{n}.

Furthermore, decl(ℙ) contains the formula

B_{1} → (p(l, y) ↔ ∃v.B_{2} ∧ r = y), where {v} = var(B_{2} ∧ r = y)\var(B_{1} → p(l, y)). Instantiating this formula with η and using the fact that y is a tuple of variables not occurring elsewhere we get

decl(ℙ) ⊧ B_{1}η → (p(lη, y) ↔ ∃v.B_{2}η ∧ rη = y).

Because of (2) this shows

decl(ℙ) ⊧ p(sϑ, y) ↔ ∃v.B_{2}η ∧ rη = y. Instantiating y with tϑ we see

decl(ℙ) ⊧ p(s, t)ϑ ↔ ∃v.B_{2}η ∧ rη = tϑ. However, this is the claim that had to be proved.

2. ⟨G_{1}, ϑ_{1}⟩ = ⟨s = t, ϑ⟩, μ = mgu(sϑ, tϑ) is a most general unifier of sϑ and tϑ that is both idempotent and relevant, and ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨true, ϑμ⟩. We have to show

decl(ℙ) ⊧ sϑ = tϑ ↔ true ∧ μ. However, this is an easy consequence of Clark’s equational theory [Cla78].

3. ⟨G_{1}, ϑ_{1}⟩ = ⟨s = t, ϑ⟩, the terms sϑ and tϑ are not unifiable, and, furthermore,

we have ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨false, ϑ⟩. We then have to show

decl(ℙ) ⊧ sϑ = tϑ ↔ false. Again, this is an easy consequence of Clark’s equational theory.

4. ⟨G_{1}, ϑ_{1}⟩ = ⟨not Q, ϑ⟩, we have ⟨Q, ϑ⟩ →_{ℙ}^{∗} ⟨false, ϑη⟩, and, furthermore,

⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨true, ϑ⟩. The induction hypothesis yields then

decl(ℙ) ⊧ Qϑ ↔ ∃v.false ∧ η, for a suitable v. This is equivalent to

decl(ℙ) ⊧ ¬Qϑ ↔ true. and this is the claim that had to be proved.

5. ⟨G_{1}, ϑ_{1}⟩ = ⟨not Q, ϑ⟩, we have ⟨Q, ϑ⟩ →_{ℙ}^{∗} ⟨true, ϑη⟩, and, furthermore,

⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨false, ϑ⟩. The induction hypothesis yields

decl(ℙ) ⊧ Qϑ ↔ ∃v.true ∧ η for a suitable v. Instantiating this formula with η and using the fact that, due to the well–signedness of the query not Qϑ, we must have Qϑη = Qϑ, we can conclude

decl(ℙ) ⊧ Qϑ. This is the same as

decl(ℙ) ⊧ ¬Qϑ ↔ false, which is the claim that had to be proved.

6. ⟨G_{1}, ϑ_{1}⟩ = ⟨true ∧ G, ϑ⟩ and ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨G, ϑ⟩.

In this case the claim is trivial.

7. ⟨G_{1}, ϑ_{1}⟩ = ⟨false ∧ G, ϑ⟩ and ⟨G_{2}, ϑ_{1}ϑ_{2}⟩ = ⟨false, ϑ⟩.

In this case the claim is trivial.

8. ⟨G_{1}, ϑ_{1}⟩ = ⟨L ∧ B_{2}, ϑ⟩, where L is a literal such that

⟨L, ϑ⟩ →_{ℙ}^{∗} ⟨B_{1}, ϑη⟩. (3) Since ⟨G_{2}, ϑ_{2}⟩ = ⟨B_{1} ∧ B_{2}, ϑη⟩ we have to show

decl(ℙ) ⊧ (L ∧ B_{2})ϑ ↔ ∃v.(B_{1} ∧ B_{2})ϑη ∧ η, (4) where {v} = var((B_{1} ∧ B_{2})ϑη ∧ η)\var((L ∧ B_{2})ϑ). Because of (3) the induction hypothesis yields

decl(ℙ) ⊧ Lϑ ↔ ∃u.B_{1}ϑη ∧ η, (5) where {u} = var(B_{1}ϑη∧η)\var(Lϑ). It can be shown that u = v. Therefore,

(4) is a consequence of (5) and the fact that for arbitrary formulas A and substitutions φ

⊧ φ → (A ↔ Aφ) is valid. _{□}

The soundness and completeness of Prolog resolution are simple consequences of lemma 8.

Theorem 9 (Soundness) Assume that ℙ is a program that is universally terminating, complete, confluent, and well–signed, and G is a well–signed query. Then we have the following:

1. If ϑ is a computed answer for G, then decl(ℙ) ⊧ Gϑ.

2. If the Prolog resolution of G fails, then decl(ℙ) ⊧ ¬G.

Proof: We prove both claims separately.

1. Since ϑ is a computed answer for G we must have

⟨G, id⟩ →_{ℙ}^{∗} ⟨true, ϑ⟩. Repeated application of Lemma 8 shows

decl(ℙ) ⊧ G ↔ ∃v.true ∧ ϑ, where {v} = var(ϑ)\var(G). From this the claim follows by instantiating with ϑ and using the fact that, since ϑ is ground, we have ⊧ ϑϑ.

2. In this case we have

⟨G, id⟩ →_{ℙ}^{∗} ⟨false, η⟩ for a suitable substitution η. This time Lemma 8 shows

decl(ℙ) ⊧ G ↔ ∃v.false ∧ η, where {v} = var(η)\var(G). From this the claim is immediate. □

Theorem 10 (Completeness) Assume that ℙ is a program that is universally terminating, complete, confluent, and well–signed, and G is a well–signed query. Then we have the following:

1. If decl(ℙ) ⊧ Gφ and Gφ is ground, then φ|_{var(G)} is a computed answer for G.

2. If decl(ℙ) ⊧ ¬G, then the Prolog resolution of G fails.

Proof: We prove both claims separately.

1. The normal form of ⟨G, id⟩ is either of the form ⟨false, η⟩ or ⟨true, ϑ⟩. In the first case Lemma 8 shows decl(ℙ) ⊧ ¬G which, due to the fact that decl(𝔓) is consistent, contradicts the assumption decl(ℙ) ⊧ Gφ. Therefore we must have

⟨G, id⟩ →_{ℙ}^{∗} ⟨true, ϑ⟩

for a suitable substitution ϑ. Lemma 8 shows

decl(ℙ) ⊧ G ↔ ∃v.ϑ, where {v} = var(ϑ)\var(G). Instantiating with φ we see

decl(ℙ) ⊧ Gφ ↔ ∃v.ϑφ. Our assumption decl(ℙ) ⊧ Gφ therefore shows decl(ℙ) ⊧ ∃v.ϑφ. Assume that ϑ = {x_{1}/s_{1}, ⋯ x_{n}/s_{n}}. Since the s_{i} are ground we therefore have

decl(ℙ) ⊧ ∃v.x_{1}φ = s_{1} ∧ ⋯ ∧ x_{n}φ = s_{n}.

We know that x_{i}φ is ground for x_{i} ∈ var(G). Therefore, Clark’s equational theory shows that x_{i}φ = s_{i} for all x_{i} such that x_{i} ∈ var(G). Hence our claim is proved in this case.

2. Assume that the Prolog resolution of G does not fail. Then there would be a computed answer ϑ and the Soundness Theorem would show decl(ℙ) ⊧ Gϑ. This would contradict decl(ℙ) ⊧ ¬G. □

6 Applications

Providing a declarative semantics for Prolog is of more than a mere theoretical interest. It offers the possibility of applying formal methods to Prolog programs. For instance, Stärk has shown how to verify pure Prolog programs [Stä95, Stä96]. Using the declarative semantics developed in this paper it is possible to verify even programs using the cut operator.

However, at the present stage a complete verification of programs is very costly. Therefore, except for certain safety–critical systems, verification is economically not viable. Nevertheless, there are a number of properties of programs that can be verified more or less automatically. One of these properties is completeness. It can be shown that the property of provable completeness defined below entails completeness.

Definition 11 (Provable Complete) If p is a predicate with signature

p(+σ, −τ) and if p is implemented by n clauses of the form

p(l_{i}, r_{i}) ← B_{i} ∧! ∧ C_{i}, i = 1, ⋯, n, then p is provable complete iff for every tuple s of ground terms satisfying s ∈ σ we are able to show

decl(ℙ) ⊧ ⋁_{i=1}^{n} ∃v_{i}.l_{i} = s ∧ B_{i}, (∗)

where {v_{i}} = var(l_{i} = s ∧ B_{i}).

Experience has shown that (∗) is a verification condition that can be proven automatically, even if the implicit quantification over all s ∈ σ is taken into account. Therefore, automatic theorem provers can be used to spot predicates whose implementations are incomplete. We have implemented a tool called Pan that checks, among other properties, the completeness of a program [SG95]. So far, our experience has shown that checking the completeness of a program can uncover subtle errors which might otherwise go undetected. This corresponds to similar experiences that have been observed with the Mercury ^{4} system [SHC95]. Mercury is a modern, purely declarative successor of Prolog. The Mercury compiler offers a determinism analysis of programs. This analysis corresponds roughly to our checking of completeness. The Mercury team has reported [HSC96] that the determinism analysis facilitates the maintenance of programs greatly. We have made similar experiences using the completeness analysis implemented in our tool.

Besides checking completeness, our tool is able to verify the property of a program being universally terminating. The details are presented in [Mül95].

Up to now declarative languages have not made a significant impact on software industry. Our opinion is that this situation can be changed by exploiting the fact that the application of formal methods is much easier for a language possessing a clean, declarative semantics than it is for an imperative language. Recent advances (in particular, we would like to mention here the work of Bouhoula et. al. [Bou94, BR95], and Bachmair and Ganzinger [BG94]) in the field of automatic theorem proving should be exploited and transferred to the field of static analysis of declarative languages. Our own experiences with the use of theorem provers in software verification [Str95] have shown that the time has come for a closer integration of these fields. This will result in both a higher productivity and a higher quality in the use of declarative languages. We view our work as a step in this direction.

Acknowledgments. The authors would like to thank Andrea Engelhardt, Fergus J. Henderson, and Prof. Helmut Schwichtenberg for several helpful discussions on the topic of this paper. Furthermore, thanks go to Martin Müller for designing and implementing that part of our Pan that is responsible for checking the universal termination of predicates.

4 Mercury is available at http://www.cs.mu.oz.au/~zs/mercury.html.

References

[AE93] Krzysztof R. Apt and Sandro Etalle. On the unification free Prolog programs. In S. Sokolowski, editor, Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS ‘93), Lecture Notes in Computer Science. Springer Verlag, 1993. Available at:

http://www.cwi.nl/cwi/publications/index.html.

[And95] James Andrews. The logical semantics of the prolog cut. In John W. Lloyd, editor, International Logic Programming Symposium ‘95. MIT, 1995.

[Apt90] Krzysztof R. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 10, pages 495–574. Elsevier, 1990.

[Apt92] Krzysztof R. Apt, editor. Logic Programming. The MIT Press, 1992.

[Apt93] Krzysztof R. Apt. Declarative programming in Prolog. In D. Miller, editor, Proceedings of International Logic Programming Symposium (ILPS ‘93), Cambridge, Mass./London, 1993. The MIT Press. Available at:

http://www.cwi.nl/cwi/publications/index.html.

[BG94] L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

[BLR92] François Bronsard, T. K. Lakshman, and Uday S. Reddy. A framework of directionality for proving termination of logic programs. In Apt [Apt92], pages 321–335.

[Bör89] E. Börger. A logical operational semantics of full Prolog, part I: Selection core and control. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, Computer Science Logic CSL ’89, pages 36–64. Springer-Verlag, Lecture Notes in Computer Science 440, 1989.

[Bou94] Adel Bouhoula. SPIKE: a system for sufficient completeness and parameterized inductive proofs. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 836–840, Nancy, France, 1994. Springer-Verlag.

[BR95] Adel Bouhoula and Michaël Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 1995.

[Cla78] K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293–322. Plenum Press, New York, 1978.

[dBdV89] A. de Bruin and E.P. de Vink. Continuation semantics for Prolog with cut. In Theory and practice of software engineering, volume 351 of Lecture Notes in Computer Science, pages 178–192. Springer-Verlag, 1989.

[DM85] P. Dembinski and J. Maluszynski. And–parallelism with intelligent backtracking for annotated logic programs. In Proceedings of the International Symposium on Logic Programming, 1985.

[HSC96] Fergus Henderson, Zoltan Somogyi, and Thomas Conway. Determinism analysis in the mercury compiler. In Proceedings of the Australian Computer Science Conference, 1996. Available at:

http://www.cs.mu.oz.au/~zs/mercury/papers.html.

[JM84] N. D. Jones and A. Mycroft. Stepwise development of operational and denotational semantics for prolog. In 1984 International Symposium on Logic Programming, pages 281–288. IEEE, 1984.

[Llo87] J. W. Lloyd. Foundations of Logic Programming. Springer–Verlag, Berlin, second edition, 1987.

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

[MO84] Alan Mycroft and Richard A. O’Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23:295–307, 1984.

[Mül95] Martin Müller. Automatisierbare Terminierungsnachweise von Prolog– Programmen. Master’s thesis, Universität Marburg, 1995. Available at:

http://www.mathematik.uni-marburg.de/~mueller/termnach.ps.

[PS95] Andreas Podelski and Gert Smolka. Operational semantics of constraint logic programs with coroutining. In Leon Sterling, editor, Proceedings of the 1995 International Conference on Logic Programming, pages 449–463, Kanagawa, Japan, 13–18 June 1995. The MIT Press.

[SG95] Karl Stroetmann and Thomas Glaß. Augmented prolog — An evolutionary approach. In Donald A. Smith, Olivier Ridoux, and Peter Van Roy, editors, Proceedings of the Workshop Visions for the Future of Logic Programming: Laying the Foundations for a Modern Successor to Prolog, pages 59–70, 1995. The Proceedings of this workshop are available at:

ftp://ps-ftp.dfki.uni-sb.de/pub/ILPS95-FutureLP/.

[SHC95] Zoltan Somogyi, Fergus Henderson, and Thomas Conway. Logic programming for the real world. In Donald A. Smith, Olivier Ridoux, and Peter Van Roy, editors, Proceedings of the Workshop Visions for the Future of Logic Programming: Laying the Foundations for a Modern Successor to Prolog, pages 83–94, 1995. The Proceedings of this workshop are available at:

ftp://ps-ftp.dfki.uni-sb.de/pub/ILPS95-FutureLP/.

[Stä95] Robert F. Stärk. Formal methods for logic programming systems. Technical report, Department of Mathematics, Stanford University, 1995. Available at:

http://www-leland.stanford.edu/~staerk/list.html.

[Stä96] Robert F. Stärk. Total correctness of pure Prolog programs: A formal ap-

proach. This volume.

[Str95] Karl Stroetmann. Seduct — a proof compiler for first order logic. In Manfred Broy and Stefan Jänichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science. Springer Verlag, 1995.

[Vod88] Paul J. Voda. The logical reconstruction of cuts as one solution operators. In John W. Lloyd, editor, Proceedings of the Workshop on Meta-programming in Logic Programming, pages 379–384. 1988.

This article was processed using the L^{A}TEX macro package with LLNCS style