3.2 Negazione intensionale

La tecnica della negazione intensionale (NI) [BaMPT90,Man88] si prefigge lo scopo di superare i limiti computazionali della negazione come fallimento finito. Abbiamo visto infatti che la n.a.f. può essere usata solo come test e non può calcolare sostituzioni di risposta a goal negativi. L'obbiettivo principale della NI è quindi quello di ottenere una rappresentazione simmetrica della conoscenza positiva e negativa presente in un programma logico attraverso una trasformazione che consenta di rappresentare direttamente in modo intensionale l'informazione negativa che un programma logico contiene implicitamente.

La negazione intensionale realizza la trasformazione del programma P definendo per ogni predicato $p$ un nuovo predicato $\sim p$, inteso come il complemento di $p$, che verrà utilizzato all'interno di interrogazioni laddove si vogliano calcolare valori per cui vale $\neg p$.

La chiamata al predicato $\sim p$ calcolerà l'insieme di fallimento finito di $p$, visto che in generale non si può ottenere una definizione che consenta di calcolare l'intero complemento di $p$, il quale in generale è un insieme non effettivo.

La manipolazione di programmi con variabili locali, cioè con variabili che compaiono in atomi del corpo ma non nella testa, comporta la generazione di teorie non di Horn. Ad esempio una clausola della forma $p(x) \leftarrow q(y)$ determina per $\sim p$ la definizione $\sim p(x) \leftarrow \forall y$ $\sim q(y)$ che richiede un trattamento adeguato mediante una nuova forma di risoluzione (risoluzione SLDN [BMPT90]).

Poiché per ottenere informazione negativa da un programma logico è necessario fare riferimento ad una teoria derivata dal programma logico stesso, per i nostri scopi illustreremo una teoria che è una estensione propria del completamento, nel senso che estende la teoria dell'uguaglianza con l'assioma del dominio chiuso (DCA).

L'assioma DCA, imponendo che il dominio di un modello di ( $P^{*},U^{*}_{DCA}$) sia formato da oggetti costruiti con l'interpretazione di costanti e funzioni nel linguaggio di P, consente di ottenere l'insieme dei termini che rappresentano il complemento di un termine non ristretto.

Un termine non ristretto è un termine nel quale non compaiono variabili ripetute.

Definizione 3.2 (Domain closure axiom)  

Data una segnatura $\Sigma$, DCA rispetto a $\Sigma$ è espresso da

$$\forall x (\bigvee_{c \in \Sigma} \exists z.x=c(z))$$

Esempio 3.3  

Considerando $\Sigma_{Nat}$ = $\{ 0,s(\_) \}$, l'assioma DCA si esprime come:

$$\forall x (x=0 \vee \exists z.x=s(z))$$

Si ha che l'insieme N dei numeri naturali è un modello per $U^{*}_{DCA}$, mentre l'insieme $N \cup \{ \star \}$ non può esserlo, perché $\star$ non è costruibile attraverso $0$ e $s$.

Definizione 3.3 (Negazione dei termini)  

L'operatore Not, dato un termine non ristretto $t \in \Sigma$, restituisce un insieme di termini, inteso come il complemento di $t$ rispetto a $U^{*}_{DCA}$.

$Not_{\Sigma}(x)$ = $\{$ $\}$, se x è una variabile;

$Not_{\Sigma}(c)$ = $\Sigma^{0} \setminus \{ c \}$ $\cup$ $\{ f(x) \mid f \in \Sigma^{n}, n > 0 \}$ se $c \in \Sigma^{0}$

