Applications of the Situation Calculus To Formalizing Control and Strategy Information: The Prolog Cut Operator

1 Introduction

The situation calculus (McCarthy and Hayes [7]) is a for­ malism for representing and reasoning about actions in dynamic domains. It is a many-sorted predicate calculus with some reserved predicate and function symbols. For example, to say that block A is initially clear, we write:

where H is a reserved binary predicate and stands for "holds", and So is a reserved constant symbol denot­ ing the initial situation. As an another example, to say that the action stack(x,y) causes on(x,y) to be true, we write: 1

where the reserved function do( a, s) denotes the resulting situation of doing the action a in the situation s, and Poss(a, s) is the precondition for a to be executable in s. This is an example of how the effects of an action can be represented in the situation calculus. Generally, in the situation calculus:

1 In this paper, free variables in a displayed formula are assumed to be universally quantified.

• situations are first-order objects that can be quan­ tified over;
• a situation carries information about its history, i.e the sequence of actions that have been per­ formed so far. For example, the history of the situation do(stack(A, B), do(stack(B, C) , S0 )) is [stack(B, C), stack(A, B)], i.e. the sequence of ac­ tions that have been performed in the initial situa­ tion to reach this situation. As we shall see later, our foundational aXioms will enforce a one-to-one correspondence between situations and sequences of actions.

We believe that these two features of the situation cal­ culus make it a natural formalism for representing and reasoning about control knowledge. For example, in AI planning, a plan is a sequence of actions, thus isomorphic to situations. So control knowledge in planning, which often are constraints on desirable plans, becomes con­ straints on situations (Lin [4]). Similarly, when we talk about control information in logic programming, we are referring to constraints on derivations, i.e. sequences of actions according to (Lin and Reiter [6]).

Although our long term goal is to develop a general framework for representing and reasoning about control knowledge in problem solving using the situation calcu­ lus, our focus in this paper is the Prolog cut operator, the central search control operator in Prolog. We pro­ vide a situation calculus semantics for logic programs with cut, and show that our semantics is well-behaved when the programs are properly stratified. We also show that according to this semantics, the conventional imple­ mentation of the negation-as-failure operator using cut is provably correct with respect to the stable model se­ mantics of Gelfand and Lifschitz [2]. To the best of our knowledge, this is the first time a connection has been shown between a declarative semantics of negation and that of cut.

This paper is organized as follows. Section 2 briefly reviews the basic concepts in the situation calculus and logic programming. Section 3 reviews the situation calculus semantics of (Lin and Reiter [6]) for cut-free logic programs. For the purpose of this paper, the key prop­ erty of this semantics is that derivations in logic pro­ gramming are identified with situations. Section 4 ex­ tends this semantics to logic programs with cut. This is done by an axiom on accessible situations, that is, those situations whose corresponding derivations are not "cut off" by cut. Section 5 shows some properties of our se­ mantics, and finally section 6 concludes this paper.

2 Logical Preliminaries

2.1 The Situation Calculus

The language of the situation calculus is a many-sorted second-order one with equality. We assume the follow­ ing sorts: situation for situations, action for actions, flu­ ent for propositional fluents such as clear whose truth values depend on situations, and object for everything else. As we mentioned above, we assume that So is a reserved constant denoting the initial situation, H a re­ served predicate for expressing properties about fluents in a situation, do a reserved binary function denoting the result of performing an action, and Poss a reserved bi­ nary predicate for action preconditions. In addition, we assume the following two partial orders on situations:

• <: following convention, we write < in infix form. By s < s' we mean that s' can be obtained from s by a sequence of executable actions. As usual, s ~ s' will be a shorthand for s < s 1 V s = s 1 ·
• C: we also write C in infix form. By s C s' we mean that s can be obtained from s' by deleting some of its actions. Similarly, s ~ s' stands for s C s' V s = s'.

We shall consider only the discrete situation calculus with the following foundational axioms: 2

The first two axioms are unique names assumptions for situations. The third axiom is second order induction.

2 Except for the one about C, these axioms are taken from (Lin and Reiter [5]), which also proves some useful properties about them.

