Sumar
O substituție este o funcție parțială de la variabile la termeni, σ : V → Trm(L).
Un unificator pentru doi termeni t1 și t2 este o substituție θ astfel încât θ(t1) = θ(t2).
Un unificator ν pentru t1 și t2 este un cel mai general unificator dacă pentru orice alt unificator ν′, există o substituție μ astfel încât ν′ = ν ; μ.
Algoritmul de unificare (de la seminar)
Ținem două liste: S (lista soluție) și R (lista de rezolvat).
| Regula | S | R |
|---|---|---|
| Inițial | ∅ | t₁ = t'₁, ..., tₙ = t'ₙ |
| SCOATE (pentru t = t) | S | R' |
| DESCOMPUNE (pentru f(t₁,...) = f(t'₁,...)) | S | R', t₁ = t'₁, ..., tₙ = t'ₙ |
| REZOLVĂ (pentru x = t, x nu apare în t) | x = t, S[x ← t] | R'[x ← t] |
| Final | S | ∅ |
Eșec dacă:
- În R există
f(...) = g(...)cuf ≠ g. Constantele sunt funcții de aritate 0. - În R există
x = t(saut = x) șixapare înt(occurs check).
În Prolog: unify_with_occurs_check/2
Atenție la specificația de limbaj! Variabilele din limbaj sunt și cele din Prolog, deci se scriu cu Majusculă.
?- unify_with_occurs_check(h(a, X), h(Y, b)).
X = b, Y = a.
?- unify_with_occurs_check(A, f(A)).
false. % — occurs check! A apare în f(A)
Recomandare din Lab 4: alias mai scurt.
eq(X, Y) :- unify_with_occurs_check(X, Y).
Exemplu — când eșuează
Din model_rezolvat.pl, Exercițiul 5:
Fie L = (R, F, C, ari) o structură de ordinul I, unde F = {f, g, h}, C = {u, v, w} iar ari(f) = 2, ari(g) = 1, ari(h) = 3. Considerăm a, b, c, d variabile.
(a) f(g(a), h(b, c, v)) cu f(g(u), h(g(w), w, g(a)))?
?- unify_with_occurs_check(f(g(A), h(B, C, v)), f(g(u), h(g(w), w, g(A)))).
false.
De ce false? Se încearcă unificarea v = g(A), dar v e constantă (arity 0) iar g(A) e termen compus cu g/1 — DESCOMPUNE cere același functor.
(b) f(g(a), h(b, c, d)) cu f(g(u), h(g(w), w, g(a)))?
?- unify_with_occurs_check(f(g(A), h(B, C, D)), f(g(u), h(g(w), w, g(A)))).
A = u, B = g(w), C = w, D = g(u).
Aici merge, pentru că d (devenit D) e variabilă și acceptă g(A) = g(u).
Convenție sintactică
% constante și functori — literă mică sau cifre
a, b, 3, foo
% variabile — literă mare sau underscore
X, Y, MyVar, _Temp, _
Dacă scriem unify_with_occurs_check(a, A), Prolog înțelege a ca constantă și A ca variabilă — unificarea va reuși cu A = a. Dacă în specificația limbajului a e variabilă, trebuie să scrii A în Prolog.
De ce occurs check?
Fără el, X = f(X) „reușește” și creează un termen infinit — o sursă clasică de erori. De aceea Prolog standard expune unify_with_occurs_check/2; operatorul = simplu nu face occurs check (pentru performanță).