$Not_{\Sigma}(f(s_{1}, \ldots ,s_{m})$ = $\Sigma^{0}$ $\cup$ $\{ g(x) \mid g\in \Sigma^{n}, n>0 , g \neq f \}$ $\cup$
$\{ f(x_{1}, \ldots , x_{k-1}, s, x_{k+1}, \ldots , x_{m}) \mid k= 1, \ldots ,m$ e $s \in Not_{\Sigma}(s_{k})$ se f $\in \Sigma^{m}$, $m> 0$.

L'ultima regola contiene implicitamente la definizione dell'estensione di $Not_{\Sigma}$ in grado di operare su ennuple di termini, ovvero

$Not_{\Sigma}(<t_{1}, \ldots ,t_{n}>)$ = $\{<x_{1}, \ldots , x_{k-1}, s, x_{k+1}, \ldots , x_{n} > \mid k= 1,\ldots ,m$ e $s \in Not_{\Sigma}(s_{k}) \}$.

Esempio 3.4  

Considerando la segnatura $\Sigma_{Nat}$, calcoliamo il complemento di $s(s(x))$:

$$Not(s(s(x))) = \{0 \} \cup \{ s(t) \mid t \in Not(s(x)) \}$$

Poiché

$$Not(s(x)) = \{0 \} \cup \{ s(t) \mid t \in Not(x) \}$$

e $Not(x)$ = $\{ \}$

si ha che

$$Not(s(s(x))) = \{0 \} \cup \{ s(0) \}$$

Fondamentale è l'ipotesi che i termini da complementare siano non ristretti, come è evidente dal seguente esempio:

Esempio 3.5  

Data la segnatura $\Sigma$ = $\{ a, b, f(x,y) \}$ si ha

$$Not(f(x,x)) = \{ a, b \}$$

mentre il complemento di f(x,x) è l'insieme $\{ a, b \} \cup \{f(x, y) \mid x \neq y \}$.

In generale non si può rappresentare il complemento di un termine ristretto mediante un insieme finito di termini.

Il seguente teorema [BMPT90] assicura la correttezza dell'operatore Not.

Teorema 3.4  

Sia $\bar{t}$ una tupla non ristretta di termini, $Not( \bar{t} ) = \{\bar{t_{1}}, \ldots,\bar{t_{1}} \}$, e $\bar{x}$ una tupla di variabili nuove. Allora

$$U^{*}_{DCA} \models \forall \bar{x} ( \forall . \bar{x} \neq ... ...arrow \bigvee_{1, \ldots ,m} \exists . \bar{x} = \bar{t_{i}} )$$

Per definire i predicati $\sim p$, si ricava l'informazione negativa dal completamento del programma, come esemplificato dal seguente

Esempio 3.6  

Sia P il programma su $\Sigma_{Nat}$

$p(0) \leftarrow$

$p(s(s(x))) \leftarrow p(x)$

che definisce i numeri naturali pari.

Il suo completamento è:

$\forall y (p(y) \leftrightarrow (y=0 \vee \exists x (y = s(s(x)), p(x)))$

consideriamo la negazione logica di entrambe le parti della definizione completata di p

$\forall y (\neg p(y) \leftrightarrow \neg (y=0 \wedge \exists x (y = s(s(x)), p(x)))$ che è equivalente a

$\forall y (\neg p(y) \leftrightarrow (y \neq 0 \wedge \neg \exists x (y = s(s(x)), p(x)))$ che è equivalente a

$\forall y (\neg p(y) \leftrightarrow (y \neq 0 \wedge \forall x (y \neq s(s(x)) \vee \neg p(x)))$ che è equivalente a

$\forall y (\neg p(y) \leftrightarrow (y \neq 0 \wedge \forall x (y \neq s(s(x)) \vee (y = s(s(x)), \neg p(x) )))$ che è equivalente a

$\forall y (\neg p(y) \leftrightarrow (y \neq 0 \wedge \forall x (y \neq s(s(x)) \vee \exists x (y = s(s(x)), \neg p(x) )))$

distribuendo rispetto a $\vee$

$\forall y (\neg p(y) \leftrightarrow (y \neq 0 \wedge \forall x (y \neq s(s(x))) \vee (y \neq 0 ), \exists x (y = s(s(x)), \neg p(x) )))$.

Poiché vale $U^{*}_{DCA}$, per il teorema 3.4 si ha che

$y \neq 0$ è equivalente a $\exists x (y = s(x))$, dal momento che $Neg(0) = s(x)$

$\forall x (y \neq s(s(x)))$ è equivalente a $y = 0$ $\vee$ $y = s(0)$

Quindi si ottiene

$\forall y (\neg p(y) \leftrightarrow (\exists x (y = s(x)), y = 0 \vee$

$(\exists x ( y = s(x) ) \vee y = s(0) \vee \exists z ( y = s(z) ), \exists x ( y = s(s(x)) ), \neg p(x)))$

Unificando la congiunzione di formule del tipo $\{x = t, x = \bar{t} \}$

si ottengono le seguenti formule

$\exists x (y = s(x)), y = 0 \rightarrow false$ perché $0$ e $s(x)$ non sono unificabili;

$\exists x ( y = s(x) ) \vee y = s(0) \rightarrow y = s(0)$;

$\exists z ( y = s(z) ), \exists x ( y = s(s(x)) ) \rightarrow \exists z (y = s(s(z)))$

Quindi possiamo interpretare $\neg p$ come un nuovo predicato $\sim p$ così definito:

$\sim p(s(0)) \leftarrow$

$\sim p(s(s(x))) \leftarrow \sim p(x)$

che come ci si aspettava definisce i numeri naturali dispari.

L'idea illustrata nell'esempio precedente può essere formalizzata definendo due operatori, NegC e @. Il primo opera su una singola clausola e ne esplicita i potenziali contributi alla negazione del predicato di testa $p$, il secondo mette insieme i contributi di ciascuna clausola per la definizione di $\sim p$.

I programmi logici considerati sono quelli left linear, definiti come i programmi che non contengono termini ristretti nelle teste delle clausole.

Definizione 3.4 (Operatore NegC)  

Sia C una clausola del tipo

$$p(t) \leftarrow p_{1}(t_{1}), \ldots ,p_{k}(t_{k} )$$

tale che t è non ristretto ed ogni eventuale variabile locale compare in al più un letterale del corpo. Allora NegC(C) è il seguente insieme di regole:

$$\begin {array}{ll} \par\sim p(s)\leftarrow & \mbox{per ogni }... ...box{ e } z_{i} = vars(t_{i}) \setminus vars(t) \par\end{array}$$

L'operatore binario di combinazione @ è il seguente:

Definizione 3.5  

Siano $R_{1}$ ed $R_{2}$ le regole

$$A_{1} \leftarrow B_{1}$$

$$A_{2} \leftarrow B_{2}$$

dove $B_{1}$ e $B_{2}$ sono congiunzioni (eventualmente vuote) di letterali universali. Allora $R_{1}$ @ $R_{2}$ è la regola

$$A_{1} \theta \leftarrow (B_{1}, B_{2}) \theta$$

se esiste $\theta = mgu(A_{1}, A_{2})$, altrimenti è la regola vuota.

Quindi la tecnica di negazione intensionale può essere definita per mezzo dell'operatore Neg che, dato un programma logico, costruisce le definizioni di un predicato $\sim p$ per ogni $p \in \Pi$

Definizione 3.6  

Sia P un programma logico sul linguaggio $L = < \Pi ,\Sigma >$ e sia CL(p) l'insieme delle clausole di P il cui predicato di testa è $p \in \Pi$. Allora

$$\begin{array}{ll} \par Neg(p) = \{ \sim p(x) \leftarrow \} & ... ...) = \{ C_{1}, \ldots, C_{n} \}, \\ \; & n > 0 \par\end{array}$$

Riferendoci al programma dell'esempio 3.6 abbiamo:

$$NegC( \; p(0) \leftarrow \; ) = \{ \sim p(s(x)) \leftarrow \}$$

$$NegC( \; p(s(s(x))) \leftarrow p(x) \; ) = \{ \sim p(0) \left... ...w, \sim p(s(0)) \leftarrow, \sim p(s(s(x))) \leftarrow p(x) \}$$

Poiché le uniche applicazioni di @ che hanno successo sono

$$( \sim p(s(x)) \leftarrow ) @ ( \sim p(s(0)) \leftarrow ) = ( \sim p(s(0)) \leftarrow ) \mbox{ e}$$

$$( \sim p(s(x)) \leftarrow ) @ ( \sim p(s(s(x))) \leftarrow \sim p(x) ) = ( \sim p(s(s(x))) \leftarrow \sim p(x) )$$

otteniamo per $\sim p$ le regole

$$\sim p(s(0)) \leftarrow$$

$$\sim p(s(s(x))) \leftarrow \sim p(x)$$

come nell'esempio 3.6.

Come già accennato in precedenza, per trattare i letterali quantificati universalmente viene introdotta una estensione della procedura di risoluzione SLD, detta SLDN.

Un goal del tipo $\forall \bar{y}$ $\sim q( \bar{x}, \bar{y} )$, dove $\bar{y}$ sono le variabili locali, viene computato in due passi:

1. Viene valutato il goal $\sim q( \bar{x}, \bar{y} )$ utilizzando le clausole per $\sim q$. Sia $\theta$ una sostituzione di risposta calcolata per questo goal.
2. Viene valutato il goal $q(\bar{x}, \bar{z}) \theta$ dove $\bar{z}$ è una tupla di variabili nuove che rimpiazza $\bar{y}$. Se questa valutazione fallisce finitamente allora $\theta$ è una sostituzione di risposta calcolata per $\forall \bar{y}$ $\sim q( \bar{x}, \bar{y} )$.

La correttezza e la completezza della SLDN sono state provate rispetto al completamento $( P^{*}, U^{*}_{DCA} )$, che costituisce la teoria di riferimento per la tecnica di trasformazione. Tali risultati si possono estendere al completamento standard $( P^{*}, U^{*} )$ grazie al seguente teorema:

Teorema 3.5  

Sia P un programma logico e $p(\bar{t})$ un atomo. Le seguenti affermazioni sono equivalenti:

• $( P^{*}, U^{*}_{DCA} ) \models \forall \neg p(\bar{t})$.

• $( P^{*}, U^{*} ) \models \forall \neg p(\bar{t})$.

• $p(\bar{t})$ ha solamente derivazioni SLD fair finitamente fallite.