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

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

小さな習慣は続いてたり増えてたりしますいいことなんですけど、小さいままなんですよね大きくしたいんだけど何かやめない限り大きくするすきまがない うーん残業？やっぱそこ？ここんとこ少し増えてるからなあ それでももう今さら途切れさせるのはもったい…

形式のチェックが続きます (<=len n args) nがargsの要素数以下かどうか <=lenは、引数リストの長さが指定した数以下かどうかを返します。 反対じゃないかな なおnが0以下のときは'nil nが0でargsが'()なら'tにしてもよさそうな気がするけど

ここから抜粋 問題解決大全 作者: 読書猿 出版社/メーカー: フォレスト出版 発売日: 2017/12/18 メディア: Kindle版 この商品を含むブログ (4件) を見る そこで、先延ばしを克服するのではなく、人間の「仕様」として受入、利用するアプローチを紹介しよう。…

普通に集合を扱う関数 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) 式のリストが正しいか 今まで出てきた関数の中ではなかなかの大モノ

(lookup name defs) defsからnameの定義を探す 見つからないときはnameを返す ちょっと不思議な仕様だけど役に立つのかな

なんのことかというと子供の話○○しなさい、って言ってもなかなかそのとおりにしてくれなかったりしますよね言うことを聞いてくれるようにいろんな言い換えを考えます

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…

コレ エイスース 7.9型タブレットパソコン ZenPad 3 8.0 SIMフリーモデル （ブラック）ASUS ZenPad 3 8.0 Z581KL-BK32S4 出版社/メーカー: エイスース メディア: この商品を含むブログ (3件) を見る 以前使っていたiPad Airはすっかり子供のものになってしま…

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

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

パネラーの後藤義雄氏の「せんみつでいい」（プログラミング教育をした1000人に３人しかプログラミングが身につかなかったとしても、裾野が広がって頂が高くなればいいんだ）は大失言だったかと。残りの997人が教材費払う合理的理由も、国税をつぎ込む合理性…

コード書いたら動かしたいしせっかく動かしたら残したいので結局テスト的なものを書くことになります (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は関数では書けませんよ、っていうパタ…

付録CはJ-Bob自体の定義と解説です 本編にはYコンビネータとか継続渡しとかインタプリタみたいな中ボス大ボスがいなかったので ここがそういう位置づけになるのかもしれません ソースはダウンロード済みですが自分で打ち込みながら進めようと思います 全ソー…

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

進んでみたらわかることを期待して進む 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-+の公理を使います。 : を経由し…

手帳にメモってそれを見ることができるようになった、というあたりが いいサイクルの回り始めだったと思います 『ちょっとしたことでうまくいく 発達障害の人が上手に働くための本』 - kb84tkhrのブログ せっかくなんでこのへんのことも書いておこうかと特に…

(+ (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を使って都合のいい前提を作る作戦が使える

(wt x)は常に自然数でしょうか？ わかりませんが、できると思います。 （証明が）できる、ってことかな？ could beみたいに書いてあったのかもしれないな それはともかくとして (natp (wt x))を'tに書き換えて、外側のifをif-trueで取り除けば いやーん 関数…

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