Resolução da unificação de Prolog

Question

Por que isso funciona:

   power(_,0,1) :- !.
   power(X,Y,Z) :-
      Y1 is Y - 1,
      power(X,Y1,Z1),
      Z is X * Z1.

E isso dá uma exceção de estouro de pilha?

power(_,0,1) :- !.
power(X,Y,Z) :-
  power(X,Y - 1,Z1),
  Z is X * Z1.

Answer 1

Porque as operações aritméticas são realizadas apenas em cláusulas através do is operador. No seu primeiro exemplo, Y1 está vinculado ao resultado do cálculo de y - 1. No final, o sistema tenta provar o poder da cláusula (x, y - 1, z1), que unifica com o poder (x ', y', Z ') ligação x' = x, y '= y - 1, z' = z. Isso depois se opõe novamente, então y '' = y - 1 - 1, etc para o infinito, nunca realizando o cálculo.

O Prolog é principalmente apenas a unificação dos termos - o cálculo, no sentido "comum", deve ser solicitado explicitamente.

Answer 2

Ambas as definições não funcionam corretamente.

Considerar

?- pow(1, 1, 2).

quais loops para ambas as definições porque a segunda cláusula pode ser aplicada independentemente do segundo argumento. O corte na primeira cláusula não pode desfazer isso. A segunda cláusula precisa de uma meta Y > 0 antes do objetivo recursivo. Usando (is)/2 ainda é uma boa ideia obter soluções reais.

O melhor (para iniciantes) é começar com sucessor-aritmético ou clpfd e para evitar Prólogo completamente.

Veja por exemplo: PROLOD PROLOCE - LOOP Infinito