HIGHER-ORDER (NON-)MODULARITY

21st International Conference on Rewriting Techniques and Applications

CLAUS APPEL 1 AND VINCENT VAN OOSTROM 2 AND JAKOB GRUE SIMONSEN 1 ; E-mail address ; J. G. Simonsen: [e-mail]

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2642/pdf/10002.AppelClaus.2642.pdf
PID  :  44841

来源: CEUR

【 摘 要 】

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.