Unification and Anti-unification in Applicative Matching Logic

Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern in normal form is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. The number of structural components can be reduced by unification and anti-unification. Algorithms for both processes have already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language, while generalizing the unification problem and mechanizing a proven-sound solution in Coq, as well as exploring certain possible extensions of the unification algorithm in a semi-formalized manner.