Унификация, переименование правил и бюджет глубины

(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)))