6.2.2.1 Analizzatore

L'analizzatore partizionerà l'insieme dei predicati del programma in base a condizioni sufficienti per la terminazione. Infatti, a causa della nota indecidibilità dell' halting problem, le tecniche effettive di decisione sulla terminazione dei programmi possono verificare solamente criteri sufficienti ma non necessari.

È auspicabile, per l'efficienza del metodo di negazione, che le tecnica usata identifichi una classe di programmi terminanti che approssimi il meglio possibile la classe dei programmi che effettivamente terminano.

Qui di seguito esporremo un criterio che verifica condizioni sufficienti per la terminazione di programmi normali stratificati nvi, left linear, i cui predicati non siano mutuamente ricorsivi (tale ultima ipotesi non è affatto restrittiva perchè con tecniche di unfolding ogni programma mutuamente ricorsivo può essere trasformato in un altro equivalente non mutuamente ricorsivo).

Definizione 6.4   Dato l'atomo $p(t_{1}, \ldots, t_{n})$, definiamo $ground\_args(p(t_{1}, \ldots, t_{n}))$ = { $t_{i} \mid t_{i}$ è ground }. Inoltre, definiamo $nonground\_args(p(t_{1}, \ldots, t_{n}))$ = $\{t_{1}, \ldots, t_{n} \} \setminus {\em ground\_args(p(t_{1}, \ldots, t_{n}))}$

Definizione 6.5  

Dato un atomo $p(t_{1}, \ldots, t_{n})$ e un modo $d_{p}$, definiamo $nonground\_input(p(t_{1}, \ldots, t_{n}))$ = { $t_{i} \mid t_{i} \in nonground\_args(p(t_{1}, \ldots, t_{n})) \wedge d_{p}(i) = '+'$}.

Il criterio stabilisce se una query del tipo $\leftarrow p(\bar{t})$ termina rispetto ad un modo $d_{p}$. Per i nostri scopi, sarà necessario applicarlo a ogni query del tipo $\leftarrow p(\bar{x})$, $\forall d_{p}$, $\forall p \in \Pi$. In questo modo si otterrà la partizione di $\Pi$ desiderata, in base alle proprietà di terminazione dei predicati in $\Pi$ per goal totalmente non ground.

Il criterio testa la terminazione di una particolare query e non di un generico predicato essenzialmente per utilizzare le informazioni che si ottengono durante l'applicazione del criterio stesso.

Infatti, poiché la verifica di terminazione di una query richiederà in generale (cioè quando non si ha a che fare con clausole unitarie) l'applicazione ricorsiva del criterio, tale applicazione potrà essere più mirata nel senso di utilizzare le informazioni sugli argomenti della query, che saranno contenute nella sostituzione $\theta$ iniziale.

Esempio 6.4  

Dato il programma

$$p(x) \leftarrow r(x), q(x)$$

$$r(1) \leftarrow$$

$$q(x) \leftarrow \ldots$$

l'applicazione del criterio alla query $\leftarrow p(x)$ renderà sufficiente, una volta stabilito che la query $\leftarrow r(x)$ termina per x=1, verificare la terminazione della query $\leftarrow q(1)$.

Il criterio consiste essenzialmente in una applicazione accorta della risoluzione SLDCNF, nel senso che si procede al passo successivo di risoluzione solo quando sono verificate condizioni sufficienti alla terminazione. In effetti i casi critici sono quelli di clausole ricorsive: in tal caso deve essere verificata una particolare condizione sulle norme degli argomenti del predicato che ricorre.

Definizione 6.6   Criterio

Una query del tipo $\leftarrow p(\bar{t})\theta$ termina, rispetto al modo $d_{p}$, con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{k}, v_{k})$, dove $\sigma_{i}$ è una sostituzione e $v_{i}$ è un insieme di vincoli (diseguaglianze soddisfacibili o primitive), nel caso in cui:

• $p(\bar{t})\theta$ sia un letterale positivo, se ogni clausola la cui testa unifica con $p(\bar{t})\theta$ è terminante con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{k}, v_{k})$.

