kb84tkhrのブログ

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

定理証明手習い (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)ならばxzに等しい、みたいなやつ
ならば?

例によって1ステップずつしつこく練習させてくれます

J-Bobは、ある式を別の式に書き換えるのを手助けしてくれるプログラムです。

以下次号