Relating higher-order and first-order rewriting

Título:

Relating higher-order and first-order rewriting

Autor:

Bonelli, Eduardo

Colaboradores:

; Kesner, Delia; Rios, Alejandro

Temas:

SISTEMAS DE REESCRITURA

En:

Journal of Logic and Computation, 15(6), pp. 901-947

Resumen:

We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory E. 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, E = ∅). 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.

URL/DOI:

http://dx.doi.org/ 10.1093/logcom/exi050

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Descripción física:

1 archivo (435,2 KB)

Idioma:

Inglés

Publicación:

Oxford University Press, 2005

Puede solicitar más fácilmente el ejemplar con: A0285

Ver estantes