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、¬、∨、∀、(、)と変数だけになるわけだし

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

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

「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))))))

これはどうかな

> (time (IsVarType (+ (expt 17 3) 1) 3))
cpu time: 7 real time: 6 gc time: 0
#f

微妙なところ
型が大きいと時間がかかりそうですが先へ進みます

ところで

僕「"変数"の" "の意味は?」
ミルカ「メタ数学の概念という意味」

実はここで何を言っているかすっきりわかってなかったりするんですよね
P上の変数と、メタ数学上の"変数"があるってことですよね

ただの数であってP上の数(fff0とか)じゃないから、P上の変数じゃないってこと?
いやP上の変数はx1とかだし
xの実体はただの数で、メタ数学上の解釈で初めて変数になる、ってことですかね

たとえば2^9*3^17^2*5^11*7^17*11^13っていう数は
∀x2(x1)っていう式を表してるわけですけどこれはPの式?
それともメタ数学の概念?
一見Pの式には見えませんが、見慣れない文字と表記方法で書いてるってだけなんですよね
だから自分的にはPの式に思えるんですけどね

ミルカ「つまり、xは意味の世界での変数を表しているのではない。形式的
  体系Pのほうで定義された変数のゲーデル数を表しているんだ」

ミルカさんもそう言ってはいると思うんですが
「メタ数学の概念」という言葉がピンときてません
もしかして大事なことかもしれませんがこれくらいにして

このへんで、ゲーデル数を直接作る関数を作っておきます
これからテストで使いそうなので

まずは変数を(expt 17 3)とか書かないでいいようにしておきます
x1を(var 1 1)、z3を(var 3 3)などと書くことにします

(define (var n c) (expt (P (+ 6 n)) c))

ゲーデル数を作る方

(define (gnum . seq)
  (define (iter s k n)
    (if (null? s)
        n
        (iter (cdr s) (+ k 1) (* (expt (P k) (car s)) n))))
  (iter seq 1 1))

さっきの∀x2(x1)で試してみましょう

> (gnum call (var 1 2) clp (var 1 1) crp)
155150868122395845239730380258828948544470333645526905417109467051986545180149117421814751229978010870695495625428839601792638246935390849457292566300089904991446507775000000000

合ってるかどうかさっぱりわかりませんね

> (* (expt 2 call)
     (expt 3 (var 1 2))
     (expt 5 clp)
     (expt 7 (var 1 1))
     (expt 11 crp))
155150868122395845239730380258828948544470333645526905417109467051986545180149117421814751229978010870695495625428839601792638246935390849457292566300089904991446507775000000000

やや信頼性に欠けるテストですがまあいいことにしましょう

定義12 xは"変数"である

(define (IsVar x)
  (∃ n ≦ x (IsVarType x n)))

定義13 ¬(x)

素直に式の形を表現していきます
定義に寄ってxがひとつの記号を表してたり列を表してたりするので注意が必要
この定義では列ですね

(define (¬ x)
  (** (<> cnot) (paren x)))
> (profile (paren (<> 7)))
Profiling results
-----------------
  Total cpu time observed: 61815ms (out of 63058ms)
  Number of samples taken: 1121 (once every 55ms)
  (Hiding functions with self<1.0% and local<2.0%: 1 of 16 hidden)

============================================================================
                                  Caller
 Idx    Total         Self      Name+src                              Local%
        ms(pct)       ms(pct)     Callee
============================================================================
 :
 略
 :
------------------------------------------------------------------------
                                  run [10]                            100.0%
[11] 61815(100.0%)     0(0.0%)  ** ...tudy/Incompleteness/incompleteness.rkt:265:0
                                  loop [12]                           100.0%
----------------------------------------------------------------------------
                                  ** [11]                             100.0%
[12] 61815(100.0%)    50(0.1%)  loop ...dy/Incompleteness/incompleteness.rkt:242:6
                                  loop [13]                            99.9%
----------------------------------------------------------------------------
                                  loop [12]                           100.0%
[13] 61765(99.9%)    432(0.7%)  loop ...y/Incompleteness/incompleteness.rkt:135:14
                                  loop [14]                            98.9%
----------------------------------------------------------------------------
                                  loop [13]                           100.0%
[14] 61065(98.8%)  40141(64.9%) loop ...y/Incompleteness/incompleteness.rkt:172:14
                                  loop [15]                            34.3%
----------------------------------------------------------------------------
                                  loop [14]                           100.0%
