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.RTA.2013.271
URN: urn:nbn:de:0030-drops-40674
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4067/
Go to the corresponding LIPIcs Volume Portal

Smolka, Gert ; Tebbi, Tobias

Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification

pdf-format:
20.pdf (0.5 MB)

Abstract

A recursion scheme is an orthogonal rewriting system with rules of the form f(x1,...,xn) -> s. We consider terms to be equivalent if they rewrite to the same redex-free possibly infinite term after infinitary rewriting. For the restriction to the nonnested case, where nested redexes are forbidden, we prove the existence of principal unifiers modulo scheme equivalence. We give an algorithm computing principal unifiers by reducing the problem to a novel fragment of semi-unification we call anchored semi-unification. For anchored semi-unification, we develop a decision algorithm that returns a principal semi-unifier in the positive case.

BibTeX - Entry

@InProceedings{smolka_et_al:LIPIcs:2013:4067,
  author =	{Gert Smolka and Tobias Tebbi},
  title =	{{Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{271--286},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4067},
  URN =		{urn:nbn:de:0030-drops-40674},
  doi =		{10.4230/LIPIcs.RTA.2013.271},
  annote =	{Keywords: recursion schemes, semi-unification, infinitary rewriting}
}

Keywords: recursion schemes, semi-unification, infinitary rewriting
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

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