Editing Frame problem (section)

== Solutions ==
The following solutions depict how the frame problem is solved in various formalisms. The formalisms themselves are not presented in full: what is presented are simplified versions that are sufficient to explain the full solution.

===Fluent occlusion solution===
This solution was proposed by [[Erik Sandewall]], who also defined a [[formal language]] for the specification of dynamical domains; therefore, such a domain can be first expressed in this language and then automatically translated into logic. In this article, only the expression in logic is shown, and only in the simplified language with no action names.

The rationale of this solution is to represent not only the value of conditions over time, but also whether they can be affected by the last executed action. The latter is represented by another condition, called occlusion. A condition is said to be ''occluded'' in a given time point if an action has been just executed that makes the condition true or false as an effect. Occlusion can be viewed as “permission to change”: if a condition is occluded, it is relieved from obeying the constraint of inertia.

In the simplified example of the door and the light, occlusion can be formalized by two predicates <math>\mathrm{occludeopen}(t)</math> and <math>\mathrm{occludeon}(t)</math>. The rationale is that a condition can change value only if the corresponding occlusion predicate is true at the next time point. In turn, the occlusion predicate is true only when an action affecting the condition is executed.

:<math>\neg \mathrm{open}(0)</math>
:<math>\neg \mathrm{on}(0)</math>
:<math>\mathrm{open}(1) \wedge \mathrm{occludeopen}(1)</math>
:<math>\forall t . \neg \mathrm{occludeopen}(t) \implies (\mathrm{open}(t-1) \iff \mathrm{open}(t))</math>
:<math>\forall t . \neg \mathrm{occludeon}(t) \implies (\mathrm{on}(t-1) \iff \mathrm{on}(t))</math>

In general, every action making a condition true or false also makes the corresponding occlusion predicate true. In this case, <math>\mathrm{occludeopen}(1)</math> is true, making the antecedent of the fourth formula above false for <math>t=1</math>; therefore, the constraint that <math>\mathrm{open}(t-1) \iff \mathrm{open}(t)</math> does not hold for <math>t=1</math>. Therefore, <math>\mathrm{open}</math> can change value, which is also what is enforced by the third formula.

In order for this condition to work, occlusion predicates have to be true only when they are made true as an effect of an action. This can be achieved either by [[Circumscription (logic)|circumscription]] or by predicate completion. It is worth noticing that occlusion does not necessarily imply a change: for example, executing the action of opening the door when it was already open (in the formalization above) makes the predicate <math>\mathrm{occludeopen}</math> true and makes <math>\mathrm{open}</math> true; however, <math>\mathrm{open}</math> has not changed value, as it was true already.

===Predicate completion solution===
This encoding is similar to the fluent occlusion solution, but the additional predicates denote change, not permission to change. For example, <math>\mathrm{changeopen}(t)</math> represents the fact that the predicate <math>\mathrm{open}</math> will change from time <math>t</math> to <math>t+1</math>. As a result, a predicate changes if and only if the corresponding change predicate is true. An action results in a change if and only if it makes true a condition that was previously false or vice versa.

:<math>\neg \mathrm{open}(0)</math>
:<math>\neg \mathrm{on}(0)</math>
:<math>\neg \mathrm{open}(0) \implies \mathrm{changeopen}(0)</math>
:<math>\forall t. \mathrm{changeopen}(t) \iff (\neg \mathrm{open}(t) \iff \mathrm{open}(t+1))</math>
:<math>\forall t. \mathrm{changeon}(t) \iff (\neg \mathrm{on}(t) \iff \mathrm{on}(t+1))</math>

The third formula is a different way of saying that opening the door causes the door to be opened. Precisely, it states that opening the door changes the state of the door if it had been previously closed. The last two conditions state that a condition changes value at time <math>t</math> if and only if the corresponding change predicate is true at time <math>t</math>. To complete the solution, the time points in which the change predicates are true have to be as few as possible, and this can be done by applying predicate completion to the rules specifying the effects of actions.

