フレーム問題

この解決策は、動的ドメインの仕様記述のための形式言語も定義したErik Sandewall氏によって提案されました。そのため、このようなドメインはまずこの言語で表現され、その後自動的に論理に変換されます。この記事では、論理式のみを示し、アクション名を含まない簡略化された言語のみを使用します。

この解決策の根拠は、時間の経過に伴う条件の値だけでなく、最後に実行されたアクションによって条件が影響を受けるかどうかも表現することにあります。後者は、オクルージョンと呼ばれる別の条件によって表現されます。条件が特定の時点でオクルージョンされているとは、その条件を真または偽にするアクションが直前に実行されたことを意味します。オクルージョンは「変更の許可」と見なすことができます。条件がオクルージョンされている場合、慣性の制約から解放されます。

ドアとライトの単純化された例では、遮蔽は2つの述語によって形式化できる。${\displaystyle \mathrm {occludeopen} (t)}$そして${\displaystyle \mathrm {オクルーデオン} (t)}$その理由は、条件の値が変わるのは、対応するオクルージョン述語が次の時点で真である場合に限られるからである。そして、オクルージョン述語は、条件に影響を与えるアクションが実行された場合にのみ真となる。

${\displaystyle \neg \mathrm {開く} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \mathrm {open} (1)\wedge \mathrm {occludeopen} (1)}$

${\displaystyle \forall t.\neg \mathrm {occludeopen} (t)\implies (\mathrm {open} (t-1)\iff \mathrm {open} (t))}$

${\displaystyle \forall t.\neg \mathrm {occludeon} (t)\implies (\mathrm {on} (t-1)\iff \mathrm {on} (t))}$

一般的に、条件を真または偽にするすべてのアクションは、対応する遮蔽述語も真にします。この場合、${\displaystyle \mathrm {occludeopen} (1)}$が真であるため、上記の第4式の前件は偽となる。${\displaystyle t=1}$したがって、制約は次のようになります。${\displaystyle \mathrm {open} (t-1)\iff \mathrm {open} (t)}$当てはまらない${\displaystyle t=1}$。 したがって、${\displaystyle \mathrm {開く} }$値を変更することができ、それは3番目の式によって強制されるものでもある。

この条件が機能するためには、オクルージョン述語は、アクションの結果として真になった場合にのみ真でなければなりません。これは、限定または述語の補完によって実現できます。オクルージョンは必ずしも変化を意味するわけではないことに注意が必要です。たとえば、既に開いているドアを開けるアクションを実行すると（上記の形式化において）、述語は${\displaystyle \mathrm {occludeopen} }$真実であり、${\displaystyle \mathrm {開く} }$確かにそうですが、${\displaystyle \mathrm {開く} }$価値は変わっていません。なぜなら、それは既に真実だったからです。

このエンコーディングは流暢なオクルージョンソリューションに似ていますが、追加の述語は変更の許可ではなく変更を表します。たとえば、${\displaystyle \mathrm {changeopen} (t)}$述語が事実を表している${\displaystyle \mathrm {開く} }$時間の経過とともに変化する${\displaystyle t}$に${\displaystyle t+1}$結果として、述語が変化するのは、対応する変化述語が真である場合に限る。アクションが変化をもたらすのは、それが以前は偽であった条件を真にする場合、またはその逆の場合に限る。

${\displaystyle \neg \mathrm {開く} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \neg \mathrm {open} (0)\implies \mathrm {changeopen} (0)}$

${\displaystyle \forall t.\mathrm {changeopen} (t)\iff (\neg \mathrm {open} (t)\iff \mathrm {open} (t+1))}$

${\displaystyle \forall t.\mathrm {changeon} (t)\iff (\neg \mathrm {on} (t)\iff \mathrm {on} (t+1))}$

3つ目の式は、ドアを開けるとドアが開くということを別の言い方で表現したものです。正確には、ドアが以前に閉まっていた場合、ドアを開けるとドアの状態が変わると述べています。最後の2つの条件は、ある時点で条件の値が変わることを示しています。${\displaystyle t}$対応する変化述語が時刻において真である場合に限る${\displaystyle t}$解決策を完成させるには、変更述語が真となる時点をできるだけ少なくする必要があり、これはアクションの効果を指定するルールに述語補完を適用することで実現できます。

アクション実行後の条件の値は、条件が真となるのは、以下の条件が満たされる場合のみであるという事実によって決定されます。

1. その行為によって条件が真になる。または
2. その条件は以前は真であり、その行為によって偽になるわけではない。

後継状態公理は、これら2つの事実を論理的に形式化したものである。例えば、${\displaystyle \mathrm {opendoor} (t)}$そして${\displaystyle \mathrm {closedoor} (t)}$は、時刻に実行されたアクションを示すために使用される 2 つの条件です。${\displaystyle t}$ドアを開閉する場合、実行例は次のようにエンコードされます。

