EoPL reading (128) 2.3 Representation Strategies for Data Types
小出しになってしまってますがご容赦下さい。続きです。
t が var-term 以外のケイスを以下に。
- u が var-term の場合、引数を入れ替えて unify-term 呼び出し
- u が constant-term の場合
- t が constant-term で値が同一なら (empty-subst) を戻す
- u が app-term の場合
- t が app-term なら unify-terms に app-term の中身を渡して戻りを戻す
試験が以下ですが、unify-terms が #f を戻すケイスもあるな。ちょっと unify-terms 分についてここではオミットします。
(test* "(unify-term '(constant-term 1) '(var-term x))"
(extend-subst 'x (constant-term 1) (empty-subst))
(unify-term '(constant-term 1) '(var-term x)))
(test* "(unify-term '(constant-term 1) '(constant-term 1))"
(empty-subst)
(unify-term '(constant-term 1) '(constant-term 1)))ここからがある意味本番か。とりあえず unify-terms が #f 戻すケイスを列挙してみる。
- リストの流さが合ってない場合
- car 要素を unify-term した結果が #f の場合
- cdr 要素を unify-terms した結果が #f の場合
最後の試験はこれだけで良いのかどうか微妙ですが
(test* "(unify-terms '() '(var-term a))"
#f
(unify-terms '() '(var-term a)))
(test* "(unify-terms '(var-term a) '())"
#f
(unify-terms '(var-term a) '()))
(test* "(unify-terms '((var-term x)) '((app-term ((var-term x)))))"
#f
(unify-terms '((var-term x)) '((app-term ((var-term x))))))
(test* "(unify-terms '((var-term a) (var-term b)) '((var-term c)))"
#f
(unify-terms '((var-term a) (var-term b)) '((var-term c))))で、ここまで書いた時点で compose-subst 実装してないコトに気づく。基本的な仕様としては
(define compose-subst (lambda (subst-car subst-cdr)
の subst-car の末端の substitution が subst-cdr になれば良いはず。
(cases substitution subst-car
(empty-subst-rec ()
(empty-subst))
(extended-subst-rec (id term sub)
(extend-subst id term subst-cdr)))))というカンジかなぁ。試験が以下。
(test-section "compose-subst")
(test* "(compose-subst (empty-subst) (empty-subst))"
(empty-subst)
(compose-subst (empty-subst) (empty-subst)))
(test* "(compose-subst (extend-subst x (var-term y) (empty-subst)) (extend-subst y (constant-term 1) (empty-subst)))"
(extend-subst 'x (var-term 'y) (extend-subst 'y (constant-term 1) (empty-subst)))
(compose-subst (extend-subst 'x (var-term 'y) (empty-subst))
(extend-subst 'y (constant-term 1) (empty-subst))))うーむ。本当に良いのだろうか。とりあえずここまで来たら確認はもう少しだな。ただ、以下の処理の検証とかまだあまりきちんとできてない。
(let ((new-ts (subst-in-terms (cdr ts) subst-car)) (new-us (subst-in-terms (cdr us) subst-car)))
とりあえず単純なヤツから。
(test* "(unify-terms '((var-term a) (var-term b)) '((constant-term 1) (constant-term 2)))"
(extend-subst 'a
(constant-term 1)
(extend-subst 'b (constant-term 2) (empty-subst)))
(unify-terms '((var-term a) (var-term b))
'((constant-term 1) (constant-term 2))))ソースが
(compose-substs subst-car subst-cdr))))))))))
ってなってた。compose-subst に修正したら試験パス。
再開
理解が微妙なのが
- unify-term で memv してるナニ
- unify-terms で cdr 要素について subst-in-terms してるソレ
ちょっと集中して検討してみます。まず最初のナニですが
(cases term t (var-term (tid) (if (or (var-term? u) (not (memv tid (all-ids u)))) (unit-subst tid u)
という事で t が var-term で u が app-term なケイス限定なのかな。例えば
(unify-term '(var-term x) '(app-term ((var-term y))))
みたいなカンジ。これは x という変数が (y) という手続き呼び出しに置き替えなナニ。これって確かに x が (x) に、というのは微妙なのか。あるいは
(unify-term '(var-term x) '(app-term ((var-term y) (var-term x))))
というケイス。これは x が (y x) に変換。なんとなく再帰ループを連想してしまう。のでチェックしてるのだろうな、という事なんですがダウトでしょうか。
次。cdr を変換しているのは何故か、という事なんですが、サンプルとしてどんな式があり得るのかな。例えば以下?
((var-term x) (var-term y) (var-term y))
と
((var-term z) (constant-term 1) (constant-term 1))
を unify-terms に渡すとすると最初に subst-car に格納されるのは
(extend-subst x (var-term z) (empty-subst))
で、これは new-ts とか new-us を生成するナニには影響はしないはず。うん、しないな。イメージ的には次だな。
((var-term y) (var-term y))
と
((constant-term 1) (constant-term 1))
になります。これは
(extend-subst y (constant-term 1) (empty-subst))
という substitution を生成するんですが、これを cdr に適用する事で ts 側は
((constant-term 1))
になって us 側はそのまんまの
((constant-term 1))
になってこの car を unify-term に渡すと (empty-subst) が戻りますな。でもなんとなくオチてないな。ただ、unify-terms って
(x y y)
という式を
(z 1 1)
という式に置き換えるという事なのか。もう少し複雑な式をイメージした方が良いのかな。例えば以下とか?
(x (x 1 2) (x 3 4))
あ、unify-terms とか unify-term って substitution なオブジェクトのコンストラクタなのか。ここまでのソレを試験にしてみて終わり、で良い気がしてます。とりあえず試験を作りましょう。
(test* "(unify-terms '((var-term x) (var-term y) (var-term y)) '((var-term z) (constant-term 1) (constant-term 1)))"
(extend-subst 'x
(var-term 'z)
(extend-subst 'y (constant-term 1) (empty-subst)))
(unify-terms '((var-term x) (var-term y) (var-term y)) '((var-term z) (constant-term 1) (constant-term 1))))これで OK ってコトにします。実装と試験を以下に。
まず実装。# substitution なソレのみ
(add-load-path ".")
(load "define-datatype")
(load "term")
(define-datatype substitution substitution?
(empty-subst-rec)
(extended-subst-rec
(id symbol?)
(term term?)
(sub substitution?)))
(define empty-subst
(lambda ()
(empty-subst-rec)))
(define extend-subst
(lambda (i t s)
(extended-subst-rec i t s)))
(define apply-subst
(lambda (s i)
(cases substitution s
(empty-subst-rec ()
(var-term i))
(extended-subst-rec (id term sub)
(if (eqv? i id)
term
(apply-subst sub i))))))
(define subst-in-term
(lambda (t s)
(cases term t
(var-term (id) (apply-subst s id))
(constant-term (datum) (constant-term datum))
(app-term (terms)
(let f ((rslt '()) (terms terms))
(if (null? terms)
(app-term rslt)
(f (append rslt (list (subst-in-term (car terms) s)))
(cdr terms))))))))
(define subst-in-terms
(lambda (l s)
(map (lambda (t) (subst-in-term t s)) l)))
(define unit-subst
(lambda (id term)
(extend-subst id term (empty-subst))))
(define var-term?
(lambda (t)
(cases term t
(var-term (id) #t)
(else #f))))
(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)))
(define compose-subst
(lambda (s-car s-cdr)
(cases substitution s-car
(empty-subst-rec ()
(empty-subst))
(extended-subst-rec (id term sub)
(extend-subst id term s-cdr)))))
(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-terms 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 ts) 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-subst subst-car subst-cdr))))))))))次が試験。これも 2.25 マターなソレだけ。
(use gauche.test)
(add-load-path ".")
(load "substitution")
(test-start "ex.2.25")
(test-section "var-term?")
(test* "(var-term? '(var-term a))"
#t
(var-term? '(var-term a)))
(test* "(var-term? '(constant-term 1))"
#f
(var-term? '(constant-term 1)))
(test* "(var-term? '(app-term ((var-term x) (var-term y))))"
#f
(var-term? '(app-term ((var-term x) (var-term y)))))
(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)))))
(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)))
(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)))
(test* "(unify-term (var-term a) (var-term a)) returns"
'(extended-subst-rec a (var-term a) (empty-subst-rec))
(unify-term '(var-term a) '(var-term a)))
(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)))))
(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)))))
(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)))))
(test-section "unify-term (2)")
(test* "(unify-term '(var-term x) '(app-term ((var-term x))))"
#f
(unify-term '(var-term x) '(app-term ((var-term x)))))
(test* "(unify-term '(constant-term 1) '(app-term ((var-term x))))"
#f
(unify-term '(constant-term 1) '(app-term ((var-term x)))))
(test* "(unify-term '(constant-term 1) '(constant-term 2))"
#f
(unify-term '(constant-term 1) '(constant-term 2)))
(test* "(unify-term '(app-term ((var-term x))) '(constant-term 1))"
#f
(unify-term '(app-term ((var-term x))) '(constant-term 1)))
(test* "(unify-term '(app-term ((var-term x))) '(var-term x))"
#f
(unify-term '(app-term ((var-term x))) '(var-term x)))
(test* "(unify-term '(var-term x) '(var-term y))"
(extend-subst 'x (var-term 'y) (empty-subst))
(unify-term '(var-term x) '(var-term y)))
(test* "(unify-term '(var-term x) '(constant-term 1))"
(extend-subst 'x (constant-term 1) (empty-subst))
(unify-term '(var-term x) '(constant-term 1)))
(test* "(unify-term '(var-term x) '(app-term ((var-term y))))"
(extend-subst 'x '(app-term ((var-term y))) (empty-subst))
(unify-term '(var-term x) '(app-term ((var-term y)))))
(test* "(unify-term '(constant-term 1) '(var-term x))"
(extend-subst 'x (constant-term 1) (empty-subst))
(unify-term '(constant-term 1) '(var-term x)))
(test* "(unify-term '(constant-term 1) '(constant-term 1))"
(empty-subst)
(unify-term '(constant-term 1) '(constant-term 1)))
(test-section "unify-terms")
(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) '()))
(test* "(unify-terms '((var-term x)) '((app-term ((var-term x)))))"
#f
(unify-terms '((var-term x)) '((app-term ((var-term x))))))
(test* "(unify-terms '((var-term a) (var-term b)) '((var-term c)))"
#f
(unify-terms '((var-term a) (var-term b)) '((var-term c))))
(test* "(unify-terms '((var-term a) (var-term b)) '((constant-term 1) (constant-term 2)))"
(extend-subst 'a
(constant-term 1)
(extend-subst 'b (constant-term 2) (empty-subst)))
(unify-terms '((var-term a) (var-term b))
'((constant-term 1) (constant-term 2))))
(test* "(unify-terms '((var-term x) (var-term y) (var-term y)) '((var-term z) (constant-term 1) (constant-term 1)))"
(extend-subst 'x
(var-term 'z)
(extend-subst 'y (constant-term 1) (empty-subst)))
(unify-terms '((var-term x) (var-term y) (var-term y)) '((var-term z) (constant-term 1) (constant-term 1))))
(test-section "compose-subst")
(test* "(compose-subst (empty-subst) (empty-subst))"
(empty-subst)
(compose-subst (empty-subst) (empty-subst)))
(test* "(compose-subst (extend-subst x (var-term y) (empty-subst)) (extend-subst y (constant-term 1) (empty-subst)))"
(extend-subst 'x (var-term 'y) (extend-subst 'y (constant-term 1) (empty-subst)))
(compose-subst (extend-subst 'x (var-term 'y) (empty-subst))
(extend-subst 'y (constant-term 1) (empty-subst))))
(test-end)今から 2.4 節を見ます。
