kb84tkhrのブログ

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

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

しばらくOptが出てこないというのは勘違い

定義7 列の長さ

(: len (-> GSequence Natural))

; 元のソース
(define (len x)
  (Min≦ x (λ (k) (and (> (prime k x) 0)
                      (= (prime (+ k 1) x) 0)))))

; 素因数分解を利用する版
(define (len x)
  (none-to-zero (factorization-length (factorization x))))

定義8 列の連結

まずは元の定義・・・

(: M8 (-> GSequence GSequence Natural))
(define (M8 x y)
  (expt (P (+ (len x) (len y))) (+ x y)))

(: ** (-> GSequence GSequence GSequence))
(define (** x y)
  (gsequence+
   (Min≦ (M8 x y)
         (λ (z)
           (and (∀≦ (len x)
                    (λ (m) (⇒ (<= 1 m)
                              (= (elm (gsequence+ z) m)
                                 (elm x m)))))
                (∀≦ (len y)
                    (λ (n) (⇒ (<= 1 n)
                              (= (elm (gsequence+ z)
                                      (+ (len x) n)) (elm y n))))))))))

これは若干不満
型のエラーが出ないようにしていったらこうなってしまったんですが
zNatural型でelmに適用するときGSequence型にしてるというのが
最初からzGSequence型にしたいんですけど
そうするとMin≦の引数の型に合わなくなってしまうし
Min≦(や∀≦∃≦)をPolymorficな関数にするのがいいのかな?

(: Min≦ (-> Natural (-> Natural Boolean) Natural))

の代わりに

(: Min≦ (All (a) (-> a (-> a Boolean) a)))

とか
そうすると今度はinstが必要になってきてしまうし・・・
Allといっても何でもOKってわけじゃないし・・・
どう書くんでしょうね?

なかなか難しいです

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

そういえばGuideにパターンマッチをやってくれるmatchの例が上がってました

