2017-10-17から1日間の記事一覧
定義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)))))))) 変数が束縛…
定義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)))))))) 変数が束縛…