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 のケイス。

  • (unify-term ’(constant-term 1) ’(var-term x))
  • (unify-term ’(app-term *1
  • (unify-term ’(app-term *2

二番目は #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 云々については明日。

*1:var-term x) (constant-term 1))) ’(var-term x

*2:var-term y) (constant-term 1))) ’(var-term x