[15] 20924(33.8%)  20924(33.8%) loop ...dy/Incompleteness/incompleteness.rkt:107:7
----------------------------------------------------------------------------
5467500000000000
> 

incompleteness.rkt:172:14はprimesのloop、ncompleteness.rkt:107:7はPのloopです
ほとんどが素数を求めてる時間っぽいですね

同じことをもういちど実行すると瞬時に計算が終わります
素数をハッシュに覚えたままだからかと
もしかして今まで高速化できたと思ってたのもそのせいかも(涙

> (profile (paren (<> 7)))
Profiling results
-----------------
  Total cpu time observed: 98ms (out of 141ms)
  Number of samples taken: 2 (once every 49ms)

========================================================================
                              Caller
 Idx  Total      Self       Name+src                              Local%
      ms(pct)    ms(pct)      Callee
========================================================================
 :
 略
 :
------------------------------------------------------------------------
                              run [10]                            100.0%
[11]  98(100.0%)  0(0.0%)   ** ...tudy/Incompleteness/incompleteness.rkt:265:0
                              loop [12]                           100.0%
------------------------------------------------------------------------
                              ** [11]                             100.0%
[12]  98(100.0%)  0(0.0%)   loop ...dy/Incompleteness/incompleteness.rkt:242:6
                              loop [13]                           100.0%
------------------------------------------------------------------------
                              loop [12]                           100.0%
[13]  98(100.0%) 98(100.0%) loop ...y/Incompleteness/incompleteness.rkt:135:14
------------------------------------------------------------------------
5467500000000000

うーんどうするかなあ
ちょっとアイデアがありません
ここらへんであきらめて関数を定義するだけにする?

2種類のキレイ好き

世界には2種類のキレイ好きがいるようですね

ひとつめのキレイ好きは、そのまんまですがキレイだとうれしくて
掃除するのも楽しいというタイプ
キレイ好きと言って思い浮かべるのはこっちでしょうか

もうひとつのキレイ好きは、キレイなのが好きというより汚いのが嫌だから
掃除するというタイプ
掃除してても特に楽しいわけじゃないようです
完璧にキレイな状態が標準で、少しでもホコリが落ちてるとマイナス

まあウチのヨメのことなんですけどね
大変そうだなあと思います

ダンナがこんなだしね
自分は、汚いのはかなり平気だし掃除もそんなに嫌いじゃありません
特に、目に見えてきれいになるようなときは楽しいんですけど
今は毎日掃除してていつもキレイなので掃除はそんなに楽しくはありません

まあでもそういう状態が長く続くとちょっと汚いのは嫌だなあと
いう気になってきます
生まれてからずっとそういう状態だとちょっとのホコリも許せない、
ってなっちゃっても不思議ではないのかなあ

でももうちょっといいかげんにできると楽だよ?

ハーディ『ある数学者の弁明』私家版翻訳、ですってよ

ハーディっていう数学者がいまして、自分には数学自体の功績よりも
ラマヌジャンを見つけて育てたっていう方が印象的な人なんですが
なんかユニークな人でもあったみたいで
この人の書いた「ある数学者の弁明」って本が面白そうだな―読んで
みたいなーと思っていたんですよね 

ある数学者の生涯と弁明 (シュプリンガー数学クラブ)

ある数学者の生涯と弁明 (シュプリンガー数学クラブ)

 

なんか題名だけでも面白そうな気がしませんか

こんなことが書いてあるそうです(ちょっと先回りですが引用)

専門の数学者にとって、自分が数学について書いているというのは憂鬱なものだ。数学者の役割とは何かをなすこと、新しい定理を証明すること、数学という学問に何かを付け加えることであって、自分や他の数学者がしてきた仕事について語ることではない。(略)解説、批評、評価といったことは、二流の知性の仕事である。

今だったら炎上上等的なスタンス?
他も読んでみたくなります

でもあんまり本屋では見かけなくて
ていうかたぶん一時は絶版してたらしくて
どうやら再出版されたようなんですがやっぱり見かけなくて
でもさすがに題名だけで買う気もしなくて
今までずっとほしいものリストに入ってたんですが

自力で翻訳したものをオンラインで公開されてる方がいました

イギリスの数学者G. H. ハーディ(1877–1947)がその晩年に書いた『ある数学者の弁明』(原題:A Mathematician's Apology)という本があります。すでに出版されている日本語訳もあるのですが(柳生孝昭訳の『ある数学者の生涯と弁明』所収)、日本における著作権保護期間が終了していますので、別の翻訳をつくってみました。

ハーディ『ある数学者の弁明』私家版翻訳

これはちょっとうれしい

本よりもちょっとボリュームが少ないかな、と思ったんですが

原著は1940年にケンブリッジ大学出版局から出版され、またその後、C. P. スノーによる長い「序文(Foreword)」を加えた版が1967年に出ました。この翻訳では1967年版を底本とし、ハーディの書いた部分のみを訳出しています。

 だそうなのでそのせいかもしれません
気のせいかもしれません

読むのはこれからです
楽しみ楽しみ

あ、英語なら
http://www.math.ualberta.ca/~mss/misc/A%20Mathematician's%20Apology.pdf
で読めるようです

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

「10.8.3 列」の続きの続き

このへんのMinの入れ子で時間がかかってるというのはありそうな話です
IsPrime以下は一応書き換え済みなのでこの範囲で高速化してみますか

primeを書き直し
素数が歯抜け無しで出てくるとは限らない、という前提はキープ

; 元のソース
;(define (CanDivideByPrime x p)
;  (and (CanDivide x p) (IsPrime p)))
;
;(define (prime n x)
;  (cond ((= n 0) 0)
;        (else (Min p ≦ x (and (< (prime (- n 1) x) p)
;                              (CanDivideByPrime x p))))))

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

elmを書き直し
これでMinを使っている関数はlenしかなくなりました

; 元のソース
;(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))))))

