2026-07-23T05:30:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10515 2024-03-06T10:46:07Z ddc:004 open_access

Deriving an Abstract Machine for Strong Call by Need Biernacka, Małgorzata Charatonik, Witold abstract machines reduction semantics Strong call by need is a reduction strategy for computing strong normal forms in the lambda calculus, where terms are fully normalized inside the bodies of lambda abstractions and open terms are allowed. As typical for a call-by-need strategy, the arguments of a function call are evaluated at most once, only when they are needed. This strategy has been introduced recently by Balabonski et al., who proved it complete with respect to full beta-reduction and conservative over weak call by need. We show a novel reduction semantics and the first abstract machine for the strong call-by-need strategy. The reduction semantics incorporates syntactic distinction between strict and non-strict let constructs and is geared towards an efficient implementation. It has been defined within the framework of generalized refocusing, i.e., a generic method that allows to go from a reduction semantics instrumented with context kinds to the corresponding abstract machine; the machine is thus correct by construction. The format of the semantics that we use makes it explicit that strong call by need is an example of a hybrid strategy with an infinite number of substrategies. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Małgorzata Biernacka and Witold Charatonik 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.8 urn:nbn:de:0030-drops-105159 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.8 eng https://creativecommons.org/licenses/by/3.0/legalcode