kb84tkhrのブログ

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

2017-12-24から1日間の記事一覧

ゲーデルの不完全性定理の証明のアレを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…