Logic Programming: Solve the term constraint f(X; Y; g(a)) = f(g(Y ); Z; X)

Question

I was not able to attend my programming language class the other day due to my wonderful car crapping out on me. I am working on our homework assignment, I am doing pretty good till I got to this scary looking question:

"5. Solve the term constraint f(X; Y; g(a)) = f(g(Y ); Z; X). Show steps."

Now, I have read the slides, but I cannot make out what he is trying to say (He is from China) and he does an awful job of explaining things.

I was wondering if any of you kind folks would be able to show me how to solve a problem similar to this one. Explain it as if I am a five year old.

Thanks for your time.

Edit: I was in the wrong section on the lecture notes, I found this:

• Any term constraint is processed in the following way

• Case 1: itis of formc1=c2 where c1 and c2 are constants – If c1 isidentical identicalto c2, discard discard it; otherwise otherwise report no solution solution

• Case 2: it is of form x=t1 (x is variable and t1 a term) – Assign t1 to x, discard this constraint, and replace all x in allterm constraints by t1 ift1 has no x inside it; otherwise report no sol iuton

• Case 3: itis ofthe formf(s1,…,sn) = g(t1,…,tn)(f,g: function symbols,si and ti:terms) – If fisidentical identicalto g,replace replace the termconstraint constraint by constraints constraints

s1=t1 and s2=t2,……,sn=tn; otherwise: no solution

– Repeat this process until no more constraints left or a report of no‐solution solution exists.

It is not quit clear to me yet, I am going to keep reading over it till it does. I'll post back what I think the solution is, maybe one of you can tell me if I got it right.

Answer 1

f(X; Y; g(a)) = f(g(Y ); Z; X).

Your first step is to notice that f/3 = f/3, which is case 3. Case 3 will succeed if X=g(Y), Y=Z, and g(a) = X.

Then X=g(Y) might trivially be true; let's replace X with g(Y) in both sides:

f(g(Y); Y; g(a)) = f(g(Y); Z; g(y))

OK, moving along let's unify Y with Z. I don't see a case for this.

f(g(Y); Y; g(a)) = f(g(Y); Y; g(Y))

Moving along, the next thing we have is g(a) = g(Y). This succeeds unifying Y=a. The resultant term is:

f(g(a); a; g(a)) = f(g(a); a; g(a))

which is looks obvious. X = g(a), Y = Z = a.

I have no idea if this is right, but that's my guess.