|
Descripción
|
|
|---|---|
| We show how to connect the syntactic and the functional correspondence for normalisers and abstract machines implementing hybrid (or layered) reduction strategies, that is, strategies that depend on subsidiary sub-strategies. Many fundamental strategies in the literature are hybrid, in particular, many full-reducing strategies, and many full-reducing and complete strategies that deliver a fully reduced result when it exists. If we follow the standard program-transformation steps the abstract machines obtained for hybrids after the syntactic correspondence cannot be refunctionalised, and the junction with the functional correspondence is severed. However, a solution is possible based on establishing the shape invariant of well-formed continuation stacks. We illustrate the problem and the solution with the derivation of substitution-based normalisers for normal order, a hybrid, full-reducing, and complete strategy of the pure lambda calculus. The machine we obtain is a substitution-based, eval/apply, open-terms version of Pierre Crégut's full-reducing Krivine machine KN. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
Science of Computer Programming |
|
ISSN
|
0167-6423 |
|
Factor de impacto JCR
|
0,568 |
|
Información de impacto
|
Datos JCR del año 2012 |
|
Volumen
|
1776 |
|
DOI
|
|
|
Número de revista
|
|
|
Desde la página
|
|
|
Hasta la página
|
|
|
Mes
|
SIN MES |
|
Ranking
|
|