License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.26
URN: urn:nbn:de:0030-drops-123482
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12348/
Go to the corresponding LIPIcs Volume Portal

Cerna, David M. ; Kutsia, Temur

Unital Anti-Unification: Type and Algorithms

pdf-format:
LIPIcs-FSCD-2020-26.pdf (0.6 MB)

Abstract

Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions.

BibTeX - Entry

@InProceedings{cerna_et_al:LIPIcs:2020:12348,
  author =	{David M. Cerna and Temur Kutsia},
  title =	{{Unital Anti-Unification: Type and Algorithms}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12348},
  URN =		{urn:nbn:de:0030-drops-123482},
  doi =		{10.4230/LIPIcs.FSCD.2020.26},
  annote =	{Keywords: Anti-unification, tree grammars, unital theories, collapse theories}
}

Keywords: Anti-unification, tree grammars, unital theories, collapse theories
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: Implementation: https://github.com/Ermine516/UnitAU

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