Fie limbajul de ordinul I L = (F, R, C, ari) unde F := {h, g, f, ∗, +, p}, C := {a, b, c}, iar x, y, z, u, v ∈ Var, descrise astfel:

• x, y, z, u, v ∈ Var
• a, b, c ∈ C (constantele pot fi privite ca funcții de aritate 0)
• h, g ∈ F₁
• f, ∗, + ∈ F₂
• p ∈ F₃

Decideți dacă există unificatori pentru următorii termeni și verificați că Prolog răspunde conform rezultatului pe care l-ați obținut. În Prolog, folosim predicatul unify_with_occurs_check/2.

Recomandare. Definiți un alias mai scurt:

eq(X, Y) :- unify_with_occurs_check(X, Y).

Exemple:

?- eq(h(a, X), h(Y, b)).
X = b, Y = a

?- eq(A, f(A)).
false

De ce false în al doilea caz? Occurs check — A apare în f(A).

Continuați cu exercițiile:

1. f(h(a), g(x)) cu f(y, y)
2. p(a, x, g(x)) cu p(a, y, y)
3. p(x, y, z) cu p(u, f(v, v), u)
4. p(x, f(x, x)) cu f(g(y), f(z, g(a)))
5. x + (y * y) cu (y * y) + z
6. f(g(x), x) cu f(y, y)
7. p(a, u, h(x)) cu p(y, f(y, z), z)

Atenție la specificația de limbaj! Variabilele din limbaj sunt și cele din Prolog, deci se scriu cu Majusculă. În exemplele de mai sus, variabilele x, y, z, u, v devin în Prolog X, Y, Z, U, V.