David Cerna, Teimuraz Kutsia,
"Higher-Order Pattern Generalization Modulo Equational Theories with a unit element"
, Serie Submitted to the RISC Report Series, RISC, JKU, Hagenberg, Linz, 2019
Original Titel:
Higher-Order Pattern Generalization Modulo Equational Theories with a unit element
Sprache des Titels:
Englisch
Original Kurzfassung:
We consider anti-unification for simply typed lambda terms in theories defined by associativity,commutativity, identity (unit element) axioms and their combinations, and develop a sound andcomplete algorithm which takes two lambda terms and computes their equational generalizations inthe form of higher-order patterns. The problem is finitary: the minimal complete set of suchgeneralizations contains finitely many elements. We define the notion of optimal solution andinvestigate special fragments of the problem for which the optimal solution can be computed in linearor polynomial time
Forschungs-