4.4.4 · Операционные ограничения логического программирования

Пределы логического программирования и замкнутый мир

Математические на вид правила получают операционный поиск, поэтому недостающие факты, направление правил и границы завершения меняют вывод запроса.

Вопрос для размышления

Какие выводы следуют из логического отношения, а какие определяются конкретной базой данных и процедурой поиска?

Различение логического отрицания и отрицания как неудачи
Формулирование предположения о замкнутом мире, необходимого для вывода при отсутствии фактов
Разделение декларативного значения отношения и процедуры его поиска
Наблюдение за тем, как симметричное правило доказывает один запрос и зацикливается на другом
Использование видимой границы работы вместо выдачи незавершающегося поиска за ответ

Первая программа намеренно определяет not-known-role? как неудачу при поиске факта роли. Она возвращает true для ada, cy и zoe. ada и cy являются известными людьми, для которых роль manager отсутствует, тогда как zoe отсутствует в отношении known-person. Граница базы данных с замкнутым миром превращает каждый неудачный поиск в логическое отрицание.

Вторая программа задает для married симметричное операционное правило: если прямой факт отсутствует, поменять аргументы местами и выполнить поиск снова. Это доказывает (married mickey minnie) после одной перестановки, поскольку существует обратный факт. То же самое правило бесконечно чередуется для несвязанной пары, если только вычислитель не обнаружит повторение или не исчерпает видимый бюджет работы. Логическое утверждение может быть симметричным, но направление и управление правила все равно определяют поведение этого исполняемого поиска.

Код SICP971 из 1,048,576 байт UTF-8

(begin
  (define facts
    '((known-person ada)
      (known-person ben)
      (known-person cy)
      (role ada programmer)
      (role ben manager)))
  (define (fact? candidate remaining)
    (cond ((null? remaining) #f)
          ((equal? candidate (car remaining)) #t)
          (else (fact? candidate (cdr remaining)))))
  (define (known-person? person)
    (fact? (list 'known-person person) facts))
  (define (known-role? person role)
    (fact? (list 'role person role) facts))
  (define (not-known-role? person role)
    (not (known-role? person role)))
  (define (role-status person role)
    (cond ((known-role? person role) 'proved)
          ((known-person? person) 'not-proved-for-known-person)
          (else 'unknown-person)))
  (list (not-known-role? 'ada 'manager)
        (not-known-role? 'cy 'manager)
        (not-known-role? 'zoe 'manager)
        (role-status 'ada 'manager)
        (role-status 'cy 'manager)
        (role-status 'zoe 'manager)))

Примеры

Результат—

Вывод: —
Значение: —
Диагностика: —

Трасса выполнения0 / 0 событий

Ожидаемый результат

Первая программа возвращает (#t #t #t not-proved-for-known-person not-proved-for-known-person unknown-person). Вторая программа возвращает ((proved ((mickey minnie) (minnie mickey)) 3) (truncated ((donald daisy) (daisy donald) (donald daisy) (daisy donald) (donald daisy)) 0)).

На что обратить внимание в трассе

В первом запуске сравните три одинаковых булевых значения неудачи поиска роли с отдельными проверками known-person, сохраняющими различные эпистемические состояния. Во втором запуске проследите за каждой перестановкой аргументов, просмотром прямых фактов, расширением пути и уменьшением бюджета. Один запрос достигает факта после одной перестановки, а другой повторяет те же две пары, пока явная граница не сообщит об усечении.

Попробуйте сами

Измените программу и сравните результат.

Добавьте (known-person zoe) без добавления роли, затем добавьте (married daisy donald). Предскажите, какой статус изменится в первом запуске и какой симметричный запрос теперь завершится во втором.

Показать подсказку

Добавление факта known-person переводит zoe из неизвестного человека в известного человека без записанной роли. Добавление прямого факта married дает обратному запросу путь вывода в одну перестановку.

Завершить этот урок

В этой главе пройдено 0 из 23 урока0%