kb84tkhrのブログ

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

定理証明手習い (44) set?/atomsの証明

set?/atomの定理に戻りましょう。

え、そっち?
set?/tとかset?/nilは?

この定理の証明は、ちょっとだけ意外で、ちょっとだけ楽しく、ちょっとだけで終わります。

set?/add-atomsの特殊ケースにすぎないのでちょっとだけで終わりそうな予感はしますが
意外で楽しい、とは?

何かしら前提が必要です。そこで、if-trueの公理を使いましょう。
if-trueの公理を使うことで、必要なときにいつでも前提を導入できます。

ふむ
わかるけど
といっても'tではねえ

次の式の前提を(set? '())にしたいのですが、どうすれば't(set? '())に書き換えられるんでしょう?

(if 't 
    (equal (set? (add-atoms a '())) 't) 
    't)

なるほど?
なんか昔そういうことやりたかった気がしないでもない
あきらめたけど

if-trueの公理により、関数set?の定義の本体でxs'()としたようなAnswer部とElse部に持つif式に、'tを書き換えてみましょう。

やってることもやる意味もわかりませんがとにかくやってみましょう
関数set?の定義の本体

(if (atom xs)
    't
    (if (member? (car xs) (cdr xs))
        'nil
        (set? (cdr xs))))

xs'()とする

(if (atom '())
    't
    (if (member? (car '()) (cdr '()))
        'nil
        (set? (cdr '()))))

if-trueが使えるように(atom '())はこの時点で評価してしまう

(if 't
    't
    (if (member? (car '()) (cdr '()))
        'nil
        (set? (cdr '()))))

確かに'tな式ではある
E部はかなり無茶してる感じだけど

'tをこの式に変えるには・・・これでいいのか

(if-true 't 
         (if (member? (car '()) (cdr '()))
             'nil
             (set? (cdr '()))))

if-trueの公理により、Else部に好きな式を持ち出せます。

確かにそうですがいまだに何がどうなるのか想像がつきません

関数atomを使って、やはり関数set?の定義におけるif式のQuestion部のxs'()に置き換えたものへと、'tを書き換えましょう。

それ、さっき(atom '())を評価して'tにしたとこじゃないですか?
if-trueを使うための一時の方便ってことか

't(atom '())は等しいので、関数atomは逆向きに使えるのです。

そうそれがやりたかったんですよ
できるの?
ていうかどう書いたらいいの?

     ((Q Q) (atom '()))

あらできた
あれーなんか昔やってみてダメだった気がするんだけどなあ
そうなのできるの

で?

xs'()にして関数set?の定義を使いましょう!

はい?
うん、確かに(set '())の形になってるけど・・・

     ((Q) (set? '()))

できた
(set? '())'tになるだけじゃなくって定義で開かれることもあるわけかそうか

しかし何かぐるぐる回ってる気がする

  1. set?/add-atomsの定理を使いたい
  2. (set? '())という前提がほしい
  3. if-trueを使って前提を入れる この時点では前提は't
  4. (set? '())を定義を使って展開する
  5. if-trueを使えるようにするため、いったん(atom '())を評価して'tにする
  6. if-trueでさっき入れた前提の't(set? '())から作った式に入れ替える
  7. 't(atom '())に戻す → 前提が(set? '())を展開した式に戻る
  8. 展開した式を(set? '())に戻す
  9. (set? '())という前提ができた

短く言えば(set? '())'tだから(if (set? '()) ...という前提は
いつでも入れられるということ
そんなことは始めからわかってはいましたが
ちょっとだけ意外どころではないですよ!
8ステップだからちょっとだけで終わるというのは本当ですが