Purezza di predicati Prolog che utilizzano le primitive impuri

Question

so che var/1, nonvar/1 e !/0 sono primitivi impuri, ma non il loro uso rende ogni programma che utilizza impure?

Ho scritto il seguente predicato plus/3 che si comporta come se fosse puro o almeno è quello che pretendo. Il predicato è dimostrativo, non progettato per essere efficiente.

% nat(X) is true if X is a natural number 

nat(0). 
nat(X):- nonvar(X), !, X > 0. 
nat(X):- nat(X1), X is X1 + 1. 

% plus(A, B, C) is true if A,B and C are natural numbers and A+B=C 

plus(A, B, C):- 
    nat(A), 
    (nonvar(C), C < A, !, false ; true), 
    plus_(B, A, C). 

plus_(A, B, C):- 
    nat(A), 
    (nonvar(C), C < A, !, false ; true), 
    C1 is A + B, 
    (C = C1 ; nonvar(C), C < C1, !, false). 

Ho due domande:

1. E 'possibile che questo predicato plus/3 davvero pura?
2. In generale, come si può dimostrare che una particolare relazione ha una purezza logica?

---

Questa domanda segue la discussione su questo answer.

Answer 1

1. È il predicato sopra più/3 veramente puro?

Ha un po 'strano comportamento: A volte accetta espressioni aritmetiche, e qualche volta no; e questo anche se tutti gli argomenti vengono valutati:

?- plus(3,5-3,5). 
true ... 

?- plus(3,2,3+2). 
false. 

?- plus(3,2,3+b). 
ERROR: </2: Arithmetic: `b/0' is not a function 

?- plus(3,2,3+Z). 
ERROR: </2: Arguments are not sufficiently instantiated 

avrei preferito essere preoccupato per l'inefficienza del nat/1 per casi come:

?- time((nat(X), X > 9999)). 
% 50,025,002 inferences, 27.004 CPU in 27.107 seconds (100% CPU, 1852480 Lips) 
X = 10000 ; 
% 10,006 inferences, 0.015 CPU in 0.015 seconds (99% CPU, 650837 Lips) 
X = 10001 ; 
% 10,005 inferences, 0.016 CPU in 0.016 seconds (99% CPU, 631190 Lips) 
X = 10002 ... 

Quindi, mi sembra che la definizione è puro. Tuttavia, questo stile di programmazione rende abbastanza difficile garantire questa proprietà. Un minimo cambiamento avrà effetti disastrosi.

2. In generale, come si può dimostrare che un particolare relazione ha la purezza logica?

Il modo più semplice è la costruzione. Cioè, usando solo blocchi di costruzione monotonici puri. I.e. Prolog senza alcun built-in e usando solo congiunzione e disgiunzione di obiettivi regolari. Qualsiasi programma costruito in questo modo sarà pure e monotono. Quindi, eseguire questo programma con il flag Prolog si verifica come impostato su true o error.

Aggiungi a questo pure built-in come (=)/2 e dif/2.

Aggiungi a questo built-in che tenta di emulare relazioni pure e che producono errori di istanziazione quando non sono in grado di farlo. Pensa a (is)/2 e ai predicati di confronto aritmetico. Alcuni di questi sono abbastanza al limite come call/N che potrebbe chiamare alcuni predicati impuri.

Aggiungi library(clpfd) con flag clpfd_monotonic impostato su true.

Molti costrutti sono puri e puri per determinati usi, ma impuri per gli altri. Pensare if-then-else che è perfetto per il confronto aritmetica:

..., (X > Y -> ... ; ...), ... 

ma che non funziona insieme con un obiettivo puro come

..., (X = Y -> ... ; ...), ... % impure 

Ciò che resta sono impuri built-in che può essere utilizzato costruire predicati che si comportano in modo puro; ma la cui definizione in quanto tale non è più pura.

Ad esempio, prendere in considerazione tagli veramente verdi. Questi sono estremamente rari e ancora più rari qui su SO. Vedi this e that.

Un altro modello comune per fornire un rapporto puro sono condizionali come:

..., (var(V) -> something with var ; the equivalent with nonvar), ... 

e per evitare i casi che non sono coperti in modo pulito, gli errori possono essere gettati.

Answer 2

Per quanto riguarda la domanda "il precedente è plus/3 veramente puro?" Posso solo dire: non ho idea di quali proprietà siano preservate qui, perché il codice, a causa di tutti questi predicati extra logici, è così complicato e difficile da seguire che è difficile dire cosa stia effettivamente facendo. E devo davvero dire facendo in questo caso, perché questo è lontano dal codice dichiarativo che è che descrive qualcosa di cui possiamo facilmente parlare relativamente. In questo caso, tutti i tipi di proprietà che ci aspettiamo dal codice dichiarativo potrebbero essere distrutti.

Il modo migliore per dimostrare in generale che una relazione è puro è quello di limitare se stessi al pura e monotona sottoinsieme di Prolog. È per questo motivo che questa proprietà è così importante, perché questo sottoinsieme è chiuso in composizione. Una volta lasciato questo sottoinsieme, diventa molto difficile dimostrare qualsiasi proprietà sui tuoi programmi, come dimostra chiaramente il tuo esempio.

Ad esempio, per dimostrare il vostro plus/3 monotona, è necessario mostrare, tra molte altre cose, che se ?- plus(X, _, _), X = Tfallisce per qualsiasi termine T, quindi ?- X = T, plus(X, _, _) fa non riescono. Dato che in generale non è decidibile se una query fallisce, loops o riesce e quindi in generale non possiamo nemmeno determinare un singolo lato di questa implicazione, figuriamoci entrambi, posso solo dire: Buona fortuna!