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...

Descripción completa

Detalles Bibliográficos
Autor principal: Bonelli, Eduardo
Publicado: 2001
Materias:
Artificial intelligence
Computer science
Differentiation (calculus)
Equational theory
First-order rewriting
Higher-order
Higher-order rewriting
Extended abstracts
Lambda calculus
Calculations
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli
http://hdl.handle.net/20.500.12110/paper_03029743_v2051LNCS_n_p47_Bonelli
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_03029743_v2051LNCS_n_p47_Bonelli
record_format dspace
spelling paper:paper_03029743_v2051LNCS_n_p47_Bonelli2023-06-08T15:28:21Z From higher-order to first-order rewriting Bonelli, Eduardo 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. 2001 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli 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, Eduardo
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.
author Bonelli, Eduardo
author_facet Bonelli, Eduardo
author_sort Bonelli, Eduardo
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
publishDate 2001
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli
http://hdl.handle.net/20.500.12110/paper_03029743_v2051LNCS_n_p47_Bonelli
work_keys_str_mv AT bonellieduardo fromhigherordertofirstorderrewriting
_version_ 1768542987325800448

Ejemplares similares