2026-07-22T14:20:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20340 2024-07-05T06:20:34Z ddc:004 open_access

Optimizing a Non-Deterministic Abstract Machine with Environments Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Schmitt, Alan Abstract machine Explicit substitutions Refocusing 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 λ-calculus without a fixed reduction strategy, i.e., with the full non-deterministic β-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 λ-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 λ-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Małgorzata Biernacka and Dariusz Biernacki and Sergueï Lenglet and Alan Schmitt 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.11 urn:nbn:de:0030-drops-203409 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.11 eng https://creativecommons.org/licenses/by/4.0/legalcode