Х. Абельсон, Дж. Дж. Сассман, Дж. Сассман - Структура и интерпретация компьютерных программ (1108516), страница 101
Текст из файла (страница 101)
Метаязыковая абстракцияПри унификации, как и при одностороннем сопоставлении с образцом, нам нужнопринимать предлагаемое расширение кадра только в том случае, когда оно не противоречит имеющимся связываниям. Процедура extend-if-possible, используемая приунификации, подобна extend-if-consistent из сопоставителя, за исключением двухпроверок, отмеченных в программе значком «***». В первом случае, если переменная,которую мы пытаемся сопоставить, не найдена, но значение, с которым мы ее сопоставляем, само является (другой) переменной, требуется проверить, нет ли у этой второйпеременной значения, и если да, сопоставить его.
Если же обе стороны сопоставлениянесвязаны, мы любую из них можем связать с другой.Вторая проверка связана с попытками связать переменную с образцом, который ее саму содержит. Такая ситуация может возникнуть, когда в обоих образцах повторяются переменные. Рассмотрим, например, унификацию образцов (?x ?x) и (?y hвыражение,содержащее ?yi) в кадре, где не связаны ни ?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.80 В общем случае унификация ?y с выражением, содержащим ?y, требует нахождения неподвижной точкиуравнения ?y = hвыражение, содержащее ?yi. Иногда возможно синтаксическим образом создать выражение, которое кажется решением уравнения. Например, кажется, что ?y = (f y) имеет неподвижнуюточку (f (f (f ...))), которую мы можем получить, начав с выражения (f ?y) и систематически подставляя (f ?y) вместо ?y. К сожалению, не у всякого такого уравнения имеется осмысленная неподвижнаяточка. Вопросы, возникающие здесь, подобны вопросам работы с бесконечными последовательностями в математике.
Например, мы знаем, что решение уравнения y = 1 + y/2 равно 2. Если мы начнем с выражения1 + y/2 и будем подставлять 1 + y/2 вместо y, то получим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 + · · · .Несмотря на то, что формальные преобразования, ведущие к этим двум уравнениям, одинаковы, первый результат является верным утверждением о бесконечных последовательностях, а второй нет. Подобным образоми при работе с унификациями работа с произвольными синтаксически правильными выражениями может привести к ошибкам.4.4.
Логическое программирование439(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-matchvar (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)(cond ((var? e)(if (equal? var e)true(let ((b (binding-in-frame e frame)))(if b(tree-walk (binding-value b))false))))((pair? e)(or (tree-walk (car e))(tree-walk (cdr e))))(else false)))(tree-walk exp))4.4.4.5.
Ведение базы данныхОдна из важных задач при разработке логических языков программирования — такорганизовать работу, чтобы при проверке каждого образца просматривалось как можноменьше ненужных записей из базы. В нашей системе, помимо того, что мы храним всеутверждения в одном большом потоке, мы в отдельных потоках храним утверждения,carы которых являются константными символами, в таблице, индексируемой по этимсимволам. Чтобы получить утверждения, которые могут сопоставляться с образцом, мысначала смотрим, не является ли car образца константным символом. Если это так,то мы возвращаем (сопоставителю для проверки) все хранимые утверждения с тем же440Глава 4. Метаязыковая абстракцияcar. Если car образца не является константным символом, мы возвращаем все хранимые утверждения. Более изысканные методы могли бы использовать еще информациюиз кадра, либо пытаться оптимизировать и тот случай, когда car образца не являетсяконстантным символом.
Мы избегаем встраивания критериев для индексации (использование car, обработка только случая с константными символами) в программу: вместоэтого мы вызываем предикаты и селекторы, реализующие эти критерии.(define THE-ASSERTIONS the-empty-stream)(define (fetch-assertions pattern frame)(if (use-index? pattern)(get-indexed-assertions pattern)(get-all-assertions)))(define (get-all-assertions) THE-ASSERTIONS)(define (get-indexed-assertions pattern)(get-stream (index-key-of pattern) ’assertion-stream))Процедура get-stream ищет поток в таблице и, если ничего там не находит, возвращает пустой поток.(define (get-stream key1 key2)(let ((s (get key1 key2)))(if s s the-empty-stream)))Правила хранятся подобным же образом, с использованием car заключения правила.Однако в заключениях правил могут стоять произвольные образцы, и таким образом, ониотличаются от утверждений тем, что могут содержать переменные.
Образец, в car которого стоит константный символ, может сопоставляться не только с правилами, у которыхcar заключения содержит тот же символ, но и с правилами, где в начале заключениястоит переменная. Таким образом, при поиске правил, которые могут сопоставляться собразцом, у которого в начале константный символ, мы возвращаем как правила с этимсимволом в car заключения, так и правила с переменной в начале заключения.
Ради этого мы храним правила с переменными в начале заключения в отдельном потоке,который находится в таблице под индексом ?.(define THE-RULES the-empty-stream)(define (fetch-rules pattern frame)(if (use-index? pattern)(get-indexed-rules pattern)(get-all-rules)))(define (get-all-rules) THE-RULES)(define (get-indexed-rules pattern)(stream-append(get-stream (index-key-of pattern) ’rule-stream)(get-stream ’? ’rule-stream)))4.4. Логическое программирование441Процедура add-rule-or-assertion! вызывается из query-driver-loop, когдатребуется добавить к базе данных правило или утверждение.
Каждая запись сохраняетсяв индексе, если это требуется, а также в общем потоке правил либо утверждений базыданных.(define (add-rule-or-assertion! assertion)(if (rule? assertion)(add-rule! assertion)(add-assertion! assertion)))(define (add-assertion! assertion)(store-assertion-in-index assertion)(let ((old-assertions THE-ASSERTIONS))(set! THE-ASSERTIONS(cons-stream assertion old-assertions))’ok))(define (add-rule! rule)(store-rule-in-index rule)(let ((old-rules THE-RULES))(set! THE-RULES (cons-stream rule old-rules))’ok))Чтобы вставить в базу утверждение или правило, мы проверяем, можно ли его проиндексировать. Если да, то мы сохраняем его в соответствующем потоке.(define (store-assertion-in-index assertion)(if (indexable? assertion)(let ((key (index-key-of assertion)))(let ((current-assertion-stream(get-stream key ’assertion-stream)))(put key’assertion-stream(cons-stream assertioncurrent-assertion-stream))))))(define (store-rule-in-index rule)(let ((pattern (conclusion rule)))(if (indexable? pattern)(let ((key (index-key-of pattern)))(let ((current-rule-stream(get-stream key ’rule-stream)))(put key’rule-stream(cons-stream rulecurrent-rule-stream)))))))Следующие процедуры определяют, как используется индекс базы данных.
Образец(утверждение или заключение правила) сохраняется в таблице, если он начинается спеременной или константного символа.442Глава 4. Метаязыковая абстракция(define (indexable? pat)(or (constant-symbol? (car pat))(var? (car pat))))Ключ, под которым образец сохраняется в таблице — это либо ? (если он начинается спеременной), либо константный символ из его начала.(define (index-key-of pat)(let ((key (car pat)))(if (var? key) ’? key)))Для поиска записей, которые могут соответствовать образцу, используется индекс в томслучае, когда образец начинается с константного символа.(define (use-index? pat)(constant-symbol? (car pat)))Упражнение 4.70.Какова цель выражений let в процедурах add-assertion! и add-rule!? Что неправильно вследующем варианте add-assertion!? Подсказка: вспомните определение бесконечного потокаединиц из раздела 3.5.2: (define ones (cons-stream 1 ones)).(define (add-assertion! assertion)(store-assertion-in-index assertion)(set! THE-ASSERTIONS(cons-stream assertion THE-ASSERTIONS))’ok)4.4.4.6.