Relating Higher-order and First-order Rewriting

EDUARDO BONELLI, DELIA KESNER, ALEJANDRO RÍOS

JOURNAL OF LOGIC AND COMPUTATION

Oxford University Press

Año: 2005 vol. 15 p. 901 - 947

0955-792X

We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory . In particular, we obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty equational theory (that is, = ). This class includes of course the -calculus. Our technique does not rely on the use of a particular substitution calculus but on an axiomatic framework of explicit substitutions capturing the notion of substitution in an abstract way. The axiomatic framework specifies the properties to be verified by a substitution calculus used in the translation. Thus, our encoding can be viewed as a parametric translation from higher-order rewriting into first-order rewriting, in which the substitution calculus is the parameter of the translation.