why nominal unification is a first-order unification?
-
04-11-2019 - |
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