15
Пример: логический вывод
Вследующих трех главах вашему вниманию предлагаются три само стоятельные программы. Они были выбраны, чтобы показать, какой вид могут принимать программы на Лиспе, и продемонстрировать зада чи, для решения которых этот язык особенно хорошо подходит.
Вэтой главе мы напишем программу, совершающую логические «умо заключения», основанные на наборе правил «если-то». Это классиче ский пример, который не только часто встречается в учебниках, но и от ражает изначальную концепцию Лиспа как языка «символьных вы числений». Многие ранние программы на Лиспе имеют черты той, кото рая описана ниже.
15.1. Цель
В данной программе мы собираемся представлять информацию в зна комой нам форме: списком из предиката и его аргументов. Представим факт отцовства Дональда по отношению к Нэнси таким образом:
(parent donald nancy)
Помимо фактов наша программа будет использовать правила, которые сообщают, что может быть выведено из имеющихся фактов. Мы будем представлять эти правила так:
(<- заголовок тело)
где заголовок соответствует следствию, а тело – условию. Переменные внутри них мы будем представлять символами, начинающимися со зна ка вопроса. Таким образом, следующее правило:
(<- (child ?x ?y) (parent ?y ?x))
254 Глава 15. Пример: логический вывод
сообщает, что если y является родителем x, то x является ребенком y, или, говоря более точно, мы можем доказать любой факт вида (child x y) через доказательство (parent y x).
Тело (условная часть правила) может быть составным выражением, включающим логические операторы and, or, not. Так, правило, согласно которому, если x является мужчиной и родителем y, то x – отец y, выгля дит следующим образом:
(<- (father ?x ?y) (and (parent ?x ?y) (male ?x)))
Одни правила могут опираться на другие. К примеру, правило, опреде ляющее, является ли x дочерью y, опирается на уже определенное пра вило родительства:
(<- (daughter ?x ?y) (and (child ?x ?y) (female ?x)))
При доказательстве выражений может применяться любое количество правил, необходимых для достижения твердой почвы фактов. Этот про цесс иногда называют обратной цепочкой логического вывода (backward chaining). Обратной потому, что вывод сперва рассматривает часть-след ствие, чтобы увидеть, будет ли правило полезным, прежде чем продол жать доказательство части-условия. А цепочкой он называется потому, что правила зависят друг от друга, формируя цепочку (скорее даже де рево) правил, которая ведет от того, что мы хотим доказать, к тому, что мы уже знаем.°
15.2. Сопоставление
Чтобы написать нашу программу для обратной цепочки логического вывода, нам понадобится функция, выполняющая сопоставление с об разцом (pattern-matching). Эта функция должна сравнивать два списка, возможно, содержащие переменные, и проверять, есть ли такая комби нация значений переменных, при которой списки стали бы равными. Например, если ?x и ?y – переменные, то два списка:
(p ?x ?y c ?x) (p a b c a)
сопоставляются, если ?x = a и ?y = b, а списки
(p ?x b ?y a) (p ?y b c a)
сопоставляются при ?x = ?y = c.
На рис. 15.1 показана функция match, сопоставляющая два дерева. Если они могут совпадать, то она возвращает ассоциативный список, пока зывающий, каким образом они совпадают:
> (match ’(p a b c a) ’(p ?x ?y c ?x)) ((?Y . B) (?X . A))
T
15.2. Сопоставление |
255 |
>(match ’(p ?x b ?y a) ’(p ?y b c a)) ((?Y . C) (?X . ?Y))
T
>(match ’(a b c) ’(a a a)
NIL
По мере поэлементного сравнения match накапливает присваивания пе ременным значений, которые мы называем связями (bindings), в пере менной binds. Если сопоставление завершилось успешно, то match воз вращает сгенерированные связи, в противном случае возвращает nil. Так как не все успешные сопоставления генерируют хоть какие-то свя зи, match, по тому же принципу, что и gethash, возвращает второе значе ние, указывающее на успешность сопоставления.
> (match ’(p ?x) ’(p ?x)) NIL
T
(defun match (x y &optional binds) (cond
((eql x y) (values binds t))
((assoc x binds) (match (binding x binds) y binds)) ((assoc y binds) (match x (binding y binds) binds)) ((var? x) (values (cons (cons x y) binds) t))
((var? y) (values (cons (cons y x) binds) t)) (t
(when (and (consp x) (consp y)) (multiple-value-bind (b2 yes)
(match (car x) (car y) binds) (and yes (match (cdr x) (cdr y) b2)))))))
(defun var? (x) (and (symbolp x)
(eql (char (symbol-name x) 0) #\?)))
(defun binding (x binds) (let ((b (assoc x binds)))
(if b
(or (binding (cdr b) binds) (cdr b)))))
Рис. 15.1. Функции для сопоставления
Когда match возвращает nil и t, как произошло выше, это означает, что имеет место успешное сопоставление, не создавшее связей для перемен ных. Алгоритм действия match можно описать следующим образом:
1.Если x и y равны с точки зрения eql, то они сопоставляются; иначе:
2.Если x – это переменная, уже ассоциированная со значением, то она сопоставляется с y, если значения совпадают; иначе:
256 |
Глава 15. Пример: логический вывод |
3.Если y – это переменная, уже ассоциированная со значением, то она сопоставляется с x, если значения совпадают; иначе:
4.Если переменная x не ассоциирована со значением, то с ней связыва ется текущее значение; иначе:
5.Если переменная y не ассоциирована со значением, то с ней связыва ется текущее значение; иначе:
6.Два значения сопоставляются, если они оба – cons-ячейки, их carэлементы сопоставляются, а cdr сопоставляются с учетом получен ных связей.
Вот два примера, демонстрирующие по порядку все шесть случаев:
> (match ’(p ?v b ?x d (?z ?z)) ’(p a ?w c ?y ( e e)) ’((?v . a) (?w . b)))
((?Z . E) (?Y . D) (?X . C) (?V . A) (?W . B)) T
Чтобы найти ассоциированное значение (если оно имеется), match вызы вает binding. Эта функция должна быть рекурсивной, так как в резуль тате сопоставления могут получиться пары, в которых переменная свя зана со значением косвенно, например ?x может быть связан с a через список, содержащий (?x . ?y) и (?y . a).
> (match ’(?x a) ’(?y ?y)) ((?Y . A) (?X . ?Y))
T
Сопоставив ?x с ?y, а ?y с a, мы видим косвенную связь переменной ?x со значением.
15.3. Отвечая на запросы
Теперь, когда введены основные концепции сопоставления, мы можем перейти непосредственно к назначению нашей программы: если мы име ем выражение, вероятно, содержащее переменные, то исходя из имею щихся фактов и правил мы можем найти все ассоциации, делающие это выражение истинным. Например, если у нас есть только тот факт, что
(parent donald nancy)
и мы просим программу доказать
(parent ?x ?y)
то она вернет нечто, похожее на
(((?x . donald) (?y . nancy)))
Это означает, что наше выражение может быть истинным лишь в одном случае: ?x – это donald, а ?y – nancy.
15.3. Отвечая на запросы |
257 |
Поскольку у нас есть функция сопоставления, можно утверждать, что мы на правильном пути. Теперь нам нужно научиться определять пра вила. Соответствующий код приведен на рис. 15.2. Правила содержатся в хеш-таблице *rules* в соответствии с предикатами в заголовках. Это вводит ограничение, что переменные не могут находиться на месте пре дикатов. От него можно избавиться, если хранить такие правила в от дельном списке, но тогда для доказательства чего-либо нам пришлось бы сопоставлять друг другу каждое правило из этого списка.
(defvar *rules* (make-hash-table))
(defmacro <- (con &optional ant) ‘(length (push (cons (cdr ’,con) ’,ant)
(gethash (car ’,con) *rules*))))
Рис. 15.2. Определение правил
Мы будем использовать макрос <- для определения и правил, и фактов. Факт представляется в виде правила, содержащего только заголовок. Это соответствует нашему представлению о правилах. Правило гласит, что для доказательства заголовка необходимо доказать тело, а раз тела нет, то и доказывать нечего. Вот два уже знакомых нам примера:
>(<- (parent donald nancy))
1
>(<- (child ?x ?y) (parent ?y ?x))
1
Вызов <- возвращает номер нового правила для заданного предиката; оборачивание length вокруг push позволяет избежать большого объема информации, выводимой в toplevel.
На рис. 15.3 содержится большая часть кода, нужного нам для вывода.
Функция prove является осью, вокруг которой вращается весь логиче ский вывод. Она принимает выражение и необязательный набор связей. Если выражение не содержит логических операторов, то вызывается prove-simple. Именно здесь происходит сам обратный вывод. Эта функ ция ищет все правила с истинным предикатом и пытается сопоставить заголовок каждого из них с фактом, который мы хотим доказать. Затем для каждого совпавшего заголовка доказывается его тело с учетом но вых связей, созданных match. Вызовы prove возвращают списки связей, которые затем собираются mapcan:
>(prove-simple ’parent ’(donald nancy) nil) (NIL)
>(prove-simple ’child ’(?x ?y) nil)
(((#:?6 . NANCY) (#:?5 . DONALD) (?Y . #:?5) (?X . #:?6)))
258 Глава 15. Пример: логический вывод
(defun prove (expr &optional binds) |
|
(case (car expr) |
|
(and (prove-and (reverse (cdr expr)) binds)) |
|
(or |
(prove-or (cdr expr) binds)) |
(not (prove-not (cadr expr) binds)) |
|
(t |
(prove-simple (car expr) (cdr expr) binds)))) |
(defun prove-simple (pred args binds) |
|
(mapcan #’(lambda (r) |
|
|
(multiple-value-bind (b2 yes) |
|
(match args (car r) binds) |
|
(when yes |
|
(if (cdr r) |
|
(prove (cdr r) b2) |
|
(list b2))))) |
|
(mapcar #’change-vars |
|
(gethash pred *rules*)))) |
(defun change-vars (r) |
|
(sublis (mapcar #’(lambda (v) (cons v (gensym "?"))) |
|
|
(vars-in r)) |
|
r)) |
(defun vars-in (expr) |
|
(if (atom expr) |
|
(if (var? expr) (list expr)) |
|
(union (vars-in (car expr)) |
|
|
(vars-in (cdr expr))))) |
|
|
Рис. 15.3. Вывод |
|
Оба полученных значения подтверждают, что есть лишь один путь до казательства. (Если доказать утверждение не получилось, возвращает ся nil.) Первый пример был выполнен без создания каких-либо связей, в то время как во втором примере переменные ?x и ?y были связаны (кос венно) с nancy и donald.
Между прочим, мы видим здесь хороший пример высказанной ранее (стр. 39) идеи: поскольку наша программа написана в функциональном стиле, мы можем тестировать каждую функцию отдельно.
Теперь пара слов о том, зачем нужен gensym. Раз мы собираемся исполь зовать правила, содержащие переменные, то нам нужно избегать нали чия двух правил с одной и той же переменной. Рассмотрим два правила:
(<- (child ?x ?y) (parent ?y ?x))
(<- (daughter ?y ?x) (and (child ?y ?x) (female ?y)))
В них утверждается, что для любого x и y 1) x является ребенком y, если y является родителем x; 2) y является дочкой x, если y является ребен ком x и y – женщина. Связь между переменными в рамках одного пра
15.3. Отвечая на запросы |
259 |
вила имеет большое значение, а вот факт, что два правила используют одинаковые имена для определения переменных, совершенно случаен.
Если мы воспользуемся этими правилами в том виде, в каком только что их записали, то они не будут работать. Если мы попытаемся дока зать, что a – дочь b, то сопоставление с заголовком второго правила даст связи ?y = a и ?x = b. Имея такие связи, мы не сможем воспользоваться первым правилом:
> (match ’(child ?y ?x) ’(child ?x ?y)
’((?y . a) (?x . b)))
NIL
Для гарантии того, что переменные будут действовать лишь в пределах одного правила, мы заменяем все переменные внутри правила на gensym. Для этой цели определена функция change-vars. Так мы приобретаем за щиту от совпадений с другими переменными в определениях других правил. Но, поскольку правила могут применяться рекурсивно, нам также нужна защита при сопоставлении с этим же правилом. Для этого change-vars должна вызываться не только при определении правил, но и при каждом их использовании.
Теперь остается лишь определить функции для доказательства состав ных утверждений. Соответствующий код приведен на рис. 15.4. Обра ботка выражений or или not предельно проста. В первом случае мы со бираем все связи, полученные из каждого выражения в or. Во втором случае мы просто возвращаем имеющиеся связи, если выражение внут ри not возвратило nil.
(defun prove-and (clauses binds) (if (null clauses)
(list binds)
(mapcan #’(lambda (b)
(prove (car clauses) b)) (prove-and (cdr clauses) binds))))
(defun prove-or (clauses binds)
(mapcan #’(lambda (c) (prove c binds)) clauses))
(defun prove-not (clause binds) (unless (prove clause binds)
(list binds)))
Рис. 15.4. Логические операторы
Функция prove-and лишь чуть сложнее. Она работает как фильтр, дока зывая первое выражение для каждого из наборов связей, полученных из остальных выражений. По этой причине выражения внутри and рас
260 |
Глава 15. Пример: логический вывод |
сматриваются в обратном порядке. Переворачивание результата proveand компенсирует это явление (так как результирующий список выра жений формируется функцией в обратном порядке, в конце ее выполне ния этот список нужно развернуть) .
Теперь у нас есть рабочая программа, но она не очень удобна для конеч ного пользователя. Разбирать списки связей, возвращаемых prove, до вольно сложно, а ведь с усложнением выражений они будут только рас ти. Эту проблему решает макрос with-answer, изображенный на рис. 15.5. Он принимает запрос (не вычисленный) и вычисляет свое тело для каж дого набора связей, полученных при обработке запроса, связывая каж дую переменную запроса со значением, которое она имеет в текущем экземпляре связей:
> (with-answer (parent ?x ?y)
(format t "~A is the parent of ~A.~%" ?x ?y)) DONALD is the parent of NANCY.
NIL
Этот макрос расшифровывает полученные связи и предоставляет удоб ный способ использования prove в наших программах. На рис. 15.6 по казан результат его раскрытия, а рис. 15.7 демонстрирует некоторые примеры использования этого макроса.
(defmacro with-answer (query &body body) (let ((binds (gensym)))
‘(dolist (,binds (prove ’,query)) (let ,(mapcar #’(lambda (v)
‘(,v (binding ’,v ,binds))) (vars-in query))
,@body))))
Рис. 15.5. Интерфейсный макрос
(with-answer (p ?x ?y) (f ?x ?y))
;;; раскрывается в:
(dolist (#:g1 (prove ’(p ?x ?y))) (let ((?x (binding ’?x #:g1))
(?y (binding ’?y #:g1))) (f ?x ?y)))
Рис. 15.6. Раскрытие вызова with-answer