(: assert-symbols! ((Listof Any) -> (Listof Symbol)))
(define (assert-symbols! lst)
  (match lst
    [(list (? symbol? #{s : (Listof Symbol)}) ...) s]
    [_ (error "expected only symbols, given" lst)]))

ここで使えるはず

(: opt-apply (All (a b) (-> (Opt a) (-> a b) (Opt b))))
(define (opt-apply x func)
  (if (None? x)
      (None)
      (Some (func (Some-v x)))))

上の例を見て#{}の書き方についてひとしきり悩んでましたが
実は使わなくても書けてしまいました

(: opt-apply (All (a b) (-> (Opt a) (-> a b) (Opt b))))
(define (opt-apply x func)
  (match x
    [(None) (None)]
    [(Some y) (Some (func y))]))

できました
matchのように、Typed Racketに対応してない式では#{}を使うのが便利」って
書いてあったんですが、今はmatchも型に対応したってことなんでしょうね

なお[(None) (None)]のふたつめの(None)はないとエラーになります
condだとふたつめの式がなければひとつめの式の値を返してくれてたと思うんですけど

none-to-zeroも同様

(: none-to-zero (All (a) (-> (Opt a) (U Zero a))))
(define (none-to-zero optvar)
  (match optvar
    [(None) 0]
    [(Some y) y]))

本筋に戻って

定義6 n番目の要素

まずはもともとの定義から

(: CanDivideByPower (-> Natural Natural Natural Boolean))
(define (CanDivideByPower x n k)
  (CanDivide x (expt (prime n x) k)))

これは単なる自然数に関する述語と見ていいのでは
次は本体
xは少なくとも列 → GSequene
値は列かもしれないけど単なる記号かもしれない → GNumber

(: elm (-> GSequence Natural GNumber))
(define (elm x n)
  (gnumber
   (Min≦ x (λ (k) (and (CanDivideByPower x n k)
                       (not (CanDivideByPower x n (+ k 1))))))))

次は素因数分解
型は同じ

(define (elm x n)
  (gnumber (none-to-zero (factor-expt (factorization-nth (factorization x) n)))))

ここから先はしばらくOptのことは忘れてもいいはず

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

ここで自然数の世界からゲーデル数の世界に入ります
GNumberなどの型がやっと登場

定数

(define c0 : GSymbol (gsymbol (gnumber 1)))
(define cf : GSymbol (gsymbol (gnumber 3)))
 :
 :

(define c0 : GSymbol 1)ではエラーになるのはしかたないんだけど
ちょっとめんどくさいなあ
こうかな?

(define gsymbol+
  (case-lambda [([x : Natural]) (gsymbol (gnumber x))]
               [([x : GNumber]) (gsymbol x)]))

(define c0 : GSymbol (gsymbol+ 1))
(define cf : GSymbol (gsymbol+ 3))
 :
 :

case-lambdaオーバーロードみたいなことをする式で
case->はその型
でもこの書き方だと、誰かが作った関数と同じ処理を新しい型について
実行しようとしたとき、その関数自体を書き換えなきゃいけなくて
ちょっとやりにくかったりしないかなあ
独立してもうひとつ関数を定義するだけでオーバーロードされるような
書き方はできないんだろうか

気になったのはReferenceに

Note that each formals must have a different arity.

と書いてあったこと
arityって引数の数のことだよなあ?型のことは言ってないよな?
素のRacketには型がないから引数の数でしか区別つかないけど
Typed Racketではそんなことないと思いたい
ていうかちゃんと型でも区別してるっぽいけど
ドキュメントが間違ってるとか追いついてないとかそういう話?

でもそれくらいにして先に進む
gsymbol+みたいな関数を作って使うべきかどうかも考えつつ

変数

(: var (-> Natural Natural GSymbol))
(define (var n c) (gsymbol+ (expt (P (+ 6 n)) c)))

ゲーデル数を求めるユーティリティ関数

を作ってたらやっぱりこういうのがほしくなりました

(: gsequence+ (case-> (-> Natural GSequence)
                    (-> GNumber GSequence)))
(define gsequence+
  (case-lambda [([x : Natural]) (gsequence (gnumber x))]
               [([x : GNumber]) (gsequence x)]))

うーん毎回こういうのを書きたくなるとなると、なにか不自然なことを
しようとしているんじゃないかという不安が出てくるな
間違ってはいないと思うんだけど

で本体

(: gnum (-> GNumber * GSequence))
(define (gnum . seq)
  (: iter (-> (Listof GNumber) Natural GSequence GSequence))
  (define (iter s k n)
    (if (null? s)
        n
        (iter (cdr s) (+ k 1) (gsequence+ (* (expt (P k) (car s)) n)))))
  (iter seq 1 (gsequence+ 1)))

値は列の列かもしれないけど少なくとも列なのでGSequence
1をGSequenceの値として認めていいのかどうか微妙な気もするけど
長さ0の列と見る、としてもそれほど不自然ではないんじゃないかな

一発で型エラーを出さずに書くのはなかなか難しい
それくらい見逃してよ・・・と言いたくなる気もするけど
バグ取りしてもらうためにやってるんだからだまっとくか
いい仕事してくれること期待してますよ

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

Factorizationからn番目のFactorを取り出します

(: factorization-nth (-> (Opt Factorization) Natural (Opt Factor)))
(define (factorization-nth facz n)
  (: F (-> Factorization Natural (Opt Factor)))
  (define (F f n)
    (cond ((null? f) (None))
          ((= n 1) (Some (car f)))
          (else (F (cdr f) (assert (- n 1) natural?)))))
  (if (or (None? facz) (= n 0))
      (None)
      (F (Some-v facz) n)))

これはこれで考えて作ったんですがどうもすっきりしてません
内部関数のFFactorでなく(Opt Factor)を返すので
opt-applyが使えません
2箇所でNoneを返しているのもどことなく気に入らない

(Opt Factor)からprimeexptを取り出します

(: factor-prime (-> (Opt Factor) (Opt Natural)))
(define (factor-prime x)
  ((inst opt-apply Factor Natural) x Factor-prime))

(: factor-expt (-> (Opt Factor) (Opt Natural)))
(define (factor-expt x)
  ((inst opt-apply Factor Natural) x Factor-expt))

carとかcdrで済んでたんですけどねえ
instくらい不要にできないかなあ

さてここまで失敗をNoneで表していますが
ゲーデルが作った範囲では例外を0で表しているので
どこかでNoneから0に変換する必要があります

ていうかもともと0でうまくいくようになってるので、Noneはあるだけ邪魔って話
がそこは勉強なので

というわけでNoneを0に変える関数

(: none-to-zero (All (a) (-> (Opt a) (U Zero a))))
(define (none-to-zero optvar)
  (if (None? optvar)
      0
      (Some-v optvar)))

(Opt Natural)型以外で使うことはあんまりなさそうですが
何でも動くので(Opt a)にしてあります

はーやっと元の流れに戻りました
primeはこうなってます

(: prime (-> Natural Natural Natural))
(define (prime n x)
  (none-to-zero (factor-prime (factorization-nth (factorization x) n))))

素因数分解して、n番目を持ってきて、素数パートを持ってきて、
途中で失敗してたら0にする
まあまあすっきり書けましたね?

塾やべえな

子供の塾の説明会に行ってみたんですがすごいですね
レベル高すぎ
といっても内容がすごく難しいとかじゃなくて
方針っていうか考え方というか
とにかくそこまで子供に考えさせるのか、っていうところに驚きました

これはついていければすごいことになるなと
しかも先生方の話し方もプロっぽさを感じさせますし
ノウハウでついていかせてしまうんじゃないかと
そういうやり方との相性みたいなものもあるかもしれませんが

自分も大学時代は家庭教師だとか塾講師とかやってまして
今は何かと経験もあるのでもし今やればもっとうまく教えられるんじゃないかと
思ってたりもしたんですがもう全然レベルが違う
自分もこういう教育受けてみたかった気がします
ていうか国語の読解とか、もしかして自分が受けてもいいかも?と思ったほど

しかし振り返って小学校からこういうレベルで訓練を受けてきた連中と
田舎で塾にも行かずほとんど学校とZ会だけで勝負してたのかと思うとアレ
ン十年前の話なんで今とは違うところも多々あるとは思いますが

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

では本体に戻って書き換え
型の部分を再掲

(struct None ())
(struct (a) Some ([v : a]))
(define-type (Opt a) (U None (Some a)))

(define-type Factor (Pairof Natural Natural))
(define-type Factorization (Listof Factor))

Factorization(Listof Factor)か`(Listof (Opt Factor))
ちょっと悩みましたがところどころFactorNoneになってることは
ないだろうということで(Listof Factor)でいきます
うまく書けなかったら戻る

つまりFactorization全体がまるごとNoneになるという表現

(: factorizations (HashTable Natural (Opt Factorization)))
(define factorizations (make-hash))
(hash-set! factorizations 0 None)
(hash-set! factorizations 1 None)

でもなんで書き換え前はエラーの値を()じゃなくて((0 . 0))
してたんだっけということが気になったり
なにかそのほうが便利だったかな
まあいいや

Noneを返さなければいけない特殊ケースはすでに
factorizationsの中に登録してあるので
素因数分解を実際に計算する部分にはNoneは出てきません
関数に型をつけただけ

(: factorization (-> Natural (Opt Factorization)))
(define (factorization x)
  (cond ((hash-ref factorizations x #f))
        (else
         (let loop ((n : Natural 1)
          :

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

どうも型周りのカンがつかめなくていろいろ試行錯誤してたら
収拾がつかなくなってきたんですがいったんこのへんで書いておきます

型の定義はこうなってます
FactorPairofではなくてstructで表現することに
これは単にせっかくそういうのがあるんだからこうしとこうという程度の話

(struct None () #:transparent)
(struct (a) Some ([v : a]) #:transparent)
(define-type (Opt a) (U None (Some a)))

(struct Factor ([prime : Natural] [expt : Natural]) #:transparent)
(define-type Factorization (Listof Factor))

#:transparentっていうのは、値の表示を親切にしてくれるキーワードです
お勉強中はこの方が便利
デフォルトでそうなってないってことはたぶん性能が下がったりしてるのかと

こう定義したとして

(define fac1 : Factor (Factor 2 1))
(define optfac1 : (Opt Factor) (None))
(define optfac2 : (Opt Factor) (Some fac1))

今までの型定義だとこんな風に表示されて

> optfac1
- : (U (Some Factor) None)
#<None>
> optfac2
- : (U (Some Factor) None)
#<Some>

#<None>はともかく、#<Some>じゃ中身がわからんじゃないか、となってたんですが
#:transparentをつけてやるとこう表示されます

> optfac1
- : (U (Some Factor) None)
(None)
> optfac2
- : (U (Some Factor) None)
(Some (Factor 2 1))

素因数分解の結果もわかりやすく

> (factorization 40)
- : (U (Some Factorization) None)
(Some (list (Factor 2 3) (Factor 5 1)))

助かります

素因数分解をする関数はそのまま変化なしです
素因数分解の長さ(素因数の数っていうか)を求める関数はまずこうなりました

(: factorization-length (-> (Opt Factorization) (Opt Natural)))
(define (factorization-length facz)
  (if (None? facz)
      (None)
      (Some (length (Some-v facz)))))

(if (None? ...) (None) (Some (... (Some-v ...))))というところは
Optの中身に関数を適用してやるイメージ
パターンぽいので関数にしてみると使いでがありそうな予感

(: opt-apply (All (a b) (-> (Opt a) (-> a b) (Opt b))))
(define (opt-apply x func)
  (if (None? x)
      (None)
      (Some (func (Some-v x)))))

これを使ったらfactorization-lengthの定義はこうなりました

(: factorization-length (-> (Opt Factorization) (Opt Natural)))
(define (factorization-length facz)
  ((inst opt-apply Factorization Natural) facz length))

ほんとは単に(opt-apply facz length)って書きたいんですが
これだと型がおかしいって言われます

Type Checker: Polymorphic function `opt-apply' could not be applied to arguments:
Argument 1:
  Expected: (U (Some a) None)
  Given:    (U (Some Factorization) None)
Argument 2:
  Expected: (-> a b)
  Given:    (All (a) (-> (Listof a) Index))

Result type:     (U (Some b) None)
Expected result: (U (Some Nonnegative-Integer) None)
 in: (opt-apply facz length)

(define (f g) ...)という定義があってgが関数型の場合
(f h)という呼び出しを行うには、hの引数の型はgの引数の型よりも
広くないといけませんが
(Some Factorization)(Some a)よりも狭いのでエラーとなります

・・・たぶん

そこで(inst opt-apply Factorization Natural)は何をやっているかというと
(All (a b) (-> (Opt a) (-> a b) (Opt b)))
aFactorizationbNaturalにしたopt-applyを作ってる
ということになります
これでエラーが出なくなりました

っていうやり方がいいやり方なのかどうかは自信がありません
無理やりキャストするみたいなことをしてる感覚ではないと思いますけど
もうちょっと楽に書けるやりかたがあってもいいような

((inst opt-apply Factorization Natural) facz length)
ちょっと見づらいのでそれだけの関数を定義するという手もありかなあ

(define opt-factorization-apply (inst opt-apply Factorization Natural))

(: factorization-length (-> (Opt Factorization) (Opt Natural)))
(define (factorization-length facz)
  (opt-factorization-apply facz length))

ちょっとやりすぎかもしれません
値がNaturalでなければまた別の関数が必要になりますし