From higher-order to first-order rewriting
We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory ε. We obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε =ø). This class includes of course...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v2051LNCS_n_p47_Bonelli |
| Aporte de: |
| id |
todo:paper_03029743_v2051LNCS_n_p47_Bonelli |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_03029743_v2051LNCS_n_p47_Bonelli2023-10-03T15:18:53Z From higher-order to first-order rewriting Bonelli, E. Kesner, D. Ríos, A. Artificial intelligence Computer science Differentiation (calculus) Equational theory First-order rewriting Higher-order Higher-order rewriting Extended abstracts Lambda calculus Calculations Calculations We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory ε. We obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε =ø). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitution calculus used in the translation. © Springer-Verlag Berlin Heidelberg 2001. Fil:Bonelli, E. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v2051LNCS_n_p47_Bonelli |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Artificial intelligence Computer science Differentiation (calculus) Equational theory First-order rewriting Higher-order Higher-order rewriting Extended abstracts Lambda calculus Calculations Calculations |
| spellingShingle |
Artificial intelligence Computer science Differentiation (calculus) Equational theory First-order rewriting Higher-order Higher-order rewriting Extended abstracts Lambda calculus Calculations Calculations Bonelli, E. Kesner, D. Ríos, A. From higher-order to first-order rewriting |
| topic_facet |
Artificial intelligence Computer science Differentiation (calculus) Equational theory First-order rewriting Higher-order Higher-order rewriting Extended abstracts Lambda calculus Calculations Calculations |
| description |
We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory ε. We obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε =ø). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitution calculus used in the translation. © Springer-Verlag Berlin Heidelberg 2001. |
| format |
SER |
| author |
Bonelli, E. Kesner, D. Ríos, A. |
| author_facet |
Bonelli, E. Kesner, D. Ríos, A. |
| author_sort |
Bonelli, E. |
| title |
From higher-order to first-order rewriting |
| title_short |
From higher-order to first-order rewriting |
| title_full |
From higher-order to first-order rewriting |
| title_fullStr |
From higher-order to first-order rewriting |
| title_full_unstemmed |
From higher-order to first-order rewriting |
| title_sort |
from higher-order to first-order rewriting |
| url |
http://hdl.handle.net/20.500.12110/paper_03029743_v2051LNCS_n_p47_Bonelli |
| work_keys_str_mv |
AT bonellie fromhigherordertofirstorderrewriting AT kesnerd fromhigherordertofirstorderrewriting AT riosa fromhigherordertofirstorderrewriting |
| _version_ |
1782028142255276032 |