ElementForm周辺が盛大にバグってました ぐぬぬ 変数と、ひとつの変数だけからなる列が混乱しまくってる どっちも整数だけど、別の型として扱ってれば検出できたかな でもさらっと考えて見るとこのプログラムって型付けしにくそうだな もう少しでひととおり…

定義37 zは、yの中でvが"自由"な範囲に、"束縛"された"変数"を持たない (define (IsNotBoundIn z y v) (not (∃ n ≦ (len y) (∃ m ≦ (len z) (∃ w ≦ z (and (= w (elm z m)) (IsBoundAt w n y) (IsFreeAt v n y))))))) こういうの見るとつい 束縛が入れ子にな…

定義35 xは公理II-nから得られる"論理式"である 定義36 xは公理IIから得られる"論理式"である (define (IsSchemaII n x) (case n ((1) (∃ p ≦ x (and (IsForm p) (= x (Implies (Or p p) p))))) ((2) (∃ p q ≦ x (and (IsForm p) (IsForm q) (= x (Implies p…

もうほとんど「Racketで書いてみる」という部分には意味がなくなっている気がする 今日このごろですが続けます 10.8.5 公理・定理・形式的証明 やっと次の節に入りました 最近はただ式をコードに置き換えてるだけって感じになってましたが どうもそれ以前の…

定義32 "(a)→(b)"、"(a)∧(b)"、"(a)⇄(b)"、"∃x(a)"を得る関数 (define (Implies a b) (Or (Not a) b)) (define (And a b) (Not (Or (Not a) (Not b)))) (define (Equiv a b) (And (Implies a b) (Implies b a))) (define (Exists x a) (Not (ForAll x (Not a…

ちょっと蒸し返しますけど (define (M23 x) (expt (P (sqr (len x))) (* x (sqr (len x))))) ここって素数指数表現が歯抜けになってないことを前提にしてることになりませんか primeからここまで、歯抜けでもいい流れできてたと思うんですが まあでも、歯抜…

定義27 xのn番目の要素をcで置き換えたもの (define (substAtWith x n c) (Min z ≦ (M8 x c) (∃ a b ≦ x (and (= n (+ (len a) 1)) (= x (** (** a (<> (elm x n))) b)) (= z (** (** a c) b)))))) aという列があって aとxのn番目の要素とbをつないだものがx…

定義24 "変数"vはxのn番目の場所では"束縛"されている (define (IsBoundAt v n x) (and (IsVar v) (IsForm x) (∃ a b c ≦ x (and (= x (** (** a (ForAll v b)) c)) (IsForm b) (<= (+ (len a) 1) n) (<= n (+ (len a) (len (ForAll v b)))))))) 変数が束縛…

前回の記事についてTwitterで泣きを入れてみたところ なんと結城先生直々にリプいただけました 2乗が出てくるからくりがつかめました いただいたリプ 「部分論理式の総数」で押さえているようです。添付画像は岩波文庫『不完全性定理』の当該部分（ゲーデル…

まだちょっとすっきりしない M23をもういちど考え直す (define (M23 x) (expt (P (sqr (len x))) (* x (sqr (len x))))) (define (IsEndedWith n x) (= (elm n (len n)) x)) (define (IsForm x) (∃ n ≦ (M23 x) (and (IsFormSeq n) (IsEndedWith n x)))) 見…

「10.8.4 変数・記号・論理式」の続き なにごともなかったかのように続けてみる 定義23 xは論理式である (define (M23 x) (expt (P (sqr (len x))) (* x (sqr (len x))))) (define (IsEndedWith n x) (= (elm n (len n)) x)) (define (IsForm x) (∃ n ≦ (M23…

「10.8.4 変数・記号・論理式」の続き 定義22 "基本論理式"から組み上げた"論理式"の列である うーナントカ以下じゃなくてナントカ未満のパターンもあったか まあいいやとりあえず1引けばおんなじことだし (define (IsFormSeq x) (and (> (len x) 0) (∀ n ≦ …

「10.8.4 変数・記号・論理式」の続き 定義21 "¬(a)"または"(a)∨(b)"または"∀v(a)"である とりあえずそのまま (define (IsNotOp x a) (= x (Not a))) (define (IsOrOp x a b) (= x (Or a b))) (define (IsForallOp x a) (∃ v ≦ x (and (IsVar v) (= x (ForAl…

「10.8.4 変数・記号・論理式」の続き 定義20 xは"基本論理式"である (define (IsElementForm x) (∃ a b n ≦ x (and (IsNthType a (+ n 1)) (IsNthType b n) (= x (** a (paren b)))))) 遅いのでなんとかしましょう 全然ダメなのも含めて全部総当りでやるの…

「10.8.4 変数・記号・論理式」の続き 定義20 xは"基本論理式"である 変数が三つになった ぐぬぬ さすがに３つめのパターンを追加するというわけにもいくまい Fear of Macrosになんかあったな・・・いやないな じゃあSMPHにも・・・あれないな どっかで再帰…

「10.8.4 変数・記号・論理式」の続き さて前回、勘違いに気づくまではもっと高速化しないとと思って 素因数分解する版を書き始めてました 乗った船なので続けてみます 素因数分解は12を((2 . 2) (3 . 1))と表現してみました ((0 . 0))というのは0とか1を因…

「10.8.4 変数・記号・論理式」の続き 定義18 "第n型の記号"である (define (IsNthType x n) (or (and (= n 1) (IsNumberType x)) (and (> n 1) (∃ v ≦ x (and (IsVarType v n) (= x (<> v))))))) さて高速化 もともと、#tが帰るようなときは遅くないんです…

「10.8.4 変数・記号・論理式」の続き 時間がかかるのはいつものパターンで書き換え (define (IsNumberType x) (let loop ((k 1)) (let ((e (elm x k))) (cond ((not (= e cf)) (and (or (= e c0) (IsVarType e 1)) (= (elm x (+ k 1)) 0))) (else (loop (+ …

「10.8.4 変数・記号・論理式」の続き 定義16 xの、n番目の後続数 定義17 nに対する"数項" (define (succ n x) (cond ((= n 0) x) (else (** (<> cf) (succ (- n 1) x))))) (define (￣ n) (succ n (<> c0))) 数項の"￣"はちょっと無理がある気もしますが気…

「10.8.4 変数・記号・論理式」の続き ものは試しでprimeをこんな風にしてみました (define (prime n x) (let ((p (P n))) (if (CanDivide x p) p 0))) 素因数分解には必ず2から歯抜け無しで素数が出てくるという前提動かしてみると > (profile (paren (<> 7…

「10.8.4 変数・記号・論理式」 ここらへんから証明っぽくなってきます 定義11 xは"第n型"の"変数"である (define (IsVarBase p) (and (> p crp) (IsPrime p))) (define (IsVarType x n) (and (>= n 1) (∃ p ≦ x (and (IsVarBase p) (= x (expt p n)))))) こ…

「10.8.3 列」の続きの続き このへんのMinの入れ子で時間がかかってるというのはありそうな話ですIsPrime以下は一応書き換え済みなのでこの範囲で高速化してみますか primeを書き直し素数が歯抜け無しで出てくるとは限らない、という前提はキープ ; 元のソー…

「10.8.3 列」の続き > (time (** 12 4)) ; [2 1]という列と[2]という列の連結 cpu time: 35571 real time: 35565 gc time: 1153 300 > (time (** 12 12)) ; [2 1]という列と[2 1]という列の連結 お返事がありません 書き直し ; 元のソース ;(define (M8 x y…

「10.8.3 列」 定義6 n番目の要素 (define (CanDivideByPower x n k) (CanDivide x (expt (prime n x) k))) (define (elm x n) (Min k ≦ x (and (CanDivideByPower x n k) (not (CanDivideByPower x n (+ k 1)))))) (P n)ではなく(prime n x)を使っているの…

「10.8.2 整数論」の続き （単位はミリ秒） > (time (P 8)) cpu time: 12989 real time: 12992 gc time: 1441 19 これだとテストもままならなくなりそうなのでもうちょっと速くなるようにしてみますか とりあえず簡単なところから ; もとの定義 ;(define (Ca…

「10.8.2 整数論」 このへんは単なる数の計算 定義1 割り切れる？関数名はできるだけ数学ガールに合わせていきます (define (CanDevide x d) (∃ n ≦ x (= x (* d n)))) 割り切れないときにx以下のnすべてについて試してしまってもったいないですがとりあえず…

「10.8.1 装備を整える」の続き 同様に∃x≦M[...]とmin x≦M[...]を定義します (define (∃≦ max f) (let loop ((x 1)) (cond ((> x max) #f) ((f x) #t) (else (loop (+ x 1)))))) (define-syntax (∃ stx) (syntax-parse stx #:literals (≦) [(_ v:id ≦ max:ex…

数学ガールのゲーデル巻を読んでると、「定義1」から「定義46」までなんだかプログラムを読んでるみたいですよね？ですよね？ 数学ガール/ゲーデルの不完全性定理 (数学ガールシリーズ 3) 作者: 結城浩 出版社/メーカー: SBクリエイティブ 発売日: 2009/10/2…