| 000 | 01641naa a2200229 a 4500 | ||
|---|---|---|---|
| 003 | AR-LpUFIB | ||
| 005 | 20250311170417.0 | ||
| 008 | 230201s2005 xx o 000 0 eng d | ||
| 024 | 8 |
_aDIF-M6518 _b6657 _zDIF005938 |
|
| 040 |
_aAR-LpUFIB _bspa _cAR-LpUFIB |
||
| 100 | 1 | _aBonelli, Eduardo | |
| 245 | 1 | 0 | _aRelating higher-order and first-order rewriting |
| 300 | _a1 archivo (435,2 KB) | ||
| 500 | _aFormato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca) | ||
| 520 | _aWe 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. | ||
| 534 | _aJournal of Logic and Computation, 15(6), pp. 901-947 | ||
| 650 | 4 | _aSISTEMAS DE REESCRITURA | |
| 700 | 1 | _aKesner, Delia | |
| 700 | 1 | _aRios, Alejandro | |
| 856 | 4 | 0 | _uhttp://dx.doi.org/ 10.1093/logcom/exi050 |
| 942 | _cCP | ||
| 999 |
_c55720 _d55720 |
||