(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) （単独の）式の置き換え ここも複数の式を置き換える関数を…

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

(extend-rec defs def) ??? 定義済みのリストに関数の新しい定義を追加してるんだけれども ただ自分を呼ぶだけの関数を追加している なんだこれ (def-contents? known-defs formals body) 仮引数と本体が正しい形か known-defsは定義済みの関数・定理のリス…

(step-args? defs def args) argsがdefの正しい引数かどうか 組み込み関数に渡す引数はクォートされたリテラルでなければなりません。 そういうものだったっけか はっきり認識できてなかったな なにかそれっぽいものがあるとは思ってた気がするけど こんなシ…

普通に集合を扱う関数 list-extendはどこぞでちょっと使いました (subset? xs ys) xsがysの部分集合かどうか (list-extend xs x) xsの末尾にxを追加する 重複はしない リストを先頭から眺めて、重複があれば終わり 末尾まで届いたら要素を追加 (list-union x…

(bound? var vars) varが束縛されているか varsは束縛変数のリスト varsが'anyならば束縛されていなくても't (exprs? defs vars es) 式のリストが正しいか 今まで出てきた関数の中ではなかなかの大モノ

implicationも見ておこう 前提が0個の場合、含意は e0 によって表す。 ここに対応 (if (atom es) e 前提が es (式のリスト)、帰結が e なのでこうなります > (implication '() '(equal x 'a)) (equal x 'a)

(defun if-c-when-necessary (Q A E) (if (equal A E) A (if-c Q A E))) お、これはアレだな Defun帰納法の Caeは、 Caと Ceが等しい場合は Caで、それ以外の場合については(if Q Ca Ce)である。 だなきっと

ひとことでどういうグループかは言い難い (if-QAE e) if型からQ、A、Eのリストを作る (QAE-if e) Q、A、Eのリストからif型を作る こうやっても書けるけどlist3と`if-cで作ってる その方がスジがいいんだろうか (defun if-QAE (es) (untag es)) (defun QAE-if…

データの表現方法としては、J-Bobの実装言語の構文を反映したものを選びました。 若干混乱中 「J-Bob」と「J-Bobの実装言語」は同じもの？違うもの？ 別だけど揃えた、ってことはな？ J-Bob/proveとかが定義されてるのがJ-Bobだと思うんだけど 今J-Bobを定義…

筆者らのJ-Bob実装で最初に定義しているのはリスト操作です。 list0 要素が0個のリストを作る list0? 要素が0個のリストかどうか

コード書いたら動かしたいしせっかく動かしたら残したいので結局テスト的なものを書くことになります (my/test "car/atom" (car 'a) '()) (my/test "car/cons" (car (cons 'a 'b)) 'a) (my/test "cdr/atom" (cdr 'a) '()) (my/test "cdr/cons" (cdr (cons 'a…

SchemeでJ-Bobを使うには (define s.car car) (define (car x) (if (pair? x) (s.car x) '())) こうやって関数を上書きして全域にしていくのね (define (if/nil Q A E) (if (equal? Q 'nil) (E) (A))) あれ これってifは関数では書けませんよ、っていうパタ…

本編は終わったのでここまでいったん振り返ってみます まず全体的には、全域性やその証明、帰納法による証明と帰納法の組み立て方など目的とするところはだいたい理解できた気がします会得した、と言うにはもっと練習してすらすら書けるようにならないとかな…

進んでみたらわかることを期待して進む J-Bob/proveに(align x)を種として与えてやると証明すべき式が出力されます (if (atom x) (equal (align (align x)) (align x)) (if (atom (car x)) (if (equal (align (align (cdr x))) (align (cdr x))) (equal (ali…

休息の時間を勝ち取りました。 おやつを食べ終わったら続けます。

142ページの ここで関数wtを使いましょう。 から : ここでも、いまと同じステップが使えそうですね。 : これで3回めになりますが、同じステップですかね？ : 次の2つのフォーカスで関数wtを使いましょう。 : まず、associate-+の公理を使います。 : を経由し…

(+ (wt (car x)) (wt (car x)))は正の数ですか？ (wt (car x))が正なら、正ですね。 そういう当たり前のことがね 次のような主張positive/wtを作れば、そのフォーカスをうまい前提に書き換えられますね。 (dethm positive/wt (x) (equal (< '0 (wt x)) 't)) …

common-addends-<の公理を使うことで、<の引数にある2つの(wt (cdr x))をキャンセルできると思います。 (if (atom x) 't (if (atom (car x)) (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) (< (wt (rotate x)) (wt x)))) これを (dethm …

ひとつめは 公理の形に合わせるためには(equal (natp (wt (car x))) 't)じゃなくて (natp (wt (car x))でないとだめ ってこと これには9章の後半で出てきた、if-trueを使って都合のいい前提を作る作戦が使える

+と<についての公理言ってることはわかります

っていう話はここまで変形しないと言えないもの？ (if (atom x) 't (if (atom (car x)) 't (< (size (cons (car (car x)) (cons (cdr (car x)) (cdr x)))) (size (cons (cons (car (car x)) (cdr (car x))) (cdr x)))))) 反例なら上に上げた主張の時点でもう…

alignか それだ見覚えあったのは 確かそのときも全関数であることの証明だった

ついに10章 （といってもラスボスは付録Cにいると思われる） rotate なんかこの動きは見たことがある 全体的に言えばrotateしてる感じはあるけど ミクロに言うと何がどうなっているのかな コンスの数は4

set?/t-nilも普通に証明できるかな できない理由は思いつかない set?/tとset?/nilをあわせた手間よりは楽にできるんじゃないかな やってみよう

A部はset?を展開して整理するだけ すぐ終わる E部はやっぱりまず前提をスルーしてその内側から set?を展開して (atom xs)を整理して (member? (car xs) (cdr xs))で持ち上げて (set? (cdr xs))で持ち上げて 整理してやるだけ

set?/tとかset?/nilを証明しないといけませんかね。 そうですよ！ 178ページです。 そんだけ 自力でやってみるかな できるとわかってるだけでも足しになる 新しい技も覚えたし（使うかどうかわからないけど

set?/atomの定理に戻りましょう。 え、そっち？ set?/tとかset?/nilは？ この定理の証明は、ちょっとだけ意外で、ちょっとだけ楽しく、ちょっとだけで終わります。 set?/add-atomsの特殊ケースにすぎないのでちょっとだけで終わりそうな予感はしますが 意外…