kb84tkhrのブログ

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

本とペンをセットで持ち運びたい

本に線を引いたり書き込んだりするようになってきたのでペンをセットで
持ち運びたいと思うようになりました

万年筆のクリップで表紙に挟んだり
マグネットで挟んで止めるタイプのペンケースをくっつけてみたりしましたが
どうも具合がよろしくない

続きを読む

定理証明手習い (63) j-bob-lang

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は関数では書けませんよ、っていうパターンにハマってないんだっけ?

続きを読む

定理証明手習い (62) C 小さなお手伝い

付録CはJ-Bob自体の定義と解説です
本編にはYコンビネータとか継続渡しとかインタプリタみたいな中ボス大ボスがいなかったので
ここがそういう位置づけになるのかもしれません

ソースはダウンロード済みですが自分で打ち込みながら進めようと思います
ソースコードが載ってるかどうかは微妙に不安

続きを読む

定理証明手習い (61) 振り返り

本編は終わったのでここまでいったん振り返ってみます

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

続きを読む

定理証明手習い (60) align/align

進んでみたらわかることを期待して進む

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 (align (align x)) (align x))
            't)
        (if (equal (align (align (rotate x)))
                   (align (rotate x)))
            (equal (align (align x)) (align x))
            't)))


Defun帰納法にしたがって自分で作ってみます
主張はこれ

続きを読む

定理証明手習い (57) 見えない

142ページの

ここで関数wtを使いましょう。

から

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

を経由して

common-addends-<を使って(wt (cdr x))をキャンセルできますからね。

まで、何やってるのかわかんね感がぱない
言われたとおりにやればそうなるんだけど

(wt (cdr x))をキャンセルできる形に持っていける見込みがあって変形していってるんだろうか
その見通しってやつが見えない

ここは「洞察」ないのかな