Swapping arguments of variables in higher-order pattern unification

Question

Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\, y\, z = t$ can be solved by $M = \lambda x y z.t$, assuming various side conditions hold (e.g. its RHS is in scope for $M$, has a rigid head, and contains no occurrences of $M$). Unlike full higher-order unification, pattern unification has most-general unifiers and a fairly well-known algorithm to find them.

It seems to be fairly well-known that the "universal variables" occurring as arguments of an existential variable in a pattern unification equation can also be eta-expanded forms of variables. For instance, $M \, x \, (\lambda u.y\, u)\,z = t$ is equivalent to $M \, x \, y \, z = t$ and has the same solutions. Often this is handled in algorithms by eta-contracting the arguments of $M$, which is slightly odd (since in most other contexts it seems better to treat eta-equivalence through expansion) but seems to mostly work.

However, what about something like $M \, x\, (\lambda uv. y\, v\, u)\, z = t$? Here the variable $y$ is not just eta-expanded, but its two arguments are swapped. But in the presence of eta-conversion, knowing the value of $\lambda uv. y\, v\, u$ is equivalent to knowing the value of $y$, and so the above equation has the solution $M = \lambda x y' z. t[y \mapsto (\lambda uv. y'\, v\, u)]$. Has anyone considered extending pattern unification to include cases like this?

Answer 1

I have developed this, but haven't yet published it in a more strucured/formal manner.

• "Enhanced pattern unification" abstract here.
• Demo implementation.
• Video recording.

You're absolutely on the right track when noting that $\eta$-contraction is odd in pattern unification. An important point in the updated pattern unification algorithm is that we only do $\eta$-expansion, similarly as in conversion checking. I give a short summary of the algorithm.

In the usual pattern unification, we create a partial inverse substitution from the spine of arguments. So e.g. $M\,x\,y = t$ yields $[x \mapsto a, y \mapsto b]$ where $a,\,b$ are fresh variables, and the solution becomes $M \mapsto \lambda\,a\,b.\,t[x \mapsto a, y \mapsto b]$. The $t$ substitution fails if $t$ depends on variables other than $x$ and $y$; that's why it's a partial substitution.

The updated algorithm generalizes the spine inversion step, so that it can go under $\lambda$ and pairing. It turns out that this may require performing pattern unification recursively during inversion.

For example, in $M\,(\lambda\,x\,y.\,f\,y\,x) = f$, we want to "invert" the term $\lambda\,x\,y.\,f\,y\,x$ by mapping it to the fresh variable $a$. Using informal notation, we need $$(\lambda\,x\,y.\,f\,y\,x) \mapsto a$$ this is decomposed to $$\forall xy.\, f\,y\,x \mapsto a\,x\,y$$ at which point we have the recursive pattern problem $f\,y\,x \mapsto a\,x\,y$. So we perform the same kind of pattern unification on this problem, inverting the $y\,x$ spine to $[y \mapsto b, x \mapsto c]$, yielding $[f \mapsto \lambda\,b\,c.\,a\,c\,b]$ as the result for the original spine inversion problem. Finally we get $M \mapsto \lambda\,a\,b\,c.\,a\,c\,b$. Thus, instead of $\eta$-contracting spine entries, we $\eta$-expand in the solutions.

More generally, I conjecture that whenever $f$ is a definitional isomorphism in a decidable type theory with $\Pi$ and $\Sigma$, the extended pattern unification algorithm solves $M\,(f\,x) = x$ as $M \mapsto \lambda\,x.\,f^{-1}\,x$. I haven't yet proven this formally, I'm fairly confident though. Unit types can be also handled, but in that case purely syntax-directed inversion is not enough, we need to track types (the same thing happens in conversion checking for unit $\eta$).