Higher-Order Equational Pattern Anti-Unification [Preprint]

TL;DR

This paper presents a sound and complete algorithm for higher-order pattern anti-unification in lambda calculus with associative, commutative, and associative-commutative theories, including optimal solutions for specific fragments.

Contribution

It introduces a novel algorithm for anti-unification in complex algebraic theories and explores computational complexity for special cases.

Findings

Algorithm is sound and complete for the specified theories.

Minimal complete set of generalizations is finite.

Optimal solutions can be computed efficiently in certain fragments.

Abstract

We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.