定理証明手習い (61) 振り返り
本編は終わったのでここまでいったん振り返ってみます
まず全体的には、全域性やその証明、帰納法による証明と帰納法の組み立て方など
目的とするところはだいたい理解できた気がします
会得した、と言うにはもっと練習してすらすら書けるようにならないとかなあ
数学ガールを始め不完全性定理の本を読んでて形式の世界のお作法に
ちょっと慣れてたおかげでとっつきやすかったというのがある気がします
慣れてなくても本にしたがってやっていけばできるとは思いますけど
あとは粒々で
疑問が疑問のままだったところとか
しおり3本重要
特にJ-Bobに慣れるまでは行ったり来たりが多くなります
トリ頭なので！
定理証明手習い (15) 型？ - kb84tkhrのブログ
(if (equal x '()) 't 'nil)はどう見ても(equal x '())なんですが どうやって変形していいかわかりません
これは結局できずじまい
関数の場合は「種」に尺度を入れてやるようです すると、全域性を主張する式が返されます どんなしくみで式を作ってるんでしょうか
定理証明手習い (20) 尺度 - kb84tkhrのブログ
これは8章でやりました
J-Bobのコードがどうやってるかは付録Cで
ここで
定理証明手習い (22) partialの証明 - kb84tkhrのブログ(< (size x) (size x))なはずはないから偽、となってて 意味的にはわかりますが形式的にはごにょごにょしてません？
これは今なら証明できますね
こんな感じ
(J-Bob/prove (dethm.align/align)
'(((dethm smaller-same (x)
(if (natp x) (equal (< x x) 'nil) 't))
nil
((A 1 1) (identity-+ x))
((A 1 2) (identity-+ x))
((A 1) (common-addends-< '0 '0 x))
((A 1) (< '0 '0))
((A) (equal-same 'nil))
(() (if-same (natp x) 't)))))一瞬うまく行った気がしましたが前半の前提で
定理証明手習い (40) 種 - kb84tkhrのブログflatten-inductionが残ってしまいました 何か間違ってるのかなあ
これは付録Cでなにかつかめることを期待
142ページの
ここで関数wtを使いましょう。から
common-addends-<を使って(wt (cdr x))をキャンセルできますからね。まで、何やってるのかわかんね感がぱない
定理証明手習い (57) 見えない - kb84tkhrのブログ
もう一回見てみましたがやはりぱない
あとは環境ですね
ずーっと定義が連鎖しているので1ファイルに全部書いてて
最後の方は1回1回の実行に時間がかかりました
分割コンパイルできればいいと思うんですがやり方がよく分からず
Racketならモジュールに分ければいいと思うんですが
r5rsではどうするのがいいのか
あとr5rsにするとDrRacketのデバッガがうまく動かないのかな？
始めのうち思った通りにならないとデバッガを動かしてみたくなりましたが
じきに慣れてきてそういう場面もなくなって放置でした
といったところで
