kb84tkhrのブログ

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

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

定義24 "変数"vはxのn番目の場所では"束縛"されている

(define (IsBoundAt v n x)
  (and (IsVar v)
       (IsForm x)
       (∃ a b c ≦ x (and (= x (** (** a (ForAll v b)) c))
                         (IsForm b)
                         (<= (+ (len a) 1) n)
                         (<= n (+ (len a) (len (ForAll v b))))))))

変数が束縛されるのは∀v(b)の形でbの中にvが含まれているとき、と

bの中にまた∀v(c)があっても大丈夫かな?
束縛されてることには変わりないからいいのか

定義25 "変数"vはxのn番目の場所では"束縛"されてない

(define (IsFreeAt v n x)
  (and (IsVar v)
       (IsForm x)
       (= v (elm x n))
       (<= n (len x))
       (not (IsBoundAt v n x))))

いろいろチェックがついてますが見たまま

定義26 vはxの"自由変数"である

(define (IsFree v x)
  (∃ n ≦ (len x) (IsFreeAt v n x)))

xのどこでもいいから1箇所でもvがFreeに現れていれば

さて、動かすのをあきらめてみるともうほとんど書き写してるだけっていう状態ですが
これでいいんでしょうか