predicato Prolog - loop infinito

Question

Ho bisogno di creare un predicato Prolog per la potenza di 2, con i numeri naturali. numeri naturali sono: 0, s (0), s (s (0)) ans così via ..

Ad esempio:

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

Questo è il mio codice:

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

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

E funziona perfettamente con il primo esempio, ma entra in un ciclo infinito nel secondo ..
Come posso risolvere questo?

Answer 1

Questo accade perché l'ordine di valutazione di pow2. Se si cambia l'ordine di pow2, si avrà il primo esempio bloccato nel ciclo infinito .. Quindi è possibile controllare prima se Y è un var o nonvar.

Come così:

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

Ecco una versione che termina per il primo o secondo argomento essere vincolato:

 
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). 

Puoi determine its termination conditions con CTI.

Quindi, come sono arrivato a questa soluzione? L'idea era di trovare un modo in cui il secondo argomento poteva determinare la dimensione del primo argomento. L'idea chiave è che per tutti i ∈ N: 2 ⁱ > i.

Quindi ho aggiunto un ulteriore argomento per esprimere questa relazione. Forse puoi rafforzarlo un po 'oltre?

---

Ed ecco il motivo per cui il programma originale non termina. Fornisco il motivo come failure-slice. Vedi tag per maggiori dettagli e altri esempi.

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

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

È questo piccolo frammento che è la fonte per la non-terminazione! Guarda Z che è una nuova nuova variabile! Per risolvere il problema, questo frammento deve essere modificato in qualche modo.

---

E qui è il motivo per cui la soluzione di @ Keeper non pone fine per 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).