kb84tkhrのブログ

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

定理証明手習い (20) 尺度

全域性を証明するために尺度を導入します 関数が再帰的に呼び出されるたびに尺度が減少することを示すことによって いつかは再帰が終わることを証明します 無限下降法的な何か? sizeはリストを作るために必要なconsの数でした 以下のような公理を使って全域…

今度は0.9mm芯書き比べ

もやっと感がおさまらないので結局0.9mmの芯もいろいろ買ってきました 今回試してみるのはこの4種類この間買ったCampus 0.9mm 2Buni Nano Dia 0.9mm 2BPILOT neox GRAPHITE 0.9mm 2Bプレスマン用替芯 0.9mm 2B前回ちょっと薄めに感じたAinSTEINは候補から外…

定理証明手習い (19) atom

前回のlist?シリーズでlist?のA部の(equal x '())(=list0?)が list1?やlist2?では'nilに置き換えられているのは 何か一般的な書き換え規則があるんでしょうか Scheme風に書いた方では#tが#fになってます 何かあるような気がしますが思いつきません 他の再帰…

定理証明手習い (18) atom

対話的定理証明器という言葉を見かけました j-bobに1行足しては結果を見てまた1行足す、ってやってるのを思い出して ああこれは対話してたんだ、と思うなど さて (defun list0? (x) (equal x '())) (defun list1? (x) (if (atom x) 'nil (list0? (cdr x)))) …

定理証明見習い (17) 部分関数

部分関数の置き換えを認めると矛盾が発生する 部分関数の例はこれ (defun partial (x) (if (partial x) 'nil 't)) こうじゃないのはなぜか (defun partial (x) (partial x)) いちおう値を返しそうな雰囲気はかもし出しておきたい、くらいかな であれば、こう…

Campus 0.9mm 2B

というわけでCampus 0.9mm 2Bの芯を買ってきたわけなんですが 違う・・・薄い じゃあ今入ってるこの芯は何なの家には0.9mmの替芯なんてないしそれ以外で入れ替える機会なんてあるかなあKOKUYOだけどCampusじゃない芯なの? むーまたあるだけ買ってくるのかこ…

定理証明手習い (16) 全域

全域とは、どんな値を渡しても関数が値を持つということ この間pairは全域、って話が出てました 組み込み関数は、すべて全域です。 そうだったんですか! そうだったんですか! Scheme手習いでは lのcarは何ですか。 ここで lは'()です。 答えはありません。…

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

0.7mm 2B シャーペン芯

普段の筆記用具は万年筆なわたしですが鉛筆も嫌いではありませんでもシャーペンはカキカキした書き味があまり好きではなくて使ってませんでした鉛筆も削らなきゃいけないとか何本も持たなきゃいけないとかで常用はしてません芯ホルダーにトライしてみたこと…

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

定理証明手習い (13) Jabberwockyリベンジ

これって本当に定理なんですか? たぶん定理ですね。 関数や定理を定義する書き方がわかったので、これでjabberwockyも まっとうに定義できるようになったはず (jabberwockyは再帰的な関数じゃないから) brillig、slithy、mimsy、mome、uffish、frumious、…

定理証明手習い (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 '())))))) でもこれだと証明が長いときは見づらそう 証明が間違って…

定理証明手習い (11) J-Bob/define

正誤表ができてますね github.com どっちかというとScheme手習いやScheme修行の方が正誤表ほしかったかなあこの本はだいたい安心して読めてる感じ訳も自然な気がする さて本題証明できた関数や定理はJ-Bob/defineを使って他の証明で使いまわせるようにできま…

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

「3 名前に何が?」では関数定義と証明が出てきます 関数はその定義で置き換えることができます(Defunの法則) ここでは「再帰的でない」関数が対象です 再帰的な関数はどうするんでしょうか Dethmの法則と似てるところもありますが定理はそもそも再帰でき…

定理証明手習い (9) 「2 もう少し、いつものゲームを」

ifの公理が出てきます ifでは数ではなくてQ、A、Eで置き換え対象を指定します (if 't x y)とxは等しい (if-true) (if 'nil x y)とyは等しい (if-false) (if x y y)とyは等しい (if-same) 3つめ公理はどうやって使うんでしょうか (dethm if-same (x y) (equal…

定理証明手習い (8) 増殖

1章のラスト近く 式を簡単にしていくのではなく複雑にしていっています こうやっていくらでも式をでっちあげられるから定理の自動証明は難しいんだ、 っていうアピールですかね? (my/test "chapter1.example11" (J-Bob/step (my/prelude) '(cons y (equal (…

定理証明手習い (7) やっぱりテスト風に

公理を書き換えたりすると今までの結果が全部怪しくなるのでやっぱりテストを書こう でもフレームワークっていうほどのものじゃないからちょっとだけ自分で書くことに my/testをマクロにしてるのは、'を取ったり付けたりするのに それ以外に方法を思いつかな…

定理証明手習い (6) 公理も自分で

ところで preludeは、J-Bobの公理および最初に用意されている関数の集まりです。 公理も自分で書いてみたい 最初に公理が必要になるのはこれ ; chapter1.example3 (J-Bob/step (prelude) '(atom (cons a b)) '((() (atom/cons a b)))) j-bob.scmをチラ見して…

定理証明手習い (5) 「B デザートには証明を」

さらに「B デザートには証明を」には出てきた式が全部J-Bobで書いてあります なので本編と付録Aと付録Bをいったりきたりすることになります なのでしおりが3本ほしかったりするわけです J-Bobでの記述はこんな感じ (defun chapter1.example1 () (J-Bob/step…

定理証明手習い (4) J-Bob初体験

J-Bobは、ある式を別の式に書き換えるのを手助けしてくれるプログラムです。 「A 放課後」でJ-Bobの使い方が紹介されています 章の内容に沿って書かれているのでとりあえず言われるまま入れてみます > (J-Bob/step (prelude) '(car (cons 'ham '(eggs))) '()…

定理証明手習い (A) というわけで

(どういうわけ)しおり紐3本はさんでみました!

DynalistとWorkflowy

たいしたアクセスもないこのブログですがアクセス解析を見ているとここ2ヶ月くらいはずっとこの記事がアクセス数1位をキープしてますはっきり数は出ませんがアクセス数も増えてるんじゃないかなちょっとずつDynalistがポピュラーになってきてるんでしょう…

定理証明手習い (3) 「1.いつものゲームに新しいルールを」

『Scheme手習い』を読んだことは? 'nil #tですよ! ある式に等しい式は無数にあるが、値はひとつしかない 変数の値が決まってなくても式の値が決まることがある 注目する部分を「フォーカス」、その外側を「文脈」と呼ぶ フォーカスを、それに等しい式で置…

定理証明手習い (2) J-Bobを動かす

「自分で動かしながら楽しみたい」という読者のために、J-Bobという簡素な定理証明支援系を用意してあります。 必須じゃないという書き方ですね でもせっかくですから動かしてみたい まずはThe Little Proverのページにアクセスしてみます J-BobはGitHubから…

あけましておめでとうございます

定理証明手習い (1) はじめに、とか

では『定理証明手習い』ゆっくり読んでいきます Litter Schemerシリーズは何冊もあって全貌はよくわかってないんですが 知ってる範囲では以下の4冊があります The Little Schemer (Scheme手習い) The Seasoned Schemer (Scheme修行) The Reasoned Schemer (…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (58)

大詰め 定義43 xはaとbの"直接の帰結"である (define (IsConseq [x : GForm] [a : GForm] [b : GForm]) : Boolean (or (= a (Implies b x)) (∃ v <= x (and (IsVar (gsymbol+ v)) (= x (ForAll (gsymbol+ v) a)))))) 定義44 xは"形式的証明"である (define (…

なにか語りかけ口調になる

自分の思いつきを書き留めているだけで誰かのために書いてるわけではないんですけどねでもブログに書くんだと思うと言葉遣いが変わります不思議ですね ていうかアウトプットの練習と思って書きはじめたのに自分の思いつきを書き留めてるだけ、ってのは目的に…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (57)

定義40 xは公理IVから得られる"論理式"である (define (IsAxiomIV [x : GForm]) (∃ u v y n <= x (and (IsVarType (gsymbol+ u) (+ n 1)) (IsVarType (gsymbol+ v) n) (IsForm (gsequence+ y)) (not (IsFree (gsymbol+ u) (gform+ y))) (= x (Exists (gsymbo…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (56)

定義36 xは公理IIから得られる"論理式"である (define (IsAxiomII [x : GForm]) : Boolean (or (IsSchemaII 1 x) (IsSchemaII 2 x) (IsSchemaII 3 x) (IsSchemaII 4 x))) 定義37 zは、yの中でvが"自由"な範囲に、"束縛"された"変数"を持たない (define (IsNo…