It amounts to the domain closure axiom that every situ­ ation has to be obtained from the initial one by repeatly applying the function do. In other words, it says that every situation is either the initial situation So or the result of performing a sequence of actions in the initial situation, exactly the isomorphism between situations and sequences of actions that we mentioned earlier. As can be expected, induction will play an important role in this paper.

Axioms ( 4) and (5) define < inductively. Generally, s ~ s' if s' can be obtained from s by performing some executable actions.

In this paper we shall assume that actions are always possible: (Va, s)Poss(a, s). Under this assumption, the partial order < reduces to the "prefix" relation: 3 Given a situation S = do([o:1, ... , o:nJ, So), S' ~ S iff there is a 0 ~ k ~ n such that S' = do([o:1, ... , o:k], So). In particular, we have (Vs)S0 ~ s.

Axiom (6) defines c. Informally, s ~ s' iff s can be obtained from s' by deleting some of its actions. More precisely, suppose S' = do([o:1, ... , o:nJ, So). Then S ~ S' iff there are integers 1 ~ i 1 ~ · · · ~ ik ~ n, 0 ~ k ~ n, such that S = do([o:ip .. . , o:iJ, So). Figure 1 illustrates a function f as required by axiom (6) for proving

Notice that ~ is a special case of ~: if s ~ s' then s ~ s'. As we shall see, the partial order C will play a crucial role in this paper.

In the following, we shall denote by :E the set of the above axioms.

2.2 Logic Programs

We consider definite logic programs with cut.

An atom pis a fluent term F(t1 , ... , tn), where F is a fluent of arity objectn, and h, ... , tn are terms of sort object. A goal G is an expression of the form

3 Given a sequence of actions [a1 , ... ,an], we use do([a1, ... ,an], s) to denote the resulting situation of perform­ ing the sequence of actions in s . Inductively, do(O, s) = s and do([aiL], s) = do(L, do( a, s)).

where n 2: 0, and for each 1 :S i :S n, li is either an atom, an equality atom of the form t = t', or ! .

.Without loss of generality, we assume that a clause {rule) is an expression of the form

where F is a fluent of the arity objectn, x1 , ... , Xm are distinct variables of sort object, and G is a goal. Notice that the more common form of a clause

can be taken to be a shorthand for the following clause:

where x1, ... , Xn are fresh variables notinG and t 1 , . . . , tn. Finally, a (definite) program is a finite set of clauses. The definition of a fluent symbol F in a program P is the set of clauses in P that have F in their heads.

Since a goal is not a situation calculus formulas, we need a way to refer to its truth values. Given a goal G = l1 & · · · & ln, and a situation term S, we define H(G, S), the truth value of G in the situation S, to be the situation calculus formula

where for each 1 :S i :S n:

1. If l; is t = t', then H(l;, S) is l;.
2. If l; is ! , then H(l;, S) is the tautology true.

For example, H(x =a & parent(x, y) & ! , S0 ) is

3 A Logical Semantics

The cut operator in Prolog plays two roles. As a goal, it succeeds immediately. As a search control operator, it prevents a Prolog interpreter from backtracking past it. Consequently, our semantics for programs with cut will come in two stages. First, we consider the "pure logical" semantics of the programs when cut is taken to be a goal that succeeds immediately. For this purpose, we shall use the situation calculus semantics for logic programs without cut proposed by Lin and Reiter ([6]) .. For our purpose here, the key of this semantics is that program clauses are identified with the effects of actions in the situation calculus, so a branch in a search tree becomes a sequence of actions, thus isomorphically, a situation. This is important because the effect of a cut on the search tree can then be modeled by restrictions on situations. So our second step in formalizing the cut operator is to define a relation call Ace on situations so that Ace( s) holds with respect to a logic program if the sequence of actions in s corresponds to a successful derivation according to the program.

The rest of this section is basically a review of [6] with a minor notational difference: while we reify fluents and use the special predicate H, Lin and Reiter [6] treat ftu­ ents as predicate symbols. For example, H(broken, s) would be written as broken(s) in [6].

According to [6), clauses are treated as rules, so that the application of such a rule in the process of answering a query is like performing an action. Formally, given a clause of the form

Lin and Reiter [6] introduce a unique action A of the arity objectn -+ action to name this clause. The only effect of this action is the following:

where xis (x1, .. . , xn), and {is the tuple of variables that are in G but not in x. For example, suppose gp(x,y) is the action that names the following clause:

then we have the following effect axiom:

Now suppose that P is a program and F a fluent. Suppose the definition ofF in P is

where A1 , . . . , Ak are action names of the corresponding clauses. Then we have the following corresponding effect axioms for the fluent F:

where yi, 1 :S i :S k, is the tuple of variables in G; which are not in x. We then generate the following successor state axiom (Reiter [8]) for F:

Intuitively, this axiom says that F is true in a successor situation iff either it is true initially or the action is one that corresponds to a clause in the definition of F and the body of the clause is satisfied initially. In particular, if the definition of F in the program P is empty, then (7) becomes H(F(x), do( a, s)) = H(F(x), s) .

In· the following, we call (7) the successor state axiom for F wrt toP.

Given a logic program P, the set of successor state axioms wrt P, together with some domain independent axioms, is then the "pure logical meaning" of P:

Definition 1 The basic action theory V for P is

where

• :E is the set of foundational axioms given in Sec­ tion 2.1.
• D88 is the set of successor state axioms for the ftu­ ents according to P.
• Duna is the following set of unique names axioms:

for every pair f, g of distinct function symbols, and

for every function symbol f . Notice that Duna in­ cludes unique names axioms for actions.

• Ds 0 is:

Definition 2 Let P be a program, and V its correspond­ ing basic action theory. A situation term S is called a plan for a goal G iff V f= H ( G, S) .

Therefore query answering in logic programs literally becomes planning in the style of (Green [3]) in the situ­ ation calculus. This semantics has some nice properties. It is closely related to a recent proposal by Wallace [10], and generalizes the Clark completion semantics. Fur­ thermore, in the propositional case, it is equivalent to Gelfond and Lifschitz's stable model semantics. For de­ tails, see (Lin and Reiter [6]).

Example 1 Consider the following program for max(x,y,z), z is the maximum of {x,y}: 4

Here le(x,y) means that xis less than or equal toy, and 1 and 2 are constants. \Ve have the following successor state axioms for max and le:

4 This is a typical example of improper uses of cut. We'll return to this point later.

From these successor state axioms, it is easy to see that performing first B1 (1, 2), then A1 (1, 2, 2) in So will result in a situation satisfying max(1, 2, 2). Thus we have the following desirable conclusion:

On the other hand, it is also clear that the action A2(x,y,x) will make max(x,y,x) true, so we also have:

which is not so desirable. Of course, the reason is that the basic action theory V does not take into account the effects of ! on the search space. According to Pro­ Jog's search strategy, which attempts rules in the order as they are given, the second rule (A2) for max will not be attempted if the subgoalle(x, y) before ! in the first rule for max succeeds. Therefore the derivation corre­ sponding to do(A2(x, y, x), S0 ) will not be considered if there is a derivation for le(x, y), which· is the case here if x = 1 and y = 2.

Let us call a situation accessible if the derivation cor­ responding to this situation 5 is legal, i.e. not ruled out by the cut. Our goal in defining a semantics for the cut operator is then to characterize the set of accessible sit­ uations. This is what we are going to do in the next section.

4 A Semantics for Cut

A clause containing cut:

means that if G1 succeeds, then any derivation of F(x) must use either

1. A rule before this one; or
2. This rule with the first derivation of G1 .

We now proceed to formalize this informal reading.

First, notice that we need two ordering relations: one on rules for deciding the precedence of rules, and the other on situations for defining "the first derivation".

5 In the following, the terms situations and derivations will be used interchangeably.

In the following, we shall assume that we are given an ordering-< on actions (rules), and will define an ordering on situations using -<. Intuitively, if o: -< /3, then during the process of search, the action o: will be considered be­ fore the action j3. For instance, according to Prolog's or­ dering rule, for our max example, (Vx, il)Al(x) -< A2 (if).

Given a partial order on actions, there are many ways situations, i.e. sequences of actions, can be ordered, depending on particular problem solving strategies. In Prolog, a query is answered using a goal-directed search strategy, so if a plan do([o:1, ... , o:n], So) is returned, then it must be the case that O:n is first decided, then O:n-1, ... , and finally o:1. If we read s -< s' as that the sequence of actions in s is considered before that in s', then we have the following definition:

Definition 3 Given a partial order -< on actions, the derived partial order with the same name -< on situations is defined by the following axiom:

With this partial order on situations, we can then say, roughly, that a situation is a "first derivation" of a goal G if it is a derivation of G that is minimal according to -<. However, to make this precise we first need a space of derivations to define the notion of minimality. We do not want it to be the set of all plans for G because according to our definition, if D is a basic action theory for a logic program, then

So if s is a plan for G, then for any action a, do( a, s) is also a plan for G. This means that a plan for G can always be made "smaller" according to -< by appending to it some irrelevant actions. To avoid this problem, we define the notion of minimal plans:

Definition 4 For any situation termS, any goal G, we denote by minimal(G, S) the following formula:

Intuitively, minimal( G, S) holds if no actions in it can be deleted for it to be a plan of G. For our max program in section 3, it is easy to see that

But

because do(B1 (1, 2), So) C do([B1 (1, 2), A1 (1, 2, 2)], So). It can be seen that for any goal G, if there is a plan for it, then there is a minimal plan for it:

We are now ready to formalize the informal reading of a clause containing ! at the beginning of this section. For this purpose, we introduce a new predicate Acc(s), meaning that s is not "cut off" by cut.

If a program contains the cut rule cut(x), and the goal G1 succeeds, then for Ace( s) to hold, it must be the case that for every minimal plan s1 ofF in s, either it uses a rule before this cut rule or it uses this cut rule with the first derivation of G1:

where (is the tuple of the free variables that are in G1 but not in x, and generally, for any goal G, and situation termS, and any tuple y of variables, first-der(G, S, YJ means that S is the first derivation of G with the vari­ ables in y fixed: 6

where v is the tuple of variables that are in G but not in :iJ.

Here we notice that in the axiom (ll), the formula

corresponds to "G1 succeeds", the case

corresponds to "the derivation s1 of F(x) uses a rule before the cut rule", and the other case corresponds to "uses this rule with the first derivation of G1".

Now given a program P, suppose

are all the axioms about Ace as given above for every occurrence of ! in P (a single clause may have multiple occurrences of ! ) . We call the following the accessibility axiom of P:

Notice that this axiom attempts to define Ace recursively since the predicate also occurs in the right hand side of the equivalence. This should not be surprising. For ex­ ample, the logical formalization of negation in logic pro­ grams normally requires fixed-point constructions, and negation is usually implemented by cut.

6 Notice that if none of G and S contains variables, then first-der(G, st, i7) is independent of fj.

Definition 5 (Extended Action Theory) Let P be a program, and ~ a given set of axioms about ~ on ac­ tions. The extended action theory £ of P is the the following set:

where V is the basic action theory for P, and Ace is the accessibility axiom of P of the form {12).

Definition 6 Let P be a program, £ its extended action theory, and G a goal. A situation term S is an accessible plan for G iff£ f= Acc(S) 1\ H(G, S) .

We illustrate the definitions with our max example. Suppose we use Prolog's search strategy, and order the actions as:

Notice that we do not care about how the rules about le are ordered. Since the only occurrence of ! is in A1 , the accessibility axiom is

Now let £ be the extended action theory of the pro­ gram. First of all, we can show that

thus

This is intuitively right since the only appearance of ! is in the definition of max, and the presence of ! has no effect on le. For max, we can show:

So the max program indeed defines max correctly. How­ ever since

this use of cut is not ideal in the sense that it does more than search control.

In general, we say that the cuts in a program P are for pure search control if for any goal G,

Some ramification of this definition for identifying im­ proper uses of cut will be explored further in the full version 7 of this paper.

5 Some Properties

As we have noticed, the accessibility axiom attempts to define Ace recursively. A natural question then is if the recursion will yield a unique solution for the predicate. In general, the answer is negative. However, if a program is properly stratified, then the axiom will yield a unique solution.

Let P be a program, and F a fluent. We say that the definition ofF in Pis cut-free if none of the clauses that are relevant to F contains ! . Here a clause is relevant to F if, inductively, either it's in the definition ofF or it's relevant to another fluent that appears in the definition of F. For example, the definition of le in the max ex­ ample is cut-free. For cut-free fluents, Ace does not play a role:

Proposition 1 Let P be a program, and £ its extended action theory. If the definition of a fluent F in P is cut-free, then we have:

Cut-free fluents are the ground case of stratified pro­ grams:

Definition 7 A program P is stratified if there is a func­ tion f from fluents in P to natural numbers such that

1. IfF is cut-free in P, then f(F) = 0.

2. IfF is not cut-free, then f(F) is

1 + max{f(F') I F' appears in the definition ofF}.

Theorem 1 Let P be a stratified program, and £ its corresponding extended action theory. There is a formula ~ that does not mention Ace such that

We end this section with a theorem that shows the cor­ rectness of the usual implementation of negation using cut.

Let P be a logic program with negation (not) but without cut . Suppose that for each fluent F in P, F'

7 1n preparation. But see http:/ /www.cs.ust.hk/-fl.in

is a new fluent of the same arity. Let P' be the logic program obtained by replacing every literal of the form not F(i) in P by F'(i), and by adding, for each new fluent F', the following two clauses:

AF(x):

F'(x) :- F(i) & ! & fail.

A'p(x): F'(i).

Suppose that for each fluent F, the action AF is ordered before the action A'p.

Theorem 2 Let £ be the extended action theory of P', and V the action theory for P as defined in {Lin and Reiter [6]}. For fluent F in P, and any tuple t of terms of sort object, we have V f= (3s)H(F(i), s) iff £ f= (3s).Acc(s) 1\ H(F(i), s).

From this theorem, we conclude that the usual im­ plementation of negation using cut is correct with re­ spect to the semantics given in (Lin and Reiter [6]). As noted in (Lin and Reiter [6]), the semantics given there for logic programs with negation yields the same results as that given in (Wallace [10]) , and the latter has been shown to be equivalent to the stable model semantics of (Gelfond and Lifschitz [2]) when only Herbrand models are considered. Therefore we can also conclude that the usual implementation of negation in terms of cut is cor­ rect with respect to the stable model semantics for logic programs with negation in the propositional case.

6 Concluding Remarks

We have applied the situation calculus to logic program­ ming by giving a semantics to programs with cut. We have shown that this semantics has some desirable prop­ erties: it is well-behaved when the program is stratified, and that according to this semantics, the usual imple­ mentation of negation-as-failure operator by cut is prov­ ably correct with respect to the stable model semantics.

Our more long term goal is to use the situation calcu­ lus as a general framework for representing and reason­ ing about control and strategic information in problem solving. In this regard, we have made some preliminary progress in applying the situation calculus to formaliz­ ing control knowledge in planning. As we mentioned in Section 1, in AI planning, a plan is a sequence of actions, thus isomorphic to situations. So control knowledge in planning, which often are constraints on desirable plans, becomes constraints on situations. Based on this idea, in (Lin [4]), we formulate precisely a subgoal ordering in planning in the situation calculus, and show how in­ formation about this subgoal ordering can be deduced from a background action theory. We also show for both linear and nonlinear planners how knowledge about this ordering can be used in a provably correct way to avoid unnecessary backtracking.

Regarding our situation calculus semantics for the cut operator, there are many directions for future work.

First of all, there is a need to compare our semantics with recent work of [1; 9]. More importantly, we should use this semantics to clarify the proper roles of cut in logic programming, to study the possibility of a better control mechanism, and to do verifications and syntheses of logic programs with cut.

Acknowledgements

Part of this work was done while the author was with the Cognitive Robotics Group of the Department of Com­ puter Science at the University of Toronto. This work is also supported in part by grant DAG96/97.EG34 from the Hong Kong Government.

The author would like to thank Eyal Amir, Yves Lesperance, Hector Levesque, and especially Ray Reiter for helpful discussions relating to the subject of this pa­ per and/or comments on earlier versions of this paper.