• $p(\bar{t})\theta$ sia un letterale negativo della forma $\neg Q$, se la query $\leftarrow Q$ termina, rispetto a $d_{p}$, con risposte $A_{1}, \ldots , A_{h}$ e $v_{1}, \ldots ,v_{k}$ sono la negazione di $A_{1}, \ldots , A_{h}$ e $\sigma_{1}, \ldots , \sigma_{k}$ sono uguali a $\theta$.

• $p(\bar{t})\theta$ sia una uguaglianza del tipo $r=s$, se $\exists \bar{\theta} = mgu(r,s)$ e $\sigma_{1} = \theta \circ \bar{\theta}$ e $v_{1} = true$ (k=1).

• $p(\bar{t})\theta$ sia una disuguaglianza, se è valida, con risposta $\sigma_{1} = \theta$ e $v_{1} = true$, altrimenti se è insoddisfacibile, senza risposta (k=0).

Una query del tipo $\leftarrow (p_{1}(\bar{t}_{1}), \ldots, p_{n}(\bar{t}_{n})) \theta$ termina senza risposta se $(p_{1}(\bar{t}_{1})) \theta$ è una diseguaglianza insoddisfacibile, altrimenti termina con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{k}, v_{k})$ se $\leftarrow (p_{1}(\bar{t}_{1})) \theta$ termina con risposta $(\sigma_{11}, v_{11}), \ldots , (\sigma_{1k_{1}}, v_{1k_{1}})$ e $\leftarrow v_{1j}(p_{2}(\bar{t}_{2}), \ldots, p_{n}(\bar{t}_{n})) \theta \circ \sigma_{1j}$, $1 \leq j \leq k_{1}$, terminano con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{k}, v_{k})$.

Una clausola che unifica con $p(\bar{t}) \theta$ se è della forma :

• $p(\bar{s}) \leftarrow$, è terminante con risposta $(\theta \circ \sigma, true)$, dove $\sigma = \{\bar{s} /(\bar{t})\theta \}$.

• $p(\bar{s}) \leftarrow p_{1}(\bar{s}_{1}), \ldots ,p_{n}(\bar{s}_{n})$ e $\forall i$ $p \neq p_{i}$ (cioè non è ricorsiva) è terminante con risposta $(\sigma_{1}, v_{1}), \ldots , (\sigma_{h}, v_{h})$ se la query $\leftarrow (p_{1}(\bar{s}_{1}), \ldots ,p_{n}(\bar{s}_{n})) \sigma$, dove $\sigma = \{\bar{s} \backslash (\bar{t})\theta \}$, termina con risposta $(\sigma_{1}, v_{1}), \ldots , (\sigma_{h}, v_{h})$, con i modi calcolati secondo il teorema 6.1.

• $p(\bar{s}) \leftarrow p_{1}(\bar{s}_{1}), \ldots ,p_{n}(\bar{s}_{n})$ è terminante con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{h}, v_{h})$ se, posto $i = min \{j \in [1,n] \mid p_{j} = p \}$ e i modi sono calcolati secondo il teorema 6.1, valgono le seguenti condizioni:
  • la query $\leftarrow (p_{1}(\bar{s}_{1}), \ldots ,p_{i-1}(\bar{s}_{i-1})) \sigma$, dove $\sigma = \{ \bar{s}/(\bar{t})\theta \}$ termina con risposte $(\gamma_{1}, v_{1}), \ldots, (\gamma_{l}, v_{l})$.

  • se $nonground_{input}(\leftarrow (p_{i}(s_{1i},\ldots,s_{n_{i}i}) )\gamma_{j})\neq \phi$, $1 \leq j \leq l$, allora le norme di tali termini devono essere limitate e $\forall k \in [1,\ldots ,n]$ $\mid~(s_{k})~\gamma_{j}~\mid~>~\mid~(s_{ki})\gamma_{j}~\mid$ altrimenti deve valere, $\forall k\in [1,\ldots ,n]$, $\mid~(s_{k})\gamma_{j}~\mid~>~\mid~(s_{ki})\gamma_{j}~\mid$. Siano $(\lambda_{1}, w_{1}), \ldots, (\lambda_{m}, w_{m})$ le risposte alle query $\leftarrow (v_{j}, p_{i} (s_{1i}, \ldots, s_{n_{i},i}) \gamma_{j})$, $1 \leq j \leq l$.

  • le query $\leftarrow (w_{j}, p_{i+1}(\bar{s}_{i+1}), \ldots, p_{n}(\bar{s}_{n})) \lambda_{j}$, $1 \leq j \leq m$, terminano con risposte $(\sigma_{1}, v_{1}), \ldots , (\sigma_{h}, v_{h})$.

Teorema 6.2 (Terminazione del criterio)  

Dato un programma P e la query $\leftarrow (p_{1}(\bar{t}_{1}),\ldots,p_{n}(\bar{t}_{n}))\theta$, il criterio applicato a tale query termina.

dim. (per induzione sulla lunghezza della query)

Il criterio applicato a $\leftarrow (p_{1}(\bar{t}_{1}),\ldots,p_{n}(\bar{t}_{n}))\theta$ termina perché $p_{1}(\bar{t}_{1})\theta$ è una disuguaglianza insoddisfacibile oppure perché termina applicato alle queries $\leftarrow p_{1}(\bar{t}_{1})\theta$ e $\leftarrow ( v_{1j}, p_{2}(\bar{t}_{2}), \ldots, p_{n}(\bar{t}_{n})) \theta \circ \theta_{1j}$.

Quindi è sufficiente dimostrare che il criterio termina se viene applicato alla query del tipo $\leftarrow p(\bar{t})\theta$.

In questo caso termina:

• perché $p(\bar{t})\theta$ è una uguaglianza

• oppure perché è una diseguaglianza

• oppure perché è un letterale negativo del tipo $\neg Q$: infatti, poiché il programma P si assume sia stratificato, procedendo per induzione sul valore di level mapping dei predicati, si può fare la seguente ipotesi induttiva: le queries del tipo $\leftarrow r(\bar{t})$, con valore di level mapping di $r$ minore di quello di Q, terminano. Allora anche $\leftarrow Q$ termina, perché può dar luogo solo ad applicazioni del criterio a query il cui valore di level mapping é minore.

• oppure perché $p(\bar{t})\theta$ è un letterale positivo e il criterio applicato ad ogni clausola la cui testa unifica con $p(\bar{t})\theta$ stabilisce se tale clausola è terminante o meno.

Infatti se:

• la clausola è un fatto il criterio termina

• la clausola non è un fatto e non è ricorsiva il criterio si applica ricorsivamente alle queries corrispondenti ai letterali nel corpo della clausola. Supponiamo ora che il criterio termini applicato alle clausole il cui predicato di testa abbia un valore di level mapping inferiore a quello del predicato di testa della clausola in esame (ipotesi induttiva). Poiché il programma è stratificato, il criterio terminerà anche sulla clausola in esame perché terminerà sulla query corrispondente al corpo. Infatti i predicati che compaiono nel corpo unificheranno solo con clausole su cui, per l'ipotesi induttiva, il criterio termina.

