Memorias de investigación
Research Publications in journals:
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
Year:2019

Research Areas
  • Information technology and adata processing

Information
Abstract
We exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut?s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ?correspond?, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ?index alignment?, ?parameters-as-levels? and ?balanced derivations?. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alphaconversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a fullreducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.
International
Si
JCR
Si
Title
Journal of Functional Programming
ISBN
0956-7968
Impact factor JCR
0,595
Impact info
Volume
29
10.1017/S0956796819000017
Journal number
From page
1
To page
38
Month
SIN MES
Ranking
Participants

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