kb84tkhrのブログ

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

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

Orxは列ですがForallxは記号
間違えそうです

さてさらに数が大きくなりそうですが大丈夫でしょうか

> (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が論理式であるかどうかはチェックしたくなりませんか?
NotOrxyも同様

遡ってみると確かに定義12までは入力チェック不要
列を扱う場合は何の列かというのさえ気にしなければなんでもあり
でも式を扱うようになるとそもそも使える記号が
0、f、¬、∨、∀、(、)と変数だけになるわけだし

今はまだチェックできないから、ってことじゃないよな・・・?