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

さてPが定義できたので素因数分解と定義3の再定義を
まずは補助関数から

(: times-divide (-> Natural Natural (Values Natural Natural)))
(define (times-divide x p)
  (let loop ((k : Natural 1) (x : Natural x))
    (cond ((not (CanDivide x p)) (values x (cast (- k 1) Natural)))
          (else (loop (+ k 1) (cast (/ x p) Natural))))))

castはしかたないのかなあ
kは1から増えていくだけだから(- k 1)はNaturalだよ、とか
(CanDivide x p)だから(/ x p)はNaturalだよ、って
わかってくれるといいんだけど・・・

と思ってもういちど調べたら
後者はquotientに書き換えるだけでした
divがないなあと思ってあきらめてたんですが名前が違いました

前者はガイドに別の書き方が載ってました
assertを使います

(: times-divide (-> Natural Natural (Values Natural Natural)))
(define (times-divide x p)
  (let loop ((k : Natural 1) (x : Natural x))
    (cond ((not (CanDivide x p)) (values x (assert (- k 1) natural?)))
          (else (loop (+ k 1) (quotient x p))))))

(- k 1)がnatural?であることをassertすると、
コンパイラの型チェックも(- k 1)もnatural?と思って通してくれます
castよりもちょっとだけスジがいい気がします
結果は変わらないですけど

もし何かの間違いで(- k 1)が負になってしまったら当然ランタイムエラーになります

ところでnatural?はtyped/racketモジュールに含まれていません
racket/mathで定義されています
こんなふうにrequireしてやりたいところ

(require/typed racket/math
               [natural? (-> Any Boolean : Natural)])

: Naturalという部分は、natural?が真だったら
与えられた引数はNaturalですよ、と教えてあげるため
これがOccurence Typingのカラクリのひとつ

これが契約に変換されるはずなんですがそこでエラーになります

Type Checker: Type (-> Any Boolean : Nonnegative-Integer) could not be converted to a contract: cannot generate contract for function type with props or objects. in: (-> Any Boolean : Natural)

Referenceにもnumber?とかはうまくいかないんだよねーって書いてあります
もともと、typed/racketにあるexact-nonnegative-integer?の
単なる別名なので自分で定義してやります

(: natural? (-> Any Boolean : Natural))
(define natural? exact-nonnegative-integer?)

これでうまくいくようになりました
この間書いたcastもこっちに直します

Occurence Typingがもっと進んでいくと今回の(- k 1)あたりも
勝手にNaturalだってわかってくれるようになったりするんでしょうか
難しそうな分野ですが