Unification algorithm

[msimi]

from agents import *
from logic import *
A, B, C, D, E, F, G, P, Q, x, y, z, F, G, u = map(Expr, 'ABCDEFGPQxyzFGu')
unify(P(A, x, F(G(y))), P(z, F(z), F(u)))
{z: A, x: F(z), u: G(y)}
=> I think this should return instead {z: A, x: F(A), u: G(y)}

The unifier returned does not make the two expressions identical as it should

subst({z: A, x: F(z), u: G(y)}, P(A, x, F(G(y))))
P(A, F(z), F(G(y)))
subst({z: A, x: F(z), u: G(y)}, P(z, F(z), F(u)))
P(A, F(A), F(G(y)))

[SiluPanda]

Ma'am, can you kindly post the code file name? Or the link to this code snippet?

[msimi]

The file is logic.py from the AIMA-Python repository and I am referring to the function unify within it Implementing unification. — M. Simi

…

On 26 Mar 2019, at 19:31, Silu Panda ***@***.***> wrote: Ma'am, can you kindly post the code file name? Or the link to this code snippet? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1053 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AIq8ffqruC9p_qc74nu0r4oXrAgjmoZGks5vamd0gaJpZM4cMHEV>.

[dmeoli]

Unification is implemented in logic.py: unify (Robinson's algorithm) plus unify_var, occur_check, subst, and a second Martelli–Montanari variant unify_mm. The specific non-normal-form result reported here is also fixed — cascade_substitution (called from unify_var) normalizes the substitution, so e.g. unify(P(A, x, F(G(y))), P(z, F(z), F(u))) now returns {z: A, x: F(A), u: G(y)}, and substituting it into both expressions yields the identical P(A, F(A), F(G(y))). Closing as implemented.