6.4 Aspetti implementativi

Il criterio, pur non essendo completo per ovvi motivi teorici, è troppo costoso poiché in pratica calcola tutte le risposte secondo SLDCNF ogni qualvolta non ci sia pericolo di cadere in rami infiniti. Ciò è vero considerando anche che in fondo si tratta di un'analisi preliminare non presente in altri metodi di negazione.

È quindi indispensabile cercare di abbassarne il costo, anche se questo può voler dire indebolire il criterio ottenendo così una partizione meno precisa dei predicati in $P_{1}$ e $P_{2}$.

Un metodo per ottenere tale risultato può essere quello di imporre particolari strategie nella costruzione dell'albero di derivazione SLDCNF. In particolare si può pensare, sempre procedendo depth first, di limitare ad un prefissato valore il livello di profondità dell'albero. Se entro tale livello non si è stabilito che la query in esame termina, tale query viene considerata non terminante.

Un'altra possibilità è quella di stabilire interattivamente con l'utente tale valore di profondità: si può pensare di presentare all'utente la partizione ottenuta con un certo valore, chiedendo se continuare o meno l'analisi.

A livello implementativo si potrà conservare l'informazione sulla terminazione delle queries già esaminate per evitare una ripetizione dell'analisi. Oltre ad ottenere un miglioramento in tempo, ciò permetterà di rendere più accettabile i limiti sui livelli di profondità a cui spingere l'analisi. Infatti l'analisi di queries già risolte in precedenza si svolgerà in un passo solo.

Sempre per rendere più accettabile il limite sul numero di livelli può essere utile analizzare la terminazione dei predicati secondo l'ordinamento che si può ottenere considerando il valore della level mapping, visto che stiamo trattando programmi stratificati. In pratica però si fa affidamento sull'ordine con cui vengono elencate le clausole dei programmi.

Un altro metodo per indebolire il criterio rendendolo meno costoso può essere quello di non negare le risposte ottenute da sottogoal corrispondenti a letterali negativi. In pratica quando la query in esame è del tipo $\leftarrow \neg Q$, ci si limita a verificare la terminazione di $\leftarrow Q$ senza produrre i vincoli ottenibili dalla negazione delle corrispondenti risposte. In tal modo si evita il costo dovuto alla negazione delle risposte, semplificando anche la definizione del criterio (non esistono più i vincoli).