Predicado Prólogo - bucle infinito

Question

Necesito crear un predicado Prolog para potencia de 2, con los números naturales. Los números naturales son: 0, s (0), s (s (0)) ans así sucesivamente ..

Por ejemplo:

?- pow2(s(0),P). 
P = s(s(0)); 
false. 
?- pow2(P,s(s(0))). 
P = s(0); 
false. 

Este es mi código:

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    pow2(N,Z), 
    times2(Z,Y). 

Y funciona perfectamente con el primer ejemplo, pero ingresa un bucle infinito en el segundo ..
¿Cómo puedo solucionar esto?

Answer 1

Esto sucede porque la orden de evaluación de pow2. Si cambia el orden de pow2, tendrá el primer ejemplo atorado en el bucle infinito. Para que pueda verificar primero si Y es var o nonvar.

así:

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), 
    pow2(N,Z). 

Answer 2

Aquí es una versión que termina para el primer o segundo argumento está obligado:

 
pow2(E,X) :- 
    pow2(E,X,X). 

pow2(0,s(0),s(_)). 
pow2(s(N),Y,s(B)) :- 
    pow2(N,Z,B), 
    add(Z,Z,Y). 

Puede determine its termination conditions CTI.

Entonces, ¿cómo se me ocurrió esa solución? La idea era encontrar una manera de cómo el segundo argumento podría determinar el tamaño del primer argumento. La idea clave es que para todo i ∈ N: 2 ⁱ > i.

Así que agregué un argumento adicional para expresar esta relación. Tal vez puedas fortalecerlo un poco más?

---

Y aquí está la razón por la cual el programa original no termina. Doy la razón como failure-slice. Ver etiqueta para más detalles y otros ejemplos.

 
?- pow2(P,s(s(0))), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- 
    pow2(N,Z), false, 
    times2(Z,Y). 

¡Este es el pequeño fragmento que constituye la fuente de la no terminación! ¡Mira Z que es una nueva variable! Para solucionar el problema, este fragmento debe modificarse de alguna manera.

---

Y aquí es la razón por @ solución del Guardián no pongan fin a pow2(s(0),s(N)).

 
?- pow2(s(0),s(N)), false. 

add(0,Z,Z) :- false. 
add(s(X),Y,s(Z)) :- 
    add(X,Y,Z), false. 

times2(X,Y) :- 
    add(X,X,Y), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- false, 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), false, 
    pow2(N,Z).