2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2015)

Kyoto, Japan

July 6, 2015 to July 10, 2015

ISSN: 1043-6871

ISBN: 978-1-4799-8875-4

pp: 141-155

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2015.23

ABSTRACT

In CSL-LICS 2014, Accattoli and Dal Lago DBLP:conf/csl/AccattoliL14 showed that there is an implementation of the ordinary (i.e. Strong, pure, call-by-name) &#x03BB;-calculus into models like RAM machines which is polynomial in the number of &#x03B2;-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, that is an intermediary step towards the strong case, and we present three results. First, we adapt useful sharing, refining the meta-theory. Then, we introduce 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 optimisation that leads to an implementation having only a linear overhead with respect to the number of &#x03B2;-steps.

INDEX TERMS

Context, Calculus, Random access memory, Explosions, Polynomials, Complexity theory, Syntactics

CITATION

B. Accattoli and C. S. Coen, "On the Relative Usefulness of Fireballs,"

*2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, Kyoto, Japan, 2015, pp. 141-155.

doi:10.1109/LICS.2015.23

CITATIONS