Я хочу доказать некоторую теорему, используя Пролог, однако она всегда возвращает «Out of global stack» - PullRequest
Новая
       18

Я хочу доказать некоторую теорему, используя Пролог, однако она всегда возвращает «Out of global stack»

2 голосов
/ 04 апреля 2019

Я делаю домашнее задание ИИ по доказательству теории групп в алгебре.

Теорема может быть представлена ​​следующим образом: 

A1. i(e,X) = X                   (identity)
A2. i(X, e) = X                  (identity)
A3. i(comp(X),X) = e             (complement)
A4. i(X, comp(X)) = e            (complement)
A5. i(X, i(Y,Z)) = i(i(X,Y),Z)   (associativity)

THEOREM: If G is a group such that for every X,
A6. i(X,X) = e,
then G is commutative, i.e., for every X; Y ,
i(X,Y) = i(Y,X):

and the commutative part can be represented as 
A7. i(a, b, c)                          clause derived from negated conclusion
A8. -i(b, a, c)                         clause derived from negated conclusion

И я преобразовал их в формат Пролога следующим образом: 

% A7
i(a, b, c).
% A1
i(e, X, X) .
%A2
i(X, e, X).
% A3
i(comp(X), X, e).
% A4
i(X, comp(X), e).
% A51
i(U, Z, W) :- i(X, Y, U), i(Y, Z, V), i(X, V, W).
% A52
i(X, V, W) :- i(X, Y, U), i(Y, Z, V), i(U, Z, W).
% A6
i(X, X, e).

Затем я хотел доказать теорему, поэтому я набрал «i (b, a, c)» в консоли Prolog и получил следующее сообщение об ошибке: 

?- i(b,a,c).
ERROR: Out of global-stack.
ERROR: No room for exception term.  Aborting.
ERROR: Out of global-stack.
ERROR: No room for exception term.  Aborting.
ERROR: Out of global-stack.
ERROR: No room for exception term.  Aborting.
% Execution Aborted

Пожалуйста, помогите мне, большое спасибо!

1 Ответ

2 голосов
/ 04 апреля 2019

Предложения A51 и A52 рекурсивны влево , что приводит к ошибкам вне стека.Каноническим решением для работы с левой рекурсией в Прологе является использование системы, поддерживающей табулирование (например, XSB, YAP, SWI-Prolog, B-Prolog или Ciao).Но есть еще одна проблема в вашем коде.Предложения A3 и A4 могут привести к созданию циклических терминов.Например, загружая только предложение A3: 

?- i(X, X, Y), cyclic_term(X).
X = comp(X),
Y = e.

Если вы закомментируете предложения A3 и A4 и добавите в начало своего исходного файла директиву: 

:- table(i/3).

Вы получите: 

?- i(b,a,c).
true.
...