Situation calculus

The actions form a sort of the domain. Variables of sort action can be used and also functions whose result is of sort action. Actions can be quantified. In the example robot world, possible action terms would be ${\displaystyle move(x,y)}$ to model the robot moving to a new location ${\displaystyle (x,y)}$, and ${\displaystyle pickup(o)}$ to model the robot picking up an object o. A special predicate Poss is used to indicate when an action is executable.

In the situation calculus, a dynamic world is modeled as progressing through a series of situations as a result of various actions being performed within the world. A situation represents a history of action occurrences. In the Reiter version of the situation calculus described here, a situation does not represent a state, contrarily to the literal meaning of the term and contrarily to the original definition by McCarthy and Hayes. This point has been summarized by Reiter as follows:

A situation is a finite sequence of actions. Period. It's not a state, it's not a snapshot, it's a history.[2]

The situation before any actions have been performed is typically denoted ${\displaystyle S_{0}}$ and called the initial situation. The new situation resulting from the performance of an action is denoted using the function symbol do (Some other references[3] also use result). This function symbol has a situation and an action as arguments, and a situation as a result, the latter being the situation that results from performing the given action in the given situation.

The fact that situations are sequences of actions and not states is enforced by an axiom stating that ${\displaystyle do(a,s)}$ is equal to ${\displaystyle do(a',s')}$ if and only if ${\displaystyle a=a'}$ and ${\displaystyle s=s'}$. This condition makes no sense if situations were states, as two different actions executed in two different states can result in the same state.

In the example robot world, if the robot's first action is to move to location ${\displaystyle (2,3)}$, the first action is ${\displaystyle move(2,3)}$ and the resulting situation is ${\displaystyle do(move(2,3),S_{0})}$. If its next action is to pick up the ball, the resulting situation is ${\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))}$. Situations terms like ${\displaystyle do(move(2,3),S_{0})}$ and ${\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))}$ denote the sequences of executed actions, and not the description of the state that result from execution.

Statements whose truth value may change are modeled by relational fluents, predicates that take a situation as their final argument. Also possible are functional fluents, functions that take a situation as their final argument and return a situation-dependent value. Fluents may be thought of as "properties of the world"'.

In the example, the fluent ${\displaystyle {\textit {isCarrying}}(o,s)}$ can be used to indicate that the robot is carrying a particular object in a particular situation. If the robot initially carries nothing, ${\displaystyle {\textit {isCarrying}}(Ball,S_{0})}$ is false while ${\displaystyle {\textit {isCarrying}}(Ball,do(pickup(Ball),S_{0}))}$ is true. The location of the robot can be modeled using a functional fluent ${\displaystyle location(s)}$ that returns the location ${\displaystyle (x,y)}$ of the robot in a particular situation.

Some actions may not be executable in a given situation. For example, it is impossible to put down an object unless one is in fact carrying it. The restrictions on the performance of actions are modeled by literals of the form ${\displaystyle {\textit {Poss}}(a,s)}$, where a is an action, s a situation, and Poss is a special binary predicate denoting executability of actions. In the example, the condition that dropping an object is only possible when one is carrying it is modeled by:

${\displaystyle {\textit {Poss}}(drop(o),s)\leftrightarrow {\textit {isCarrying}}(o,s)}$

As a more complex example, the following models that the robot can carry only one object at a time, and that some objects are too heavy for the robot to lift (indicated by the predicate heavy):

${\displaystyle {\textit {Poss}}(pickup(o),s)\leftrightarrow (\forall z\ \neg {\textit {isCarrying}}(z,s))\wedge \neg heavy(o)}$

Given that an action is possible in a situation, one must specify the effects of that action on the fluents. This is done by the effect axioms. For example, the fact that picking up an object causes the robot to be carrying it can be modeled as:

${\displaystyle Poss(pickup(o),s)\rightarrow {\textit {isCarrying}}(o,do(pickup(o),s))}$

