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 unification:extended pattern unificatio 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?