EoPL reading (122) 2.3 Representation Strategies for Data Types
Exercise 2.25
all-ids ってどっかで見たんだけどな、と思いつつ grep しても出てこなかった。テキストを遡ってみたら 2.10 にあるな。2.2 節はディレクトリ別にしてたので出てこなかったのか。以下なカンジ。
(add-load-path ".") (load "define-datatype") (load "expression") (define all-ids (lambda (exp) (let f ((rslt '()) (exp exp)) (cases expression exp (var-exp (id) (if (memv id rslt) rslt (append rslt (list id)))) (lit-exp (datum) rslt) (primapp-exp (prim rand1 rand2) (f (f rslt rand1) rand2)) (lambda-exp (id body) (f (append rslt (list id)) body)) (app-exp (rator rand) (f (f rslt rator) rand))))))
これって expression が対象になってるので書き換え必要ですな。あ、やっぱ名前 let でヤッてますな。なんとなく昨日でっち上げたソレはダウトな気がしてたんですが、どうもダウト臭い。
たまには名前 let 以外ってコトで以下。
(define all-ids (lambda (t) (define all-ids-inner (lambda (ret t) (cases term t (constant-term (datum) ret) (var-term (id) (if (memv id ret) ret (append ret (list id)))) (app-term (terms) (let f ((ret ret) (terms terms)) (if (null? terms) ret (f (all-ids-inner ret (car terms)) (cdr terms)))))))) (all-ids-inner '() t)))
一応以下の試験にパスしてるんで OK と見ます。
(test-section "all-ids") (test* "(all-ids '(constant-term 1)) returns" '() (all-ids '(constant-term 1))) (test* "(all-ids '(var-term a)) returns" '(a) (all-ids '(var-term a))) (test* "(all-ids '(app-term ((constant-term 1) (constant-term 2)))) returns" '() (all-ids '(app-term ((constant-term 1) (constant-term 2))))) (test* "(all-ids '(app-term ((var-term a) (var-term a)))) returns" '(a) (all-ids '(app-term ((var-term a) (var-term a))))) (test* "(all-ids '(app-term ((app-term ((var-term a) (var-term b))) (var-term c)))) returns" '(a b c) (all-ids '(app-term ((app-term ((var-term a) (var-term b))) (var-term c)))))
で、ちょっと休憩して手続き定義をニラむ事に。まず unify-term の var-term な分岐ですが
- t が var-term
- u が var-term 又は tid が u に含まれる id が無い場合 (unit-subst tid u) 呼び出し
- 上記条件ダウトの場合 #f を戻す
ってどーゆー意味でしょ。ちなみに unit-subst は
(unit-subst 'a '(var-term x))
とかな場合、
(extended-subst-rec 'a '(var-term x) (empty-subst-rec))
を戻す?
あ、これでは駄目だ。(var-term a) と (var-term x) が unify-term に渡された場合に上記の substitution なオブジェクトが戻るはず。これだと上記の substitution な apply-subst に (var-term a) を渡しても (var-term x) を渡しても (var-term x) が戻ります。成程。
とりあえず現状で unit-subst を実装できれば、app-term は別途試験な事にすれば試験で確認できそげ。
とりあえず以下の手続きを追加。
(define unify-term (lambda (t u) (cases term t (var-term (tid) (if (or (var-term? u) (not (memv tid (all-ids u)))) (unit-subst tid u) #f)) (else (cases term u (var-term (uid) (unify-term u t)) (constant-term (udatum) (cases term t (constant-term (tdatum) (if (equal? tdatum udatum) (empty-subst) #f)) (else #f))) (app-term (us) (cases term t (app-term (ts) (unify-term ts us)) (else #f)))))))) (define unify-terms (lambda (ts us) (cond ((and (null? ts) (null? us)) (empty-subst)) ((or (null? ts) (null? us)) #f) (else (let ((subst-car (unify-term (car ts) (car us)))) (if (not subst-car) #f (let ((new-ts (subst-in-terms (cdr us) subst-car)) (new-us (subst-in-terms (cdr us) subst-car))) (let ((subst-cdr (unify-terms new-ts new-us))) (if (not subst-cdr) #f (compose-substs subst-car subst-cdr))))))))))
で、まず以下の試験を追加。
(test-section "unify-term") (test* "(unify-term (var-term a) (var-term x)) returns" '(extended-subst-rec a (var-term x) (empty-subst-rec)) (unify-term '(var-term a) '(var-term x)))
無事パス。ええと、次は u が var-term でない場合か。一番簡単なケイスとしては constant-term なんですが、
(unify-term (var-term a) (constant-term 1))
これは以下が戻ってくるのか。
(extended-subst-rec a (constant-term 1) (empty-subst-rec))
なるほどたしかに unify (何
では試験で確認。
(test* "(unify-term (var-term a) (constant-term 1)) returns" '(extended-subst-rec a (constant-term 1) (empty-subst-rec)) (unify-term '(var-term a) '(constant-term 1)))
試験パス。がしかし、app-term だったらどうなるんだろ。あ、その前に以下なケイスだとどうなるか、というと。
(unify-term (var-term a) (var-term a))
これは #f が戻るのかな。これはおそらく
If no such unifire exists, it returns #f.
というソレに合致するのか。あ、違うや。var-term だからセイフか。
# ぢつは試験して分かってたりして (とほほ
てーコトはこれは app-term の中に同じ変数があるケイスになるのでしょうか。たしかに
x が (x 1 2) に置換されては微妙か。
逆に x が (y 1 2) に置換されるのはセイフという事か。
(test* "(unify-term (var-term x) (app-term ((var-term y) (constant-term 1) (constant-term 2)))) returns" '(extended-subst-rec x (app-term ((var-term y) (constant-term 1) (constant-term 2))) (empty-subst-rec)) (unify-term '(var-term x) '(app-term ((var-term y) (constant-term 1) (constant-term 2)))))
だんだん assert が見辛くなってきた。逆に app-term の中の y が x だと #f が戻るのか。
(test* "(unify-term (var-term x) (app-term ((var-term x) (constant-term 1) (constant-term 2)))) returns" #f (unify-term '(var-term x) '(app-term ((var-term x) (constant-term 1) (constant-term 2)))))
これも試験パス。これで一応 unify-term の cases な最初のブロックは全部カバーしたはず。次は最初の引数が var-term 以外で次の引数が var-term のケイス。
二番目は #f が戻るのか。あるいは次の分岐。
- (unify-term ’(constant-term 1) ’(constant-term 1))
- (unify-term ’(constant-term 1) ’(constant-term 2))
- (unify-term ’(constant-term 1) ’(app-term ((var-term x) (constant-term 1))))
これは一番てっぺんは (empty-subst-rec) が戻って以降はどちらも #f のはず。以下が試験。
(test* "(unify-term ’(constant-term 1) ’(var-term x)) returns" '(extended-subst-rec x (constant-term 1) (empty-subst-rec)) (unify-term '(constant-term 1) '(var-term x))) (test* "(unify-term ’(app-term ((var-term x) (constant-term 1))) ’(var-term x)) returns" #f (unify-term '(app-term ((var-term x) (constant-term 1))) '(var-term x))) (test* "(unify-term ’(app-term ((var-term y) (constant-term 1))) ’(var-term x)) returns" '(extended-subst-rec x (app-term ((var-term y) (constant-term 1))) (empty-subst-rec)) (unify-term '(app-term ((var-term y) (constant-term 1))) '(var-term x))) (test* "(unify-term ’(constant-term 1) ’(constant-term 1)) retuens" '(empty-subst-rec) (unify-term '(constant-term 1) '(constant-term 1))) (test* "(unify-term ’(constant-term 1) ’(constant-term 2)) returns" #f (unify-term '(constant-term 1) '(constant-term 2))) (test* "(unify-term ’(constant-term 1) ’(app-term ((var-term x) (constant-term 1)))) returns" #f (unify-term '(constant-term 1) '(app-term ((var-term x) (constant-term 1)))))
一応全部パスしてます。unify-terms 云々については明日。