LIPIcs.RTA.2010.17.pdf
- Filesize: 172 kB
- 16 pages
Document
Higher-Order (Non-)Modularity
Authors
-
Part of:
Volume:
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2010-07-06
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.RTA.2010.17
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.
Keywords
- Higher-order rewriting
- modularity
- termination
- normalization
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads