Разрешение аксиомы

StackOverflow https://stackoverflow.com/questions/4318930

Вопрос

Я стараюсь понять, как работает разрешение аксиомы в Prolog.

Давайте предположим, что я определяю две основные операции на естественных числах:

  • S (термин) (обозначает преемник) и

  • Добавить (термин, другой срок).

Семантика добавления дается

  • Добавить (0, x1) -> x1

  • Добавить (x1, 0) -> x1

  • добавить (s (x1), y1) -> s (добавить (x1, y1)))

Тогда я хотел бы решить уравнение

Добавить (x, add (y, z)) = s (0)

Я полагаю, что одна стратегия может быть

  • Проверьте, является ли правая сторона (RHS) уравнения равна левой стороне (LHS)

  • Если не посмотрите, можно ли найти решение, поиск наиболее общего Unifier

  • Если нет, то попробуйте найти аксиому, которая может быть использована в этом уравнении. Стратегия выполнения этой работы может состоять в том, чтобы (для каждой аксиомы): попытаться решить RHS уравнения, равного RHS аксиомы. Если есть решение, попытайтесь решить LHS уравнения, равное LHS аксиомы. Если это удастся, то мы нашли правильную аксиому.

  • В конце концов, если нет решения, а LHS и RHS уравнения являются одинаковой операцией (то есть той же подписью, но не одинаковыми операндами), примените алгоритм на каждый операнд, и решение обнаруживается, если решение обнаруживается для каждого операнда.

Я думаю, что этот (простой) алгоритм может работать. Тем не менее, я хотел бы знать, есть ли у кого -то опыт решения этой проблемы? Кто -нибудь знает, где я могу найти какую -то документацию о лучшем алгоритме?

заранее спасибо

Это было полезно?

Решение

То, что вы ищете, называется сужение. Отказ Он реализован на некоторых функциональных языках, таких как Карри, но не в самой Прологе.

Другие советы

Программа Prolog - это набор предикатов.

Предикат - это коллекция пунктов.

В пункте есть форма

Head :- Body.

значение "Head это правда, если Body правда".

Есть форма сокращения

Head.

что означает то же самое, что

Head :- true.

куда true это встроенный, который всегда правда.

Возвращаясь к Body часть пункта, Body является целью, которая может принимать одну из следующих форм (A, B, и C обозначают произвольные цели):

Atom            % This is true if Atom is true (see below).
A, B            % This is true if A is true and B is true.
(A ; B)         % This is true if A is true or B is true.
\+ A            % This is true if A is not true.
(A -> B ; C)    % If A is true then B must be true, else C must be true.

В Prolog есть некоторые специальные правила, касающиеся порядка оценки (слева направо) и «разрезания» (которые обрезают дерево поиска), но это мелкие детали, которая выходит за рамки этого краткого урока.

Теперь, чтобы решить, есть ли Atom правда, Atom может быть одной из следующих форм (X и Y обозначают произвольные термины):

true                % or some other builtin with given truth rules.
X = Y               % True if X and Y are successfully unified.
p(X, Y, ...)        % True if p(X, Y, ...) matches the head of some clause
                    % and the Body is true.

Термин, по сути, любой кусок синтаксиса.

Ключевым моментом здесь является то, что у Prolog нет функций! Где на функциональном языке вы можете определить функцию add(X, Y) который оценивается на сумму X и Y, в Prolog, вы определяете предикат, голова которого add(X, Y, Z) Что, если это удастся, объединяет Z с термином, обозначающим сумму X и Y.

Учитывая все это, мы можем определить ваши правила в Прологе следующим образом:

add(0, Y, Y).                        % 0 + Y = Y.
add(Y, 0, Y).                        % Y + 0 = Y.
add(s(X), Y, s(Z)) :- add(X, Y, Z).  % s(X) + Y = s(X + Y).

где я использую 0 Обозначать ноль (!) И s(X) обозначать преемника X.

Рассмотрим оценку add(s(s(0)), s(0), Z):

add(s(s(0)), s(0), Z)                 % Only the third head for add matches, so...
---> Z = s(Z0), add(s(0), s(0), Z0).

add(s(0), s(0), Z0)                   % Only the third head for add matches, so...
---> Z0 = s(Z1), add(0, s(0), Z1).

add(0, s(0), Z1)                      % Only the first head for add matches, so...
---> Z1 = s(0).

Поместить все эти объединения для Z Вместе у нас есть Z = s(s(s(0))).

Теперь вы можете спросить: «Что произойдет, если более одной головы совпадает в пункте» или «что произойдет, если путь оценки не удастся?» Пролог учебник!

Надеюсь это поможет.

«Представление и рассуждение знаний» Брэхмана и Левеска дает довольно хорошее представление о том, как эти вещи работают.

Лицензировано под: CC-BY-SA с атрибуция
Не связан с StackOverflow
scroll top