# Are these examples of unification problems?

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.

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$.
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$.