Memorias de investigación
Ponencias en congresos:
A Syntactic and Functional Correspondence between Reduction Semantics and Reduction-Free Full Normalisers
Año:2013
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
Descripción
Olivier Danvy and others have shown the syntactic correspondence between reduction semantics (a small-step semantics) and abstract machines, as well as the functional correspondence between reduction-free normalisers (a big-step semantics) and abstract machines. The correspondences are established by program transformation (so-called interderivation) techniques. A reduction semantics and a reduction-free normaliser are interderivable when the abstract machine obtained from them is the same. However, the correspondences fail when the underlying reduction strategy is hybrid, i.e., relies on another sub-strategy. Hybridisation is an essential structural property of full-reducing and complete strategies. Hybridisation is unproblematic in the functional correspondence. But in the syntactic correspondence the refocusing and inlining-of-iterate-function steps become context sensitive, preventing the refunctionalisation of the abstract machine. We show how to solve the problem and showcase the interderivation of normalisers for normal order, the standard, full-reducing and complete strategy of the pure lambda calculus. Our solution makes it possible to interderive, rather than contrive, full-reducing abstract machines. As expected, the machine we obtain is a variant of Pierre Crégut's full Krivine machine KN.
Internacional
Si
Nombre congreso
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
Tipo de participación
960
Lugar del congreso
Roma, Italia
Revisores
Si
ISBN o ISSN
978-14-5031-842-6
DOI
10.1145/2426890.2426911
Fecha inicio congreso
21/01/2013
Fecha fin congreso
22/01/2013
Desde la página
107
Hasta la página
116
Título de las actas
PEPM '13 Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation
Esta actividad pertenece a memorias de investigación
Participantes
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa