Higher-Order (Non-)Modularity

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

doi:10.4230/LIPIcs.RTA.2010.17

Document

Higher-Order (Non-)Modularity

Authors Claus Appel, Vincent van Oostrom, Jakob Grue Simonsen

Part of: Volume: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Rewriting Techniques and Applications (RTA)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-07-06

PDF

File

PDF

LIPIcs.RTA.2010.17.pdf

Filesize: 172 kB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.RTA.2010.17
URN: urn:nbn:de:0030-drops-26427

Subject Classification

Keywords

Higher-order rewriting
modularity
termination
normalization

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Claus Appel, Vincent van Oostrom, and Jakob Grue Simonsen. Higher-Order (Non-)Modularity. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 17-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.RTA.2010.17

Author Details

Claus Appel

Vincent van Oostrom

Jakob Grue Simonsen

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail