On the Relative Usefulness of Fireballs

DOI10.1109/LICS.2015.23MaRDI QIDQ4635799zbMATH OpenFDO

Authors Beniamino Accattoli, Claudio Sacerdoti Coen

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

finite automatafunctional programminglambda calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Abstract: In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) $lambda$-calculus into models like RAM machines which is polynomial in the number of $$-steps, answering a long-standing question. The key ingredient was the use of a calculus with useful sharing, a new notion whose complexity was shown to be polynomial, but whose implementation was not explored. This paper, meant to be complementary, studies useful sharing in a call-by-value scenario and from a practical point of view. We introduce the Fireball Calculus, a natural extension of call-by-value to open terms for which the problem is as hard as for the ordinary lambda-calculus. We present three results. First, we adapt the solution of Accattoli and Dal Lago, improving the meta-theory of useful sharing. Then, we refine the picture by introducing the GLAMoUr, a simple abstract machine implementing the Fireball Calculus extended with useful sharing. Its key feature is that usefulness of a step is tested---surprisingly---in constant time. Third, we provide a further optimization that leads to an implementation having only a linear overhead with respect to the number of $$-steps.

Recommendations

• Types of fireballs
• Generalized flame balls
• Interactions of flame balls
• Flame balls with thermally sensitive intermediate kinetics
• On self-drifting flame balls
• On self-drifting flame balls
• On the fluid mechanics of fires
• scientific article; zbMATH DE number 6303056

Cited in

(16)

• Eager functions as processes
• (In)efficiency and reasonable cost models
• On the value of variables
• The useful MAM, a reasonable implementation of the strong -calculus
• Open call-by-value
• The Negligible and Yet Subtle Cost of Pattern Matching
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• A Fresh Look at the λ-Calculus
• Deriving an abstract machine for strong call by need
• scientific article; zbMATH DE number 7204428 (Why is no real title available?)
• Types of fireballs
• Strong call-by-value and multi types
• Positive focusing is directly useful
• A fresh inductive approach to useful call-by-value
• IMELL cut elimination with linear overhead
• Optimizing a non-deterministic abstract machine with environments

This page was built for publication: On the Relative Usefulness of Fireballs

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