27 Ottobre 2000
Dato il seguente programma Prolog:
conv(0,0):- !.
conv(N,s(L)) :- not (N=0),
Q is N-1,
conv(Q,L).
conv(N,s(L)) :- conv(Q,L),
N is Q+1.
si mostri l’albero di derivazione SLDNF relativo alla query:
:- conv(1,M), conv(R,s(M)).
not (R=0); R non ancora istanziata, perché il risultato dell’uguaglianza è vero?
Nell'albero in tutti i casi in cui compare uno di questi gol, la negazione per fallimento prova a vedere se R=0, unifica con successo R a 0 (l'= in questo caso e' l'unificazione di fatto) e quindi poi il not fallisce.
