DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2014.391

Metaconfluence of Calculi with Explicit Substitutions at a Distance

Authors: Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract

Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms. The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of lambda-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.

Cite as

Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 391-402, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{demoura_et_al:LIPIcs.FSTTCS.2014.391,
  author =	{de Moura, Fl\'{a}vio L. C. and Kesner, Delia and Ayala-Rinc\'{o}n, Mauricio},
  title =	{{Metaconfluence of Calculi with Explicit Substitutions at a  Distance}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{391--402},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.391},
  URN =		{urn:nbn:de:0030-drops-48588},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.391},
  annote =	{Keywords: Confluence, Explicit Substitutions, Lambda Calculi}
}

Search Results

Documents authored by de Moura, Flávio L. C.

Metaconfluence of Calculi with Explicit Substitutions at a Distance

Abstract

Cite as

Thanks for your feedback!

Could not send message