Swapping arguments of variables in higher-order pattern unification

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?

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

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$$).

• "Intuitively, since definitional equality is decidable, definitional isomorphism should be also decidable" Really?
– cody
Dec 28 '21 at 22:52
• @cody I refined the wording. But I still don't see why the existence of definitional isos between given types would not be decidable. The language of def isos is very restricted compared to general terms. Haven't yet given an algorithm, I just think now that it's plausible. Dec 28 '21 at 23:55
• Can we make a precise statement about isos? Under the assumption that judgmental ("definitional") equality is decidable, it is clearly decidable whether $f$ and $g$ are (judgmental) inverses of each other. Now, given just $f$, where would a candidate $g$ come from? Dec 29 '21 at 14:09
• @AndrejBauer edited, hopefully it's more precise now. Inverses come from the inversion algorithm. Dec 29 '21 at 14:50
• Thanks. Excuse my ignorance, but is "the inversion algorithm" something that is known under that name, or are you referring to something you developed and will be known in the future? Dec 29 '21 at 15:04