2.2 Unificazione

In questa sezione sarà trattato il meccanismo che permette di calcolare legami tra variabili e valori, obbiettivo principale dei sistemi di programmazione logica.

Una sostituzione $\theta$ è un insieme finito di associazioni tra variabili e termini, della forma $\{v_{1}/t_{1}, \ldots ,v_{n}/t_{n} \}$, con le variabili $v_{1}, \ldots ,v_{n}$ distinte tra di loro e $v_{i} \neq t_{i}$ per i=1,$\ldots ,n$.

Un termine è ground se non contiene variabili. Una sostituzione è detta ground quando ogni termine $t_{i}$ è ground .

Una espressione è un termine, oppure un letterale oppure una congiunzione o disgiunzione di letterali. Sia E una espressione e $\theta = \{v_{1}/t_{1}, \ldots ,v_{n}/t_{n} \}$ una sostituzione.L'espressione $E\theta$, detta istanza di E secondo $\theta$, è il risultato dell'applicazione di $\theta$ ad E, ottenuto rimpiazzando simultaneamente ogni occorrenza di variabile $x_{i}$ in E con il termine $t_{i}$ per $i=1,\ldots ,n$.

Se E è ground, allora E$\theta$ è chiamata istanza ground di E. Una sostituzione $\theta$ è più generale di una sostituzione $\eta$ se esiste una sostituzione $\gamma$ per cui $\eta = \theta \circ \gamma$.

Dato un programa P, con ground(P) indichiamo l'insieme di tutte le istanze ground delle clausole in P.

Dati le espressioni $E_{1}$ ed $E_{2}$ una sostituzione $\theta$ è un unificatore per tali espressioni se $E_{1}\theta = E_{2}\theta$. Un unificatore $\theta$ per $E_{1}$ ed $E_{2}$ è detto most general unifier (mgu) se, per ogni unificatore $\sigma$ per $E_{1}$ ed $E_{2}$, esiste una sostituzione $\gamma$ tale che $\sigma = \theta \circ \gamma$.

A Robinson è dovuto il seguente teorema:

Esiste un algoritmo (algoritmo di unificazione) che, prese due espressioni qualsiasi, produce il corrispondente mgu se sono unificabili. Altrimenti termina notificando la non esistenza di tale unificatore.