問題4.76できない

急に難しくなった。続き。

4.76

できなかったけど途中まで。
まずユニフィケーションに似てるらしいのでそこら辺を見てみます。

(define (unify-match p1 p2 frame)
  (cond ((eq? frame 'failed) 'failed)
        ((equal? p1 p2) frame)
        ((var? p1) (extend-if-possible p1 p2 frame))
        ((var? p2) (extend-if-possible p2 p1 frame))
        ((and (pair? p1) (pair? p2))
         (unify-match (cdr p1)
                      (cdr p2)
                      (unify-match (car p1)
                                   (car p2)
                                   frame)))
        (else 'failed)))

再帰的に全ての式についてユニファイ調べてます。変数の場合のextend-if-possibleを見てみます。

(define (extend-if-possible var val frame)
  (let ((binding (binding-in-frame var frame)))
    (cond (binding
           (unify-match
            (binding-value binding) val frame))
          ((var? val)
           (let ((binding (binding-in-frame val frame)))
             (if binding
                 (unify-match
                  var (binding-value binding) frame)
                 (extend var val frame))))
          ((depends-on? val var frame)
           'failed)
          (else (extend var val frame)))))

binding-in-frameはframe中のvarをassocで発見して返します。だからbindingがあるなら変数をそのvalueに置き換えてもう一度unifyするわけです。valの方が変数だったら基本的に同じ事をして、バインドが見つからなかったらextendします。extendはフレームにたいして新しい束縛を追加します。
varのバインドが見つからず、val、var、frameについてdepends-on?かどうか判定します。

(define (depends-on? exp var frame)
  (define (tree-walk e)
    (cond ((var? e)
           (if (equal? var e)
               true
               (let ((b (binding-in-frame e frame)))
                 (if b
                     (tree-walk (binding-value b))
                     false))))
          ((pair? e)
           (or (tree-walk (car e))
               (tree-walk (cdr e))))
          (else false)))
  (tree-walk exp))

これは、valがvarに依存しているかどうかの判定です。だから、valの中にvarが含まれていれば真になります。そうするとextend-if-possibleはfailするのでunifyもfailします。どれでもなければ(extend var val frame)します。

本題に入って、現在のconjoinはframeをどんどん拡張していってand処理を実現してます。問題4.76によればこれは少し効率が悪く、最初のframeで各式を処理し、それらをmergeした方がframeの拡張分の走査が必要なくなり効率的であるということらしいです。そうすると、mergeする部分をconjoin-mergeとして抽象化してやるとこれはdisjoinと似た手続きで書けるはずで、

(define (conjoin conjuncts frame-stream)
  (if (empty-conjunction? conjuncts)
      the-empty-stream
      (conjoin-merge
       (qeval (first-conjunct conjuncts) frame-stream)
       (conjoin (rest-conjuncts conjuncts) frame-stream))))

たぶんこんな風になるはず。次にconjoin-mergeを考えてみる。まず入力は二つのフレームのストリームで、出力は二つのストリームの各フレームに対して無矛盾な組み合わせをmergeして拡張したフレームの混ぜ合わせストリームです。ややこしい。
だから二つのフレームを取って、それらが矛盾ならthe-empty-streamを、無矛盾なら拡張したフレームを返すような手続きmerge-framesを抽象化してconjoin-mergeを書いてみます。

(define (conjoin-merge fs1 fs2)
  (if (or (stream-null? fs1) (stream-null? fs2))
      the-empty-stream
      (interleave-delayed
       (stream-filter 
        (lambda (frame) (not (eq? 'failed)))
        (stream-map
         (lambda (frame1)
           (merge-frames frame1 (stream-car fs2)))
         fs1))
       (delay (conjoin-merge fs1 (stream-cdr fs2))))))    

たぶんこんな感じじゃないでしょうか。qevalがthe-empty-nullを返す(失敗する)場合、conjoinなので全部失敗します。だからfs1かfs2のどちらかがthe-empty-streamであるなら式全体が失敗したことになるのでthe-empty-streamを返します。うーんいいのかな。まあ次いこう。
merge-framesは今回のconjoinの肝で、二つのframeを組み合わせます。frameはvariableとvalueのバインドの対のリストとして表現されています。無矛盾であれば拡張したフレームを、矛盾であれば'failedを返すようにします。この際の無矛盾性の判定が、たぶんunificationに似てるんじゃないでしょうか。ということで書いてみます。

だめだ、分からない。ググる。extend-ifを使うのかぁ。
...動かない。降参。

他の方のを見てるとここら辺飛ばしてるみたいなので僕も飛ばしてもいいかな。ちょっと重すぎるので。よし4.76,4.77,4.78,4.79は飛ばす。いつかやります。