TY - GEN
T1 - A strong distillery
AU - Accattoli, Beniamino
AU - Barenbaum, Pablo
AU - Mazza, Damiano
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015/1/1
Y1 - 2015/1/1
N2 - Abstract machines for the strong evaluation of λ-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.
AB - Abstract machines for the strong evaluation of λ-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.
U2 - 10.1007/978-3-319-26529-2_13
DO - 10.1007/978-3-319-26529-2_13
M3 - Conference contribution
AN - SCOPUS:84952332721
SN - 9783319265285
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 231
EP - 250
BT - Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Proceedings
A2 - Park, Sungwoo
A2 - Feng, Xinyu
PB - Springer Verlag
T2 - 13th Asian Symposium on Programming Languages and Systems, APLAS 2015
Y2 - 30 November 2015 through 2 December 2015
ER -