Question

In my understanding, if a unification solves equations of terms that are not higher-order terms, then it is a first-order unification.

If a unification solves equations of terms that are higher-order terms, then it is a higher-order unification. Therefore a unification solves equations of $\lambda$-terms should be a higher-order Unification.

That is what I thought.

Read about unification

the paper nominal unification said that nominal unification is a first order unification, but it is solving equations of $\lambda$-terms.

Why nominal unification is a first-order unification while clearly solving equations of higher-order terms?

Also, that paper shows an example of unification

$$ \lambda a.\lambda b.(b \, M_6) =?= \lambda a.\lambda a.(a \, M_7) $$

on the right side $\lambda a.\lambda a.(a \, M_7)$, what is that? Why two abstractions have same bound variable $a$ ?

I am confused, could anyone clearify it to me, thanks!

No correct solution

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