${\displaystyle \neg \mathrm {開く} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \mathrm {オープンドア} (0)}$

${\displaystyle \forall t.\mathrm {open} (t+1)\iff \mathrm {opendoor} (t)\vee (\mathrm {open} (t)\wedge \neg \mathrm {closedoor} (t))}$

この解決策は、行動の結果ではなく、条件の価値を中心に据えています。言い換えれば、すべての行動に公式があるのではなく、すべての条件に公理があります。行動の前提条件（この例には含まれていません）は、別の公式によって形式化されます。後継状態の公理は、レイ・ライターが提案した 状況計算の変種で使用されます。

流暢な計算は、状況計算の一種です。これは、状態を表すのに述語ではなく一階述語論理の項を用いることで、フレーム問題を解決します。一階述語論理において述語を項に変換することを実体化と呼びます。流暢な計算は、条件の状態を表す述語が実体化される論理体系と見なすことができます。

一階述語論理における述語と項の違いは、項は対象（他の対象から構成される複雑な対象である場合もある）を表すものであるのに対し、述語は与えられた項の集合に対して評価された際に真偽を判定できる条件を表すという点にある。

流暢な計算では、各可能な状態は、他の項の合成によって得られる項で表され、各項は状態において真である条件を表します。たとえば、ドアが開いていてライトが点灯している状態は、次の項で表されます。${\displaystyle \mathrm {open} \circ \mathrm {on} }$用語はそれ自体では真偽を判断できないことに注意することが重要です。なぜなら、用語は条件ではなく対象だからです。言い換えれば、用語は${\displaystyle \mathrm {open} \circ \mathrm {on} }$これは可能な状態を表しており、それ自体が現在の状態であることを意味するものではありません。これが特定の時点での実際の状態であることを指定するには、別の条件を記述することができます。例:${\displaystyle \mathrm {state} (\mathrm {open} \circ \mathrm {on} ,10)}$これは時刻における状態であることを意味します${\displaystyle 10}$。

流暢な微積分で提示されるフレーム問題の解決策は、状態を表す項が動作の実行時にどのように変化するかを記述することによって、動作の効果を指定することです。例えば、時刻 0 でドアを開ける動作は、次の式で表されます。

${\displaystyle \mathrm {state} (s\circ \mathrm {open} ,1)\iff \mathrm {state} (s,0)}$

ドアを閉めるという行為は、条件を真から偽に変えるものであり、少し異なる方法で表現されます。

${\displaystyle \mathrm {state} (s,1)\iff \mathrm {state} (s\circ \mathrm {open} ,0)}$

この公式は、適切な公理が与えられている場合に有効です。${\displaystyle \mathrm {状態} }$そして${\displaystyle \circ }$例えば、同じ条件を2回含む用語は有効な状態ではありません（例えば、${\displaystyle \mathrm {state} (\mathrm {open} \circ s\circ \mathrm {open} ,t)}$は常に偽である${\displaystyle s}$そして${\displaystyle t}$)

イベント計算は、フルーエント計算と同様に、フルーエントを表すための用語を使用しますが、後継状態公理のように、フルーエントの値を制約する1つ以上の公理も持ちます。イベント計算には多くのバリエーションがありますが、最も単純で有用なものの1つは、慣性の法則を表すために単一の公理を使用します。

${\displaystyle {\mathit {holdsAt}}(F,T2)\leftarrow }$

