Как реализовать возведение чисел Пеано в Пролог? - PullRequest
Новая
       26

Как реализовать возведение чисел Пеано в Пролог?

0 голосов
/ 25 сентября 2018

Я пытаюсь реализовать возведение в степень с помощью приведенного ниже кода, но простой запрос, такой как 2 ^ 1 (ex(s(s(0)), s(0), Z).), зависает навсегда. 

nat(0).
nat(s(X)) :- nat(X).
su(0, X, X) :- nat(X).
su(s(X), Y, s(Z)) :- su(X, Y, Z).

mu(0, _, 0).
mu(s(X), Y, Z) :- su(Y, A, Z), mu(X, Y, A).

ex(_, 0, s(0)).
ex(X, s(Y), Z) :- mu(X, A, Z), ex(X, Y, A).

1 Ответ

0 голосов
/ 26 сентября 2018

Насколько я вижу, это неэффективно, потому что mu/3 вызывается с двумя свободными переменными.Действительно: 

ex(X, s(Y), <b>Z</b>) :- mu(X, <b>A</b>, <b>Z</b>), ex(X, Y, A).

И A, и Z в данный момент неизвестны (я выделил их жирным шрифтом).

Теперь ваш mu/2не в состоянии справиться с этим должным образом.Если мы запросим mu/3 с помощью mu(s(0), A, Z), мы получим: 

?- mu(s(0), A, Z).
A = Z, Z = 0 ;
ERROR: Out of global stack

Таким образом, он застрял в бесконечной рекурсии.

Это связано с тем, что он будет приниматьвторое предложение mu/3 и: 

mu(s(X), <b>Y</b>, <b>Z</b>) :- su(<b>Y</b>, <b>A</b>, <b>Z</b>), mu(X, Y, A).

Итак, su/3 вызывается с тремя неизвестными переменными.В результате этого su/3 может продолжать предлагать значения «до конца времен»: 

?- su(A, B, C).
A = B, B = C, C = 0 ;
A = 0,
B = C, C = s(0) ;
A = 0,
B = C, C = s(s(0)) ;
A = 0,
...

, даже если рекурсивный mu(X, Y, A) отклоняет все эти предложения, su/3 никогда не прекратит предлагать новыеРешения.

Поэтому, возможно, было бы лучше иметь это в виду, когда мы проектируем предикаты для mu/3 и ex/3.

Мы можем, например, использовать аккумулятор здесь, который накапливает значения и возвращает конечный продукт.Преимущество этого в том, что мы работаем с реальными значениями, когда выполняем вызов su/3, например: 

mu(A, B, C) :-
    mu(A, B, 0, C).

mu(0, _, 0, S, S).
mu(s(X), Y, I, Z) :-
    su(Y, I, J),
    mu(X, Y, J, Z).

Теперь, если мы введем mu/3 только с фиксированным первым параметром, мы увидим: 

?- mu(s(0), X, Y).
X = Y, Y = 0 ;
X = Y, Y = s(0) ;
X = Y, Y = s(s(0)) ;
X = Y, Y = s(s(s(0))) ;
...
?- mu(s(s(0)), X, Y).
X = Y, Y = 0 ;
X = s(0),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(s(0)))) ;
X = s(s(s(0))),
Y = s(s(s(s(s(s(0)))))) ;
...
...

Таким образом, это означает, что мы по крайней мере теперь не застряли в цикле для mu/3 с фиксированным только первым параметром.

Мы можем использовать ту же стратегию для определения ex/3 предикат: 

ex(X, Y, Z) :-
    ex(X, Y, s(0), Z).

ex(X, 0, Z, Z).
ex(X, s(Y), I, Z) :-
    mu(X, I, J),
    ex(X, Y, J, Z).

Затем нам удается вычислить показатели, такие как 2 1 и 2 2 :

?- ex(s(s(0)), s(0), Z).
Z = s(s(0)) ;
false.
?- ex(s(s(0)), s(s(0)), Z).
Z = s(s(s(s(0)))) ;
false.

Обратите внимание, что в вышеприведенном есть некоторые недостатки, например, при расчете, для которого значение равно 4, все равно будет цикл: 

?- ex(X, Y, s(s(s(s(0))))).
ERROR: Out of global stack

Переписав предикаты, мы можемтакже избегайте этого.Но я оставляю это как упражнение.

...