Ex. 4.76
SQLでいうところの、表結合での索引検索と全表検索のことである。
ふつうは、A and B の Aの結果とBの結果がともに少ないときは全表検索が有利である。Aの結果とBの結果がある程度多いときは索引検索が有利になる。しかし、queryシステムには索引がないので、例えば (?x . Adam) をキーに表を絞り込むということができない。結局全表検索になる。なので最初から全表検索＆結合のほうが有利である。
方針： A and B について
- A のフレームストリームを取得する (a1 a2 a3 ...)
- B のフレームストリームを取得する (b1 b2 b3 ...)
- フレーム a1と(b1 b2 b3 ...) の各フレームを結合可能なら結合する。((a1 b1) (a1 b3) ...)とか
- フレーム a2と(b1 b2 b3 ...) の各フレームを結合可能なら結合する。((a2 b2) ...)とか
- ...
- 上の結合結果をまとめて結合する ( (a1 b1) (a2 b2) (a1 b3) ... ) ← interleaveで結合する
1, 2の A と B を独立に実行し、6 で interleave でまとめるのは or つまり disjoin をまねして作ればよい。
難しそうなのは、3, 4, 5 ... の部分である。問題のヒントに従って unify-match のまねをして作る。
unify-match の復習
(unify-match '(son Adam ?x)① '(son Adam Cain)② '()③) ↓ son① と son② を比較。一致するので ()③ をそのまま返す。 ↓ Adam① と Adam② を比較。一致するので ()③ をそのまま返す。 ↓ ?x① と Cain② を比較。変数なので extend-if-possible を呼び出す。 これはフレーム拡張の可否を判定して拡張する。 ((?x . Cain))③ を返す。 ↓ 結果 ((?x . Cain))③ となる。
拡張できない場合
(unify-match '(son Adam ?x)① '(son Adam Cain)② '((?x . Enoch))③) ↓ son、Adamの処理(上と同じ) ↓ ?x① と Cain② を比較。変数なので extend-if-possible を呼び出す。 これはフレーム拡張の可否を判定してから拡張する。 ?x はすでに他の値に束縛 ((?x . Enoch))③されているので拡張不可と判定。 ↓ 結果 failed となる。
rule とユニファイする場合
(unify-match '(son Adam ?x)① '(son ?m ?s)② '()③) ↓ son① と son②は同じなのでフレームそのまんま。 ↓ Adam① と ?m②を比較。変数なので extend-if-possible を呼び出す。 フレームを拡張して ((Adam . ?1m))③ を返す。 ↓ ?x① と ?s②を比較。変数なので extend-if-possible を呼び出す。 フレームを拡張して ((Adam . ?1m) (?x . ?1s))③を返す。 ↓ 結果 ((Adam . ?1m) (?x . ?1s))③ となる。
このあと rule 本体の適用があるが、それは unify-match の仕事ではない。
conjoin への利用
conjoin で利用できるのは、extend-if-possible のフレーム拡張の可否判定の部分。 これが、a1 と b1 の矛盾判定に使える。、、、と思ったけどあんまり使えなかった。
A と Bの各々を組み合わせは2重ループになる。stream-flatmap を2重にして表現する。
こんな感じ
(define (conjoin conjuncts frame-stream)
(if (empty-conjunction? conjuncts)
frame-stream
(let ((stream-A (qeval (first-conjunct conjuncts) frame-stream))
(stream-B (qeval (car (rest-conjuncts conjuncts)) frame-stream)))
(stream-flatmap
(lambda (frame-a)
(stream-flatmap
(lambda (frame-b)
(join-a-and-b frame-a frame-b))
stream-B))
stream-A))))
(define (join-a-and-b frame-a frame-b)
(define (check-loop b)
(if (eq? b '())
#t
(let ((var (binding-variable (car b))))
(let ((binding-a (recursive-search-in-frame var frame-a))
(binding-b (recursive-search-in-frame var frame-b)))
(cond ((eq? binding-a #f) (check-loop (cdr b)))
((eq? binding-b #f) (check-loop (cdr b)))
((equal? (binding-value binding-a) (binding-value binding-b))
(check-loop (cdr b)))
(else #f))))))
(if (check-loop frame-b)
(singleton-stream (append frame-a frame-b))
the-empty-stream))
(define (recursive-search-in-frame variable frame)
(let ((binding (assoc variable frame)))
(cond ((eq? binding #f) #f)
((var? (binding-value binding))
(recursive-search-in-frame (binding-value binding) frame))
(else binding))))
A と Bを独立に実行して、互いに矛盾のないフレームを結合する → この仕様自体が A 、B を無限ストリームであることを許さない(無限ストリームが矛盾してないかどうかは判定不可なので)。なので、check-loop は有限長のストリーム用である。
変数束縛の矛盾の有無の判定は (check-loopの中の判定文)
AとBの変数の束縛チェーンが最終的に異なる値に束縛されてたらNG それ以外はOK 例えば、Aの変数の束縛チェーンが最終的に値に束縛されていなければ、それでOK とか
という感じにした。間違ってるかも。変数の束縛チェーンが値を含まない場合でも、変数同士だけで矛盾することがある？あまり、良くわかっていない。
あと、recursive-search-in-frame をループの度に実行とか、計算コスト減っているのでしょうか。
ちょっとだけテスト
;;; Query input: (and (job ?a ?b) (same ?a (Bitdiddle Ben))) ;;; Query results: (and (job (Bitdiddle Ben) (computer wizard)) (same (Bitdiddle Ben) (Bitdiddle Ben))) ------ ;;; Query input: (and (job ?a ?b) (same (Bitdiddle Ben) ?a)) ;;; Query results: (and (job (Bitdiddle Ben) (computer wizard)) (same (Bitdiddle Ben) (Bitdiddle Ben)))