6
$\begingroup$

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!

$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 8, 2016 at 16:34
  • $\begingroup$ 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 $\endgroup$
    – alim
    Nov 8, 2016 at 16:55
  • 1
    $\begingroup$ 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$. $\endgroup$ Nov 8, 2016 at 17:01
  • $\begingroup$ I got it now. I wonder why they don't just write as $\lambda y.\lambda x.M$. $\endgroup$
    – alim
    Nov 8, 2016 at 17:06
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 8, 2016 at 23:21

1 Answer 1

8
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thank you for your answer. Now I have much clear understanding on them. Just one thing: Nominal Unification and higher-order unification takes such different approach, because they take different approach on how to do substitution operation, right? I think that is the starting point of them, then everything becomes that much different as you explained above. am I thinking right? $\endgroup$
    – alim
    Nov 11, 2016 at 6:16
  • $\begingroup$ "Doing a similar reduction for higher-order unification would involve reducing to terms in βηβη-normal form...", I did not understand that, could you explain in a bit detail with examples? $\endgroup$
    – alim
    Nov 11, 2016 at 6:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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