EoPL reading (123) 2.3 Representation Strategies for Data Types

scheme EoPL

Exercise 2.25

unify-terms を検討。

  • ts と us が両方同時に '() なら (empty-subst) を戻す
  • ts あるいは us のどちらかが '() なら #f を戻す

以下。

(test* "(unify-terms '() '())"
       '(empty-subst-rec)
       (unify-terms '() '()))

(test* "(unify-terms '() '(var-term a))"
       #f
       (unify-terms '() '(var-term a)))

(test* "(unify-terms '(var-term a) '())"
       #f
       (unify-terms '(var-term a) '()))

試験は無論パス。問題はここから先。

  • 引数リストの両方の car を unify-term して subst-car に
  • subst-car が #f なら #f 戻して終了

で、その後なんですが以下。

  • 引数リストの cdr と subst-car を subst-in-terms に渡してそれぞれ new-ts, new-us に
  • new-ts と new-us を unify-terms にして戻りを subst-cdr に
    • これ、残りを置き換えとくイメージですか

むむ。再帰してないってカン違いしてましたが、ここで再帰呼び出しか。ざっくりここで cdr 要素について掘り下げてって最終的に compose-subst するのか。ちょっとイメージし辛いので若干ズルを。unify-term を見るに、引数の両方が app-term だった場合に、unify-terms が呼び出されているのが分かる。
以下を例にしてトレイスしてみます。

(unify-term '(app-term ((var-term x) (constant-term 1)))
            '(app-term ((var-term y) (constant-term 2))))

これはまず、(var-term x) と (var-term y) を unify-term して

(extend-subst-rec x (var-term y) (empty-subst))

が戻る。これは subst-car にセットされる。次に上記の substitution と リストの cdr 要素を渡して subst-in-terms が呼び出されて

((constant-term 1))

とか

((constant-term 2))

とかが戻ってくる。これが new-ts とか new-us とか。で、unify-term に渡されるのですが、これがダウトで #f が戻ってきます。失敗。
両方同じ値でリトライ。片方をもう片方に合わせるとすると、unify-terms の中の unify-term な呼び出しにより (empty-subst) が戻る。正確には (empty-subst-rec) です。
てーコトは compose-subst に渡されるのは

subst-car が (extend-subst-rec x (var-term y) (empty-subst))
subst-cdr が (empty-subst)

になる。それで compose なのか。subst-car の末端要素が subst-cdr にならないと駄目という読み。

(list (car subst-car) (cadr subst-car) (caddr subst-car) subst-cdr)

を戻せば良さげに見えますがイージー杉でしょうか。再帰なナニを見るに、

  • subst-car には引数の car 要素の substitution が格納
    • 基本的に末端は (empty-subst) なナニになってるはず
  • subst-cdr には (empty-subst) まで遡って順に substitution が作られてく
    • extend-subst-rec なリストの末端要素は substitution なオブジェクト

って意味解りにくい。下記のリストだとどうか。

(unify-term '(app-term ((var-term x) (var-term z)))
            '(app-term ((var-term y) (var-term a))))

これ、以下が戻るはずなんですがダウトかなぁ。

(extend-subst-rec x
                  (var-term y)
		  (extend-subst-rec z
                                    (var-term a)
                                    (empty-subst-rec)))

なんなくイケてそうなカンジですが眠くて思考力が落ちてます。記憶も朧なんですが、以下な試験を投入。

(test* "(unify-terms '((var-term a) (constant-term 1))
                     '((var-term b) (constant-term 2)))"
       #f
       (unify-terms '((var-term a) (constant-term 1))
                     '((var-term b) (constant-term 2))))

(test* "(unify-terms '((var-term a) (constant-term 1))
                     '((var-term b) (constant-term 1)))"
       '(extended-subst-rec a (var-term b) (empty-subst-rec))
       (unify-terms '((var-term a) (constant-term 1))
		    '((var-term b) (constant-term 1))))

(test* "(unify-terms '((var-term x) (var-term z))
                     '((var-term y) (var-term a)))"
       '(extended-subst-rec x 
			    (var-term y)
			    (extended-subst-rec z
						(var-term a)
						(empty-subst-rec)))
       (unify-terms '((var-term x) (var-term z))
		    '((var-term y) (var-term a))))

二番目のソレが失敗します。

got #<error "pair required, but got ()"

うーむ。目視では (empty-subst-rec) が二重になってるから、か。

(compose-subst (empty-subst-rec) (empty-subst-rec))

は NG ですな。てコトは卑怯なニゲ方は以下か。

(define compose-subst
  (lambda (s1 s2)
    (if (eqv? s1 '(empty-subst-rec))
	s1
	(list (car s1) (cadr s1) (caddr s1) s2))))

これは非道。でも試験にパスしない。どうも if な条件式が微妙だった模様。

(define compose-subst
  (lambda (s1 s2)
    (if (eqv? 'empty-subst-rec (car s1))
	s1
	(list (car s1) (cadr s1) (caddr s1) s2))))

今日はへろへろなので残り (試験?) は明日。