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

今日はムスメがあっちむいてホイでずーっと勝負がつかなかったの、とか言うのでしめしめこれはチャンス、と思ってすかさずあっちむいてホイで10回やっても勝負がつかない確率ってどれくらいだと思う？と聞いてみました 頭の中では3/4の10乗だから3の10乗÷4の…

わからん わかるのは、自分の定義したreverseでは常に(reverse (reverse x))がxに なるとは限らない、ということだけ あらかじめxを最後まで見て'()で終わっているかを確認して、っていうことは できるかもしれないけどそこまでするものかよくわからない そ…

(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 …

最初の主張 (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…

今Eテレの100分de名著で法華経やってますね100分で名著ではお経が読み物としてときどき取り上げられてます お経が読み物ってどういうこと？って思う人が多いんじゃないでしょうか私もそう思ってましたお経は呪文じゃありません読めば意味がわかる文章なんで…

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 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) ; ← ここ！これ！きっと！ …

行き詰まり気味なのでまず確実に進捗できそうなところを済ませます (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 (…

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

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

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

J-Bob/defineを定義していきます rewrite/proveは再利用 その後も、'tを返すか定義のリストに証明された定義を付け足すかくらいなので それほど大きな違いはありません

この間、手帳用の筆記用具を万年筆からボールペンに変えました手帳のサイズに合うもので、そこそこいい感じのものを探してフリクションボールスリムビズに 1000円のわりにはまずまずの高級感があっていい感じなんですがどうもインクが乾きがち書き始めがかす…

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

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

先日、1000円のカット屋に言ってきましたもうずいぶん昔から1000円とか1500円のとこしかいってませんそんなにこだわりはないので ただ、1000円クラスになるとちょっと、ただのオッサンオバサンにしか見えないような美容師さんの割合が増える気がします腕前と…

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

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

ずーっと昔から、そのうち読もうと思ってて去年辺りからまた話題になって気になってたんですがKindleで99円の邦訳が出てることに気づいてやっと読みました 一九八四年 作者: ジョージ・オーウェル 出版社/メーカー: オープンシェルフパブリッシング 発売日: …

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

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

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

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

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

(defun totality/< (meas formals app) (app-c '< (list2 (sub-e formals (app.args app) meas) meas))) 名前からすると全域性に関する何か measは尺度のことかな measの仮引数にappの引数をあてはめたものが measよりも小さい、という式を作っている 尺度が…

exprs-recs 式のリストから再帰的な関数適用を抽出する expr-recs 式から再帰的な関数適用を抽出する 変数なら数えない クォートなら数えない ifならQ、A、E部の関数適用を抽出 関数適用で名前が一致したらそれ自身＋引数に含まれる関数適用を抽出 名前が一…

やっと形式チェックではない処理 (sub-var vars args var) 変数に対応する引数 vars 変数のリスト args 引数のリスト var 変数 (sub-es vars args es) （複数の）式の置き換え (sub-e vars args e) （単独の）式の置き換え ここも複数の式を置き換える関数を…

ZenPadにSIM挿しましたMineoのDコースこれが3回線め あんまり真面目に検討して選んだわけではなくて、今Mineo使ってて特に不満もないからというだけ

list2-or-more? リストの要素が2個以上か proof? 証明かどうか 証明である、とは？