Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
A Syntactic and Functional Correspondence between Reduction Semantics and Reduction-Free Full Normalisers
Year:2013
Research Areas
  • Information technology and adata processing
Information
Abstract
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.
International
Si
Congress
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
960
Place
Roma, Italia
Reviewers
Si
ISBN/ISSN
978-14-5031-842-6
10.1145/2426890.2426911
Start Date
21/01/2013
End Date
22/01/2013
From page
107
To page
116
PEPM '13 Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation
Participants
  • Autor: Alvaro Garcia Perez (UPM)
  • Autor: Pablo Nogueira Iglesias (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2019 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)