(define (elm x n)
  (let ((np (prime n x)))
    (let loop ((k 1) (x x))
      (cond ((not (CanDivide x np)) (- k 1))
            (else (loop (+ k 1) (/ x np)))))))

実行

> (time (paren (<> c0)))
cpu time: 14 real time: 14 gc time: 0
7500000000000

おk

しかしこれも2^7500000000000とかが出てくるまでの命

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

「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)
;  (expt (P (+ (len x) (len y))) (+ x y)))
;
;(define (** x y)
;  (Min z ≦ (M8 x y)
;       (and (∀ m ≦ (len x)
;               (⇒ (<= 1 m) (= (elm z m) (elm x m))))
;            (∀ n ≦ (len y)
;               (⇒ (<= 1 n) (= (elm z (+ (len x) n)) (elm y n)))))))

(define (** x y)
  (let ((lenx (len x)))
    (let loop ((k 1) (n x))
      (let ((yk (elm y k)))
        (if (= yk 0)
            n
            (loop (+ k 1) (* n (expt (P (+ lenx k)) yk))))))))

実行

> (time (** 12 4))
cpu time: 0 real time: 0 gc time: 0
300
> (time (** 12 12))
cpu time: 0 real time: 1 gc time: 0
2100

おk

定義9 xだけからなる列

(define (<> x) (expt 2 x))

定義10 xをカッコに入れた列

(define (paren x)
  (** (** (<> clp) x) (<> crp)))
> (time (paren (<> c0)))
cpu time: 55863 real time: 55844 gc time: 3880
7500000000000

さっきのテストじゃ全然甘かった
つらい
ただの(0)という式を作るだけで1分かかることもつらければ
(0)ゲーデル数が7500000000000というのも相当なつらさ
いや相当などころではないか
式の列を作ったら最低でも2^7500000000000になるんだもんな

先のことは考えず目の前の問題を何とかする方向で
調べてみると簡単にプロファイルが取れるようなのでやってみます

> (require profile)
> (profile (paren (<> c0)))
Profiling results
-----------------
  Total cpu time observed: 53481ms (out of 53918ms)
  Number of samples taken: 936 (once every 57ms)

============================================================================
                                  Caller
 Idx    Total         Self      Name+src                              Local%
        ms(pct)       ms(pct)     Callee
============================================================================
                                  loop [14]                           100.0%
 [1] 53481(100.0%) 13314(24.9%) ??? ...udy/Incompleteness/incompleteness.rkt:30:27
                                  CanDivideByPower [3]                 59.3%
                                  loop [14]                            29.5%
----------------------------------------------------------------------------
 [2] 53481(100.0%)     0(0.0%)  loop ...ib/mred/private/wx/common/queue.rkt:400:18
                                  call-with-break-parameterization [4]100.0%
----------------------------------------------------------------------------
                                  ??? [1]                             100.0%
 [3] 53481(100.0%)  2100(3.9%)  CanDivideByPower ...eness/incompleteness.rkt:157:0
                                  loop [14]                            96.1%
