kb84tkhrのブログ

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

littleprover

定理証明手習い(a2) しゅくだい(10)

再考します、と言ってはみたもののイメージはつかめてなかったり (reverse/reverseだって証明はもっと簡単にできるイメージだった・・・) 再掲 reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである…

定理証明手習い(a1) しゅくだい(9)

rcons版のreverse/reverseを証明します reverse2/reverse2はどうしようかな rconsとreverseの定義・証明 (defun defun.rcons () (J-Bob/define (prelude) '(((defun rcons (x y) (if (atom x) (cons y x) (cons (car x) (rcons (cdr x) y)))) (size x) ((Q) …

定理証明手習い(a0) しゅくだい(8)

想定以上に寝かせることになってしまいましたがアドバイスいただきましたので考えてみます寝かせたわりには特にアイデアは思いついていません reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである、…

J-Bobを作ってみよう(11) おしまい

まあ一度真正面からどう動いているのか見てやろうかと ソースは組み込み関数を増やす前のものに戻しました とりあえずこんな感じのベタなことをしてみました これでも意外とつかめるかもしれないし

J-Bobを作ってみよう(10) 組み込み関数を追加する

たかだか証明を数ステップ進めるだけで関数を何百万会も呼ばなきゃいけないのかという疑問を脇に押しのけてたくさん呼ばれてる関数を組み込み関数にしてみます なんにも頭を使わない力技

J-Bobを作ってみよう(9) J-Bobをプロファイリング

J-Bobを動かしてみます >> (load "j-bob.jbb") Welcome to J-Bob #<void> >> (J-Bob/step '((dethm car/cons (x y) (equal (car (cons x y)) x))) '(car (cons 'ham '(eggs))) '((() (car/cons 'ham '(eggs))))) 'ham >> (show-profile) '((untag 18159) (elem1 93</void>…

J-Bobを作ってみよう(8) 簡易プロファイラ

関数の呼び出し回数が見えるようにしてみようかと envに覚えるようにしておいて、japplyかなにかのタイミングで更新すればよさそう リストのままだと更新しづらい(気がする)から、structにしてみようか こういうの「純粋」なやりかたではどうやるのかな ま…

J-Bobを作ってみよう(7)

テストを移植しながら調べているとここが無限ループとは言わないまでも やたらと時間がかかっていることを発見しました なおインデントは自分で直しています(以下同文 >> (defs? (tdefs) '((defun double (x) (add x x)) (defun len (xs) (if (atom xs) '0 …

J-Bobを作ってみよう(5) テスト

どうやって調べようか テストを移植するかな これまで書いたテストを再利用するためにはまずmy/testが書けなきゃいけなくて そのためには最低限displayとbeginがほしい

J-Bobを作ってみよう(3) 関数定義、関数適用、REPL

さていよいよ関数定義と関数適用です よく覚えていないのでとりあえず雑に書いてみます J-Bobではクロージャとか考えなくてもよさそうな気がしている まずは関数定義 J-Bobのdefunは式一つ書ければいいんだよな・・・?

J-Bobを作ってみよう(2) 組み込み関数

組み込み関数も作ればもうちょっとそれっぽい式で遊べるはず 関数が大きくなっていきますがしばらくは何も考えずにcondの下に生やしていって 大きくなりすぎたなと感じてから考えます でも(car e)くらいはなんとかしたほうがいいな (let ((op (car e))) (con…

J-Bobを作ってみよう(1) quote、if

J-Bobといっても証明する方じゃなくて j-bob-lang.scmで定義される方のやつです 証明する方のJ-Bobが動いて各種証明ができるレベルを目標とします 定理証明手習い、終わりのつもりだったんですけどこんなこと書いてあったの思い出しまして 読者のみなさんも…

定理証明手習い(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 …

定理証明手習い(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) re…

定理証明手習い(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)…

定理証明手習い(94) しゅくだい(3)

(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、を証明します (J-Bob/prove (defun.reverse) '(((dethm atom/reverse2 (x res) (if (atom x) 't (equal (atom (reverse2 x res)) 'nil))) (reverse2 x res) ; ← ここ!これ!きっと! …

定理証明手習い(94) しゅくだい(2)

行き詰まり気味なのでまず確実に進捗できそうなところを済ませます (defun defun.reverse2 () (J-Bob/define (prelude) '(((defun reverse2 (x res) (if (atom x) res (reverse2 (cdr x) (cons (car x) res)))) (size x) ((Q) (natp/size x)) (() (if-true (…

定理証明手習い (93) しゅくだい

「(reverse (reverse x))がどんなリストについてもxになるか」…(略)…読者への宿題にしておきます。 付録Cやってるあいだに証明も忘れかけてる気がするのでちょうどいいおさらい 最初は、これを証明すればいいかな、と思ったんですけどね

定理証明手習い (91) おさらい(1)

さすがに間が空きすぎて、始めのうち何をやってたか忘れてるような気がするのでおさらい ほんとは最初にざっとみてこれくらい把握しておくんだろうなあ はじめに、とか 帰納法を使うことで再帰的な関数についての事実を明らかにする方法を知る 入力の可能性…

定理証明手習い (92) おさらい(2)

5 何回も何回も何回も考えよう 定理の証明 洞察:内側から外側へと書き換えるべし Ifの持ち上げ 洞察:Ifを外側へ 洞察:いつも心に定理を

定理証明手習い (89) J-Bob/prove

(rewrite/prove defs def seed steps) 関数定義なら全域性の主張、 定理なら帰納法の主張を証明します 違うのは種から主張をつくるところだけかな rewrite/prove+1 (defs pf e) そこまでの証明が終わっていれば次の証明を行う rewrite/prove+ (defs pfs) 複…

定理証明手習い (88) J-Bob/step

(rewrite/step defs claim step) claimをstepで書き換える equality/defで組み込み関数を置き換えるとき、defには組み込み関数の 「定義」では(当然ながら)なく、関数名が単に入っていました どっかでわざわざ組み込み関数かどうかを判断して渡してるのか…

定理証明手習い (87) equality/def

パターンに分けてequality/pathを呼びます (defun equality/def (claim path app def) claim 主張 path フォーカスへのパス app 関数適用 def 定義

定理証明手習い (86) follow-premsの復習とequality/path

(app-of-equal e) equalの適用か (equality focus a b) focusを書き換えられる式 (equality/equation focus concl-inst) 帰結でフォーカスを書き換える conclはきっとconclusionでDethmの法則でいうところの帰結のこと 次の場合、置き換えた結果であるbody(e…

定理証明手習い (85) 演算子の適用

(rands args) argsのクォートをはがす (eval-op app) 組み込み演算子を適用する apply-opはタグなしの値を受け取るようになっているので、randsではがしてから 渡します 逆に言うと、組み込み演算子を適用できるのはクォートされた値のみ 変数には適用できな…

定理証明手習い (84) 演算子

(unary-op rator rand) (組み込みの)単項演算子の演算を行う (binary-op rator rand1 rand2) (組み込みの)二項演算子の演算を行う (apply-op rator rands) (組み込みの)演算子の演算を行う rator、なんだかわかった・・・ opeが省略されてたのか そり…

定理証明手習い (83) Dethmの法則?

具体的な形になった定理をつかう前に、follow-premsで延滞をチェックする必要があります。このチェックにより、等しいことが証明可能な2つの式を表す具体的な帰結が、等式として得られます。 わかったようなわからないような (equal (car (cons 'a 'b)) 'a)…

定理証明手習い (82) 式の置き換え

(find-focus-at-direction dir e) 式eの、dirで指定された部分式 dirがeの適切な位置を示しているかはまったく気にしてない模様 'Qって指定されたけどそもそもeはifじゃないとか '3って指定されたけど引数が2個しかないとか そういうの

定理証明手習い (81) 帰納法の構成

前回は全域性の主張の構成 今回は帰納法の構成 後ろから読んでいく (defun induction/claim (defs seed def) seedが種、defが定理の定義 (if (equal seed 'nil) (dethm.body def) 種が'nilなら定理の本体を返す (induction/defun (app.args seed) (dethm.bod…