|
Descripción
|
|
|---|---|
| Nominal rewriting is based on the observation that if we add support for α-equivalence to first-order syntax using the nominal-set approach, then systems with binding, including higher-order reduction schemes such as λ-calculus beta-reduction, can be smoothly represented. Nominal rewriting maintains a strict distinction between variables of the object-language (atoms) and of the meta-language (variables or unknowns). Atoms may be bound by a special abstraction operation, but variables cannot be bound, giving the framework a pronounced first-order character, since substitution of terms for variables is not capture-avoiding. We show how good properties of first-order rewriting survive the extension, by giving an efficient rewriting algorithm, a critical pair lemma, and a confluence theorem for orthogonal systems. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
INFORM COMPUT |
|
ISSN
|
0890-5401 |
|
Factor de impacto JCR
|
0,983 |
|
Información de impacto
|
|
|
Volumen
|
205 |
|
DOI
|
|
|
Número de revista
|
6 |
|
Desde la página
|
917 |
|
Hasta la página
|
965 |
|
Mes
|
SIN MES |
|
Ranking
|
|