J-Bobを作ってみよう(1) quote、if
J-Bobといっても証明する方じゃなくて
j-bob-lang.scmで定義される方のやつです
証明する方のJ-Bobが動いて各種証明ができるレベルを目標とします
定理証明手習い、終わりのつもりだったんですけどこんなこと書いてあったの思い出しまして
続きを読む読者のみなさんも、できれば好きな言語で J-Bob とその言語を実装してみてください。
考え方（の考え方）を教える（のって難しい）
今日はムスメがあっちむいてホイでずーっと勝負がつかなかったの、とか言うので
しめしめこれはチャンス、と思ってすかさず
あっちむいてホイで10回やっても勝負がつかない確率ってどれくらいだと思う？
と聞いてみました
頭の中では3/4の10乗だから3の10乗÷4の10乗、
3の10乗は81x81x9だから6000くらい、
4の10乗は2の10乗がだいたい1000だから1000✕1000で100万か、
100回に1回はないくらいなんだな、などと見当をつけたりしつつ
まあそんなところまで期待しているわけではまったくなく
考え方があってれば万々歳のつもりで聞いています
定理証明手習い(99) しゅくだい(7)
わからん
わかるのは、自分の定義したreverseでは常に(reverse (reverse x))がxに
なるとは限らない、ということだけ
あらかじめxを最後まで見て'()で終わっているかを確認して、っていうことは
できるかもしれないけどそこまでするものかよくわからない
それなら証明できるかって言うと大分自信ない
定理証明手習い(98) しゅくだい(6)
(if (equal res '()) ...を使おう
前提がついてないとこれができなくて詰む
((E A A 1 1 2) (equal-if res '()))
((E A A 1 2) (equal-if res '()))
((E E A A 1 1 2) (equal-if res '()))
((E E A A 1 2) (equal-if res '()))↓
(if (atom x)
't
(if (atom (cdr x))
(if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
(if (if (equal (cons (car x) res) '())
(equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x))
't)
(if (equal res '()) (equal (reverse2 (reverse2 x '()) '()) x) 't)
't)))定理証明手習い(97) しゅくだい(5)
最初の主張
(if (atom x)
(if (equal res '()) (if (atom x) 't (equal (reverse2 (reverse2 x res) res) x)) 't)
(if (if (equal (cons (car x) res) '())
(if (atom (cdr x))
't
(equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x)))
't)
(if (equal res '()) (if (atom x) 't (equal (reverse2 (reverse2 x res) res) x)) 't)
't))(if (atom x) ...)を消す
仏教を勉強してみる
今Eテレの100分de名著で法華経やってますね
100分で名著ではお経が読み物としてときどき取り上げられてます
お経が読み物ってどういうこと？って思う人が多いんじゃないでしょうか
私もそう思ってました
お経は呪文じゃありません
読めば意味がわかる文章なんです
漢文になってるからわからないだけで
お経って呪文でしょ？
昔のお坊さんは仏教を学問としてやってたっていうけどどういうこと？
お釈迦様が実在の人物って言ったって教祖様が祭り上げられてるだけなんじゃ？
禅宗って仏教に入ってるけどほんとのところ仏教と禅って何の関係が？
などと思っている人（全部自分）にはおすすめしたい
目からウロコかもしれませんよ（おっとキリスト教入った
今の自分にはお釈迦様が普通に歴史上の人物でしかも天才、というふうに見えてます
またこの、書いてる佐々木閑さんとか植木雅俊さんの解説がよくて
宗教っぽさを感じさせず、エビデンスと推理で仏教の本当の姿を
浮き彫りにしようという感じがとても好き
おふたりとも理系出身なのでそういう感じになるのかも知れません
しかも淡々と解説しているだけでなく情熱も感じます
いきおいあまって植木雅俊さんの「サンスクリット原典現代語訳 法華経」を
ポチりそうになりました（ふみとどまりました
仏教そのものだけでなく、大乗と小乗の勢力争いとか日本の仏教はどうして
こうなっているとか、そういう歴史とか政治っぽい話も面白いです
あとは禅宗の始まりとか読んでみたいなあ
そもそも仏教関連がアンテナにかかるようになったのは
マインドフルネスとかそういうあたりからなので
定理証明手習い(96) しゅくだい(4)
reverse/reverseの証明に戻ってここからです
(if (atom x)
't
(equal
(if (atom (reverse2 x '()))
(reverse2 x '())
(reverse2 (reverse2 x '()) '()))
x))(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、が証明されたので
((E 1 Q) (atom/reverse2 x '()))
((E 1) (if-false (reverse2 x '())
(reverse2 (reverse2 x '()) '())))して
こうなりました
