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

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

Descripción

Título: A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers
Autor/es:
  • García-Pérez, Álvaro
  • Nogueira, Pablo
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: PEPM'13
Fechas del Evento: 21-22 Jan 2013
Lugar del Evento: Roma, Italia
Título del Libro: PEPM '13: proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation
Fecha: 2013
ISBN: 978-1-4503-1842-6
Materias:
Palabras Clave Informales: 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
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (962kB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 30253
Identificador DC: http://oa.upm.es/30253/
Identificador OAI: oai:oa.upm.es:30253
Identificador DOI: 10.1145/2426890.2426911
URL Oficial: http://dl.acm.org/citation.cfm?id=2426890.2426911
Depositado por: Memoria Investigacion
Depositado el: 26 Jun 2014 13:29
Ultima Modificación: 23 Nov 2017 10:22
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM