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

大詰め 定義43 xはaとbの"直接の帰結"である (define (IsConseq [x : GForm] [a : GForm] [b : GForm]) : Boolean (or (= a (Implies b x)) (∃ v <= x (and (IsVar (gsymbol+ v)) (= x (ForAll (gsymbol+ v) a)))))) 定義44 xは"形式的証明"である (define (…

自分の思いつきを書き留めているだけで誰かのために書いてるわけではないんですけどねでもブログに書くんだと思うと言葉遣いが変わります不思議ですね ていうかアウトプットの練習と思って書きはじめたのに自分の思いつきを書き留めてるだけ、ってのは目的に…

定義40 xは公理IVから得られる"論理式"である (define (IsAxiomIV [x : GForm]) (∃ u v y n <= x (and (IsVarType (gsymbol+ u) (+ n 1)) (IsVarType (gsymbol+ v) n) (IsForm (gsequence+ y)) (not (IsFree (gsymbol+ u) (gform+ y))) (= x (Exists (gsymbo…

定義36 xは公理IIから得られる"論理式"である (define (IsAxiomII [x : GForm]) : Boolean (or (IsSchemaII 1 x) (IsSchemaII 2 x) (IsSchemaII 3 x) (IsSchemaII 4 x))) 定義37 zは、yの中でvが"自由"な範囲に、"束縛"された"変数"を持たない (define (IsNo…

今日はひさしぶりに仕事でプログラム書いたといっても1行書くごとに1回検索みたいな感じなのでそんなに進まないけど 若干自分の仕事範囲を超えてる気もするけど一応プログラム書けるよ、っていうアピールも兼ねて できるかどうか試してみる、くらいの状況な…

定義33 xを、nだけ"型持ち上げ"したもの (define (typelift [n : Natural] [x : GForm]) (Min y <= (expt x (expt x n)) (∀ k <= (len x) (or (and (not (IsVar (elm x k))) (= (elm (gform+ y) k) (elm x k))) (and (IsVar (elm x k)) (= (elm (gform+ y) k…

結局キャストをいっぱい書くのが面倒になってこんな関数を作っていたりする (: gsequence+ (case-> (-> Natural GSequence) (-> GNumber GSequence))) (define gsequence+ (case-lambda [([x : Natural]) (gsequence (gnumber x))] [([x : GNumber]) (gseque…

定義25 "変数"vはxのn番目の場所では"束縛"されてない (define (IsFreeAt [v : GSymbol] [n : Natural] [x : GForm]) : Boolean (and (IsVar v) (IsForm x) (= v (elm x n)) (<= n (len x)) (not (IsBoundAt v n x)))) 定義26 vはxの"自由変数"である (defin…

定義23 xは論理式である (define (M23 [x : GSequence]) : Natural (expt (P (sqr (len x))) (* x (sqr (len x))))) (define (IsEndedWith [n : GSeqSeq] [x : GSequence]) : Boolean (= (elm n (len n)) x)) (define (IsForm [x : GSequence]) : Boolean (∃…

やっぱりマクロで書いてみたくなったので手持ちの武器の範囲を超えない程度に もういちどやってみる Minは型だけじゃなくて構造に近いレベルで差異があるので分けた (define-syntax (define-equipment stx) (syntax-parse stx ((_ name term notfound found)…

定義21 "¬(a)"または"(a)∨(b)"または"∀v(a)"である (: IsNotOp (-> GSequence GSequence Boolean)) (define (IsNotOp x a) (= x (Not a))) (: IsOrOp (-> GSequence GSequence GSequence Boolean)) (define (IsOrOp x a b) (= x (Or a b))) (: IsForallOp (-…

やっぱり型で悩んでいる たとえば(IsNumberType x)で言うと xは列であることを期待しているという意味ではGSequenceなんだけれども xは1から順に総当りで試していくだけの数だからGNumberな気もする 一方、(2以上なら)どんな数だって素因数分解はできるわけ…

IsVarTypeの型は (: IsVarType (-> GSymbol Natural Boolean))ではなくて (: IsVarType (-> GNumber Natural Boolean))の方が適切でしたかね xが記号かどうかもわかってないわけだから 型チェックがチェックしてくれるのはいいとして 自分が適切な型を与えて…

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

定義9 xだけからなる列 (: <> (-> GSymbol GSequence)) (define (<> x) (gsequence+ (expt 2 x))) 問題なし 定義10 xをカッコに入れた列 えーとこのxは列だな 記号じゃない 定義9のxは記号 まぎらわしい こういうまぎらわしいところを型チェックが見てくれる…

今日の成果 (if (= yk 0) ...)ではダメ（元のコード） (if (= yk (gnumber 0)) ...)でもダメ (if (= (ann yk Natural) 0) ...)でもダメ (if (= (cast yk Natural) 0) ...)なら成功する (if (= (+ yk 1) 1) ...)でも成功する 関数ごと再掲 (define (** x y) (…

(: Min≦ (All (a) (-> a (-> a Boolean) a))) のaはNumberかそのサブタイプです、っていう書き方はないのかな ってところは何か名案が見つかることを期待して放置 **の素因数分解版 (define (** x y) (let ((lenx (len x))) (let loop ((k : Natural 1) (n :…

今日ブックオフで見つけた本はこれ ふしぎの国のアリスの算数パズル (やさしい科学 (別巻1)) 作者: 山崎直美 出版社/メーカー: さ・え・ら書房 発売日: 1983/10 メディア: 単行本 購入: 1人 クリック: 1回 この商品を含むブログ (6件) を見る 鏡の国のアリス…

しばらくOptが出てこないというのは勘違い 定義7 列の長さ (: len (-> GSequence Natural)) ; 元のソース (define (len x) (Min≦ x (λ (k) (and (> (prime k x) 0) (= (prime (+ k 1) x) 0))))) ; 素因数分解を利用する版 (define (len x) (none-to-zero (fa…

そういえばGuideにパターンマッチをやってくれるmatchの例が上がってました (: assert-symbols! ((Listof Any) -> (Listof Symbol))) (define (assert-symbols! lst) (match lst [(list (? symbol? #{s : (Listof Symbol)}) ...) s] [_ (error "expected onl…

ここで自然数の世界からゲーデル数の世界に入ります GNumberなどの型がやっと登場 定数 (define c0 : GSymbol (gsymbol (gnumber 1))) (define cf : GSymbol (gsymbol (gnumber 3))) : : (define c0 : GSymbol 1)ではエラーになるのはしかたないんだけど ち…

Factorizationからn番目のFactorを取り出します (: factorization-nth (-> (Opt Factorization) Natural (Opt Factor))) (define (factorization-nth facz n) (: F (-> Factorization Natural (Opt Factor))) (define (F f n) (cond ((null? f) (None)) ((= …

子供の塾の説明会に行ってみたんですがすごいですねレベル高すぎといっても内容がすごく難しいとかじゃなくて方針っていうか考え方というかとにかくそこまで子供に考えさせるのか、っていうところに驚きました これはついていければすごいことになるなとしか…

では本体に戻って書き換え 型の部分を再掲 (struct None ()) (struct (a) Some ([v : a])) (define-type (Opt a) (U None (Some a))) (define-type Factor (Pairof Natural Natural)) (define-type Factorization (Listof Factor)) Factorizationは(Listof F…

どうも型周りのカンがつかめなくていろいろ試行錯誤してたら収拾がつかなくなってきたんですがいったんこのへんで書いておきます 型の定義はこうなってます FactorはPairofではなくてstructで表現することに これは単にせっかくそういうのがあるんだからこう…

図書館でこんな本を見つけました 算数を忘れた国の冒険 脱出編 (遊々算数アドベンチャー) 作者: 正木孝昌 出版社/メーカー: 学校図書 発売日: 2003/12 メディア: 単行本 この商品を含むブログを見る 教えてもらったやり方で解くのではなくどうやって解くかを…

最近すこし時間が取れてないのでRacketネタがちょっと書けないということで何かほかに書くこと・・・というのがちょっと浮かばないネタになるかなと思って書いてあったキーワードみたいなものがいくつかあるんだけど見てても何かこう書くところまでいかない…

新しいものを買ったり、新しいことを始めたりしたときは1ヶ月後とか1年後とかに振り返りの予定を入れておくのがおすすめ振り返りの日までは、と思うと継続力の足しにもなる気がします 自分はあんまり振り返りってやつをしようとしない傾向があるんですが（し…

0の素因数分解とか、2の素因数分解の3番目の因数とか変なやつは'(0 .0)で表しました 後で型による表現も試してみたいと思います 失敗を表せればいいので、ちょうどGuideに載ってたOpt型が使えそうです (struct None ()) (struct (a) Some ([v : a])) (define…