定理証明手習い (83) Dethmの法則?
具体的な形になった定理をつかう前に、
follow-prems
で延滞をチェックする必要があります。このチェックにより、等しいことが証明可能な2つの式を表す具体的な帰結が、等式として得られます。
わかったようなわからないような
(equal (car (cons 'a 'b)) 'a)
みたいな式が得られる、ってことですかね
follow-prems
から見てみます
(defun follow-prems (path e thm)
(if (if? thm)
(if (prem-A? (if.Q thm) path e)
(follow-prems path e (if.A thm))
(if (prem-E? (if.Q thm) path e)
(follow-prems path e (if.E thm))
thm))
thm))
thm
は定理でしょうね
path
はe
におけるフォーカスを表してるんでしょうがe
はなんでしょうか
thm
とe
の関係は?
e
がthm
の証明?
thm
がif
じゃなければなにもしないでthm
をそのまま返す
if
だったら
Q部がprem-A
ならA部のfollow-prems
を返す
Q部がprem-E
ならE部のfollow-prems
を返す
どちらでもなければthm
をそのまま返す
A部やE部をたどって何かしている、くらいしかわかりません
prem-A?
とprem-E?
を見てみます
ほとんど同じなのでprem-A?
の方を
(defun prem-A? (prem path e)
(if (atom path)
'nil
(if (equal (car path) 'A)
(if (equal (if.Q e) prem)
't
(prem-A? prem (cdr path)
(find-focus-at-direction (car path) e)))
(prem-A? prem (cdr path)
(find-focus-at-direction (car path) e)))))
prem
にはthm
のQ部が入ってきます
premというからにはきっと前提となるもの
path
の先頭が'A
で、e
のQ部がprem
と等しいなら't
例で考えてみる
prem
が(equal x 'b)
path
が(A 2 A ...)
e
が(if (equal x 'a) (equal 't (if (equal x 'b) (equal y 'b) (equal y 'c))) (equal y 'd))
なら
まずはprem
と(equal x 'a)
を比較
一致しないからA部 (equal 't (if (equal x 'b) (equal y 'b)))
を見る
path
の先頭が'A
ではないので
'2
が示す(if (equal x 'b) (equal y 'b))
を見る
prem
と(equal x 'b)
が一致しているので't
これは何をやってることになるのかな
あるパスのA部に、指定された前提と同じQ部があるかどうかを確認している
Dethmの法則のことかな?
- その帰結が
if
のAnswer部(あるいはElse部)に含まれているなら、書き換え対象のフォーカスも同じQuestion部を持つif
のAnswer部(あるいはElse部)に含まれていなければならない。
premise(前提)らしき言葉は出てこないけど
〜なければならない、の部分には一致してそう
path
の示す部分式が、prem
の示す条件に合った場所にあるかどうかってことだな
てところでfollow-prems
に戻ると
path
の示す部分式が、thm
のQ部の示す条件に合った場所にあるかどうか
ってことか
follow-prems
の再帰はif
の入れ子に対応しているんだな
まだちょっと完全には理解してないけどこれくらいで先に進もう