sicp-ex-4.76



<< Previous exercise (4.75) | Index | Next exercise (4.77) >>


donald

  
 (define (new-conjoin conjuncts frame-stream) 
   (if (empty-conjunction? conjuncts) 
       frame-stream 
       (merge (qeval (first-conjunct conjuncts) 
                     frame-stream) 
              (new-conjoin (rest-conjuncts conjuncts) 
                           frame-stream)))) 
 (define (merge s1 s2) 
   (cond ((stream-null? s1) s2) 
         ((stream-null? s2) s1) 
         (else 
          (stream-flatmap (lambda (frame1) 
                            (stream-flatmap (lambda (frame2) 
                                              (merge-frame frame1 frame2)) 
                                            s2)) 
                          s1)))) 
 (define (merge-frame f1 f2) 
   (if (null? f1) 
       (singleton-stream f2) 
       (let ((b1 (car f1))) 
         (let ((b2 (assoc (car b1) f2))) 
           (if b2 
               (if (equal? (cdr b1) (cdr b2)) 
                   (merge-frame (cdr f1) f2) 
                   the-empty-stream) 
               (merge-frame (cdr f1) (cons b1 f2))))))) 

poly

Actually my solution is not complete. There are still some bugs to be improved.

If we just consider the each clause of 'and' are disjunct, and just separate the evaluation of each clause of 'and' just like the above one solution provided by donald (simply compare the cdr part of two different bindings with same variable in two frames), some input will not be seen as 'legal'.Take an instance:

 (and (append-to-form (1 2) (3 4) ?x) 
      (append-to-form (1) ?y ?x)) 

The implementation of append-to-form is the same as textbook's.

the value of '?y' is based on '?x'. But the '?x' in the second clause is apparently not bound. Its value should be seen as the same as '?x' in the first clause. But we just separate the two clauses. So it won't work and the input above will get nothing. The detail is kind of complicated.

The evaluation of first clause will get:

(((? 12 z) 3 4) ((? 14 y) 3 4) ((? 11 z) (? 12 u) ? 12 z) ((? 12 y) 3 4) ((? 12 v)) ((? 12 u) . 2) ((? x) (? 11 u) ? 11 z) ((? 11 y) 3 4) ((? 11 v) 2) ((? 11 u) . 1))

second is:

(((? 15 z) ? 17 y) ((? 15 y) ? 17 y) ((? x) (? 15 u) ? 15 z) ((? y) ? 15 y) ((? 15 v)) ((? 15 u) . 1))

As we can see, the '?x' binding in first one is ((? x) (? 11 u) ? 11 z), which is ((? x) (? 15 u) ? 15 z) in the second one. Apparently it will not be seen as the same if we simply compare its cdr part.

Actually, in some complex case, the value of bindings in the frame will always also be variables as above situation. So I think we need to find its final actual binding and extend it to the frame if there is no not-variable bindings.

the procedure "extend-if-possible" provided in the textbook will do this job:

 (define (extend-if-possible var val frame) 
   (let ((binding (binding-in-frame var frame))) 
     (cond (binding 
            (unify-match 
             (binding-value binding) val frame)) 
           ; var has no binding check if val is variable. 
           ((var? val) 
            (let ((binding (binding-in-frame val frame))) 
              (if binding 
                  ; check if var and binding are matched 
                  (unify-match 
                   var (binding-value binding) frame) 
                  ; bind var to val if both of them are variable 
                  (extend var val frame)))) 
           ; check if var itself is in val 
           ((depends-on? val var frame) 
            'failed) 
           (else (extend var val frame))))) 

My whole solution is as follows.

 (define (conjoin conjuncts frame-stream) 
   (if (empty-conjunction? conjuncts) 
       frame-stream 
       (merge 
        (qeval (first-conjunct conjuncts) frame-stream) 
        (conjoin (rest-conjuncts conjuncts) frame-stream)))) 
  
 (define (merge stream1 stream2) 
   (stream-flatmap 
    (lambda (f1) 
      (stream-filter 
       (lambda (f) (not (eq? f 'failed))) 
       (stream-map 
        (lambda (f2) (merge-frames f1 f2)) 
        stream2))) 
    stream1)) 
  
 (define (merge-frames f1 f2) 
   (cond ((null? f1) f2) 
         ((eq? 'failed f2) 'failed) 
         (else  
          (let ((var (binding-variable (car f1))) 
                (val (binding-value (car f1)))) 
            (let ((extension (extend-if-possible var val f2))) 
              (merge-frames (cdr f1) extension)))))) 
 ;;; Query input: 
 (and (append-to-form (1 2) (3 4) ?x) 
      (append-to-form (1) ?y ?x)) 
  
 ;;; Quary results: 
 (and (append-to-form (1 2) (3 4) (1 2 3 4))  
      (append-to-form (1) (2 3 4) (1 2 3 4))) 

Actually, when there are some kind of recursions existed, this will end up with an infinite loop. Take an instance:

 (rule (reverse () ())) 
  
 (rule (reverse (?x . ?y) ?z) 
       (and (reverse ?y ?v) 
            (append-to-form ?v (?x) ?z))) 

The above one is just one bug. Another one is for the consideration of 'not' and 'unique' procedure we define before. As we know this two is for filtering the result we find out. But there will be no frame to filter if we separate the evaluation of each clauses of 'and'.

That's all.