Unification
First Order
First order is the good stuff. The first part in straightforward. zip down two thing
Unification as a solving a set of equations. multiequations. We can extend unification to work on a system of equations. Doesn’t really change much.
Unification as a proof system
E-unification
It is a natural (?) question to ask how to unify equations in the presence of equations.
Unification is a raw equation solving algorithm. From our mathematics experience, we know that it isn’t always easy to solve equations.
For associativity and commutativity, you can brute force expand into every combination of AC and use regular unification. This can be expensive.
A different approach is to try to normalize with respect to the underlying theory.
It is not clear to me that e-unification is a very good idea, since it seems pretty hard.
Unification modulo a group action is doable using the group union find. That’s interesting.
Unification Hints
Hints in unification Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi interesting paper. Describes how typeclasses and canonical structures can be put under a similar umbrella as extesnible unification mechanisms.
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
Nominal Unification
See nominal logic notes
Boolean Unification
https://cs.au.dk/~magnusm/papers/oopsla20/paper_b.pdf using it in Flix type checker
successive variable elimiations lowenheim’s algorithm https://web.cs.wpi.edu/~dd/publications/unif19.pdf coq
boolean unification, the story so far
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
Anti unification
https://en.wikipedia.org/wiki/Anti-unification_(computer_science) Least general anti-unifier
eery variety of uniifcation has it’s anti varierty: higher order, E, nominal
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus babble egg stuff ruler i think uses anti-unification inductive logic programming
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.
https://hal.archives-ouvertes.fr/hal-02123709/document uniifcation modulo reverse. hmm but this says it’s really hard related to unification modulo group action? https://youtu.be/35xgRnWsUsg?t=1929 and the generalized union find?
Tiark Rompf nbe?