Ritorna all'inizio

Signatures

Una signature (firma, in italiano), è formalmente definita come una coppia $\left(\Sigma ,\mathit{ar}\right)$ dove $\Sigma$ è l'insieme di operatori

$\Sigma =\{c,f,g,\dots \}$

ar è la funzione arietà, $\mathit{ar}:\Sigma \to \mathbb{N}$

Esempio: $\Sigma =\{0,\mathrm{succ},\mathrm{plus}\}$

$\mathit{ar}\left(0\right)=0$ (funzione costante) $\mathit{ar}\left(\mathrm{succ}\right)=1$ (funzione unaria) $\mathit{ar}\left(\mathrm{plus}\right)=2$ (funzione binaria)

Termini su una signature

Siano $\Sigma =\left\{{\Sigma }_n\right\},n\in \mathbb{N}$ una signature $X=\{x,y,z,\dots \}$ un insieme infinito di variabili

$T_{\Sigma ,X}$ denota l'insieme di tutti i termini su $\Sigma ,X$

Sostituzioni

Vedremo ora come effettuare sostituzioni, ovvero assegnazioni di termini a variabili

Una sostituzione è una mappa tra un insieme di variabili $X$ e l'insieme dei termini così definito $\rho :X\to T_{\Sigma ,X}$

$\rho \left(t\right)$ ad esempio, denota il termine ottenuto sostituendo simultaneamente tutte le occorrenze delle variabili in $t$

Spesso è anche scritto come $t\rho$.

Ad esempio

$\rho =\left[x=\mathrm{succ}\left(y\right),y=0\right]$ $t=\mathrm{plus}\left(\mathrm{plus}\left(x,y\right),\mathrm{succ}\left(x\right)\right)$

$t\rho =\mathrm{plus}\left(\mathrm{plus}\left(\mathrm{succ}\left(y\right),0\right),\mathrm{succ}\left(\mathrm{succ}\left(y\right)\right)\right)$

È interessante osservare che alcune espressioni possono così diventare più generali di altre, vediamo di chiarire meglio questo concetto.

Si dice che $t$ è più generale di $t^{\prime }$ se $\exists \rho .t^{\prime }=t\rho$

In tal caso, chiamiamo $t^{\prime }$ istanza di $t$.

Unificazioni

Affronteremo il tema delle unificazioni nella sua forma più semplice, sintattica e di prim'ordine.

Il problema delle unificazioni è così definito:

Dato un insieme di potenziali uguaglianze

$\mathcal{G}=\{{\ell }_1\stackrel{?}{=}{r}_1,\dots ,{\ell }_n\stackrel{?}{=}{r}_n\}$

Dove ${\ell }_1,\dots ,{\ell }_n,r_1,\dots ,r_n\in T_{\Sigma ,X}$

La domanda è la seguente:

Possiamo trovare una sostituzione $\rho$ tale che

$\forall i\in \left[1,n\right].\rho \left({\ell }_i\right)=\rho \left(r_i\right)$ ?

Chiamiamo questo $\rho$, se esiste, una soluzione di $\mathcal{G}$.

$\mathrm{sols}\left(\mathcal{G}\right)\triangleq \{\rho \mid \forall i\in \left[1,n\right]\cdot \rho \left({\ell }_i\right)=\rho \left(r_i\right)\}$

Articoli correlati