Optimizing a Non-Deterministic Abstract Machine with Environments

Małgorzata Biernacka (1) , Dariusz Biernacki (1) , Sergueï Lenglet (2, 3, 4) , Alan Schmitt (5)

1 Uniwersytet Wroclawski = University of Wroclaw
2 MOSEL - Proof-oriented development of computer-based systems
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
4 LIPN - Laboratoire d'Informatique de Paris-Nord
5 EPICURE - Analyse sémantique et compilation pour la sécurité des environnements d'exécution

Non-deterministic abstract machine (NDAM) is a recent implementation model for programming languages where one must choose among several redexes at each reduction step, like process calculi. These machines can be derived from a zipper semantics, a mix between structural operational semantics and context-based reduction semantics. Such a machine has been generated also for the lambda-calculus without a fixed reduction strategy, i.e., with the full non-deterministic beta-reduction. In that machine, substitution is an external operation that replaces all the occurrences of a~variable at once. Implementing substitution with environments is more low-level and more efficient as variables are replaced only when needed. In this paper, we define a NDAM with environments for the lambda-calculus without a fixed reduction strategy. We also introduce other optimizations, including a form of refocusing, and we show that we can restrict our optimized NDAM to recover some of the usual $\lambda$-calculus machines, e.g., the Krivine Abstract Machine. Most of the improvements we propose in this work could be applied to other NDAMs as well.

Mots clés: Abstract machines; Explicit substitutions; Refocusing

Domaines: Théorie et langage formel [cs.FL]

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. 2024. ⟨hal-04568253⟩