kb84tkhrのブログ

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

2017-10-17から1日間の記事一覧

ゲーデルの不完全性定理の証明のアレを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)))))))) 変数が束縛…