Unlocking Normal-Order Reduction: Krivine Machine KN Simulates Pure Reduction Step-by-Step 🧠

The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

More info about this talk: https://icfp20.sigplan.org/details/icfp-2020-papers/45/The-full-reducing-Krivine-abstract-machine-KN-simulates-pure-normal-order-reduction-i

Authors:
Álvaro García Perez, IMDEA Software Institute (presenting)
Pablo Nogueira, ESNE University School of Design, Innovation and Technology

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 alpha-conversion 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 full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.

This is an official ICFP 2020 talk video edited from an author-submitted video. Video captions supported by Jane Street. On a desktop browser, you can view captions without overlapping the video by clicking the three dots to the right of “Save” and clicking “Open transcript”.