定理証明手習い (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
になるだけじゃなくって定義で開かれることもあるわけかそうか
しかし何かぐるぐる回ってる気がする
set?/add-atoms
の定理を使いたい(set? '())
という前提がほしいif-true
を使って前提を入れる この時点では前提は't
(set? '())
を定義を使って展開するif-true
を使えるようにするため、いったん(atom '())
を評価して't
にするif-true
でさっき入れた前提の't
を(set? '())
から作った式に入れ替える't
を(atom '())
に戻す → 前提が(set? '())
を展開した式に戻る- 展開した式を
(set? '())
に戻す (set? '())
という前提ができた
短く言えば(set? '())
は't
だから(if (set? '()) ...
という前提は
いつでも入れられるということ
そんなことは始めからわかってはいましたが
ちょっとだけ意外どころではないですよ!
8ステップだからちょっとだけで終わるというのは本当ですが