Higher-Order (Non-)Modularity
Claus Appel, Vincent Van Oostrom & Jakob Grue Simonsen
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.
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see
our documentation.