kb84tkhrのブログ

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

incompleteness

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (58)

大詰め 定義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 (…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (57)

定義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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (56)

定義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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (55)

定義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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (54)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (53)

定義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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (52)

定義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 (∃…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (50)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (50)

定義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 (-…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (49)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (48)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (47)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (46)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (46)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (44)

しばらく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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (43)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (42)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (41)

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)) ((= …

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (39)

では本体に戻って書き換え 型の部分を再掲 (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…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (40)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (38)

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

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (37)

素因数分解の本体 素因数分解は(Listof (Pairof Natural Natural))という型で表しています 0の素因数分解とか、2の素因数分解の3番目の因数とか変なやつは'(0 .0)で表しました

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (36)

さてPが定義できたので素因数分解と定義3の再定義を まずは補助関数から

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (35)

定義4 nの階乗 型をつけただけ

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (34)

というわけでマクロなし作戦

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (33)

関数を定義したりマクロを定義したりするややこしいマクロを直すよりも まずはできそうなところからやってみます

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (32)

では #lang typed/racket 動くだけは動いたりするかな?

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (31)

さてTyped Racketもざっと見たので型をつけていってみます 動かせないのでテストもできませんでしたが うまく型を付けられれば静的なチェックだけでもバグが見つかるのではと(実際ときどき間違えてたし) さてどんな型をつけましょうか 型っぽいものはゲー…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (30)

いっぱい関数出てきたなと思いましてね 以前、Scheme手習いでインタプリタ作ったときに書いたような 関数の呼び出し関係の図を作ってみようと思ったんですけどね たいへんな目に会いました 思ってたのを遥かに超えて複雑でした うまく配置してみようという気…

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (29)

定義43 xはaとbの"直接の帰結"である (define (IsConseq x a b) (or (= a (implies b x)) (∃ v ≦ x (and (IsVar v) (= x (ForAll v a)))))) ところで推論規則って、これだけで足りるんですか 論理学とか見ると、もっといろいろ書いてあるっぽいんですけど 推…