Unificazione (logica) 📖 Wikipedia

In logica (e informatica, specificamente nel ragionamento automatico), l'unificazione è l'applicazione di un algoritmo di soluzione di equazioni fra espressioni simboliche, ognuna della forma: parte-sinistra = parte-destra.

Per esempio, usando le variabili ${\displaystyle x,y,z}$, e considerando il simbolo di funzione ${\textstyle f}$, l'equazione ${\displaystyle f(1,y)=f(x,2)}$ costituisce un problema di unificazione sintattica del primo ordine che ha la sostituzione ${\displaystyle \{x/1,y/2\}}$ come unica soluzione.

Ci sono convenzioni diverse su cosa si può sostituire alle variabili e su quali espressioni siano considerate equivalenti. Nell'unificazione sintattica del primo ordine, le variabili possono assumere come valori i termini e l'equivalenza è puramente sintattica. Tale versione dell’unificazione ha un'unica risposta "ottima" e viene usata in programmazione logica e nell'implementazione dei sistemi di tipi dei linguaggi programmazione, specialmente negli algoritmi Hindley–Milner di inferenza dei tipi.

Nell'unificazione di ordine superiore, eventualmente limitata all'unificazione di pattern di ordine superiore, i termini possono includere le lambda espressioni e l'equivalenza è al livello della beta-riduzione. Questa versione viene utilizzata nei proof assistant e nella programmazione logica di ordine superiore, come Isabelle, Twelf, e lambdaProlog. Infine, nell'unificazione semantica o E-unificazione, l'uguaglianza è soggetta alla conoscenza di fondo e le variabili assumono valori su vari domini. Tale versione è usata nei risolutori SMT, negli algoritmi di riscrittura dei termini e nell'analisi dei protocolli crittografici.

Un problema di unificazione è un insieme finito di equazioni da risolvere ${\displaystyle E=\{l_{1}=r_{1},\ldots ,l_{n}=r_{n}\}}$, dove ${\textstyle l_{i},r_{i}}$ appartengono all'insieme dei termini o espressioni.

A seconda delle espressioni o termini ammessi in un insieme di equazioni (o problema di unificazione) e di quali espressioni siano considerate uguali, si distinguono diversi contesti di unificazione. Se si ammettono nelle espressioni variabili di ordine superiore, ovvero variabili che rappresentano funzioni, allora il processo prende il nome di unificazione di ordine superiore, altrimenti si parla di unificazione del primo ordine. Se si richiede che una soluzione renda letteralmente uguali le due parti di un'equazione, il processo si chiama unificazione sintattica o libera, altrimenti si dirà unificazione semantica o equazionale, detta anche E-unificazione.

Se la parte destra di ogni equazione è chiusa (senza variabili libere), il problema si dice di pattern matching. La parte sinistra (con variabili) di ogni equazione viene infatti detta pattern (schema).

Una sostituzione è una funzione ${\displaystyle \sigma :V\rightarrow T}$ dalle variabili ai termini; la notazione ${\displaystyle \{x_{1}/t_{1},...,x_{k}/t_{k}\}}$ indica una sostituzione che associa ogni variabile ${\displaystyle x_{i}}$ a un termine ${\displaystyle t_{i}}$ (indicata anche con ${\displaystyle x_{i}\mapsto t_{i}}$), per ${\displaystyle i=1,...,k}$, e ogni altra variabile a se stessa; le ${\displaystyle x_{i}}$ devono essere distinte a coppie. L'applicazione di una sostituzione a un termine ${\displaystyle t}$ viene scritta in notazione postfissa come ad esempio ${\displaystyle t\{x_{1}/t_{1},...,x_{k}/t_{k}\}}$; ciò comporta il rimpiazzo (simultaneo) nel termine ${\displaystyle t}$ di ogni occorrenza di ciascuna variabile ${\displaystyle x_{i}}$ con ${\displaystyle t_{i}}$. Il risultato ${\displaystyle t\sigma }$ dell'applicazione della sostituzione ${\displaystyle \sigma }$ a un termine ${\displaystyle t}$ si chiama istanza del termine ${\displaystyle t}$.

