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) λ-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, 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 β-steps.
On the relative usefulness of fireballs / Accattoli, Beniamino; SACERDOTI COEN, Claudio. - ELETTRONICO. - (2015), pp. 7174877.141-7174877.155. (Intervento presentato al convegno 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 tenutosi a Grand Prince Hotel, jpn nel 2015) [10.1109/LICS.2015.23].
On the relative usefulness of fireballs
ACCATTOLI, BENIAMINO;SACERDOTI COEN, CLAUDIO
2015
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) λ-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, 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 β-steps.File | Dimensione | Formato | |
---|---|---|---|
Accattoli,SacerdotiCoen-OntheUsefulnessofFireballs.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per accesso libero gratuito
Dimensione
1.19 MB
Formato
Adobe PDF
|
1.19 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.