Una signature (firma, in italiano), è formalmente definita come una coppia (Σ, ar) dove Σ è l'insieme di operatori
Σ = {c, f, g, ...}
ar è la funzione arietà, ar : Σ -> ℕ
Esempio: Σ = {0, succ, plus}
ar(0) = 0 (funzione costante)
ar(succ) = 1 (funzione unaria)
ar(plus) = 2 (funzione binaria)
Siano
Σ = {Σn}, n∈ℕ una signature
X = {x,y,z,...} un insieme infinito di variabili
TΣ,X denota l'insieme di tutti i termini su Σ,X
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
ρ : X -> TΣ,X
ρ(t) ad esempio, denota il termine ottenuto sostituendo simultaneamente tutte le occorrenze delle variabili in t
Spesso è anche scritto come tρ.
Ad esempio
ρ = [x = succ(y), y = 0]
t = plus(plus(x,y), succ(x))
tρ = plus(plus(succ(y),0), succ(succ(y)))
È 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' se ∃ρ. t' = tρ
In tal caso, chiamiamo t' istanza di t.
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
𝒢 = {ℓ₁ ≟ r₁, ..., ℓₙ ≟ rₙ}
Dove ℓ₁,...,ℓₙ,r₁,...,rₙ ∈ TΣ,X
La domanda è la seguente:
Possiamo trovare una sostituzione ρ tale che
∀i ∈ [ 1,n ].ρ(ℓᵢ) = ρ(rᵢ) ?
Chiamiamo questo ρ, se esiste, una soluzione di 𝒢.
sols(𝒢) ≜ {ρ | ∀ᵢ ∈ [1, ₙ] ⋅ ρ(ℓᵢ) = ρ(rᵢ)}