4.4.4.4 Правила и унификация

Процедура apply-rules - это аналог find-assertion (раздел 4.4.4.3). Она принимает на входе образец и кадр, а порождает поток расширенных кадров, применяя правила из базы данных. Stream-flatmap отображает через apply-rule поток возможно применимых правил (отобранных процедурой fetch-rules из раздела 4.4.4.5) и склеивает получившиеся потоки кадров.

(define (apply-rules pattern frame) (stream-flatmap (lambda (rule)

(apply-a-rule rule pattern frame)) (fetch-rules pattern frame)))

Процедура apply-a-rule применяет правила способом, описанным в разделе 4.4.2. Сначала она дополняет кадр-аргумент, унифицируя в его рамках заключение правила с образцом. Если это удается, она выполняет в получившемся кадре тело правила.

Однако прежде всего программа переименовывает все переменные в правиле и дает им уникальные новые имена. Это делается потому, что мы не хотим, чтобы переменные из различных применений правил смешивались друг с другом. К примеру, если в двух правилах используется переменная ?x, то каждое из них может добавить связывание этой переменной к кадру, в котором оно применяется. Однако эти два ?x не имеют друг к другу никакого отношения, и мы не должны обманываться и считать, что два связывания этих переменных обязаны соответствовать друг другу. Вместо переименования переменных мы могли бы придумать более хитрую структуру окружений; однако выбранный здесь подход с переименованиями - самый простой, хотя и не самый эффективный. (См. упражнение 4.79.) Вот процедура apply-a-rule:

(define (apply-a-rule rule query-pattern query-frame) (let ((clean-rule (rename-variables-in rule))) (let ((unify-result

(unify-match query-pattern

(conclusion clean-rule) query-frame))) (if (eq? unify-result failed) the-empty-stream (qeval (rule-body clean-rule)

(singleton-stream unify-result))))))

Селекторы rule-body и conclusion, извлекающие части правил, описаны в разделе 4.4.4.7.

Чтобы породить уникальные имена переменных, мы связываем с каждым применением правила уникальный идентификатор (например, число) и цепляем его к исходным именам переменных. Например, если идентификатор применения правила равен 7, мы можем заменить все ?x в правиле на ?x-7, а все ?y на ?y-7. (Процедуры make-new-variable и new-rule-application-id содержатся среди синтаксических процедур в разделе 4.4.4.7.)

(define (rename-variables-in rule)

(let ((rule-application-id (new-rule-application-id))) (define (tree-walk exp) (cond ((var? exp)

(make-new-variable exp rule-application-id)) ((pair? exp) (cons (tree-walk (car exp))

(tree-walk (cdr exp)))) (else exp))) (tree-walk rule)))

Алгоритм унификации реализуется в виде процедуры, которая принимает на входе два образца и кадр, а возвращает либо расширенный кадр, либо символ failed. Унификатор в основном подобен сопоставителю, но только он симметричен - переменные разрешаются с обеих сторон сопоставления. Процедура unify-match подобна pattern-match, за исключением нового отрезка кода (отмеченного знаком «***»), где обрабатывается случай, когда объект на правой стороне сопоставления является переменной.

(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 pi frame)) ; *** ((and (pair? p1) (pair? p2)) (unify-match (cdr p1)

(cdr p2)

(unify-match (car p1) (car p2) frame)))

(else failed)))

При унификации, как и при одностороннем сопоставлении с образцом, нам нужно принимать предлагаемое расширение кадра только в том случае, когда оно не противоречит имеющимся связываниям. Процедура extend-if-pos-sible, используемая при унификации, подобна extend-if-consistent из сопоставителя, за исключением двух проверок, отмеченных в программе значком «***». В первом случае, если переменная, которую мы пытаемся сопоставить, не найдена, но значение, с которым мы ее сопоставляем, само является (другой) переменной, требуется проверить, нет ли у этой второй переменной значения, и если да, сопоставить его. Если же обе стороны сопоставления несвязаны, мы любую из них можем связать с другой.

Вторая проверка связана с попытками связать переменную с образцом, который ее саму содержит. Такая ситуация может возникнуть, когда в обоих образцах повторяются переменные. Рассмотрим, например, унификацию образцов (?x ?x) и (?y (выражение, содержащее ?y)) в кадре, где не связаны ни ?x, ни ?y. Сначала ?x сопоставляется с ?y, и возникает связывание переменной ?x с ?y. Затем та же переменная ?x сопоставляется с данным выражением, которое включает ?y. Поскольку ?x уже связана со значением ?y, это приводит к тому, что с выражением сопоставляется ?y. Если мы считаем, что унификатор занят поиском набора значений для переменных, которые делают образцы одинаковыми, то значит, эти образцы содержат инструкции найти такое значение ?y, чтобы ?y был равен выражению, содержащему ?y. Общего метода для решения таких задач не существует, так что мы такие связывания отвергаем;

эти случаи распознаются предикатом depends-on?.80 С другой стороны, нам не хочется отвергать попытки связать переменную саму с собой. Рассмотрим, например, унификацию (?x ?x) с (?y ?y). Вторая попытка связать ?x с ?y вызывает сопоставление ?y (старое значение ?x) с ?y (новым значением ?x). Этот случай обрабатывается веткой equal? внутри unify-match.

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

Процедура depends-on? - это предикат. Он проверяет, зависит ли выражение, которое предлагается сделать значением переменной образца, от этой переменной. Это нужно делать по отношению к текущему кадру, поскольку выражение может содержать вхождения переменной, уже обладающей значением, которое, в свою очередь, зависит от нашей переменной. По структуре depends-on? представляет собой простой рекурсивный обход дерева, во время которого мы по необходимости подставляем значения переменных.

(define (depends-on? exp var frame) (define (tree-walk e)

80В общем случае унификация ?y с выражением, содержащим ?y, требует нахождения неподвижной точки уравнения ?y = {выражение, содержащее ?y). Иногда возможно синтаксическим образом создать выражение, которое кажется решением уравнения. Например, кажется, что ?y = (f y) имеет неподвижную точку (f (f (f ...))), которую мы можем получить, начав с выражения (f ?y) и систематически подставляя (f ?y) вместо ?y. К сожалению, не у всякого такого уравнения имеется осмысленная неподвижная точка. Вопросы, возникающие здесь, подобны вопросам работы с бесконечными последовательностями в математике. Например, мы знаем, что решение уравнения y = 1 + y/2 равно 2. Если мы начнем с выражения 1 + y/2 и будем подставлять 1 + y/2 вместо у, то получим

2 = y = 1 + y/2 = 1 + (1 + y/2)/2 = 1 + 1/2 + y/4 = • • • ,

что ведет к

2 = 1 + 1/2 + 1/4 + 1/8 + ••• .

Однако если мы попытаемся проделать те же преобразования, использовав тот факт, что решение уравнения y = 1 + 2y равно -1, то получим

-1 = y = 1 + 2y = 1 = 2(1 + 2y) = 1 + 2 + 4y = • • • ,

что ведет к

-1 = 1+2 + 4 + 8 + ••• .

Несмотря на то, что формальные преобразования, ведущие к этим двум уравнениям, одинаковы, первый результат является верным утверждением о бесконечных последовательностях, а второй нет. Подобным образом и при работе с унификациями работа с произвольными синтаксически правильными выражениями может привести к ошибкам.