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

J-Bob/defineで定義を使いまわせるようにしましたがテストはどうするかな こうかな (my/test "defun.pair" (defun.pair) (append (my/prelude) (list '(defun pair (x y) (cons x (cons y '())))))) でもこれだと証明が長いときは見づらそう 証明が間違って…

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

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

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…

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

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

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

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

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

（どういうわけ）しおり紐3本はさんでみました！

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

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

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

微妙な行き詰まり感からついこれをポチッと・・・ 『定理証明手習い』www.lambdanote.com む、埋め込みがうまくいってない？まあいいか 中身は見ずにポチったすでにほぼ信仰 電子書籍も紙書籍もあってちょっと迷ったけど応援になるかとも思って両方注文少々…