イェール射撃問題

イェール射撃問題（イェールしゃげきもんだい、英: Yale shooting problem）とは、形式的状況分析におけるあるシナリオであり、フレーム問題に対する初期の論理学的アプローチが解けなかった難問である。名称はこの問題の発案者スティーブ・ハンクス、ドリュー・マクダーモット（英語版）がイェール大学に所属していたことにちなむ。シナリオは次のとおりである。最初の時点で、フレッド（後に七面鳥であるとされた）は生きていて、銃には弾丸が装填されていないものとする。銃に弾丸を装填し、少し待機し、フレッドに向けて発砲すれば、フレッドは殺されるものと想定される。ところが、変化が最小化されるべく論理学的な定式化がなされたとすると（慣性（inertia）の表現）、装填・待機・発砲という一連の動作の後にフレッドが死亡しているという結論が必ずしも導かれない。一つの帰結は、フレッドが実際に死亡しているというものである。もう一つの（論理的には正しい）帰結は、銃から弾丸が不思議と抜かれていて、フレッドは生存しているというものである（本項において「発砲（shooting）」は空砲の場合も含む）。

技術的には、このシナリオは2つのフルーエント（英語版）（時間の経過とともに真理値が変化し得る項）： $alive$ と $loaded$ で記述できる。最初、前者は真で後者は偽である。その後弾丸が装填され、しばし時間が経過し、銃が発砲される。これを論理学的に定式化するには $0$ , $1$ , $2$ , $3$ という4つの時刻と、時刻に依存した述語 $alive(t)$ , $loaded(t)$ を考えればよい。直接的に定式化すると次のようになる：

alive(0)

\neg loaded(0)

true\rightarrow loaded(1)

loaded(2)\rightarrow \neg alive(3)

最初の2つの論理式は初期状態を表す。3番目の論理式は時刻0で弾丸が装填されることを表す。4番目の論理式は時刻2でフレッドに向けて銃が発砲されること及びその帰結を表す。これは行為の名称が省略され、行為の影響がその実行時刻において直接的に特定されるような、最も単純化された定式化である（詳細は状況計算（英語版）（situation calculus）を参照）。

これらの論理式は事実を直接的に定式化したものであるが、シナリオを満足に記述できていない。実際、 $\neg alive(1)$ はこれらすべての論理式と整合的であるが、銃の発砲前にフレッドが死亡すると考えなければならない理由は全くない。問題なのは、上記の定式化には行為とその帰結しか含まれておらず、「全てのフルーエント（の真理値）は行為がなされない限り変化しない」ことが明示されていない点である。言い換えれば「弾丸の装填という行為はフルーエント $loaded$ の値のみを変えるのであって、フルーエント $alive$ の値を変えない」という暗黙の仮定を定式化するためには、追加の論理式 $alive(0)\equiv alive(1)$ が必要である。「行為によって状態が変えられない限り、状態は変わらない」という明白な事実を述べるのに無数の論理式が必要となるこの問題は、フレーム問題（の一種）として知られている。

フレーム問題への初期の解決策の一つは、変化の最小化に基づくものであった。言い換えると、上記のような定式化（行為とその帰結のみの記述）に、時間経過に伴うフルーエントの変化は可能な限り少なくあるべしという仮定を追加するというものである。論理式群によって全ての行為の実行とその結果の惹起を記述し、一方で最小化によって、全ての変化は何らかの行為によって引き起こされるものに限定する、という発想である。

イェール射撃問題では、変化数が最小となるようなフルーエントへの付値（英語版）の一つは次のようなものである。

$alive(0)$	$alive(1)$	$alive(2)$	$\neg alive(3)$
$\neg loaded(0)$	$loaded(1)$	$loaded(2)$	$loaded(3)$

これが期待される解であり、フルーエントの変化は2回である：

loaded

が時刻1で真になり、

alive

が時刻3で偽になる。

ところが次の付値も同じ条件を満たす。

$alive(0)$	$alive(1)$	$alive(2)$	$alive(3)$
$\neg loaded(0)$	$loaded(1)$	$\neg loaded(2)$	$\neg loaded(3)$

この場合もフルーエントの変化は2回である：

loaded

が時刻1で真になり、時刻2で偽になる。

結果的にこのような評価も状態変化の有効な記述ではあるが、しかし、時刻2で $loaded$ が偽になることを説明する妥当な理由は何もない。変化の最小化という制約が「誤った」解を導き得るというこの事実が、イェール射撃問題が提案される動機となった。

イェール射撃問題は動的なシナリオの形式化に論理学を用いるにあたっての深刻な障壁だと考えられてきたが、1980年代後半から解決策が知られ始めた。その一つが、動作の特定に述語完備化（predicate completion）を用いるものである。この解決策によれば、「発砲がフレッドに死をもたらす」という事実は次の前提の下で定式化されている： $alive$ と $loaded$ が真で、発生する帰結は $alive$ が真理値を変えること（つまり偽になること）であること。ここでの論理包含を同値（if and only if）に変更することで、発砲の帰結が適切に定式化できる（論理包含が複数ある場合、述語完備化はもっと複雑になる）。

Erik Sandewall（英語版）が提出した解決案は、新しい状態、オクルージョン（occlusion、直訳すれば包蔵）を採り入れるものである。これはフルーエントに対する「変化の許可（permission to change）」を定式化したものである。この案に従うと、フルーエントの値を変え得るようなある行為の帰結は、フルーエントが新しい値をとり、オクルージョンが（一時的に）真にされることである。最小化されるべきなのは変化の集合ではなく、真であるオクルージョンの集合である。これに「オクルージョンが真でない限り、フルーエントは値を変えない」という追加条件を補完することで、問題は解決される。

イェール射撃問題のシナリオは、レイモンド・ライター（英語版）版の状況計算、フルーエント計算（英語版）（fluent calculus）、アクション記述言語（英語版）（action description language,ADL）によっても適切に定式化できる。

2005年、イェール射撃問題が初めて記述された1985年の論文が AAAI Classic Paper award に選ばれた。この問題には解決策が既に与えられているものの、最近の研究論文においてもなお言及される。問題というよりは理解に役立つ例（例えば、動作の推論のための新しい論理に関する統語論 (論理学)（英語版）の説明）として用いられるのである

参考文献

M. Gelfond and V. Lifschitz (1993). Journal of Logic Programming, 17:301–322. 論理プログラミングにおける行為（動作）と変化の表現について。
S. Hanks and D. McDermott (1987). Artificial Intelligence, 33(3):379–412. 非単調論理と時間射影（temporal projection）について。
J. McCarthy (1986). Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence, 28:89–116.
T. Mitchell and H. Levesque (2006). The 2005 AAAI Classic Paper awards. "AI Magazine", 26(4):98–99.
R. Reiter (1991). The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In Vladimir Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 359–380. Academic Press, New York.
E. Sandewall (1994). Features and Fluents. Oxford University Press.

参考文献

関連項目