Appel, Claus; van Oostrom, Vincent; Simonsen, Jakob Grue 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]. Cited in 4 Documents MSC: 68Q42 Grammars and rewriting systems 03B70 Logic in computer science Keywords:higher-order rewriting; modularity; termination; normalization PDFBibTeX XMLCite \textit{C. Appel} et al., LIPIcs -- Leibniz Int. Proc. Inform. 6, 17--32 (2010; Zbl 1236.68117) Full Text: DOI Link