ゴールと規則 - (保存用) 檜山正幸のキマイラ飼育記メモ編

どうにもならないなーー(溜め息)

「除去規則の適用」のレゾリューションアルゴリズムの圏的意味論を考えてみたが、これは複雑。なのに、Isabelleのなかでは天下り。これでは納得出来るわけがない！

それはそうと、ポールソンは、メインゴールとサブゴールズとしてゴール概念を区別している。ところが、メインゴールは定理のステートメントに対応するゴールと、相対的な親ゴールの意味がある。それでさらに、ファイナルゴールとかいう用語を導入せざるを得ない。

「親ゴール、子ゴールリスト」がプレーンでいいような気もする。で、親ゴールを子ゴールリストに展開する操作をなんというか？これが、chainだったり、refineだったり、resolveだったり、solveだったり（名詞： chaining, refinement, resolution, solution）。

グラフ操作としては、境界を保つグラフ書き換えをして、書き換え後のグラフから未知ノード（これがゴール）を選び出して並べたものが子ゴールリストになる。

グラフ書き換え規則やグラフ書き換えの全体像に対して何の言及もなく、ゴール→子ゴールリストの変換を天下りに出しているから意味不明となる。肝心なことは説明しないで天下りに押し付ける、という教育上最もマズイ方法が伝統化／習慣化してしまっているわけだ。

[追記]

Coqのときもゴールは相当にワケワカだったが、Isabelleのときは次の4つをいずれもゴールと呼ぶ。

(1)親ゴール 結論(2)
展開
(3)子ゴールのリスト
   (4)子ゴール (4)結論

証明の対象となる命題のシーケント風表現
そのシーケント風表現の右辺の論理式
あるゴールから展開された子ゴールのリスト
各々の子ゴール
子ゴールの結論

ゴール（シーケント風表現）の各部の名前

左辺はコンテキスト、仮定、仮説など色々
右辺は結論でだいたい統一されている

ゴールの内部表現は、HHF（Hereditary Harrop Formula）で、MLレベルではthm（定理）データ。HHFについては、

[/追記]