----------------------------------------------------------------------------
                                  ??? [11]                             50.0%
                                  loop [2]                             50.0%
 [4] 53481(100.0%)     0(0.0%)  call-with-break-parameterization ...heme.rkt:147:2
                                  ??? [6]                              50.0%
                                  loop [5]                             50.0%
----------------------------------------------------------------------------
                                  call-with-break-parameterization [4]100.0%
 [5] 53481(100.0%)     0(0.0%)  loop .../drracket/drracket/private/rep.rkt:1131:24
                                  call-with-exception-handler [8]     100.0%
----------------------------------------------------------------------------
                                  call-with-break-parameterization [4]100.0%
 [6] 53481(100.0%)     0(0.0%)  ??? ...lib/mred/private/wx/common/queue.rkt:505:32
                                  ??? [7]                             100.0%
----------------------------------------------------------------------------
                                  ??? [6]                             100.0%
 [7] 53481(100.0%)     0(0.0%)  ??? ...-lib/mred/private/wx/common/queue.rkt:454:6
                                  loop [9]                            100.0%
----------------------------------------------------------------------------
                                  loop [5]                            100.0%
 [8] 53481(100.0%)     0(0.0%)  call-with-exception-handler ...re-scheme.rkt:264:2
                                  profile-thunk14 [10]                100.0%
----------------------------------------------------------------------------
                                  ??? [7]                             100.0%
 [9] 53481(100.0%)     0(0.0%)  loop .../drracket/drracket/private/rep.rkt:1426:17
                                  ??? [11]                            100.0%
----------------------------------------------------------------------------
                                  call-with-exception-handler [8]     100.0%
[10] 53481(100.0%)     0(0.0%)  profile-thunk14 ...e/pkgs/profile-lib/main.rkt:9:0
                                  run [12]                            100.0%
----------------------------------------------------------------------------
                                  loop [9]                            100.0%
[11] 53481(100.0%)     0(0.0%)  ??? ...gs/drracket/drracket/private/rep.rkt:1105:9
                                  call-with-break-parameterization [4]100.0%
----------------------------------------------------------------------------
                                  profile-thunk14 [10]                100.0%
[12] 53481(100.0%)     0(0.0%)  run ...t v6.2/share/pkgs/profile-lib/main.rkt:31:2
                                  loop [13]                           100.0%
----------------------------------------------------------------------------
                                  run [12]                            100.0%
[13] 53481(100.0%)     0(0.0%)  loop ...dy/Incompleteness/incompleteness.rkt:205:4
                                  loop [14]                           100.0%
----------------------------------------------------------------------------
                                  ??? [1]                              20.5%
                                  CanDivideByPower [3]                 37.8%
                                  loop [13]                            41.7%
[14] 53481(100.0%) 33580(62.8%) loop ...dy/Incompleteness/incompleteness.rkt:22:11
                                  ??? [1]                              73.4%
                                  CanDivideByPrime [15]                 3.2%
----------------------------------------------------------------------------
                                  loop [14]                           100.0%
[15]  4486(8.4%)    4486(8.4%)  CanDivideByPrime ...eness/incompleteness.rkt:102:0
----------------------------------------------------------------------------
7500000000000
> 

Nameは関数名のはずなんですが???は何でしょう
マクロかな? → ラムダのことでした なるほど
それにloopもたくさん出てくるせいでわかりづらいですが何しろ

[14] 53481(100.0%) 33580(62.8%) loop ...dy/Incompleteness/incompleteness.rkt:22:11

が一番時間を取ってるみたいなのでここを見てます
???CanDivideByPowerloop???→CanDivideByPrimeという呼び出し順
CanDivideByPowerelmからしか呼ばれてませんね
そしてCanDivideByPowerprimeを、primeCanDivideByPrime
呼んでいます

(define (elm x n)
  (Min k ≦ x (and (CanDivideByPower x n k)
                  (not (CanDivideByPower x n (+ k 1))))))

(define (CanDivideByPower x n k)
  (CanDivide x (expt (prime n x) k)))

(define (prime n x)
  (cond ((= n 0) 0)
        (else (Min p ≦ x (and (< (prime (- n 1) x) p)
                              (CanDivideByPrime x p))))))

(define (CanDivideByPrime x p)
  (and (CanDivide x p) (IsPrime p)))

このへんのMinの入れ子で時間がかかってるというのはありそうな話です
IsPrime以下は一応書き換え済みなのでこの範囲で高速化してみますか

今日はここまで