A titolo di esempio, nel caso del primo ordine, applicando la sostituzione ${\displaystyle \{x/h(a,y),z/b\}}$ al termine ${\displaystyle f(x,a,g(z),y)}$ si ottiene: ${\displaystyle f({\underline {h(a,y)}},a,g({\underline {b}}),y)}$.

Se un termine ${\displaystyle t}$ ha un'istanza equivalente a un termine ${\displaystyle u}$, ossia se ${\displaystyle t\sigma \equiv u}$ per qualche sostituzione ${\displaystyle \sigma }$, allora ${\displaystyle t}$ viene detto più generale di ${\displaystyle u}$ e ${\displaystyle u}$ più specifico di, o sussunto da, ${\displaystyle t}$. Una sostituzione ${\displaystyle \sigma }$ è più specifica di, o sussunta da, una sostituzione ${\displaystyle \tau }$ se ${\displaystyle t\sigma }$ è sussunto da ${\displaystyle t\tau }$ per ogni termine ${\displaystyle t}$. Si dice anche che ${\displaystyle \tau }$ è più generale di ${\displaystyle \sigma }$. Più formalmente, si consideri un insieme infinito non vuoto ${\displaystyle V}$ di variabili ausiliarie tali che nessuna equazione ${\displaystyle l_{i}=r_{i}}$ del problema di unificazione contenga variabili di ${\displaystyle V}$. Allora una sostituzione ${\displaystyle \sigma }$ è sussunta da un'altra sostituzione ${\displaystyle \tau }$ se esiste una sostituzione ${\displaystyle \theta }$ tale che per tutti i termini ${\displaystyle X\notin V}$, ${\displaystyle X\sigma \equiv X\tau \theta }$.^[1] Per esempio ${\displaystyle \{x/a,y/a\}}$ è sussunta da ${\displaystyle \tau =\{x/y\}}$, tramite ${\displaystyle \theta =\{y/a\}}$, ma ${\displaystyle \sigma =\{x/a\}}$ non è sussunta da ${\displaystyle \tau =\{x/y\}}$, dato che ${\displaystyle f(x,y)\sigma =f(a,y)}$ non è un'istanza di ${\displaystyle f(x,y)\tau =f(y,y)}$.^[2]

Una sostituzione ${\displaystyle \sigma }$ è una soluzione del problema di unificazione ${\displaystyle E}$ se ${\displaystyle l_{i}\sigma \equiv r_{i}\sigma }$ per ${\displaystyle i=1,\ldots ,n}$. Tale sostituzione verrà detta unificatore di ${\displaystyle E}$.

Per un dato problema di unificazione ${\displaystyle E}$, un insieme di unificatori ${\displaystyle S}$ si dice completo se ogni sostituzione che ne sia soluzione è sussunta da una sostituzione in ${\displaystyle S}$.

Sebbene Herbrand abbia introdotto i concetti-base dell'unificazione abbozzando un algoritmo già nel 1930, si attribuisce a Robinson il primo algoritmo, di complessità esponenziale in spazio e tempo nel caso pessimo. Molti altri algoritmi più efficienti sono stati proposti, lineari in tempo nel caso pessimo sono stati scoperti in modo indipendente da Martelli e Montanari (1976) e da Paterson e Wegman (1976). Algoritmi più recenti hanno cercato di rimanere competitivi con quello di Robinson nel caso di input di ridotte dimensioni; si prendano in considerazione quello di Baader & Snyder del 2001 e quello di de Champeaux del 2022.

