×

Higher-order (non-)modularity. (English) Zbl 1236.68117

Lynch, Christopher (ed.), Proceedings of the 21st international conference on rewriting techniques and applications (RTA 2010), July 11–13, 2010, Edinburgh, Scottland, UK. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-18-7). LIPIcs – Leibniz International Proceedings in Informatics 6, 17-32, electronic only (2010).
Summary: 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.
For the entire collection see [Zbl 1213.68049].

MSC:

68Q42 Grammars and rewriting systems
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI Link