Can this given set be unified?

Question

Assuming a,b,c are constant, and the rest are variables, what is the result of unification to the following sets?

P(f(x,z),r,t) , P(w,f(g(w),h(t),b)

The obvious solution would be to do the following

S1: f(x,z) <-- w

S2: r <-- f(g(w)

S3: t <-- h(t)

Although this leaves b

Answer 1

Your parentheses aren't balanced, so for most notions of unification this isn't even a well-defined problem. That is, unification is defined on terms and these aren't terms, so the question is like $3/\text{cat}$; it just doesn't make sense.

Presumably the intent is $p(f(X,Z),R,T) = p(W,f(g(W),h(T)),B)$, but before talking about that I'll cover the $p(f(X,Z),R,T) = p(W,f(g(W)),h(T),B)$ case. In this latter case, this may simply be disallowed, i.e. $p$ can't be both of arity 3 and 4, or it will fail to unify because operations with different arities can never unify. There's two ways to think about this. One way, a la Prolog, is that the arity is part of the operations name, i.e. in Prolog one speaks of an operation p/3, meaning an operation p with arity 3 which is distinct from p/4 which has arity 4. Alternatively, you could think of $p$ as a unary operation that takes a tuple, and then this pushes the problem to unifying different sized tuples which then always fails either because the tupling operation at different arities is simply distinct, or, if tuples are represented by nested pairs so $(a,b,c)$ becomes $(a,(b,(c,())))$ say, then $()$ will fail to unify with $(X,Y)$.

In the likely case that the intended meaning was $p(f(X,Z),R,T) = p(W,f(g(W),h(T)),B)$ (or you can try this for any of these examples), go to http://swish.swi-prolog.org/ and paste p(f(X,Z),R,T) = p(W,f(g(W),h(T)),B) into the textbox on the lower right hand side and click Run. If it's not obvious, operations must be lower case and variables upper case. The only gotcha with this is most Prolog implementations, including this one, don't implement the occurs check by default. If you want to be extra cautious, you can do

unify_with_occurs_check(p(f(X,Z),R,T), p(W,f(g(W),h(T)),B))

instead.