ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (9)
「10.8.4 変数・記号・論理式」の続き
ものは試しでprime
をこんな風にしてみました
(define (prime n x)
(let ((p (P n)))
(if (CanDivide x p) p 0)))
素因数分解には必ず2から歯抜け無しで素数が出てくるという前提
動かしてみると
> (profile (paren (<> 7)))
Profiling results
-----------------
Total cpu time observed: 0ms (out of 0ms)
Number of samples taken: 0 (once every 0ms)
====================================
Caller
Idx Total Self Name+srcLocal%
ms(pct) ms(pct) Callee
====================================
5467500000000000
一瞬にして終わってしまいました
ポイントはprime
の方だったのか
(define (prime n x)
(cond ((= n 0) 0)
(else (let loop ((k 1) (cnt 0))
(let* ((p (P k))
(c (if (CanDivide x p)
(+ cnt 1)
cnt)))
(cond ((= c n) p)
((> p x) 0)
(else (loop (+ k 1) c))))))))
呼ばれるたびに素因数を試していくのでもったいないっちゃあもったいないとは
思ってたんですけどね
そうか、len
がこれ以上素因数がないことを確認しようとしてるから
そのときxまでのすべての素数を求めることになりますね
これはかなり壮大な無駄でした
素因数が見つかったら割り算していけばいいか
(define (prime n x)
;(printf "prime ~a ~a~n" n x)
(cond ((= n 0) 0)
(else (let loop ((k 1) (cnt 0) (x x))
(define (newc x p cnt)
(if (CanDivide x p) (+ cnt 1) cnt))
(define (newx x p)
(if (CanDivide x p) (newx (/ x p) p) x))
(let* ((p (P k))
(c (newc x p cnt))
(x (newx x p)))
(cond ((= c n) p)
((= x 1) 0)
(else (loop (+ k 1) c x))))))))
やってることはもうほとんど素因数分解ですね
一度素因数分解して、結果を保持しておくという作戦もありそうです
遅そうだったらそこまでやろうかな
> (profile (paren (<> 7)))
Profiling results
-----------------
Total cpu time observed: 0ms (out of 2ms)
Number of samples taken: 0 (once every 0ms)
====================================
Caller
Idx Total Self Name+srcLocal%
ms(pct) ms(pct) Callee
====================================
5467500000000000
遅くなかったのでこれで
定義14 (x)∨(y)
定義15 ∀x(a)
not
を¬
として定義してましたがその作戦はforall
で破綻することが見えたのでNot
として定義することにしました
まぎらわしいですが
or
も丸かぶりなのでOr
でいきますforall
はカブリませんが合わせてForAll
で
ところで結城先生はどういう基準でIsVar
のようにSnakeCaseにしたりforall
のように小文字だけで書いたりを使い分けてるんでしょう?
述語はSnakeCaseかな?
(define (Or x y)
(** (** (paren x) (<> cor)) (paren y)))
(define (ForAll x a)
(** (** (<> call) (<> x)) (paren a)))
Or
のx
は列ですがForall
のx
は記号
間違えそうです
さてさらに数が大きくなりそうですが大丈夫でしょうか
> (Or (<> (var 1 1)) (<> (var 2 1)))
1098415942078875156883188276624748911614734244278525624785106627500000000000
> (gnum clp (var 1 1) crp cor clp (var 2 1) crp)
1098415942078875156883188276624748911614734244278525624785106627500000000000
> (ForAll (var 1 1) (<> (var 1 2)))
1907391355716272577177453857401213581781246615597216081581480551016412719746654430560208144167891773573871493887925165104041590156805787719907593773726190619343758282225408887767321242291919846915757686316658584841638667303678601088656737960265077048917335396654851775000000000
> (gnum call (var 1 1) clp (var 1 2) crp)
1907391355716272577177453857401213581781246615597216081581480551016412719746654430560208144167891773573871493887925165104041590156805787719907593773726190619343758282225408887767321242291919846915757686316658584841638667303678601088656737960265077048917335396654851775000000000
単純な式でやってもかなりすさまじい数字になってますが大丈夫です
ユーリ「IsVar(x)はチェックしなくていいのかにゃ?」
なぜユーリはx
だけ入力チェックをしたくなったんだろうa
が論理式であるかどうかはチェックしたくなりませんか?Not
やOr
のx
、y
も同様
遡ってみると確かに定義12までは入力チェック不要
列を扱う場合は何の列かというのさえ気にしなければなんでもあり
でも式を扱うようになるとそもそも使える記号が
0、f、¬、∨、∀、(、)と変数だけになるわけだし
今はまだチェックできないから、ってことじゃないよな・・・?