# why nominal unification is a first-order unification?

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.

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!

• The Urban et al paper doesn't seem to say explicitly that nominal unification is a first-order unification, but the paper's unification works over nominal signatures which are first-order. As to the example, $\lambda x.\lambda x.M$ is a perfectly valid $\lambda$-term. – Martin Berger Nov 8 '16 at 16:34
• How come the two bound variables can have the same name as $x$ in a single term? I think they should have different names. could you explain bit in detail – alim Nov 8 '16 at 16:55
• The inner binding 'wins': In other words, $\lambda x. \lambda x.M \equiv_{\alpha} \lambda y. \lambda x.M$. That's because $x$ is not a free variable in $\lambda x.M$. – Martin Berger Nov 8 '16 at 17:01
• I got it now. I wonder why they don't just write as $\lambda y.\lambda x.M$. – alim Nov 8 '16 at 17:06
• Whoops. $\lambda x. \lambda x.M \equiv_{\alpha} \lambda x. \lambda y.M$ only when $y$ does not occur freely in $M$. As to your question, the reason is that using $\lambda x. \lambda x.M$ is a more interesting problem for unification. – Martin Berger Nov 8 '16 at 23:21

Most experience people have with unification (if any) is usually unification modulo syntactic equality: two terms unify if there is a substitution for unification variables that makes the terms syntactically identical. However, you can consider other base equivalence relations that are coarser than syntactic equality. For example, there's associative, commutative equality that let's you unify two bags (aka multisets) of terms, e.g. the term $\{\!\!\{\mathtt{x},\mathtt{y}\}\!\!\} = \{\!\!\{\mathtt{y},\mathtt{x}\}\!\!\}$ where I'm using $\{\!\!\{ \ldots \}\!\!\}$ to represent a bag. Unification with a base equivalence like this, coarser than syntactic equality, come up, for example, in checking record types. You can imagine you have a bag of record labels and you want to record types to be the same regardless of how you wrote down the labels.
So, in this context, higher-order unification is unification modulo $\alpha\beta\eta$-equivalence. The base equivalence is what makes it higher-order-unification, not the terms it operates on. I can apply normal, syntactic, first-order unification to lambda terms too. Unification modulo $\alpha\beta\eta$-equivalence means being able to unify expressions like $E(3) = (3,3)$ via a substitution such as $[E \mapsto \lambda x.(x,x)]$ as these are $\beta$-equivalent. (Following Prolog, I'll use capital letters to indicate unification variables. Also, note $[E\mapsto\lambda x.(3,3)]$ is another non-equivalent substitution which is why higher-order unification produces extra non-determinism.) Nominal unification does not unify these terms. $(\lambda x.(x,x))(3)$ is not $\alpha$-equivalent to $(3,3)$. An application will never be $\alpha$-equivalent to a pair constructor. (However, if the notation was implicitly in curried-style, i.e. $(3,3)$ meant $((,)(3))(3)$, these would syntactically unify. Generally, though, multi-ary application is never $\alpha$-equivalent to unary application.)
Nominal unification is unification modulo $\alpha$-equivalence. At a raw syntax level $\lambda x.x$ is syntactically different from $\lambda y.y$ because $x$ is different syntax than $y$. This is undesirable as we want to treat these terms as completely identical. We don't want the choice of variable name to matter to, e.g., type checking. This problem is clearly solvable because we could use deBruijn notation and the only term corresponding to the two above lambda terms would be something like $\lambda\mathbf{1}$. The power of deBruijn notation is that syntactic equality is $\alpha$-equality. Nevertheless, it would be nice not to use deBruijn notation.
So one way to implement nominal unification would be to simply convert each term to deBruijn notation and unify. This would be fine if all we needed to do was answer "yay" or "nay", but we also need to produce a substitution. If we convert $\lambda x.x$ and $\lambda y.E$ to $\lambda\mathbf{1}$ and $\lambda E$ respectively, then unify them, we get $[E \mapsto \mathbf{1}]$. But obviously $\lambda x.x \neq (\lambda y.E)[E\mapsto x]$. Basically, we need to keep track of what variable corresponds to $\mathbf{1}$ on each side of the equation. This gives us two bijections (for any particular unification variable, i.e. locally) that maps variables to deBruijn indices, here $[x \mapsto \mathbf{1}]$ and $[y\mapsto\mathbf{1}]$. We can compose these bijections to get a bijection (i.e. permutation) between variables on each side. This leads to $[E \mapsto (x\ y)\bullet x]$, in their notation, which simplifies to $[E\mapsto y]$, the desired substitution. There are some extra concerns about capturing variables that additionally complicates the picture.
Summarizing, higher-order unification means unification modulo $\alpha\beta\eta$-equivalence. Nominal unification means unification modulo only $\alpha$-equivalence. This can be reduced to syntactic unification of deBruijn terms, but if we want to produce substitutions on non-deBruijn terms we need to keep track of some extra information. Doing a similar reduction for higher-order unification would involve reducing to terms in $\beta\eta$-normal form, which thus requires such normal forms to exist hence the focus on the typed case, and leads to creating terms out of nowhere which themselves require unification.