Frame problem

• 1. Introduction

  ›

  In 1969, John McCarthy and Patrick J. Hayes posed a question that would haunt artificial intelligence for decades: how does a logical system know what stays the same? Their paper, Some Philosophical Problems from the Standpoint of Artificial Intelligence, introduced the frame problem, and it turned out to be far thornier than it first appeared.

  Picture a robot navigating a room. A door opens. A light is on. The robot acts. Now: does the light still work the same way? Did the floor change? Did the walls move? A human never asks these questions because we assume, almost automatically, that things not acted upon remain as they were. But first-order logic, the formal language researchers used to build reasoning machines, carries no such assumption. Every unchanged fact has to be stated, explicitly, as an axiom. And the number of such axioms grows without limit as the world grows more complex.

  What McCarthy and Hayes exposed was not just a technical nuisance. It pointed to something profound about the gap between human common sense and machine reasoning. The questions their paper planted would occupy logicians, philosophers, and AI researchers for the rest of the century: how do you tell a machine what it already knows without telling it everything?

• 2. The Door and the Light

  ›

  A door and a light bulb are enough to show why the frame problem is so stubborn. Consider a simple scenario with two facts: the door is closed, and the light is off. These can be represented as logical propositions. So far, so clean.

  The trouble begins the moment time enters the picture. If conditions can change, they must be expressed as predicates that depend on time. These are called fluents. The door's state at time zero and the door's state at time one are two different things, and the logic must track them separately.

  Suppose the door is closed and the light is off at time zero, and someone opens the door at time one. Three logical formulae capture this: the initial closed door, the initial dark light, and the act of opening. But those three formulae are not enough to draw the right conclusions. The logic, as written, is consistent with a world where the light changed status when the door was opened. Nothing in the three formulae rules that out.

  The solution seems obvious: add an axiom saying the light did not change. But now consider a world with dozens of objects and dozens of possible actions. Every pairing of an action with a condition it does not affect requires its own axiom. The number of required frame axioms grows with the square of the complexity of the domain, making any large-scale formal model unwieldy.

• 3. McCarthy's Circumscription

  ›

  John McCarthy's proposed fix rested on a principle of minimality: assume that as few conditions as possible have changed. If the logic can be satisfied with the light staying off, prefer that interpretation. This approach was formalized using a technique called circumscription, which reasons about minimal models of a logical theory.

  The idea has intuitive appeal. Humans seem to apply something like this rule constantly. When you leave a room and come back, you assume your chair is still there, not because you proved it, but because nothing suggested otherwise. Circumscription tried to encode that default presumption in formal terms.

  Steve Hanks and Drew McDermott, however, devised a scenario that exposed the limits of this approach: the Yale shooting problem. Their example showed that minimizing change does not always produce the result common sense would expect. A gun is loaded; time passes; the gun fires. Circumscription, applied naively, could lead to the conclusion that the gun became unloaded by itself rather than that the shooting caused the death. The minimal change principle, it turned out, was not selective enough to always point to the right minimal change.

  By the end of the 1980s, the problem as McCarthy and Hayes originally posed it was considered solved, but the Yale shooting problem had already forced a branching of solutions.

• 4. A Landscape of Solutions

  ›

  Erik Sandewall proposed the fluent occlusion solution, which added a new kind of predicate called occlusion to the formal language. A condition is occluded at a given time if an action has just been executed that directly affects it. Occlusion acts as a permission slip: only occluded conditions are allowed to change. Everything else is locked in place by default.

  The predicate completion approach, closely related but distinct, used change predicates rather than permission predicates. A condition changes at time T if and only if the corresponding change predicate is true at T. Applying predicate completion to the rules governing actions then minimizes the times when change predicates are asserted.

  Ray Reiter developed the successor state axiom approach, which works by specifying, for every condition, exactly the circumstances under which it becomes true or false after an action. Rather than one formula per action, there is one axiom per condition. Reiter built this into a variant of the situation calculus, a well-established framework for reasoning about action.

  The fluent calculus, a variant of the situation calculus, took a different tack altogether. It converted predicates about state into first-order logic terms, a process called reification. A state is then an object in the logic, composed of the conditions true within it. When an action is executed, the formula specifies how the state term changes, and the bookkeeping of unchanged conditions follows from the algebra of terms rather than from explicit axioms.

