Artículo
Foundations of strong call by need
Fecha de publicación:
08/2017
Editorial:
Association for Computing Machinery
Revista:
Proceedings of the ACM on Programming Languages
ISSN:
2475-1421
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to β-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the de nition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a β-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.
Palabras clave:
Evaluation Strategies
,
Call-By-Need
,
Completeness
,
Lambda Calculus
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(SEDE CENTRAL)
Articulos de SEDE CENTRAL
Articulos de SEDE CENTRAL
Citación
Balabonski, Thibaut; Barenbaum, Pablo; Bonelli, Eduardo Augusto; Kesner, Delia; Foundations of strong call by need; Association for Computing Machinery; Proceedings of the ACM on Programming Languages; 1; ICFP; 8-2017; 1-29; 20
Compartir
Altmétricas