===Successor state axioms solution===
The value of a condition after the execution of an action can be determined by
the fact that the condition is true if and only if:

# the action makes the condition true; or
# the condition was previously true and the action does not make it false.

A [[successor state axiom]] is a formalization in logic of these two facts. For
example, if <math>\mathrm{opendoor}(t)</math> and <math>\mathrm{closedoor}(t)</math> are two
conditions used to denote that the action executed at time <math>t</math> was
to open or close the door, respectively, the running example is encoded as
follows.

: <math>\neg \mathrm{open}(0)</math>
: <math>\neg \mathrm{on}(0)</math>
: <math>\mathrm{opendoor}(0)</math>
: <math>\forall t . \mathrm{open}(t+1) \iff \mathrm{opendoor}(t) \vee (\mathrm{open}(t) \wedge \neg \mathrm{closedoor}(t))</math>

This solution is centered around the value of conditions, rather than the
effects of actions. In other words, there is an axiom for every condition,
rather than a formula for every action. Preconditions to actions (which are not
present in this example) are formalized by other formulae. The successor state
axioms are used in the variant to the [[situation calculus]] proposed by
[[Ray Reiter]].

===Fluent calculus solution===
The [[fluent calculus]] is a variant of the situation calculus. It solves the frame problem by using first-order logic [[First-order logic#Formation rules|terms]], rather than [[Predicate variable|predicates]], to represent the states. Converting predicates into terms in first-order logic is called [[Reification (knowledge representation)|reification]]; the fluent calculus can be seen as a logic in which predicates representing the state of conditions are reified.

The difference between a predicate and a term in first-order logic is that a term is a representation of an object (possibly a complex object composed of other objects), while a predicate represents a condition that can be true or false when evaluated over a given set of terms.

In the fluent calculus, each possible state is represented by a term obtained by composition of other terms, each one representing the conditions that are true in state. For example, the state in which the door is open and the light is on is represented by the term <math>\mathrm{open} \circ \mathrm{on}</math>. It is important to notice that a term is not true or false by itself, as it is an object and not a condition. In other words, the term <math>\mathrm{open} \circ \mathrm{on}</math> represent a possible state, and does not by itself mean that this is the current state. A separate condition can be stated to specify that this is actually the state at a given time, e.g., <math>\mathrm{state}(\mathrm{open} \circ \mathrm{on}, 10)</math> means that this is the state at time <math>10</math>.

The solution to the frame problem given in the fluent calculus is to specify the effects of actions by stating how a term representing the state changes when the action is executed. For example, the action of opening the door at time 0 is represented by the formula:

: <math>\mathrm{state}(s \circ \mathrm{open}, 1) \iff \mathrm{state}(s,0)</math>

The action of closing the door, which makes a condition false instead of true, is represented in a slightly different way:

: <math>\mathrm{state}(s, 1) \iff \mathrm{state}(s \circ \mathrm{open}, 0)</math>

This formula works provided that suitable axioms are given about <math>\mathrm{state}</math> and <math>\circ</math>, e.g., a term containing the same condition twice is not a valid state (for example, <math>\mathrm{state}(\mathrm{open} \circ s \circ \mathrm{open}, t)</math> is always false for every <math>s</math> and <math>t</math>).

===Event calculus solution===
The [[event calculus]] uses terms for representing fluents, like the fluent calculus, but also has one or more axioms constraining the value of fluents, like the successor state axioms. There are many variants of the event calculus, but one of the simplest and most useful employs a single axiom to represent the law of inertia:

:<math>\mathit{holdsAt}(F,T2) \leftarrow</math>
:<math>[\mathit{happensAt}(E1,T1) \wedge \mathit{initiates}(E1, F, T1) \wedge (T1 < T2) \wedge </math>
:<math>\neg \exists E2, T [\mathit{happensAt}(E2, T) \wedge \mathit{terminates}(E2, F, T) \wedge (T1 \leq T < T2)] </math>

The axiom states that a fluent <math>F</math> holds at a time <math>T2</math>,  if an event <math>E1</math> happens and initiates <math>F</math> at an earlier time <math>T1</math>, and there is no event <math>E2</math>  that happens and terminates <math>F</math>  after or at the same time as <math>T1</math> and before <math>T2</math>.

To apply the event calculus to a particular problem domain, it is necessary to define the <math>initiates</math> and <math>terminates</math> predicates for that domain. For example:

:<math>\mathit{initiates}(opendoor, open, T). </math>
:<math>\mathit{terminates}(opendoor, closed, T). </math>
:<math>\mathit{initiates}(closedoor, closed, T). </math>
:<math>\mathit{terminates}(closeddoor, open, T). </math>

To apply the event calculus to a particular problem in the domain, it is necessary to specify the events that happen in the context of the problem. For example:

: <math>\mathit{happensAt}(opendoor, 0)</math>. 
: <math>\mathit{happensAt}(closedoor, 3)</math>.

To solve a problem, such as ''which fluents hold at time 5?'', it is necessary to pose the problem as a goal, such as:

:<math> \exists Fluent [\mathit{holdsAt(Fluent, 5)}]. </math>

In this case, obtaining the unique solution:

:<math>Fluent = closed. </math>

The event calculus solves the frame problem, eliminating undesired solutions, by using a [[non-monotonic logic]], such as first-order logic with [[Circumscription (logic)|circumscription]]<ref>Shanahan, M. (1997) ''[https://books.google.com/books?id=z8zR3Ds7xKQC Solving the frame problem: A mathematical investigation of the common sense law of inertia]''. MIT Press.</ref> or by treating the event calculus as a [[logic programming|logic program]] using [[negation as failure]].

===Default logic solution===
The frame problem can be thought of as the problem of formalizing the principle that, by default, "everything is presumed to remain in the state in which it is" ([[Gottfried Wilhelm Leibniz|Leibniz]], "An Introduction to a Secret Encyclopædia", ''c''. 1679).  This default, sometimes called the ''commonsense law of inertia'', was expressed by [[Raymond Reiter]] in [[default logic]]:

: <math>\frac{R(x,s)\; :\ R(x,\mathrm{do}(a,s))}{R(x,\mathrm{do}(a,s))}</math>

(if <math>R(x)</math> is true in situation <math>s</math>, and it can be assumed<ref>i.e., no contradicting information is known</ref> that <math>R(x)</math> remains true after executing action <math>a</math>, then we can conclude that <math>R(x)</math> remains true).

Steve Hanks and [[Drew McDermott]] argued, on the basis of their [[Yale shooting problem|Yale shooting]] example, that this solution to the frame problem is unsatisfactory.  Hudson Turner showed, however, that it works correctly in the presence of appropriate additional postulates.

===Answer set programming solution===
The counterpart of the default logic solution in the language of [[answer set programming]] is a rule with [[stable model semantics#Strong negation|strong negation]]:

:<math>r(X,T+1) \leftarrow r(X,T),\ \hbox{not }\sim r(X,T+1)</math>

(if <math>r(X)</math> is true at time <math>T</math>, and it can be assumed that <math>r(X)</math> remains true at time <math>T+1</math>, then we can conclude that <math>r(X)</math> remains true).

=== Separation logic solution ===
[[Separation logic]] is a formalism for reasoning about computer programs using pre/post specifications of the form <math>\{\mathrm{precondition}\}\ \mathrm{code}\ \{\mathrm{postcondition}\}</math>. Separation logic is an extension of [[Hoare logic]] oriented to  reasoning about mutable data structures in computer memory and other dynamic resources, and it has a special connective *, pronounced "and separately", to support independent reasoning about disjoint memory regions.<ref>{{Cite book|last=Reynolds|first=J.C.|title=Proceedings 17th Annual IEEE Symposium on Logic in Computer Science |chapter=Separation logic: A logic for shared mutable data structures |date=2002|location=Copenhagen, Denmark|publisher=IEEE Comput. Soc|pages=55–74|doi=10.1109/LICS.2002.1029817|citeseerx=10.1.1.110.7749|isbn=978-0-7695-1483-3|s2cid=6271346}}</ref><ref>{{Cite journal|last=O'Hearn|first=Peter|date=2019-01-28|title=Separation logic|journal=[[Communications of the ACM]]|language=en|volume=62|issue=2|pages=86–95|doi=10.1145/3211968|issn=0001-0782|doi-access=free}}</ref>

Separation logic employs a ''tight'' interpretation of pre/post specs, which say that the code can ''only'' access memory locations guaranteed to exist by the precondition.<ref>{{Cite book|last1=O’Hearn|first1=Peter|last2=Reynolds|first2=John|last3=Yang|first3=Hongseok|date=2001|editor-last=Fribourg|editor-first=Laurent|chapter=Local Reasoning about Programs that Alter Data Structures|title=Computer Science Logic|volume=2142|series=Lecture Notes in Computer Science|language=en|location=Berlin, Heidelberg|publisher=Springer|pages=1–19|doi=10.1007/3-540-44802-0_1|isbn=978-3-540-44802-0}}</ref> This leads to the soundness of the most important inference rule of the logic, the ''frame rule''

<math>\frac{ \{\mathrm{precondition}\}\ \mathrm{code}\ \{\mathrm{postcondition}\} }{ \{\mathrm{precondition} \ast \mathrm{frame}\}\ \mathrm{code}\ \{\mathrm{postcondition} \ast \mathrm{frame}\} }</math>

The frame rule  allows descriptions of arbitrary memory outside the footprint (memory accessed) of the code to be added to a specification: this enables the initial specification to concentrate only on the footprint.  For example, the inference

<math>\frac{ \{\operatorname{list}(x)\}\ \mathrm{code}\ \{\operatorname{sortedlist}(x)\} }{ \{\operatorname{list}(x) \ast \operatorname{sortedlist}(y)\}\ \mathrm{code}\ \{\operatorname{sortedlist}(x) \ast \operatorname{sortedlist}(y)\} }</math>

captures that code which sorts a list ''x'' does not unsort a separate list ''y,'' and it does this without mentioning ''y'' at all in the initial spec above the line.

Automation of the frame rule has led to significant increases in the scalability of automated reasoning techniques for code,<ref>{{Cite journal|last1=Calcagno Cristiano|last2=Dino Distefano|last3=Peter O'Hearn|last4=Hongseok Yang|date=2011-12-01|title=Compositional Shape Analysis by Means of Bi-Abduction|journal=[[Journal of the ACM]]|language=EN|volume=58|issue=6|pages=1–66|doi=10.1145/2049697.2049700|s2cid=52808268|url=https://ora.ox.ac.uk/objects/uuid:bcfefe74-a79c-4155-8160-c51f92f05466}}</ref> eventually deployed industrially to codebases with tens of millions of lines.<ref>{{Cite journal|first1=Dino |last1=Distefano|first2=Manuel |last2=Fähndrich|first3=Francesco |last3=Logozzo|first4=Peter |last4=O'Hearn|date=2019-07-24|title=Scaling static analyses at Facebook|journal=Communications of the ACM|language=EN|volume=62|issue=8|pages=62–70|doi=10.1145/3338112|doi-access=free}}</ref>

There appears to be some similarity between the separation logic solution to the frame problem and that of the fluent calculus mentioned above.{{explain|date=May 2022}}

===Action description languages===
[[Action description language]]s elude the frame problem rather than solving it. An action description language is a formal language with a syntax that is specific for describing situations and actions. For example, that the action <math>\mathrm{opendoor}</math> makes the door open if not locked is expressed by:

: <math>\mathrm{opendoor}</math> causes <math>\mathrm{open}</math> if <math>\neg \mathrm{locked}</math>

The semantics of an action description language depends on what the language can express (concurrent actions, delayed effects, etc.) and is usually based on [[transition system]]s.

Since domains are expressed in these languages rather than directly in logic, the frame problem only arises when a specification given in an action description logic is to be translated into logic. Typically, however, a translation is given from these languages to [[answer set programming]] rather than first-order logic.