TY - GEN
T1 - Higher-order (non-)modularity
AU - Appel, Claus
AU - van Oostrom, Vincent
AU - Simonsen, Jakob Grue
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
U2 - 10.4230/LIPIcs.RTA.2010.17
DO - 10.4230/LIPIcs.RTA.2010.17
M3 - Article in proceedings
T3 - Leibniz International Proceedings in Informatics
SP - 17
EP - 32
BT - Proceedings of the 21st International Conference on Rewriting Techniques and Applications
A2 - Lynch, Christopher
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
T2 - 21st International Conference on Rewriting Techniques and Applications
Y2 - 11 July 2010 through 13 July 2010
ER -