で書くネタも用意してないわ電車の中でも書いてないわででも小さな習慣で決めてるから何か書かないとってやつなんですが 会社の人との飲み会なんですけどレベルの高い人達の集まりで聞いてると楽しいんですけど自分がいていいんだっけって感じちょっと発言も…

こんな定理を証明します (dethm ctx?/sub (x y) (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)) そういえばこの間 'tってなんだよ'tって、と思いましたがこれはたぶん定理は常に'tでないといけないので入れてあるってことでしょう 定理証…

第7章はスター型関数に関する定理の証明 題材となるスター型関数はこれ (defun ctx? (x) (if (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x))))) まずは全域性の証明 種は(size x) 証明すべき式はこれ (if (natp (size x)) (if (atom x) 't (if…

ムスメが450分って何時間？って聞いてきたわけですそこで7時間30分だよ、って言えば話は終わりなんですけどね答えを言うのは気が進まないんです450÷60はいくつ？くらいで済ませればいいんですがそうは問屋がおろしません 1時間は何分？60分だね450分の中に60…

こんなの出てましたよ blog.workflowy.com モバイルアプリの再設計ちょっと今のモバイルアプリはひどいからがんばるよ！でもまだまだ先は長いよ！アルファ版もあるからよかったらどうぞ！ モバイルアプリからの逆輸入モバイルアプリの便利な機能はWe版やデス…

本書の目標は、帰納法を使うことで再帰的な関数についての事実を明らかにする方法を読者に知ってもらうことです。 って話でしたがやっと帰納法です 証明にも再帰を使えるんですか？ はい、使えます。 証明における再帰のことを、帰納法と呼びます。 ここでは…

Ifの持ち上げを何回か書いてると面倒になってきます これがパターンであるのなら定理として証明してしまえばいいのでは、 と思ったのですがそもそもパターンがJ-Bobで表現できるのかなあ 書けるとしたらこんな感じなんでしょうか (J-Bob/prove (defun.remb) …

ちょっと昔まで紙に字を書くってことをしなかった私ですが時代に逆行してちょっとずつ手書きが増えて来ていますそれでも中心はパソコンなのでノート1冊しか使わなくっても1冊使い切るまでには相当な時間がかかっていたものですパソコンでは書きづらい数式な…

ここでは何をやってるって言ったらいいのかな 再帰する関数の全域性が証明できるようになったので 再帰する関数を使った定理を証明する（ための準備）、でいいのかな 0要素のリスト、1要素のリスト、2要素のリストについて 定理を証明していきます 証明にも…

このまえも出てきたpartialの証明 本に書いてあることをコードで書くとこうなります > (J-Bob/prove (my/prelude) '(((defun partial (x) (if (partial x) 'nil 't)) (size x) ((Q) (natp/size x)) (() (if-true (if (< (size x) (size x)) 't 'nil) 'nil)))…

2つめの引数に含まれる'?をすべて1つめの引数の値に置き換える、subという関数を考えましょう。 これはScheme手習いで言うところの「スター型」(*のついた)関数になります car側も再帰するやつです (cons (sub x (car y)) (sub x (cdr y)))の部分は証明だと …

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

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

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

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

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

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

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

「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 '())) って…

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

この証明がもうちょっと短くできますねと書いてあります (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…

これって本当に定理なんですか？ たぶん定理ですね。 関数や定理を定義する書き方がわかったので、これで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…