
In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) $λ$-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.
Technical report for the LICS 2015 submission with the same title
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Cost Models, Abstract Machines, Lambda Calculus, Software; Mathematics (all), Logic in Computer Science (cs.LO)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Cost Models, Abstract Machines, Lambda Calculus, Software; Mathematics (all), Logic in Computer Science (cs.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 16 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
