定理証明手習い (3) 「1.いつものゲームに新しいルールを」
『Scheme手習い』を読んだことは?
'nil
#t
ですよ!
- ある式に等しい式は無数にあるが、値はひとつしかない
- 変数の値が決まってなくても式の値が決まることがある
- 注目する部分を「フォーカス」、その外側を「文脈」と呼ぶ
フォーカスを、それに等しい式で置き換えていくことにより値を求める、というのを
練習していきます
Little Schemerではこんな感じで考えてましたが
(length '(a b))
= (add1 (length '(b)))
= (add1 (add1 (length '())))
= (add1 (add1 0))
= (add1 1)
= 2
Little Proverではこんな感じ
(equal 'flapjack (atom (cons a b)))
= (equal 'flapjack 'nil)
= 'nil
何が違うかというと
Little Schemerでは仮引数に値を入れることからスタート
Little Proverでは仮引数に値を入れないでスタート
してるってことですかね
だから仮引数の値にかかわらず等しくなるような式で置き換えなければならない、と
- 真(
't
)であると想定した基本的な仮定を公理という - 常に真となる式を定理という
- 定理には証明が必要
さっきの式変形も実は公理に基づいていて使った公理は以下のように書きます
(dethm atom/cons (x y)
(equal (atom (cons x y)) 'nil))
この公理で(atom (cons a b))
を'nil
に書き換えてるわけですね
Consの公理(最初のバージョン)の日本語訳(?)
といっても、コンスはアトムではない、って言っちゃうと使えなくなっちゃうな
(atom (cons x y))
と'nil
は等しい(car (cons x y))
とx
は等しい(cdr (cons x y))
とy
は等しい
最初のバージョン、と言ってるということはまだ追加があるんでしょうね
あと何かなあ
等しいものは置き換えていいよ、っていうのがDethmの法則
えーと、参照透過性、ってやつでしたっけ
副作用があるとできないやつですね
(equal 'nil 'nil)
を't
にするのは単に関数適用?
引数が確定してれば公理じゃなくて普通に関数として評価すればいいのかな?
違うな
これも公理でした
(dethm equal-same(x)
(equal (equal x x) 't))
置き換えてもいいよ、と言ってるequal
と置き換え対象のequal
が入り混じって
なんだかややこしいです
なお、このequal
は(atom (cons x y))
を'nil
が等しいことを言っているので
(atom (cons x y))
を'nil
に書き換えるだけでなく
'nil
を(atom (cons x y))
に書き換えるのに使うこともできます
わかりませんが意外な使いみちがあるかもしれません
これも公理
Equalの公理(最初のバージョン)
(equal x x)
は't
に等しい(equal x y)
は(equal y x)
に等しい
反射律と対象律だからあとは推移律が追加になるのかな?
(equal x y)
かつ(equal y z)
ならばx
はz
に等しい、みたいなやつ
ならば?
例によって1ステップずつしつこく練習させてくれます
J-Bobは、ある式を別の式に書き換えるのを手助けしてくれるプログラムです。
以下次号