# Unification

# Union Find

# Higher Order Unification

efficient full higher order unification zipperposition

Unification Under a Mixed Prefix - miller

equality over lambda terms is similar to universalc quantification unification of stlc as logic programming This is really interesting. Interpretting lambda unificatsion as a harrop program. This is similar to what I was suggesting in harrop egglog. forall ((x = y) -> p = q) -> \x p = \y q structural vs generic equality.

Anti abstracting - if F is only applied to things it can’t contain.

Functions-as-constructors higher-order uniﬁcation:extended pattern uniﬁcatio DSP mathing. FCU unification hamana sol https://www.cs.gunma-u.ac.jp/~hamana/

What is the problem with pure alpha matching? de Bruijn indexing makes it feel like it should just be ordinary structural matching. Here’s the problem though. What is the scope of the pattern variables? If you only use the pattern variable once, maybe not a problem. Ok linear patterns. But then if you’re matching in order to instantiate this variable into something

match `\ F`

with `\0`

. If we make `F = 0`

that’s ok
`\ F F`

with `\ 0 0`

is ok also becaoue both instances of F are in scope of the same thing
The rewrite rule
`\ F -> \ F`

is highly fishy though.

Perhaps it is best to use named variables
rule : `\x F -> \y F`

matched with `\z. z`

First off match fails since `\x. _ != \z. _`

ok but then what about alpha renaming matchee to
`\x. x`

Then we get `F = x`

. Fine.
But then the other side gets \y. x where x wasn’t even in scope?

If everything is under the binder somehow (and it isn’t entirely clear what this means. We internalize rules as bodies of lambdas? Rules here are not implications. Maybe they are pseudo equalities?) \x. (F -> F)

Logically, the pattern variables could be considered existentially quantified on the exterior of the rule ex F. \x F -> \y F. This is possibly to match. F can only match things that already are around (in the signature) as the point of ex F.

Raising

MLTS

# Pattern Matching

Arguably pattern matching should be it’s own article. Depending on which you see first, you may consider unification two way pattern matching or pattern matching as one way unification. I think pattern matching is the much simpler topic

# Resources

adam gundry literate haskell “(for the free theory, abelian groups and higher-order pattern unification)” goes along with thesis

higher order pattern unification exampel in elaboration zoo Basic pattern unification in haskell

What is the pattern fragment? L_lambda subset “existential variables” applied to unique bound variables. reminscent of haskell pattern matching using distinct variables

http://conal.net/papers/elliott90.pdf conal elliott’s thesis

https://conservancy.umn.edu/bitstream/handle/11299/57268/Qi_umn_0130E_10758.pdf?sequence=1 lambda prolog implementation

See Miller and Nadathur book.

Tiark Rompf nbe?