|
Descripción
|
|
|---|---|
| Two-level lambda-calculus is designed to provide a mathematical model of capturing substitution, also called instantiation. Instantiation is a feature of the `informal meta-level¿; it appears pervasively in specifications of the syntax and semantics of formal languages. The two-level lambda-calculus has two levels of variable. Lambda-abstraction and beta-reduction exist for both levels. A level 2 beta-reduct, triggering a substitution of a term for a level 2 variable, does not avoid capture for level 1 abstractions. This models meta-variables and instantiation as appears at the informal meta-level. In this paper we lay down the syntax of the two-level lambda-calculus; we develop theories of freshness, alpha-equivalence, and beta-reduction; and we prove confluence. In doing this we give nominal terms unknowns ¿ which are level 2 variables and appear in several previous papers ¿ a functional meaning. In doing this we take a step towards longer-term goals of developing a foundation for theorem-provers which directly support reasoning in the style of nominal rewriting and nominal algebra, and towards a mathematics of functions which can bind names in their arguments. | |
|
Internacional
|
Si |
|
JCR del ISI
|
No |
|
Título de la revista
|
Electronic Notes in Theoretical Computer Science |
|
ISSN
|
1571-0661 |
|
Factor de impacto JCR
|
0 |
|
Información de impacto
|
|
|
Volumen
|
246 |
|
DOI
|
|
|
Número de revista
|
0 |
|
Desde la página
|
107 |
|
Hasta la página
|
129 |
|
Mes
|
AGOSTO |
|
Ranking
|
|