kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (9) 「2 もう少し、いつものゲームを」

littleprover

ifの公理が出てきます
ifでは数ではなくてQ、A、Eで置き換え対象を指定します

  • (if 't x y)とxは等しい (if-true)
  • (if 'nil x y)とyは等しい (if-false)
  • (if x y y)とyは等しい (if-same)

3つめ公理はどうやって使うんでしょうか

(dethm if-same (x y) (equal (if x y y) y))

次はEqualの公理に含められていますがifとも関係あり
日本語にしてしまうと意味が取れなくなってしまうのでそのまま

(dethm equal-if (x y) (if (equal x y) (equal x y) 't))

'tってなんだよ'tって、と思いましたがこれはたぶん定理は常に'tでないと
いけないので入れてあるってことでしょう

このequal-ifを適用するためにDethmの法則が更新されてます
文章で読むとちょっとわかりづらいですが
(if X (equal Y Y') ...)という公理があれば
(if X (... Y ...) ...)を(if X (... Y' ...) ...)に、
(if X ... (equal Z Z'))という公理があれば
(if X ... (... Z ...))を(if X ... (... Z' ...))に
置き換えられるということ
例をあげて1ステップずつ順番にやってくれますので進めばわかります

次の場合、置き換えた結果であるbody(e)を使ってフォーカスの書き換えができる

は「body(e)に含まれる帰結を使ってフォーカスの書き換えができる」てことですね
最初ここが飲み込めませんでした

equal-ifの公理でEqualの公理が完成します
推移律じゃなかったか
でも推移律作れそう
andはないからこう・・・

  (if (equal x y) (if (equal y z) (equal x z) 't) 't)
= (if (equal x y) (if (equal z y) (equal x z) 't) 't)
= (if (equal x y) (if (equal z y) (equal y y) 't) 't)
= (if (equal x y) (if (equal z y) 't 't) 't)
= (if (equal x y) 't 't)
= 't

かな？

> (J-Bob/step (my/prelude)
    '(if (equal x y) (if (equal y z) (equal x z) 't) 't)
    '(((A Q) (equal-swap y z))
      ((A A 1) (equal-if x y))
      ((A A 2) (equal-if z y))
      ((A A) (equal-same y))
      ((A) (if-same (equal z y) 't))
      (() (if-same (equal x y) 't))))
't

いけた

じゃあmy/axiomsにこうやって公理を付け加えたら

(defun my/axioms ()
     :
     :
    (dethm equal-trans (x y z)
      (if (equal x y) (if (equal y z) (equal x z) 't) 't))))

(if (equal a b) (if (equal b c) a b) c)みたいなのを
(if (equal a b) (if (equal b c) c b) c)のように置き換えられたりするかな？

> (J-Bob/step (my/prelude)
    '(if (equal a b) (if (equal b c) a b) c)
    '(((A A) (equal-trans a b c))))
(if (equal a b) (if (equal b c) c b) c)

できた

あてずっぽうでもけっこう動くもんだなと思ってjabberwockyも動かしてみようと
思いましたが悪戦苦闘のあげくうまくいきませんでした
ちゃんとわかってきたらできるのかな？

なお

(equal 'nil 'nil)を'tに置き換えるのにequal-sameは必要でしょうか？
そんなことはありません。'nilは値なので、関数equalの定義がそのまま使えました。

こういう場合は公理で置き換えても、単に関数適用してもどっちでもいいってことですね
疑問氷解しました

Consの公理を追加

  • xがアトムでなければ、xと(cons (car x) (cdr x))は等しい (cons/car+cdr)

Ifの公理も追加

  • xならば(if x y z)とyは等しい (if-nest-A)
  • xでなければ(if x y z)とzは等しい (if-nest-E)

it-trueやif-falseと意味は似てますがxを'tや'nilに変形することなく
置き換えられます

if-sameなんてどう使うのかと思いましたが
if-nest-Aやif-nest-Eと組み合わせるとこんなことができたり

  (A (if B C D) (if B E F))
= (if B (A (if B C D) (if B E F)) (A (if B C D) (if B E F)))) [if-same]
= (if B (A C E) (A D F)) [if-nest-A, if-nest-E]

式を簡単にするのではなくて式を増やす方向で活躍する模様
奥が深い

これでCons、Ifの公理も完成
本文と付録Aと付録Bをいったりきたりしながら読むのが忙しい