It is also possible to specify conditional effects, which are effects that depend on the current state. The following models that some objects are fragile (indicated by the predicate fragile) and dropping them causes them to be broken (indicated by the fluent broken):

${\displaystyle Poss(drop(o),s)\wedge fragile(o)\rightarrow broken(o,do(drop(o),s))}$

While this formula correctly describes the effect of the actions, it is not sufficient to correctly describe the action in logic, because of the frame problem.

While the above formulae seem suitable for reasoning about the effects of actions, they have a critical weakness—they cannot be used to derive the non-effects of actions. For example, it is not possible to deduce that after picking up an object, the robot's location remains unchanged. This requires a so-called frame axiom, a formula like:

${\displaystyle Poss(pickup(o),s)\wedge location(s)=(x,y)\rightarrow location(do(pickup(o),s))=(x,y)}$

The need to specify frame axioms has long been recognised as a problem in axiomatizing dynamic worlds, and is known as the frame problem. As there are generally a very large number of such axioms, it is very easy for the designer to leave out a necessary frame axiom, or to forget to modify all appropriate axioms when a change to the world description is made.

The successor state axioms "solve" the frame problem in the situation calculus. According to this solution, the designer must enumerate as effect axioms all the ways in which the value of a particular fluent can be changed. The effect axioms affecting the value of fluent ${\displaystyle F({\overrightarrow {x}},s)}$ can be written in generalised form as a positive and a negative effect axiom:

${\displaystyle Poss(a,s)\wedge \gamma _{F}^{+}({\overrightarrow {x}},a,s)\rightarrow F({\overrightarrow {x}},do(a,s))}$

${\displaystyle Poss(a,s)\wedge \gamma _{F}^{-}({\overrightarrow {x}},a,s)\rightarrow \neg F({\overrightarrow {x}},do(a,s))}$

The formula ${\displaystyle \gamma _{F}^{+}}$ describes the conditions under which action a in situation s makes the fluent F become true in the successor situation ${\displaystyle do(a,s)}$. Likewise, ${\displaystyle \gamma _{F}^{-}}$ describes the conditions under which performing action a in situation s makes fluent F false in the successor situation.

If this pair of axioms describe all the ways in which fluent F can change value, they can be rewritten as a single axiom:

${\displaystyle Poss(a,s)\rightarrow \left[F({\overrightarrow {x}},do(a,s))\leftrightarrow \gamma _{F}^{+}({\overrightarrow {x}},a,s)\vee \left(F({\overrightarrow {x}},s)\wedge \neg \gamma _{F}^{-}({\overrightarrow {x}},a,s)\right)\right]}$

In words, this formula states: "given that it is possible to perform action a in situation s, the fluent F would be true in the resulting situation ${\displaystyle do(a,s)}$ if and only if performing a in s would make it true, or it is true in situation s and performing a in s would not make it false."

By way of example, the value of the fluent broken introduced above is given by the following successor state axiom:

${\displaystyle Poss(a,s)\rightarrow \left[broken(o,do(a,s))\leftrightarrow a=drop(o)\wedge fragile(o)\vee broken(o,s)\wedge a\neq repair(o)\right]}$

The properties of the initial or any other situation can be specified by simply stating them as formulae. For example, a fact about the initial state is formalized by making assertions about ${\displaystyle S_{0}}$ (which is not a state, but a situation). The following statements model that initially, the robot carries nothing, is at location ${\displaystyle (0,0)}$, and there are no broken objects:

${\displaystyle \forall z\,\neg {\textit {isCarrying}}(z,S_{0})}$

${\displaystyle location(S_{0})=(0,0)\,}$

${\displaystyle \forall o\,\neg broken(o,S_{0})}$

The foundational axioms of the situation calculus formalize the idea that situations are histories by having ${\displaystyle do(a,s)=do(a',s')\iff a=a'\land s=s'}$. They also include other properties such as the second-order induction on situations.