I am thinking that is the following a problem solved by nominal unification.

$\lambda a.X = \lambda b.\lambda c.c $

where we find $X$. The answer is obvious.

The reason is that it seems in nominal unification $X$ always will be an atom, not a function such as $\lambda c.c$. The theory seems works fine with this input, just did not saw any example similar to this one.


Sure, these unify under nominal unification. You get a unifier like $X = (b\ a)\bullet\lambda c.c$ which simplifies to $X = \lambda c.c$. Figures 1 and 3 of Nominal Unification describe the relevant details of the algorithm. In particular the transitions will be $\approx?$-abstraction-2 and $\approx?$-variable followed by $\#?$-abstraction-2 and $\#?$-atom.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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