Distilling abstract machines

DOI10.1145/2628136.2628154MaRDI QIDQ2819700zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza

Publication date 29 September 2016

Published in Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1406.2370

zbMATH Keywords

abstract machinescall-by-needexplicit substitutionslambda-calculuslinear head reductionlinear logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.

Recommendations

• Abstracting abstract machines
• Systematic abstraction of abstract machines
• Optimizing abstract abstract machines
• A generative methodology for the design of abstract machines
• scientific article; zbMATH DE number 1751214
• scientific article; zbMATH DE number 1760142
• scientific article; zbMATH DE number 1823194
• scientific article; zbMATH DE number 1748284
• Deriving a lazy abstract machine

Cited in

(34)

• A generative methodology for the design of abstract machines
• The spirit of node replication
• (In)efficiency and reasonable cost models
• On the value of variables
• Classical by-need
• Reasoning about call-by-need by means of types
• The useful MAM, a reasonable implementation of the strong -calculus
• Unification for -calculi without propagation rules
• A strong distillery
• The dynamic geometry of interaction machine: a token-guided graph rewriter
• The Negligible and Yet Subtle Cost of Pattern Matching
• A Fresh Look at the λ-Calculus
• Abstract machines, optimal reduction, and streams
• scientific article; zbMATH DE number 7204428 (Why is no real title available?)
• Abstracting abstract machines
• The York Abstract Machine
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Node Replication: Theory And Practice
• A strong bisimulation for a classical term calculus
• Reasonable space for the -calculus, logarithmically
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Preorder-constrained simulations for program refinement with effects
• A fresh inductive approach to useful call-by-value
• IMELL cut elimination with linear overhead
• Mirroring call-by-need, or values acting silly
• Adjoint natural deduction
• Optimizing a non-deterministic abstract machine with environments
• A robust graph-based approach to observational equivalence
• Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
• Reasonable space for the -calculus, logarithmically
• Mirroring call-by-need, or values acting silly
• A syntactic correspondence between context-sensitive calculi and abstract machines
• Proof nets and the call-by-value \(\lambda\)-calculus
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion

This page was built for publication: Distilling abstract machines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819700)