License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.17
URN: urn:nbn:de:0030-drops-26427
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2642/
Go to the corresponding LIPIcs Volume Portal

Appel, Claus ; van Oostrom, Vincent ; Simonsen, Jakob Grue

Higher-Order (Non-)Modularity

pdf-format:
10002.AppelClaus.2642.pdf (0.2 MB)

Abstract

We show that, contrary to the situation in first-order
term rewriting, almost none of the usual properties of
rewriting are modular for higher-order rewriting, irrespective
of the higher-order rewriting format.
We show that for the particular format of simply typed
applicative term rewriting systems modularity of confluence,
normalization, and termination can be recovered
by imposing suitable linearity constraints.

BibTeX - Entry

@InProceedings{appel_et_al:LIPIcs:2010:2642,
  author =	{Claus Appel and Vincent van Oostrom and Jakob Grue Simonsen},
  title =	{{Higher-Order (Non-)Modularity }},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{17--32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2642},
  URN =		{urn:nbn:de:0030-drops-26427},
  doi =		{10.4230/LIPIcs.RTA.2010.17},
  annote =	{Keywords: Higher-order rewriting, modularity, termination, normalization}
}

Keywords: Higher-order rewriting, modularity, termination, normalization
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

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