${\displaystyle [{\mathit {happensAt}}(E1,T1)\wedge {\mathit {initiates}}(E1,F,T1)\wedge (T1<T2)\wedge }$

${\displaystyle \neg \exists E2,T[{\mathit {happensAt}}(E2,T)\wedge {\mathit {terminates}}(E2,F,T)\wedge (T1\leq T<T2)]}$

この公理は、流暢な${\displaystyle F}$一度に保持する${\displaystyle T2}$イベントが発生した場合${\displaystyle E1}$発生し、開始する${\displaystyle F}$以前の時代に${\displaystyle T1}$、イベントはありません${\displaystyle E2}$ それは起こり、そして終わる。${\displaystyle F}$ 後または同時に${\displaystyle T1}$そしてその前に${\displaystyle T2}$。

イベント計算を特定の問題領域に適用するには、${\displaystyle initiates}$そして${\displaystyle terminates}$そのドメインの述語。例：

${\displaystyle {\mathit {initiates}}(opendoor,open,T).}$

${\displaystyle {\mathit {terminates}}(opendoor,closed,T).}$

${\displaystyle {\mathit {initiates}}(closedoor,closed,T).}$

${\displaystyle {\mathit {terminates}}(closeddoor,open,T).}$

イベント計算を特定の問題に適用するには、その問題のコンテキストで発生するイベントを指定する必要があります。例えば、次のようになります。

${\displaystyle {\mathit {happensAt}}(opendoor,0)}$。

${\displaystyle {\mathit {happensAt}}(closedoor,3)}$。

「時刻5においてどのフルエントが成り立つか？」といった問題を解決するには、問題を目標として設定する必要がある。例えば、次のように。

${\displaystyle \exists Fluent[{\mathit {holdsAt(Fluent,5)}}].}$

この場合、唯一の解を得るには：

${\displaystyle Fluent=closed.}$

イベント計算は、非単調論理（一階述語論理と限定^{[ 3 ]}など）を使用したり、イベント計算を否定を失敗として用いる論理プログラムとして扱ったりすることで、望ましくない解を排除し、フレーム問題を解決します。

フレーム問題は、「すべてのものは現状のままであると想定される」（ライプニッツ『秘密百科事典序論』、 1679年頃）という原則を形式化する問題と考えることができる。このデフォルトは、慣性の常識法則と呼ばれることもあり、レイモンド・ライターによってデフォルト論理で表現された。

${\displaystyle {\frac {R(x,s)\;:\ R(x,\mathrm {do} (a,s))}{R(x,\mathrm {do} (a,s))}}}$

（もし${\displaystyle R(x)}$状況において真実である${\displaystyle s}$、そして^{[ 4 ]}は${\displaystyle R(x)}$アクション実行後も真のまま${\displaystyle a}$すると、次の結論が得られます。${\displaystyle R(x)}$（依然として真実である）。

スティーブ・ハンクスとドリュー・マクダーモットは、イェール大学の射撃実験を例に挙げ、この枠組み問題の解決策は不十分であると主張した。しかし、ハドソン・ターナーは、適切な追加公理が存在する場合には、この解決策が正しく機能することを示した。

回答集合プログラミング言語におけるデフォルト論理ソリューションの対応物は、強い否定を持つルールである。

${\displaystyle r(X,T+1)\leftarrow r(X,T),\ {\hbox{not }}\sim r(X,T+1)}$

（もし${\displaystyle r(X)}$時には真実である${\displaystyle T}$、そして、${\displaystyle r(X)}$その時も真実であり続ける${\displaystyle T+1}$すると、次の結論が得られます。${\displaystyle r(X)}$（依然として真実である）。

分離論理は、次の形式の事前/事後仕様を使用してコンピュータプログラムについて推論するための形式体系である。${\displaystyle \{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}}$分離論理は、コンピュータメモリやその他の動的リソース内の可変データ構造に関する推論を目的としたホーア論理の拡張であり、分離メモリ領域に関する独立した推論をサポートするために、「and separate」と発音される特別な接続子*を備えています。^{[ 5 ] [ 6 ]}

分離論理では、事前/事後仕様を厳密に解釈し、コードは事前条件によって存在が保​​証されたメモリ位置にのみアクセスできると規定する。 ^{[ 7 ]}これにより、この論理で最も重要な推論規則であるフレーム規則の健全性が保証される。

${\displaystyle {\frac {\{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}}{\{\mathrm {precondition} \ast \mathrm {frame} \}\ \mathrm {code} \ \{\mathrm {postcondition} \ast \mathrm {frame} \}}}}$

フレームルールでは、コードのフットプリント（アクセスされたメモリ）外の任意のメモリの説明を仕様に追加できます。これにより、初期仕様はフットプリントのみに集中できます。たとえば、推論

${\displaystyle {\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)\}}}}$

リストxをソートするコードは、別のリストyをアンソートしないということを捉えており、上記の最初の仕様ではyについて全く言及していません。

フレームルールの自動化により、コードに対する自動推論技術のスケーラビリティが大幅に向上し、 ^{[ 8 ]}最終的には数千万行のコードベースに産業的に展開されました。^{[ 9 ]}

フレーム問題に対する分離論理による解決策と、上述の流暢な計算の解決策には、何らかの類似点があるように思われる。

動作記述言語は、フレーム問題を解決するのではなく、むしろ回避する。動作記述言語は、状況や動作を記述するための構文を持つ形式言語である。例えば、動作が${\displaystyle \mathrm {opendoor} }$ロックされていない場合にドアを開ける動作は、次のように表現されます。

${\displaystyle \mathrm {opendoor} }$原因${\displaystyle \mathrm {open} }$もし${\displaystyle \neg \mathrm {locked} }$

動作記述言語の意味論は、その言語が何を表現できるか（同時動作、遅延効果など）に依存し、通常は遷移システムに基づいています。

ドメインは論理ではなくこれらの言語で表現されるため、フレーム問題は、アクション記述論理で与えられた仕様を論理に変換する場合にのみ発生します。ただし、通常、これらの言語から一階述語論理ではなく、応答集合プログラミングへの変換が行われます。