Higher-Order (Non-)Modularity

Authors Claus Appel, Vincent van Oostrom, Jakob Grue Simonsen



PDF
Thumbnail PDF

File

LIPIcs.RTA.2010.17.pdf
  • Filesize: 172 kB
  • 16 pages

Document Identifiers

Author Details

Claus Appel
Vincent van Oostrom
Jakob Grue Simonsen

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail