Situation calculus

• 1. Introduction

  ›

  Situation calculus is a formal system for reasoning about worlds that change over time. John McCarthy introduced it in 1963, and it has shaped how computer scientists and logicians think about action, consequence, and the passage of time ever since. At its heart, the calculus asks a deceptively simple question: when a robot picks up a ball, what else changes, and what stays the same? That question turns out to be one of the hardest problems in the logic of action. Ray Reiter's 1991 reformulation became the dominant version used today. The two versions differ not just in notation but in something far more fundamental: what a situation actually is.

• 2. Three Kinds of Things

  ›

  Reiter's version of the situation calculus sorts the world into three basic kinds: actions, situations, and objects, where objects include everything that is neither an action nor a situation. Fluents sit outside this sorting; they are not elements of the domain but rather predicates or functions that describe properties of the world at a given moment. The robot world used as a running example throughout the formalism keeps things concrete. A single robot moves across a grid, picks up and drops objects, and can repair broken items it is holding. Some objects are too heavy to lift; others are fragile and break when dropped. These simple facts generate surprisingly complex logical demands. Poss is the special predicate that marks when an action is actually executable in a given situation, and it anchors every statement about what the robot can do.

• 3. What a Situation Really Is

  ›

  Reiter drew a sharp line between his formalism and McCarthy's original. In the original conception by McCarthy and Hayes, a situation was "the complete state of the universe at an instant of time." Reiter rejected that reading entirely. As he put it: "A situation is a finite sequence of actions. Period. It's not a state, it's not a snapshot, it's a history." This is not a minor terminological shift. It changes the mathematical foundations. An axiom in Reiter's system enforces the point: the situation resulting from performing action a in situation s is equal to the situation resulting from performing action b in situation t if and only if a equals b and s equals t. That condition would be meaningless if situations were states, because two different actions in two different states can produce identical states. The initial situation, denoted S0, represents the empty sequence, the world before any action has occurred.

• 4. The Frame Problem

  ›

  Effect axioms describe what changes when an action is performed. The formula that picking up an object causes the robot to carry it is clean and intuitive. But these axioms carry a hidden inadequacy: they say nothing about what does not change. After the robot picks up the ball, is its location the same? Nothing in the effect axiom answers that. Each such non-effect requires its own frame axiom, a separate formula asserting that a particular fluent remains unchanged by a particular action. With many actions and many fluents, the number of required frame axioms grows large. The risk is that a designer forgets one, or fails to update all relevant axioms when the world description changes. This is the frame problem, long recognized as a central difficulty in axiomatizing dynamic worlds. Reiter's successor state axioms were developed precisely to address it.

• 5. Successor State Axioms

  ›

  The successor state axiom consolidates the frame problem into a manageable form. For each fluent, the designer enumerates all the ways that fluent can become true and all the ways it can become false. These positive and negative effect axioms are then combined into a single formula. That formula states, roughly, that a fluent is true in the successor situation if and only if the action just performed made it true, or it was already true and the action did not make it false. The fluent broken, which tracks whether an object has been dropped while flagged as fragile, gets its own successor state axiom of this form. Regression is the complementary mechanism: it allows a query about a complex situation to be transformed step by step into an equivalent query about the initial situation S0, where checking consequences is more tractable. GOLOG, a logic programming language built directly on the situation calculus, implements this regression implicitly through backward reasoning.

• 6. McCarthy's 1986 Revision

  ›

  McCarthy returned to the situation calculus in 1986 with two significant changes from the original. Functional fluents replaced the purely predicate-based approach of the original formulation; the position of an object x in situation s could now be expressed as the value of a location function rather than as a predicate literal. The second change was an attempt to use circumscription, a form of non-monotonic reasoning, to replace frame axioms entirely. This contrasts with the fluent calculus, a related but distinct approach in which a state can be an incomplete description of the universe, a collection of known facts rather than a complete world history. In the original formulation, the initial situation was not explicitly identified, because situations as complete world-states did not require an empty starting point. The modern formalism needs S0 precisely because a history must begin somewhere.

• 7. Logic Programming Formulation

  ›

  Work by Kowalski in 1979, Apt and Bezem in 1990, and Shanahan in 1997 showed that the situation calculus can be written as a logic program. This formulation introduces a meta-predicate called Holds and a variable ranging over fluents. The predicates Poss, Initiates, and Terminates in the logic program correspond directly to Poss and the positive and negative effect conditions in the axiomatic version. The left-arrow symbol in the program captures half of a logical equivalence; the other half is implicit in the program's completion, where negation is read as negation as failure. Induction axioms are also implicit, needed only when proving properties of the program rather than executing it. SLD resolution, the standard execution mechanism for logic programs, carries out regression automatically through backward reasoning, making the logic programming formulation both compact and computationally grounded. Shanahan's 1997 work remains a key reference for this translation.