CS计算机代考程序代写 prolog interpreter Unification

Unification
At the core of how Prolog computes is Unification, which is based on Substitution.
• • •
▪
There are 3 rules for unification:
Atoms unify if they are identical
▪ ▪
e.g., monday & monday unifty but not monday & wednesday.
Variables unify with anything.
e.g., X & monday unify, X & black (friday).
Compound terms unfiy only if their top-function symbols and arities match and
their arguments unify recursively.
e.g., black(X) & black(friday) unify, next(thursday, Y) & next(thursday, friday)
unify, play(sunday) & study(X) do not unify.

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,P/R,Q/a}
How to get the correct solution {P/a,R/a,Q/a}?

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}
{P/R,Q/R}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}
{P/R,Q/R}
{P/R,Q/R,Q/a}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}
{P/R,Q/R}
{P/R,Q/R,Q/a}
{P/R,Q/R,R/a}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}
{P/R,Q/R}
{P/R,Q/R,Q/a}
{P/R,Q/R,R/a}
{P/a,Q/a,R/a}

Unification Example
X = f(P,P,Q), Y = f(Q,R,a)
{P/Q}
{P/Q,P/R}
{P/Q,Q/R}
{P/R,Q/R}
{P/R,Q/R,Q/a}
{P/R,Q/R,R/a}
{P/a,Q/a,R/a}
Propagate a current unifier to the previous and vice versa!

Unify
unify(f(P,P,Q),f(Q,R,a),ε):
𝜃 = [P/a, Q/a, R/a]
X = f(P,P,Q), Y = f(Q,R,a)
fold_left (fun 𝜃 (X,Y) -> unify(X,Y,𝜃)) ε [(P,Q),(P,R),(Q,a)]
unify(P,Q,ε)
X = P, Y = Q
𝜃 = [P/Q]
Example
unify(P,R,[P/Q])
unify(Q,a,[P/R, Q/R])
X = P[P/Q] = Q, Y = R[P/Q] = R
𝜃 = [P/Q]{Q/R} ⋃ {Q/R} = [P/R, Q/R]
X = Q[P/R, Q/R] = R, Y = a
𝜃 = [P/R, Q/R]{R/a} ⋃ {R/a} = [P/a, Q/a, R/a]

Abstract Interpreter Example
Program P:
fatherOf(abe,homer).
parentOf(homer,bart).
grandfatherOf(X, Y) :–
fatherOf(X, Z), parentOf(Z, Y).
Goal G:
?-grandfatherOf(abe, U)
Resolvent: grandfatherOf(abe, U)

Program P:
fatherOf(abe,homer).
parentOf(homer,bart).
grandfatherOf(X, Y) :–
fatherOf(X, Z), parentOf(Z, Y).
Goal G:
?-grandfatherOf(abe, U)
?-grandfatherOf(abe, U)
fatherOf(abe, Z)
fatherOf(abe,homer) Resolvent: parentOf(Z, U)

Program P:
fatherOf(abe,homer).
parentOf(homer,bart).
grandfatherOf(X, Y) :–
fatherOf(X, Z), parentOf(Z, Y).
Goal G:
?-grandfatherOf(abe, U) run(P,G)
G: {grandfatherOf(abe, U)}
Resolvent: {grandfatherOf(abe, U)}
A: {grandfatherOf(abe, U)} unify(grandfatherOf(X, Y), grandfatherOf(abe, U)) 𝜃 = {X/abe, Y/U}
Resolvent: {fatherOf(abe, Z), parentOf(Z, U)}
G: {grandfatherOf(abe, U)}
A: {father(abe, Z)}
unify(fatherOf(abe, Z), father(abe, homer))
𝜃 = {Z/homer}
Resolvent: {parentOf(homer, U)}
G: {grandfatherOf(abe, U)}
A: {parentOf(homer, U)}
unify(parentOf(homer, U), parentOf(homer, bart))
𝜃 = {U/bart} Resolvent: {}
G: {grandfatherOf(abe, bart)}

• •
In the code, renaming freshens a clause (or a term) by returning a new
clause (or a new term) where the clause (or term) variables have been
renamed with fresh variables.
We may need to apply a rule multiple times in the nested loop. Keep a
rule refreshed before using avoids naming confliction.

Related Posts