L'algoritmo seguente origina da un lavoro di Martelli e Montanari (1982). Dato un insieme finito di equazioni, l'algoritmo applica regole di trasformazione per ottenere un insieme equivalente della forma ${\displaystyle \{x_{1}=u_{1},\ldots ,x_{m}=u_{m}\}}$, dove ${\displaystyle x_{1},\ldots ,x_{m}}$ sono variabili distinte e ${\displaystyle u_{1},\ldots ,u_{m}}$ sono termini che non contengono alcuna delle ${\displaystyle x_{i}}$. Un insieme siffatto può essere considerato una sostituzione. In caso non vi siano soluzioni l'algoritmo termina restituendo ${\displaystyle \bot }$, caso indicato anche con "${\displaystyle \Omega }$", o "fail" da altri autori. L'operazione di sostituzione di tutte le occorrenze della variabile ${\displaystyle x}$ nel problema ${\displaystyle G}$ con il termine ${\displaystyle t}$ viene denotata con ${\displaystyle G\{x/t\}}$. Per semplicità, i simboli di costante sono trattati come funzioni di arietà nulla.

${\displaystyle G\cup \{t=t\}\Rightarrow G}$		cancellazione
${\displaystyle G\cup \{f(s_{0},...,s_{k})=f(t_{0},...,t_{k})\}\Rightarrow G\cup \{s_{0}=t_{0},...,s_{k}=t_{k}\}}$		decomposizione
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})=g(t_{0},\ldots ,t_{m})\}\Rightarrow \bot }$	${\displaystyle {\text{se}}\ f\neq g\ {\text{o}}\ k\neq m}$	conflitto
${\displaystyle G\cup \{f(s_{0},...,s_{k})=x\}\Rightarrow G\cup \{x=f(s_{0},...,s_{k})\}}$		scambio
${\displaystyle G\cup \{x=t\}\Rightarrow G\{x/t\}\cup \{x=t\}}$	${\displaystyle {\text{se}}\ x\not \in {\text{vars}}(t)\ {\text{e}}\ x\in {\text{vars}}(G)}$	eliminazione
${\displaystyle G\cup \{x=f(s_{0},...,s_{k})\}\Rightarrow \bot }$	${\displaystyle {\text{se}}\ x\in {\text{vars}}(f(s_{0},...,s_{k}))}$	verifica

Il concetto di unificazione costituisce una delle principali idee a supporto della programmazione logica. Specificamente, l’unificazione è alla base della risoluzione, una regola d'inferenza utile a determinare la soddisfacibilità di una formula logica. In Prolog, il simbolo di uguaglianza = denota l'unificazione sintattica del primo ordine che rappresenta il meccanismo per associare il contenuto delle variabili e può essere visto come un tipo di assegnazione non ripetibile.

In Prolog:

1. Una variabile può essere unificata con una constante, un termine, o con un'altra variabile, divenendone a tutti gli effetti un suo alias. In molti dialetti moderni del Prolog e nella logica del primo ordine, una variabile non può essere unificata con un termine che la contiene; la relativa verifica si chiama occurs check.
2. Due costanti possono essere unificate solo se identiche.
3. Analogamente un termine può essere unificato con un altro termine se i simboli di funzione e le arietà dei termini sono identici e se anche gli argomenti sono unificabili contemporaneamente. Ciò vale in modo ricorsivo.
4. La maggior parte delle operazioni, fra cui +, -, *, /, non sono valutate usando =. Infatti, per esempio, 4+5 = 9 non è soddisfacibile poiché i due termini non si unificano in quanto sintatticamente diversi. L'uso di vincoli dell'aritmetica degli interi #= introduce una forma di unificazione per la quale tali operazioni sono interpretate e valutate.^[3]

• A. Martelli, e U. Montanari (1982). "An Efficient Unification Algorithm". ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169. S2CID 10921306.
• F. Baader and J.H. Siekmann (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming.
• F. Baader e Wayne Snyder (2001). "Unification Theory" Archived 2015-06-08 at the Wayback Machine. In J.A. Robinson & A. Voronkov, eds, Handbook of Automated Reasoning, volume I, p.p. 447–533. Elsevier.

• Wikimedia Commons contiene immagini o altri file su unificazione

• (EN) Eric W. Weisstein, Unification, su MathWorld, Wolfram Research.

Portale Informatica

Portale Matematica