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

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

Предположим, что я определяю две основные операции над натуральными числами:

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

  • Добавить (термин, еще один термин).

Семантика add задается через

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

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

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

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

Add (x, add (y, z)) = s (0)

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

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

  • Если нет, посмотрите, можно ли найти решение, ища наиболее общий объединитель

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

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

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

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

3 4
algorithm axiom prolog

3 ответа:

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

1

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

Предикат - это набор предложений.

Предложение имеет вид 

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.

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

Теперь, чтобы решить, является ли 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.
Термин-это, по существу, любой фрагмент синтаксиса.

Ключевая вещь, которую нужно заметить здесь, это этот пролог не имеет никаких функций! Если в функциональном языке вы можете определить функцию add(X, Y), которая вычисляется как сумма X и Y, то в прологе вы определяете предикат, головкой которого является 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))).

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

Надеюсь, что это помогает.

5

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

1