4.4.6 · Implementing the query system

Unification joins assertions and renamed rules under one frame protocol.

Implement bidirectional variable unification, rule-variable renaming, assertion and rule search, negation-as-failure, and an explicit rule-depth budget.

Guiding question

What additional machinery lets a query match not only stored facts but also conclusions derived from reusable rules?

Unify variables appearing on either side of a comparison
Follow an existing variable binding before extending a frame
Rename every rule variable for each application
Apply a rule by unifying its conclusion and evaluating its body
Combine and, or, and finite negation-as-failure over frame lists
Bound recursive rule application with an explicit remaining depth

unify-match generalizes simple assertion matching. Either input may be a variable, and an existing binding may lead to another variable or structure before the comparison finishes. Before every rule application, rename-rule replaces each logical variable with a fresh key carrying the current rule-application id. This prevents a rule’s private intermediate names from colliding with query variables or another application of the same rule.

simple-query combines direct assertion matches with rule results. A rule result unifies the query pattern with the renamed conclusion, then sends the resulting frame through qeval on the rule body. and pipelines frames, or appends alternatives, and not keeps a frame only when its subquery has no result under that frame. The explicit depth is the exact finite resource boundary for rule expansion.

SICP code6,009 of 1,048,576 UTF-8 bytes

(begin
  (define failed 'failed)
  (define (variable? expression)
    (and (pair? expression) (eq? (car expression) 'var)))
  (define (variable-key variable) (cadr variable))
  (define (binding variable frame)
    (assoc (variable-key variable) frame))
  (define (extend-if-possible variable value frame)
    (let ((record (binding variable frame)))
      (cond (record
             (unify-match (cdr record) value frame))
            ((variable? value)
             (let ((value-record (binding value frame)))
               (if value-record
                   (unify-match variable (cdr value-record) frame)
                   (cons (cons (variable-key variable) value) frame))))
            (else
             (cons (cons (variable-key variable) value) frame)))))
  (define (unify-match left right frame)
    (cond ((eq? frame failed) failed)
          ((equal? left right) frame)
          ((variable? left)
           (extend-if-possible left right frame))
          ((variable? right)
           (extend-if-possible right left frame))
          ((and (pair? left) (pair? right))
           (unify-match
             (cdr left)
             (cdr right)
             (unify-match (car left) (car right) frame)))
          (else failed)))
  (define (instantiate expression frame)
    (cond ((variable? expression)
           (let ((record (binding expression frame)))
             (if record
                 (instantiate (cdr record) frame)
                 expression)))
          ((pair? expression)
           (cons (instantiate (car expression) frame)
                 (instantiate (cdr expression) frame)))
          (else expression)))

  (define rename-counter 0)
  (define rename-table '())
  (define (fresh-variable variable)
    (let ((record (assoc (variable-key variable) rename-table)))
      (if record
          (cdr record)
          (let ((fresh
                 (list 'var
                       (list (variable-key variable)
                             rename-counter))))
            (set! rename-table
                  (cons (cons (variable-key variable) fresh)
                        rename-table))
            fresh))))
  (define (rename-rule rule)
    (set! rename-counter (+ rename-counter 1))
    (set! rename-table '())
    (define (rename expression)
      (cond ((variable? expression)
             (fresh-variable expression))
            ((pair? expression)
             (cons (rename (car expression))
                   (rename (cdr expression))))
            (else expression)))
    (list 'rule
          (rename (cadr rule))
          (rename (caddr rule))))

  (define assertions
    '((parent alice bob)
      (parent bob carol)
      (parent bob dave)
      (parent carol erin)
      (job alice engineer)
      (job bob manager)
      (job carol researcher)))
  (define rules
    '((rule
        (grandparent (var x) (var z))
        (and (parent (var x) (var y))
             (parent (var y) (var z))))))

  (define (assertion-results pattern frames)
    (define (for-frame frame records)
      (if (null? records)
          '()
          (let ((result
                 (unify-match pattern (car records) frame)))
            (if (eq? result failed)
                (for-frame frame (cdr records))
                (cons result
                      (for-frame frame (cdr records)))))))
    (if (null? frames)
        '()
        (append (for-frame (car frames) assertions)
                (assertion-results pattern (cdr frames)))))

  (define (rule-results pattern frames depth)
    (define (for-frame frame remaining-rules)
      (if (or (= depth 0) (null? remaining-rules))
          '()
          (let* ((renamed (rename-rule (car remaining-rules)))
                 (conclusion (cadr renamed))
                 (body (caddr renamed))
                 (unified (unify-match pattern conclusion frame)))
            (append
              (if (eq? unified failed)
                  '()
                  (qeval body (list unified) (- depth 1)))
              (for-frame frame (cdr remaining-rules))))))
    (if (null? frames)
        '()
        (append (for-frame (car frames) rules)
                (rule-results pattern (cdr frames) depth))))

  (define (simple-query pattern frames depth)
    (append (assertion-results pattern frames)
            (rule-results pattern frames depth)))
  (define (conjoin queries frames depth)
    (if (null? queries)
        frames
        (conjoin
          (cdr queries)
          (qeval (car queries) frames depth)
          depth)))
  (define (disjoin queries frames depth)
    (if (null? queries)
        '()
        (append (qeval (car queries) frames depth)
                (disjoin (cdr queries) frames depth))))
  (define (negate query frames depth)
    (if (null? frames)
        '()
        (append
          (if (null? (qeval query (list (car frames)) depth))
              (list (car frames))
              '())
          (negate query (cdr frames) depth))))
  (define (qeval query frames depth)
    (cond ((and (pair? query) (eq? (car query) 'and))
           (conjoin (cdr query) frames depth))
          ((and (pair? query) (eq? (car query) 'or))
           (disjoin (cdr query) frames depth))
          ((and (pair? query) (eq? (car query) 'not))
           (negate (cadr query) frames depth))
          (else
           (simple-query query frames depth))))

  (define grandparent-frames
    (qeval
      '(grandparent alice (var who))
      (list '())
      4))
  (define filtered-child-frames
    (qeval
      '(and
         (parent bob (var child))
         (not (parent (var child) erin)))
      (list '())
      4))
  (define alternative-frames
    (qeval
      '(or (job alice engineer)
           (job carol researcher))
      (list '())
      4))
  (list
    (map (lambda (frame)
           (instantiate '(grandchild (var who)) frame))
         grandparent-frames)
    (map (lambda (frame)
           (instantiate '(var child) frame))
         filtered-child-frames)
    (length alternative-frames)))

(begin
  (define failed 'failed)
  (define (variable? expression)
    (and (pair? expression) (eq? (car expression) 'var)))
  (define (variable-key variable) (cadr variable))
  (define (binding variable frame)
    (assoc (variable-key variable) frame))
  (define (extend-if-possible variable value frame)
    (let ((record (binding variable frame)))
      (cond (record
             (unify-match (cdr record) value frame))
            ((variable? value)
             (let ((value-record (binding value frame)))
               (if value-record
                   (unify-match variable (cdr value-record) frame)
                   (cons (cons (variable-key variable) value) frame))))
            (else
             (cons (cons (variable-key variable) value) frame)))))
  (define (unify-match left right frame)
    (cond ((eq? frame failed) failed)
          ((equal? left right) frame)
          ((variable? left)
           (extend-if-possible left right frame))
          ((variable? right)
           (extend-if-possible right left frame))
          ((and (pair? left) (pair? right))
           (unify-match
             (cdr left)
             (cdr right)
             (unify-match (car left) (car right) frame)))
          (else failed)))
  (define (instantiate expression frame)
    (cond ((variable? expression)
           (let ((record (binding expression frame)))
             (if record
                 (instantiate (cdr record) frame)
                 expression)))
          ((pair? expression)
           (cons (instantiate (car expression) frame)
                 (instantiate (cdr expression) frame)))
          (else expression)))

(define rename-counter 0)
  (define rename-table '())
  (define (fresh-variable variable)
    (let ((record (assoc (variable-key variable) rename-table)))
      (if record
          (cdr record)
          (let ((fresh
                 (list 'var
                       (list (variable-key variable)
                             rename-counter))))
            (set! rename-table
                  (cons (cons (variable-key variable) fresh)
                        rename-table))
            fresh))))
  (define (rename-rule rule)
    (set! rename-counter (+ rename-counter 1))
    (set! rename-table '())
    (define (rename expression)
      (cond ((variable? expression)
             (fresh-variable expression))
            ((pair? expression)
             (cons (rename (car expression))
                   (rename (cdr expression))))
            (else expression)))
    (list 'rule
          (rename (cadr rule))
          (rename (caddr rule))))

(define assertions
    '((parent alice bob)
      (parent bob carol)
      (parent bob dave)
      (parent carol erin)
      (job alice engineer)
      (job bob manager)
      (job carol researcher)))
  (define rules
    '((rule
        (grandparent (var x) (var z))
        (and (parent (var x) (var y))
             (parent (var y) (var z))))))

(define (assertion-results pattern frames)
    (define (for-frame frame records)
      (if (null? records)
          '()
          (let ((result
                 (unify-match pattern (car records) frame)))
            (if (eq? result failed)
                (for-frame frame (cdr records))
                (cons result
                      (for-frame frame (cdr records)))))))
    (if (null? frames)
        '()
        (append (for-frame (car frames) assertions)
                (assertion-results pattern (cdr frames)))))

(define (rule-results pattern frames depth)
    (define (for-frame frame remaining-rules)
      (if (or (= depth 0) (null? remaining-rules))
          '()
          (let* ((renamed (rename-rule (car remaining-rules)))
                 (conclusion (cadr renamed))
                 (body (caddr renamed))
                 (unified (unify-match pattern conclusion frame)))
            (append
              (if (eq? unified failed)
                  '()
                  (qeval body (list unified) (- depth 1)))
              (for-frame frame (cdr remaining-rules))))))
    (if (null? frames)
        '()
        (append (for-frame (car frames) rules)
                (rule-results pattern (cdr frames) depth))))

(define (simple-query pattern frames depth)
    (append (assertion-results pattern frames)
            (rule-results pattern frames depth)))
  (define (conjoin queries frames depth)
    (if (null? queries)
        frames
        (conjoin
          (cdr queries)
          (qeval (car queries) frames depth)
          depth)))
  (define (disjoin queries frames depth)
    (if (null? queries)
        '()
        (append (qeval (car queries) frames depth)
                (disjoin (cdr queries) frames depth))))
  (define (negate query frames depth)
    (if (null? frames)
        '()
        (append
          (if (null? (qeval query (list (car frames)) depth))
              (list (car frames))
              '())
          (negate query (cdr frames) depth))))
  (define (qeval query frames depth)
    (cond ((and (pair? query) (eq? (car query) 'and))
           (conjoin (cdr query) frames depth))
          ((and (pair? query) (eq? (car query) 'or))
           (disjoin (cdr query) frames depth))
          ((and (pair? query) (eq? (car query) 'not))
           (negate (cadr query) frames depth))
          (else
           (simple-query query frames depth))))

(define grandparent-frames
    (qeval
      '(grandparent alice (var who))
      (list '())
      4))
  (define filtered-child-frames
    (qeval
      '(and
         (parent bob (var child))
         (not (parent (var child) erin)))
      (list '())
      4))
  (define alternative-frames
    (qeval
      '(or (job alice engineer)
           (job carol researcher))
      (list '())
      4))
  (list
    (map (lambda (frame)
           (instantiate '(grandchild (var who)) frame))
         grandparent-frames)
    (map (lambda (frame)
           (instantiate '(var child) frame))
         filtered-child-frames)
    (length alternative-frames)))

Examples

Result—

Output: —
Value: —
Diagnostic: —

Execution trace0 / 0 events

Expected result

The engine returns (((grandchild carol) (grandchild dave)) (dave) 2).

Trace focus

Follow the query pattern into direct assertion matching and then into each renamed rule conclusion. Inspect the fresh variable keys before the grandparent body enters conjoin. For the negated parent query, show why carol is rejected and dave is retained. Confirm that the two or branches start from the same empty input frame.

Try it yourself

Change the program and compare the result.

Add an ancestor rule with a direct parent clause and a recursive clause. Run it with depth 4 and depth 1, report the answers separately, and explain how the work budget determines the result frontier.

Show hint

Use two rules with the same ancestor conclusion. The recursive body should introduce one fresh intermediate variable and call ancestor with the remaining depth budget.

Complete this lesson

0 of 23 lessons complete in this chapter0%