Relating higher-order and first-order rewriting

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, = φ)....

Descripción completa

Guardado en:
Detalles Bibliográficos
Publicado: 2005
Materias:
Explicit substitutions
First-order rewriting
Higher-order rewriting
Abstracting
Numerical methods
Parameter estimation
Equational theory
Encoding (symbols)
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p901_Bonelli
http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p901_Bonelli
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_0955792X_v15_n6_p901_Bonelli
record_format dspace
spelling paper:paper_0955792X_v15_n6_p901_Bonelli2023-06-08T15:55:54Z Relating higher-order and first-order rewriting Explicit substitutions First-order rewriting Higher-order rewriting Abstracting Numerical methods Parameter estimation Equational theory Explicit substitutions First-order rewriting Higher-order rewriting Encoding (symbols) 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. 2005 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p901_Bonelli http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p901_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 Explicit substitutions
First-order rewriting
Higher-order rewriting
Abstracting
Numerical methods
Parameter estimation
Equational theory
Explicit substitutions
First-order rewriting
Higher-order rewriting
Encoding (symbols)
spellingShingle Explicit substitutions
First-order rewriting
Higher-order rewriting
Abstracting
Numerical methods
Parameter estimation
Equational theory
Explicit substitutions
First-order rewriting
Higher-order rewriting
Encoding (symbols)
Relating higher-order and first-order rewriting
topic_facet Explicit substitutions
First-order rewriting
Higher-order rewriting
Abstracting
Numerical methods
Parameter estimation
Equational theory
Explicit substitutions
First-order rewriting
Higher-order rewriting
Encoding (symbols)
description 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.
title Relating higher-order and first-order rewriting
title_short Relating higher-order and first-order rewriting
title_full Relating higher-order and first-order rewriting
title_fullStr Relating higher-order and first-order rewriting
title_full_unstemmed Relating higher-order and first-order rewriting
title_sort relating higher-order and first-order rewriting
publishDate 2005
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p901_Bonelli
http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p901_Bonelli
_version_ 1768543285640429568

Ejemplares similares