FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Higher-Order Equational Pattern Anti-Unification

Authors: David Cerna and Temur Kutsia

Paper Information

Title:Higher-Order Equational Pattern Anti-Unification
Authors:David Cerna and Temur Kutsia
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:Simply typed lambda calculus, Anti-unification, Equational theories
Abstract:

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.

Pages:16
Talk:Jul 12 11:30 (Session 74B: Unification)
Paper: