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!

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top