A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers

García-Pérez, Álvaro and Nogueira, Pablo (2013). A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers. In: "PEPM'13", 21-22 Jan 2013, Roma, Italia. ISBN 978-1-4503-1842-6. https://doi.org/10.1145/2426890.2426911.

Description

Title: A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers
Author/s:
  • García-Pérez, Álvaro
  • Nogueira, Pablo
Item Type: Presentation at Congress or Conference (Article)
Event Title: PEPM'13
Event Dates: 21-22 Jan 2013
Event Location: Roma, Italia
Title of Book: PEPM '13: proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation
Date: 2013
ISBN: 978-1-4503-1842-6
Subjects:
Freetext Keywords: Program transformation - Reduction-based normalization - Reduction-free normalization - Reduction semantics - Reduction ries - Evaluation contexts - Continuations - Continuation-passing style - CPS) - CPS transformation - Defunctionalization - Refunctionalization - Refocusing - Normalization by evaluation
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (962kB) | Preview

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.

More information

Item ID: 30253
DC Identifier: http://oa.upm.es/30253/
OAI Identifier: oai:oa.upm.es:30253
DOI: 10.1145/2426890.2426911
Official URL: http://dl.acm.org/citation.cfm?id=2426890.2426911
Deposited by: Memoria Investigacion
Deposited on: 26 Jun 2014 13:29
Last Modified: 23 Nov 2017 10:22
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM