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

ちょっと蒸し返しますけど

(define (M23 x)
  (expt (P (sqr (len x))) (* x (sqr (len x)))))

ここって素数指数表現が歯抜けになってないことを前提にしてることになりませんか
primeからここまで、歯抜けでもいい流れできてたと思うんですが
まあでも、歯抜けありの列があれば同じ内容で歯抜けなしの列が必ずあるわけだから
別にかまわないのかな

定義28 xでk+1番目の"自由"であるvの場所

ただし、k+1番目というのは列の末尾から逆向きに数える

ここがミソらしいです

(define (freepos k v x)
  (cond ((= k 0)
         (Min n ≦ (len x)
              (and (IsFreeAt v n x)
                   (not (∃ p ≦ (len x)
                           (and (< n p)
                                (IsFreeAt v p x)))))))
        (else
         (Min n ＜ (freepos (- k 1) v x)
              (and (IsFreeAt v n x)
                   (not (∃ p ＜ (freepos (- k 1) v x)
                           (and (< n p)
                                (IsFreeAt v p x)))))))))

まずk=0のときは
そこより右に自由なvが現れない自由なvのうち一番左のもの
「一番左の」は必要ないっぽい気がしますが
Minを使うのでどうしてもついてくる、ってくらいの話ですかね

それ以外のときもほとんど同じ
探す範囲がひとつ前の自由なvの左になっただけ

けっこうややこしくなってきました
この間から動かしてないので不安です
ゲーデルさんはこのへんでストレスがたまってきたりしなかったでしょうか

定義29 xで、vが"自由"である場所の総数

(define (freenum v x)
  (Min n ≦ (len x) (= (freepos n v x) 0)))

freeposはkが自由なvよりも多くなると0を返すので
これでうまくいくわけか

定義30 xの"自由"であるvの場所のうち、k個をcで置き換えた論理式

(define (substSome k x v c)
  (cond ((= k 0) x)
        (else
         (substAtWith (substSome (- k 1) x v c)
                      (freepos (- k 1) v x)
                      c))))

1個も置き換えないならそのまま返す
k個置き換えるときは、まずk-1個置き換えたあと、末尾からk番目のvをcに置き換える

僕「substSome(k,x,v,c)を計算するとき、kはだんだん減っていくんだよ。で、末尾まで行ったときに0になって終わりになるようにするため、逆向きにしてあるんだ」

そう動いてるのはわかるんだけど、先頭まで行ったときに0になって
終わりにするのではマズい理由はあるのかな

定義31 aの"自由"であるvをすべてcで置換した"論理式"

(define (subst a v c)
  (substSome (freenum v a) a v c))

結局これを使うんだとすると、先頭から数えても末尾から数えても同じような気が
先頭から数えるほうが関数が面倒になるのかな