next up previous Sommario
Next: 2.3 Risoluzione SLD Up: 2. Fondamenti di programmazione Previous: 2.1 Linguaggi del primo   Sommario

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.


next up previous Sommario
Next: 2.3 Risoluzione SLD Up: 2. Fondamenti di programmazione Previous: 2.1 Linguaggi del primo   Sommario
Roberto Giungato 2001-03-14