Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Cerna, David M.; Kutsia, Temur http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-91826
URL:

;

Higher-Order Equational Pattern Anti-Unification

pdf-format:


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.

BibTeX - Entry

@InProceedings{cerna_et_al:LIPIcs:2018:9182,
  author =	{David M. Cerna and Temur Kutsia},
  title =	{{Higher-Order Equational Pattern Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9182},
  URN =		{urn:nbn:de:0030-drops-91826},
  doi =		{10.4230/LIPIcs.FSCD.2018.12},
  annote =	{Keywords: Simply typed lambda calculus, anti-unification, equational theories}
}

Keywords: Simply typed lambda calculus, anti-unification, equational theories
Seminar: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI