Higher-order (non-)modularity

Claus Appel; Vincent  van Oostrom; Jakob Grue Simonsen

doi:10.4230/LIPIcs.RTA.2010.17

Higher-order (non-)modularity

Claus Appel, Vincent van Oostrom, Jakob Grue Simonsen

Department of Computer Science

5 Citations (Scopus)

11 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Editors	Christopher Lynch
Number of pages	16
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date	2010
Pages	17-32
ISBN (Electronic)	978-3-939897-18-7
DOIs	https://doi.org/10.4230/LIPIcs.RTA.2010.17
Publication status	Published - 2010
Event	21st International Conference on Rewriting Techniques and Applications - Edinburgh, United Kingdom Duration: 11 Jul 2010 → 13 Jul 2010

Conference

Conference	21st International Conference on Rewriting Techniques and Applications
Country/Territory	United Kingdom
City	Edinburgh
Period	11/07/2010 → 13/07/2010

Series	Leibniz International Proceedings in Informatics
Volume	6
ISSN	1868-8969

Access to Document

10.4230/LIPIcs.RTA.2010.17Licence: CC BY-NC-ND

Appel_2010_Highter-orderFinal published version, 173 KBLicence: CC BY-NC-ND

Cite this

Higher-order (non-)modularity. / Appel, Claus; van Oostrom, Vincent; Simonsen, Jakob Grue.

Proceedings of the 21st International Conference on Rewriting Techniques and Applications. ed. / Christopher Lynch. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. p. 17-32 (Leibniz International Proceedings in Informatics, Vol. 6).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Appel, C, van Oostrom, V & Simonsen, JG 2010, Higher-order (non-)modularity. in C Lynch (ed.), Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics, vol. 6, pp. 17-32, 21st International Conference on Rewriting Techniques and Applications, Edinburgh, United Kingdom, 11/07/2010. https://doi.org/10.4230/LIPIcs.RTA.2010.17

@inproceedings{30e5b58544c444e0bf6318a669db2743,

title = "Higher-order (non-)modularity",

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. ",

author = "Claus Appel and {van Oostrom}, Vincent and Simonsen, {Jakob Grue}",

year = "2010",

doi = "10.4230/LIPIcs.RTA.2010.17",

language = "English",

series = "Leibniz International Proceedings in Informatics",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "17--32",

editor = "Christopher Lynch",

booktitle = "Proceedings of the 21st International Conference on Rewriting Techniques and Applications",

note = "21st International Conference on Rewriting Techniques and Applications ; Conference date: 11-07-2010 Through 13-07-2010",

}

TY - GEN

T1 - Higher-order (non-)modularity

AU - Appel, Claus

AU - van Oostrom, Vincent

AU - Simonsen, Jakob Grue

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.4230/LIPIcs.RTA.2010.17

DO - 10.4230/LIPIcs.RTA.2010.17

M3 - Article in proceedings

T3 - Leibniz International Proceedings in Informatics

SP - 17

EP - 32

BT - Proceedings of the 21st International Conference on Rewriting Techniques and Applications

A2 - Lynch, Christopher

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 21st International Conference on Rewriting Techniques and Applications

Y2 - 11 July 2010 through 13 July 2010

ER -