• la clausola è ricorsiva, procediamo nella dimostrazione considerando per semplicità predicati con un solo argomento (non è un'ipotesi restrittiva perché il criterio stabilisce che la condizione sulle norme debba valere per tutti gli argomenti). Dimostriamo la terminazione del criterio in riferimento alla chiamata ricorsiva. Supponiamo, per induzione sul valore della norma, che il criterio applicato alla query $\leftarrow p(s)$, con $\mid s \mid$ $<$ $\mid t \theta \mid$, termini. Allora si possono avere due casi: che almeno una clausola la cui testa unifica con $p(t)\theta$ sia non terminante (cioè non vale la condizione sulle norme), nel qual caso il criterio termina, oppure tutte siano terminanti: in questo caso la clausola $p(u) \leftarrow p(u')$ risolve con $p(t)\theta$ con mgu $\sigma$ ottenendo la query $\leftarrow p(u')\sigma$. Poiché vale la condizione sulle norme si può applicare l'ipotesi induttiva e quindi il criterio termina. Infine, il criterio applicato alla query $\leftarrow p(s)$, con $\mid s \mid$ = 1, termina perchè tale query può unificare solo con clausole ricorsive non terminanti o con clausole non ricorsive terminanti.

$\quad\Box$

Teorema 6.3 (Correttezza del criterio)  

Dato un programma P, la query $\leftarrow (p_{1}(\bar{t}_{1},\ldots,\bar{t}_{n}))\theta$ termina con risposte $(\sigma_{1},v_{1}), \ldots, (\sigma_{k},v_{k})$

$\Rightarrow$ tale query ha un albero di derivazione SLDCNF finito con sostituzioni di risposta $\sigma_{1}, \ldots, \sigma_{k}$ e diseguaglianze primitive $v_{1}, \ldots, v_{k}$.

dim. (per induzione sulla struttura del programma e della query)

Consideriamo il caso in cui la query sia del tipo $\leftarrow (p_{1}(\bar{t}_{1}) ,\ldots,p_{n}(\bar{t}_{n}))\theta$, con $n > 1$.

Se valgono le condizioni del criterio, si può avere che:

• $p_{1}(\bar{t}_{1})\theta$ è una diseguaglianza insoddisfacibile e quindi l'albero di radice $\leftarrow (p_{1}(\bar{t}_{1}),\ldots, p_{n}(\bar{t}_{n}))\theta$ è finito (termina con fail).

• $p_{1}(\bar{t}_{1})\theta$ non è una diseguaglianza insoddisfacibile e se termina la query corrispondente con risposta $(\sigma_{i},v_{i})$ $1 \leq i \leq k$, e le queries

  $\leftarrow (v_{i}, p_{2}(\bar{t}_{2}),\ldots,p_{n}(\bar{t}_{n}))\theta\circ\sigma_{i}$ terminano, l'albero sarà

  
  
  

  cioè finito.

Dimostriamo ora che una query del tipo $\leftarrow p(\bar{t}) \theta$ termina, se valgono le condizioni del criterio;

• se $p(\bar{t}) \theta$ è una diseguaglianza valida, l'albero sarà:

  
  
  

  e la risposta è $(\theta, true)$.

• se $p(\bar{t}) \theta$ è una diseguaglianza insoddisfacibile, l'albero sarà:

  
  
  

• se $p(\bar{t}) \theta$ è una uguaglianza del tipo $r=s$ ed esiste $\bar{\theta}$ mgu di $r$ ed $s$, l'albero sarà:

  
  
  

  con risposta $(\theta \circ \bar{\theta}, true)$.

• se $p(\bar{t}) \theta$ è un letterale negativo della forma $\neg Q$, e la query $\leftarrow Q$ termina con sostituzioni di risposta $A_{1}, \ldots, A_{h}$ e $v_{1}, \ldots, v_{k}$ sono la negazione di $A_{1}, \ldots, A_{h}$ , l'albero sarà:

  
  
  

  e quindi le risposte saranno $(\theta, v_{i})$, $1 \leq i \leq k$.

• se $p(\bar{t}) \theta$ è un letterale positivo, procediamo per induzione sugli strati del programma, supponendo che le queries del tipo $\leftarrow p'$ con valore di level mapping di $p'$ minore di quello di $p$ abbiano un albero finito. Dimostriamo che se ogni clausola la cui testa unifica con $p(\bar{t}) \theta$ è terminante, l'albero è finito.

  Si ha che:

  • se tutte le clausole sono fatti, sono terminanti e l'albero che si ottiene è

    
    
    

    con risposte $(\theta \circ \sigma_{1}, true), \ldots, (\theta \circ \sigma_{k}, true)$.

  • se una clausola è del tipo $p(\bar{s}) \leftarrow p_{1}(\bar{s}_{1}), \ldots , p_{n}(\bar{s}_{n})$ non ricorsiva, se valgono le condizioni del criterio, cioè la query $\leftarrow (p_{1}(\bar{s}_{1}), \ldots , p_{n}(\bar{s}_{n}))~\theta~\circ~\sigma$ termina, l'albero sarà finito perché per ipotesi induttiva tale query ha un albero finito.

  • se una clausola è tale che $\exists i$ per cui vale $p_{i}$ $=$ $p$ (cioè la clausola è ricorsiva), bisogna dimostrare la correttezza del criterio in riferimento alla chiamata ricorsiva.

    Procediamo per induzione sul valore della norma considerando separatamente il caso in cui vale

    $nonground_{input}(\leftarrow~(p_{i}(s_{1i},\ldots,s_{n_{i}i}) )\gamma_{j})~=~\phi$ da quello in cui non vale. Per semplicità, consideriamo il caso di predicati con un solo argomento.

    Nel primo caso se vale $\mid~(s)\gamma_{j}~\mid~>~\mid~(s_{i})\gamma_{j}~\mid$, con $(s_{i})\gamma_{j}$ ground, si ha:

    • (primo passo) Se $\mid~(s_{i})\gamma_{j}~\mid$ = 1, il termine $(s_{i})\gamma_{j}$ può essere solo o una costante o un termine del tipo $g(-)$, con g non riflessivo, per come è definita la norma. Quindi il sottogoal $\leftarrow (p(s_{i}))\gamma_{j}$ può risolvere solo con clausole che non sono ricorsive, sulle quali il criterio è corretto. Infatti non esistono clausole ricorsive del tipo $p(u) \leftarrow \ldots ,p(v),\ldots$ con $\mid u \mid$ = 1 tale che $\mid u\mid$ $>$ $\mid v \mid$.

    • (passo di induzione) Supponiamo che se $\mid~(s_{i})\gamma_{j}~\mid$ = h, il criterio sia corretto. Allora dimostriamo che vale nel caso che $\mid~(s_{i})\gamma_{j}~\mid$ = h+w. Infatti, se $\leftarrow p((s_{i}))\gamma_{j}$ risolve con la clausola $p(u) \leftarrow \ldots ,p(v),\ldots$ con $\mid u \mid$ = h+w $>$ $\mid v \mid$= h e sostituzione $\sigma$, si ottiene il sottogoal $\leftarrow (p(v))\sigma$, per cui vale l'ipotesi induttiva.

    Nel secondo caso è utile la seguente osservazione:

    se $(s_{i}) \gamma_{j}$ è non ground e vale $\mid (s_{i}) \gamma_{j} \mid$ $\neq$ $\infty$, allora $(s_{i}) \gamma_{j}$ non è una variabile. Infatti se così fosse, non potrebbe valere la relazione $\mid~(s)\gamma_{j}~\mid~>~\mid~(s_{i})\gamma_{j}~\mid$, perché $(s)\gamma_{j}$ dovrebbe contenere un costruttore riflessivo, eventualità che contraddirebbe l'ipotesi che $\mid (s_{i}) \gamma_{j} \mid$ $\neq$ $\infty$.

    Quindi, $(s)\gamma_{j}$ può esser solo del tipo $f(t_{1}, \ldots, t_{n})$, con $f(t_{1}, \ldots, t_{n})$ $\in$ $\Sigma$ e $\forall$ i tale che $1 \leq i \leq n$ e $t_{i}$ è non ground $\Rightarrow$ $t_{i}$ $\not \in$ $\Sigma$ (altrimenti $\mid f(t_{1}, \ldots, t_{n}) \mid$ = $\infty$).

    Quindi le variabili che compaiono in $f(t_{1}, \ldots, t_{n})$ non influiscono sul valore della norma e perciò si può procedere come nel caso precedente, per induzione sul valore della norma.

$\quad\Box$

La verifica della relazione sulle norme per tutti gli argomenti di una chiamata ricorsiva potrebbe sembrare una condizione troppo forte e si potrebbe pensare di limitarla solo alle posizioni di input. Il seguente esempio fa vedere che tale condizione è necessaria per mantenere la correttezza del criterio:

Esempio 6.5  

Considerando la definizione dei numeri pari data dalle clausole

$$pari(0).$$

$$pari(s(s(x))) \leftarrow pari(x)$$

sulla segnatura $\Sigma = \{0 : Nat, S : Nat \rightarrow Nat \}$, se l'utente volesse usarla per generare tutti i numeri pari fornirebbe il modo $d_{pari} = (-)$. Se il criterio controllasse la relazione sulle norme solo per le posizioni di input, stabilirebbe che la query $\leftarrow pari(x)$ termina, errando. D'altra parte il predicato $pari$ va trattato con la negazione intensionale.