3.3.5 Risposte pre-normalizzate e risposte in forma normale

Sia $G_{0} = \leftarrow (L_{1}, \ldots ,L_{k})$, con variabili $x_{1}, \ldots ,x_{m}$ e la composizione degli unificatori (rispetto a $x_{1}, \ldots ,x_{m}$) dalla radice al goal terminale sia $\theta$. Se l'ultimo goal è la clausola vuota, la forma pre-normalizzata di una risposta è:

$$x_{1} = x_{1} \theta \wedge \ldots \wedge x_{m} = x_{m} \theta$$

Se l'ultimo goal è $\leftarrow IE_{1}, \ldots ,IE_{n}$, dove $IE_{i}$, $1 \leq i \leq n$, sono diseguaglianze primitive, la forma pre-normalizzata è:

$$x_{1} = x_{1} \theta \wedge \ldots \wedge x_{m} = x_{m} \theta \wedge IE_{1} \wedge \ldots \wedge IE_{n}$$

La forma normale di una risposta alla query $\leftarrow Q$ con variabili $x_{1}, \ldots ,x_{m}$ è il risultato di due passi di trasformazione che vedremo.

Non-goal variabili sono le variabili che non sono in $Q$.

1. Sono rimosse le variabili e le equazioni ridondanti.

   Se y è una variabile non-goal che è uguale ad una variabile in $x_{1}, \ldots ,x_{m}$, detta x, allora ogni occorrenza di y è rimpiazzata con x. Così ogni equazione ridondante è rimossa.

2. Sono rimosse dalle risposte le diseguaglianze irrilevanti.

   Una diseguaglianza è considerata irrilevante se contiene una variabile non-goal che non appare nella parte di eguaglianze. Le variabili localmente quantificate non contano e sono standardizzate a parte.

La dimostrazione della correttezza della procedura di normalizzazione è data in [Chan88].

Vediamo un esempio:

Esempio 3.9  

Siano $x_{1}, x_{2}$ le variabili del goal, $\theta$ sia la composizione degli unificatori dalla radice al goal terminale $TG$ e $A$ sia la risposta normalizzata.

Se $\theta$ è $\{ u/x_{1}, u/x_{2}, v/x_{3} \}$ e $TG = \leftarrow v \neq f(w)$ allora $A$ è $x_{1}$ = $x_{2}$