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

A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification - Miller

Higher-Order Dynamic Pattern Unification for Dependent Types and Records - Andreas Abel and Brigitte Pientka

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

Jozef g explanation

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?