定理証明手習い (15) 型？
「4. これが完全なる朝食」のはじめに
関数
list0?を定義してください。(defun list0? (x) (if (equal x 'oatmeal) 'nil (if (equal x '()) 't (if (equal x '(toast)) 'nil 'nil)))はいはい、やり直しましょうね。
(defun list0? (x) (equal x '()))
ってくだりがあるんですが、これはただのジョークでしょうか
公理を使えば書き換えられるんでしょうか
やってみます
(if (equal x 'oatmeal) 'nil (if (equal x '()) 't (if (equal x '(toast)) 'nil 'nil)))
= (if (equal x 'oatmeal) 'nil (if (equal x '()) 't 'nil))(if (equal x '()) 't 'nil)はどう見ても(equal x '())なんですが
どうやって変形していいかわかりません
別方面から進めてみます
= (if (equal x '())
(if (equal x 'oatmeal) 'nil (if (equal x '()) 't 'nil))
(if (equal x 'oatmeal) 'nil (if (equal x '()) 't 'nil)))
= (if (equal x '())
(if (equal x 'oatmeal) 'nil 't)
(if (equal x 'oatmeal) 'nil 'nil))
= (if (equal x '())
(if (equal x 'oatmeal) 'nil 't)
'nil)
= (if (equal x '())
(if (equal '() 'oatmeal) 'nil 't) 'nil)
= (if (equal x '()) (if 'nil 'nil 't) 'nil)
= (if (equal x '()) 't 'nil)結局残りました
公理とにらめっこしてみましたが簡単にする方向には進みそうにないので
いったん式を増やすんでしょうか
妄想ではこんな風に終わりそうな気がするんですが何かが足りないような
= (if (equal x '()) 't 'nil)
= ...
= ...
= (if (equal x '()) (equal x '()) (equal x '()))
= (equal x '())逆算するとequal-ifでもうちょっといける？
= (if (equal x '()) 't 'nil)
= ...
= ...
= (if (equal x '()) (equal '() '()) (equal x '()))
= (if (equal x '()) (equal x '()) (equal x '()))
= (equal x '())(equal '() '())は公理でも関数適用でも'tに書き換えられるけど
'tを(equal '() '())に書き換えるっていうのは可能なんでしょうか
今知ってる範囲のJ-Bobでは書きようがない気がします
それにそっちがんばってもElse部がなあ
変形できないのかなあと思っても悪魔の証明みたいな感じですが
考えてみると(if (equal x '()) 't 'nil)と(equal x '())が
同じであるというためには(equal x '())が'tと'nilしか返さないという
約束が必要ですね
それがなければここで終わり？
そもそもJ-Bobでは'tと'nil以外の値はどう扱われてるんでしょうか
(define (if/nil Q A E)
(if (equal? Q 'nil) (E) (A)))
(define-syntax if
(syntax-rules ()
((_ Q A E)
(if/nil Q (lambda () A) (lambda () E)))))'nil以外は't扱いのようです
じゃあ(equal x '())が'tと'nilしか返さないっていう公理があれば
(if (equal x '()) 't 'nil)を(equal x '())に変形できるかな？
・・・
'tか'nilである＆'tではない、から'nilであることが言える？
うーんわからない
そもそも「'tと'nilしか返さない」ってどうやって書くんだ
それは公理じゃないのか？
型？
型かもしれないな
0.7mm 2B シャーペン芯
普段の筆記用具は万年筆なわたしですが鉛筆も嫌いではありません
でもシャーペンはカキカキした書き味があまり好きではなくて使ってませんでした
鉛筆も削らなきゃいけないとか何本も持たなきゃいけないとかで常用はしてません
芯ホルダーにトライしてみたこともありました
で、もうけっこう前なんですがこれならいけるかも、と思って
KOKUYOの鉛筆シャープってやつを買いました
0.7mm、0.9mm、1.3mmとラインナップがあったのでひと通り試してみたところ
0.9mmと1.3mmは期待通りの書き味
自分的には鉛筆と思って書けるレベル
たださすがにちょっと太すぎるような
でもなぜか0.7mmはシャーペンっぽいカキカキした書き味でした
細ければ固くしなきゃいけないというのは理屈なんですけど
あまり敏感な方じゃない自分でも明らかにわかるほどの差
クルトガの0.9mmとかあったら理想かも？と思いつつ
そのときはまあいいやで終わらせてました
で先日、子供の筆記用具を探してたらクルトガの0.7mmを発見
実は0.5mmまでしかないと思いこんでいたのでした
じゃあちょっと試してみるかと思いましたがあの書き味では
あまり使いたくはなりません
ということで、文房具屋で0.7mmの芯あるだけ全種類買ってきました
柔らかい書き味を求めてるので2B
そして書いてみた感想
紙はマルマンのクロッキー帳
ちょっとバッチリな感触とはいかず
強いて言えばneox GRAPHITEかなあ Nano Diaも同じくらい
鉛筆シャープ0.9の黒さが際立ちます
書いてる感触もやはりいい
なんだろうこの差は
そもそも買ったままの芯で、2Bに変えた気もしないんだけど
もともと2Bが入ってるのかな？
それとも入れ替えたことを忘れてる？（ありうる）
あと書いてて気づいたんですがシャーペンを回すクセがついてます
昔からそうだったのかなあ？
無意識に回しててクリップが引っかかってあれ？ってなるんですが
たいていのシャーペンにはクリップがついてる気がするので
鉛筆シャープを使っててついたクセなんでしょうか
芯ホルダーのときかな？
どれもクセがつくほど使ってたわけじゃないんですが
どうせ回すんだったら鉛筆シャープでよくない？という気もしてきます
デザインもシンプル可愛くてけっこう好きだし
KOKUYOだから当然入ってる芯はCampusの芯だよなあ
0.9mmも検証してみるかな
そこまでして使いたいってわけじゃないんだけど
なんかこうこのままだと宙ぶらりんな気がするのですっきりしたい
子供に0.7mmのシャーペンを使わせるつもりなので
0.7mmの芯はハズレでも子供に使わせればいいけど（！）
0.9mmは自分しか使う人がいないからちょっと慎重に
使用頻度から言って４つも買ったら一生使い切れなさそう
まずCampusを買ってみて、今の芯と同じ感じだったらそれでいいとしよう
あ、0.9mmでいいやっていうのは、無地の紙を使うようになって
好きな大きさで字を書けるっていうのもあります
無地いいですよ！
意外なほど楽に書けますよ！
おすすめです
定理証明手習い (14) 証明ゴルフ？
この証明がもうちょっと短くできますねと書いてあります
(J-Bob/prove (dethm.in-first-of-pair)
'(((dethm in-second-of-pair (a)
(equal (in-pair? (pair a '?)) 't))
nil
((1 1) (pair a '?))
((1) (in-pair? (cons a (cons '? '()))))
((1 Q 1) (first-of (cons a (cons '? '())))) ; ここと
((1 Q 1) (car/cons a (cons '? '()))) ; ここが不要
((1 E 1) (second-of (cons a (cons '? '()))))
((1 E 1 1) (cdr/cons a (cons '? '())))
((1 E 1) (car/cons '? '()))
((1 E) (equal-same '?))
((1) (if-same (equal a '?) 't))
(() (equal-same 't)))))不要な行を削除
式の形が変わるので、下から２行目も変更しました
(J-Bob/prove (dethm.in-first-of-pair)
'(((dethm in-second-of-pair (a)
(equal (in-pair? (pair a '?)) 't))
nil
((1 1) (pair a '?))
((1) (in-pair? (cons a (cons '? '()))))
((1 E 1) (second-of (cons a (cons '? '()))))
((1 E 1 1) (cdr/cons a (cons '? '())))
((1 E 1) (car/cons '? '()))
((1 E) (equal-same '?))
((1) (if-same (equal (first-of (cons a (cons '? '()))) '?) 't))
(() (equal-same 't)))))その下から２行目、微妙に長い気がします
ここはconsに展開されてなくてもいいところ
pairの評価をあとに回せばfirst-ofの方は展開しなくて済みます
(J-Bob/prove (dethm.in-first-of-pair)
'(((dethm in-second-of-pair (a)
(equal (in-pair? (pair a '?)) 't))
nil
((1) (in-pair? (pair a '?)))
((1 E 1) (second-of (pair a '?)))
((1 E 1 1 1) (pair a '?))
((1 E 1 1) (cdr/cons a (cons '? '())))
((1 E 1) (car/cons '? '()))
((1 E) (equal-same '?))
((1) (if-same (equal (first-of (pair a '?)) '?) 't))
(() (equal-same 't)))))この方がちょっと気持ちいいかな
これって、関数の評価順を自由に変えてるってことになるわけか
洞察：無関係な式は飛ばそう
なるほど
あと(equal-same '?)を(equal '? '?)に変更すればさらに２文字・・・
これはあんまり意味がないからやめておこう
公理で言えるときは公理で言っておくほうがスジがいいのかな
定理証明手習い (13) Jabberwockyリベンジ
これって本当に定理なんですか？
たぶん定理ですね。
関数や定理を定義する書き方がわかったので、これでjabberwockyも
まっとうに定義できるようになったはず
（jabberwockyは再帰的な関数じゃないから）
brillig、slithy、mimsy、mome、uffish、frumious、frabjousが何を意味しているかによりますが。
関数は、jabberwockyがちゃんと定理になるよう定義
(defun dethm.jabberwocky ()
(J-Bob/define (my/prelude)
'(((defun brillig (x) 't)
nil)
((defun slithy (x) 't)
nil)
((defun uffish (x) 't)
nil)
((defun mimsy (x) 'borogove)
nil)
((defun mome (x) 'rath)
nil)
((defun frumious (x) 'bandersnatch)
nil)
((defun frabjous (x) 'beamish)
nil)
((dethm jabberwocky (x)
(if (brillig x)
(if (slithy x)
(equal (mimsy x) 'borogove)
(equal (mome x) 'rath))
(if (uffish x)
(equal (frumious x) 'bandersnatch)
(equal (frabjous x) 'beamish))))
nil
((Q) (brillig x))
(() (if-true
(if (slithy x)
(equal (mimsy x) 'borogove)
(equal (mome x) 'rath))
(if (uffish x)
(equal (frumious x) 'bandersnatch)
(equal (frabjous x) 'beamish))))
((Q) (slithy x))
(() (if-true
(equal (mimsy x) 'borogove)
(equal (mome x) 'rath)))
((1) (mimsy x))
(() (equal-same 'borogove))))))では実行 ※結果のインデントは手で修正
> (J-Bob/step (dethm.jabberwocky)
'(cons 'gyre
(if (uffish '(callooh callay))
(cons 'gimble
(if (brillig '(callooh callay))
(cons 'borogove '(outgrabe))
(cons 'bandersnatch '(wabe))))
(cons (frabjous '(callooh callay)) '(vorpal))))
'(((2 A 2 E 1) (jabberwocky '(callooh callay)))))
(cons 'gyre
(if (uffish '(callooh callay))
(cons 'gimble
(if (brillig '(callooh callay))
(cons 'borogove '(outgrabe))
(cons (frumious '(callooh callay)) '(wabe))))
(cons (frabjous '(callooh callay)) '(vorpal))))できた
定理証明手習い (12) J-Bob/defineのテスト
J-Bob/defineで定義を使いまわせるようにしましたがテストはどうするかな
こうかな
(my/test
"defun.pair"
(defun.pair)
(append (my/prelude)
(list '(defun pair (x y)
(cons x (cons y '()))))))でもこれだと証明が長いときは見づらそう
証明が間違ってると追加されないようだから、追加されたたことだけ確認すればいいか
内部構造に依存してるのは嫌だけどすっきりはする
(define (last l)
(cond ((null? (cdr l)) (car l))
(else (last (cdr l)))))
(define (last-name l)
(cadr (last l)))
(my/test
"defun.pair"
(last-name (defun.pair))
'pair)このパターンはたくさん出てきそう
でこんな感じに書ければいいんだよなーと思ったんですが
(define (right-of str c)
(list->string (cdr (memq c (string->list str)))))
(define (name-part sym)
(string->symbol (right-of (symbol->string sym) #\.)))
(define-syntax my/test/define
(syntax-rules ()
((_ name)
(my/test
(symbol->string name)
(last-name (name))
(name-part name)))))defun.pairはシンボルじゃなくて関数なのでうまくいきませんでした
関数名とシンボルは違うのか わかってなかった
関数の名前をシンボルか文字列で取得できればいいんだけど・・・
ということで最初からシンボルで渡して、強引にevalしてやってます
evalを使うほどのことではないような何か忘れてるような
教えてえらい人
(define-syntax my/test/define
(syntax-rules ()
((_ name)
(my/test
(symbol->string name)
(last-name ((eval name (interaction-environment))))
(name-part name)))))まあ一応使えることは使えるので進みます
定理証明手習い (11) J-Bob/define
正誤表ができてますね
どっちかというとScheme手習いやScheme修行の方が正誤表ほしかったかなあ
この本はだいたい安心して読めてる感じ
訳も自然な気がする
さて本題
証明できた関数や定理はJ-Bob/defineを使って他の証明で使いまわせるようにできます
J-Bob/defineの書き方はJ-Bob/proveとほとんど同じ感じ
(J-Bob/define (<公理・定義済みの関数／定理>)
'((<関数・定理の定義>
<種>
<証明>)
...))実例
> (J-Bob/define (my/prelude)
'(((defun pair (x y)
(cons x (cons y '())))
nil)))
((dethm atom/cons (x y) (equal (atom (cons x y)) 'nil))
:
(dethm if-nest-e (x y z) (if x 't (equal (if x y z) z)))
(defun pair (x y) (cons x (cons y '()))))値は公理や関数・定理のリストになってます
証明済みかどうかのチェックして、リストの末尾に定義をくっつける、ということを
やってるようですね
で、J-Bob/defineが返してきたリストに名前をつけてやることにより使いまわします
(defun defun.pair () ; 名前をつける
(J-Bob/define (my/prelude)
'(((defun pair (x y)
(cons x (cons y '())))
nil))))
(defun defun.first-of ()
(J-Bob/define (defun.pair) ; ここで使いまわしてる
'(((defun first-of (x)
(car x))
nil))))付録Bで１章２章の例をわざわざ関数の形で書いてたのは
こういう書き方にあわせたのかも？
付録Aではいくつかの関数や定理をまとめて定義してますが
付録Bでは関数や定理をひとつずつ定義していきます
この違いはなんなんでしょうか
分けておけば必要な部分だけ使える、ていっても分けて使う場面は出てくるんでしょうか
定理証明手習い (10) J-Bob/prove
「3 名前に何が？」では関数定義と証明が出てきます
関数はその定義で置き換えることができます（Defunの法則）
ここでは「再帰的でない」関数が対象です
再帰的な関数はどうするんでしょうか
Dethmの法則と似てるところもありますが定理はそもそも再帰できないという約束でした
そして証明
まだ証明されていない定理を主張といいます
主張を証明するには、主張の式の置き換えを繰り返して'tになることを示します
証明はJ-Bob/proveの中で行います
証明で使う関数はJ-Bob/proveの中で定義しないと使えない模様
トップレベルで定義した関数をJ-Bob/proveの中から呼ぶことはできないようです
トップレベルで定義したからと言って二重定義のエラーになったりはしないので
作った関数をちょっとREPLで動かしてみたいみたいなときは
両方に定義を書くことになるのかな
(J-Bob/prove (my/prelude)
'(((defun pair (x y)
(cons x (cons y '())))
nil)))nilは「種」だそうですが詳細な説明は後で出てくるようです
(J-Bob/prove (<公理・定義済みの関数／定理>)
'((<関数・定理の定義>
<種>
<証明>)
...))となります
証明はJ-Bob/stepと同様に書いて、'tになるまで変形します
上の例では証明はありませんが実行すると'tになります
なぜかというと
与えられている
defunが再帰的ではないので、全域性が自明であるために
証明案件は'tであり、それが成功するから
だそうですがちょっとちんぷんかんぷんです
定理は'tになることを証明する、関数は全域であることを証明する、ってことでしょうか
きっともうちょっと進めばわかるようになるんではないかと
