Are these examples of unification problems?

Question

I have been studying unification, especially nominal unification (paper) gets my attention. I read the theory and examples. But I am wondering that what kind of problems occur in unifications. For examples, The following examples are from nominal unification paper. (I write distinct bound variables, so easier to see the solutions )

(1) $\lambda a. \lambda b. (X \, b) = \lambda c. \lambda d. (d \,X) $

(2) $\lambda a. \lambda b. (X \, b) = \lambda c. \lambda d. (d \, Y) $

(3) $\lambda a. \lambda b. (b \, X) = \lambda c. \lambda d. (d \, Y) $

I observed that each variable ($X$ or $Y$) occurs only once on one side of equations. Should it be always that way? Can I write the following

(4) $\lambda a. \lambda b. (X \, X) = \lambda c. \lambda d. (d \,X) $

(5) $\lambda a. \lambda b. (Y \, X) = \lambda c. \lambda d. (d \,X) $

(6) $\lambda a. \lambda b. (X \, X) = \lambda c. \lambda d. (X \,X) $

and are these possible unification problems?

I read many sources, but and all presented unification problems with variables only have once occurrences on one side of equations. I tried to find more examples, but could not find anything different.

I know the unification problems arise from logic programming. And so far, I did not see any logic programs which puts $X$ twice in a term.

Anyway, hoping someone to clarify these points.

Thanks in advance!

Answer 1

Yes, the variables can occur more than once in a term. Either way you end up with a system of equations. For plain unification, you can always have the unification variables be distinct and then add equations to unify them separately. That is, you can turn $\mathtt{p}(X,X) = \mathtt{q}(\mathtt{a},\mathtt{b})$ into $\mathtt{p}(X,Y) = \mathtt{q}(\mathtt{a},\mathtt{b})$ and $X = Y$.

Comparing predicates with duplicate variables comes up all the time in Prolog. For example, one of the most iconic Prolog programs is list append, usually written as:

append([], Ys, Ys).
append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).

If you want to be very pedantic and say these programs don't illustrate terms with duplicate variables, then you can consider another iconic Prolog technique: difference lists. The most general difference list representation of a list $[1,2,3]$ is $[1,2,3|X]\setminus X$.