• 5. The Event Calculus and Default Logic

  ›

  The event calculus addresses the frame problem through a single axiom encoding the law of inertia: a fluent holds at a given time if some event initiated it earlier, and no event terminated it in the interval between. This is a compressed but powerful statement. The entire burden of maintaining persistence across time rests on that one axiom, combined with domain-specific definitions of what events initiate or terminate which fluents.

  Solving a problem in the event calculus requires specifying which events happen, then querying which fluents hold at a target time. The event calculus eliminates unwanted solutions by using a non-monotonic logic, such as circumscription, or by treating the calculus as a logic program that uses negation as failure.

  Raymond Reiter also contributed a default logic formulation, invoking a principle that Leibniz had articulated in a manuscript around 1679: that everything is presumed to remain in the state in which it is. Reiter called this the commonsense law of inertia. His default logic rule says: if a condition is true in a given situation, and it is consistent to assume it remains true after an action, then conclude it does remain true. Hanks and McDermott's Yale shooting problem challenged this formulation as well, but Hudson Turner later showed it works correctly when appropriate additional postulates are supplied.

• 6. Separation Logic and Scalability

  ›

  Separation logic approached the frame problem from a different direction entirely, not from the world of robots and blocks, but from the world of software verification. It is an extension of Hoare logic, a system for writing pre- and post-condition specifications for computer programs, oriented toward reasoning about mutable data structures in memory.

  The key innovation is a connective pronounced "and separately," written with an asterisk, which supports independent reasoning about disjoint memory regions. A frame rule in separation logic allows descriptions of memory outside the footprint of a piece of code to be attached to a specification without mentioning that memory in the core specification at all.

  As a concrete example, a specification that a piece of code sorts a list can be augmented by the fact that it leaves a separate list untouched, and this augmentation requires no mention of the second list in the original proof about sorting. The code's footprint, meaning the memory it actually accesses, determines what needs to be specified, and everything outside that footprint is implicitly preserved.

  Automation of this frame rule produced significant increases in the scalability of automated reasoning tools for software. These techniques eventually reached industrial deployment on codebases with tens of millions of lines. The parallel with the fluent calculus solution is noted in the literature: both approaches work by making explicit what a change touches, rather than cataloguing what it leaves alone.

• 7. Eluding Rather Than Solving

  ›

  Action description languages took a pragmatic route: they sidestepped the frame problem rather than confronting it head-on. These are formal languages with syntax specifically designed to express situations and actions in a natural way. An action can be written as "causes if," and the language's semantics handle the persistence of other conditions without requiring the programmer to enumerate frame axioms.

  The semantics of such languages depend on what they can express. Some handle concurrent actions; others handle delayed effects. They are typically grounded in transition systems. When a domain is expressed in an action description language, the frame problem only reappears if and when the specification needs to be translated into first-order logic. In practice, such translations target answer set programming rather than first-order logic directly.

  Answer set programming also has its own solution to the frame problem, a direct counterpart to Reiter's default logic rule: if a condition is true at time T, and it can be assumed to remain true at time T plus one, then conclude it does. The strong negation used in answer set programming gives this rule the formal grounding needed to avoid the instabilities that plagued early default logic approaches.

  The broader lesson from all these formalisms is that the frame problem is not a single puzzle with a single answer. It is a family of related challenges about representing persistence, change, and inertia in formal systems. John McCarthy and Patrick J. Hayes named it in 1969, and in doing so gave researchers a target they would spend the next three decades refining their aim at.