2
$\begingroup$

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!

$\endgroup$
3
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.