6.2.2.4 Sintesi di

Questo modulo ottiene il programma $P^{-}$ complemento di P semplicemente facendo l'unione di comp(P1) e comp(P2).

Esempio 6.7 Dato il programma P definito sulla segnatura $\Sigma$ dell'esempio 6.5, con i modi $d_{r} = '-'$ , $d_{q} = '+'$ , $d_{p} = '-'$ ,

$\begin{displaymath}r(s(0))\leftarrow\end{displaymath}$

$\begin{displaymath}r(s(s(0)))\leftarrow\end{displaymath}$

$\begin{displaymath}q(0)\leftarrow \end{displaymath}$

$\begin{displaymath}q(s(s(x)))\leftarrow q(x)\end{displaymath}$

$\begin{displaymath}p(x)\leftarrow r(x),q(x)\end{displaymath}$

l'analizzatore stabilirà che P1={r,p}, mentre P2={q}.

Infatti il criterio dovrà essere applicato alle queries $\leftarrow r(x)$ , $\leftarrow q(x)$ e $\leftarrow p(x)$ .

Nel caso di $\leftarrow r(x)$ , si avrà che, poiché le clausole la cui testa unifica con $r(x)$ sono tutte fatti e quindi terminanti, il predicato $r$ è inserito in P1. Le risposte ottenute sono $( \{x/s(0) \},true)$ e $\{x/s(s(0)) \},true)$ .

Successivamente si passa ad esaminare $\leftarrow q(x)$ : la clausola $q(0) \leftarrow$ è terminante, mentre per la clausola ricorsiva $q(s(s(x))) \leftarrow q(x)$ bisogna verificare le due condizioni sugli argomenti. In questo caso, fallisce subito la prima, cioè quella che impone che le norme dei termini non ground di input siano limitate: infatti $\mid s(s(x)) \mid = \infty$ perché $s$ è un costruttore riflessivo in $\Sigma$ .

Esaminando infine $p(x) \leftarrow$ , si ha che la clausola $p(x)\leftarrow r(x),q(x)$ è terminante perché la query $\leftarrow r(x), q(x)$ termina. Infatti $\leftarrow r(x)$ termina con risposte $( \{x/s(0) \}, true)$ e $\{x/s(s(0)) \}, true)$ e terminano le query ottenute da $\leftarrow q(x)$ applicandovi tali risposte. $\leftarrow q(s(0))$ termina perché non unifica con alcuna clausola, mentre $\leftarrow q(s(s(0)))$ termina perché la clausola con cui unifica è terminante, valendo sulle norme la condizione imposta dal criterio ( $\mid s(s(0)) \mid = 3$ $>$ $\mid 0 \mid = 1$ ).