6.2.1 Tipi, modi e norma

Per rendere possibile l'analisi a tempo di compilazione è necessario avere informazioni sugli argomenti dei predicati. Basandosi su informazioni sul tipo dei termini presenti nelle clausole ricorsive, e sui loro modi, cioè sulla possibilità di avere posizioni occupate da termini ground o meno, il criterio può imporre una relazione che, se non verificata, assicura che la clausola non è terminante.

Quindi di seguito vengono riportate le definizione di modo e della norma utilizzata dal criterio.

Riferendoci a [Plü90] diamo la seguente

Definizione 6.1   Dato un simbolo di relazione p n-ario, modo per p è una funzione ${\em d_{p}}$ dall'insieme dei naturali {1,..., n} all'insieme {+,-}.

Se ${\em d_{p}(i)}$ = '+' chiamiamo i posizione di input di p, intendendo che tali posizioni al momento della chiamata del predicato dovrebbero essere rimpiazzate da termini ground. Similmente, se ${\em d_{p}(i)}$ = '-' chiamiamo i posizione di output di p e tale posizione andrà rimpiazzata da un termine non ground.

Un modo per un programma P è una funzione che assegna ad ogni simbolo di relazione di P un insieme non vuoto di modi.

Per la classe di programmi considerati (n.v.i) è possibile, data una clausola e dato il modo dell'atomo di testa, inferire i modi di ogni letterale di tale clausola, secondo il seguente teorema la cui dimostrazione è immediata.

Teorema 6.1  

Data la clausola

$$p(t_{01},\ldots ,t_{0n_{0}})\leftarrow p_{1}(t_{11},\ldots ,t_{1n_{1}}),\ldots ,p_{m}(t_{m1},\ldots ,t_{mn_{m}})$$

e i modi $d_{p}$ e $d_{p_{r}}$, con $1\leq r < i$ e $1\leq i \leq m$, si ha:

$$d_{p_{i}} = \left \{ \begin{array}{ll} + & \mbox{se $t_{ij}$... ...}}(h) = '-'$\ }\\ - & \mbox{altrimenti} \end{array} \right.$$

Esempio 6.2  

Data la clausola $p(x,y,z) \leftarrow q(x,y), r(x,y,z)$ e $d_{p} = (+,-,-)$, il teorema permette di inferire per $q$ il modo $d_{q} = (+,-)$ e per $r$ $d_{r} = (+,+,-)$.

L'altra nozione fondamentale per la successiva definizione della norma è quella di tipo dei termini: dato un programma P sul linguaggio L = $<\Pi,\Sigma>$, consideriamo $\Sigma$ non come una segnatura piatta, ma come una segnatura con una molteplicità di sorte che forniscono informazione di tipo sulla struttura dei termini.

Esempio 6.3   Consideriamo la seguente segnatura :

$$\Sigma = \{0 : Nat, s : Nat \rightarrow Nat, a : Foo, b : Foo, f : Foo \rightarrow Foo \}$$

Quindi ogni termine di $\Sigma$ è di tipo Nat oppure Foo.

Ogni tipo denotato da una segnatura può essere rappresentato come un grafo. Importante per la definizione di norma sui termini di un certo tipo è la nozione di costruttore riflessivo:

Definizione 6.2   Data una segnatura $\Sigma$ e c costruttore appartenente a $\Sigma$, c è riflessivo se compare in un ciclo del grafo di $\Sigma$.

Per esempio, s è un costruttore riflessivo per $\Sigma$ dell'esempio 6.3.

La seguente definizione introduce la norma utilizzata nel criterio proposto; tale definizione permette di distinguere alcuni casi critici per la terminazione. In particolare, la norma assume il valore convenzionale $\infty$ sui termini variabili di una segnatura che contiene costruttori riflessivi. Questo valore porta il criterio a concludere, insieme ad altre condizioni, che il goal in cui compaiono tali termini può non terminare: infatti la presenza di costruttori riflessivi nella segnatura può portare alla costruzione di termini di lunghezza non finita, causando la non terminazione del programma.

Un esempio di tale problema è il goal $\leftarrow p(x)$ valutato rispetto alla definizione dei numeri pari dell'esempio 3.6.

Definizione 6.3   Data una segnatura $\Sigma$ e un tipo $s$ in $\Sigma$, una norma sui termini di $\Sigma$ è una funzione così definita:

$$\begin{array}{ll} \mid c \mid_{s} = 1 & \mbox{ se c \\lq {e} una... ...e n-ario } \\ & \mbox{con codominio di tipo s}\\ \end{array}$$

dove $+$ è l'operatore di somma su $N \cup \{\infty \}$ definito nel modo usuale sui naturali e tale che, se $n \in N$, $n + \infty = \infty + n = \infty$ e $\infty + \infty = \infty$.

Se $\mid t \mid_{s} = \infty$, diciamo che il termine $t$ ha norma non limitata.

Questa norma, ricorrendo solo nel caso di termini costruiti a partire da costruttori riflessivi, è abbastanza generale da fornire valutazioni realistiche in molti casi. Considerando per esempio la segnatura

$$\Sigma = \{Nil : List, Cons: A \ast List \rightarrow List \}$$

si ha che la norma del termine $Cons(x,Cons(y,Nil))$ risulta uguale a 3 anche se il termine non è ground.