[PRL] [1406.2370] Distilling Abstract Machines (Long Version)

[Mitchell Wand]

Exploring the relationship between explicit substitutions and environment
machines...
I wonder how much of this applies to Dave/Matt/Ian AAMs?

Distilling Abstract Machines (Long Version)
Beniamino Accattoli
<http://arxiv.org/find/cs/1/au:+Accattoli_B/0/1/0/all/0/1>, Pablo Barenbaum
<http://arxiv.org/find/cs/1/au:+Barenbaum_P/0/1/0/all/0/1>, Damiano Mazza
<http://arxiv.org/find/cs/1/au:+Mazza_D/0/1/0/all/0/1>
(Submitted on 9 Jun 2014)

It is well-known that many environment-based abstract machines can be seen
as strategies in lambda calculi with explicit substitutions (ES). Recently,
graphical syntaxes and linear logic led to the linear substitution calculus
(LSC), a new approach to ES that is halfway between big-step calculi and
traditional calculi with ES. This paper studies the relationship between
the LSC and environment-based abstract machines. While traditional calculi
with ES simulate abstract machines, the LSC rather distills them: some
transitions are simulated while others vanish, as they map to a notion of
structural congruence. The distillation process unveils that abstract
machines in fact implement weak linear head reduction, a notion of
evaluation having a central role in the theory of linear logic. We show
that such a pattern applies uniformly in call-by-name, call-by-value, and
call-by-need, catching many machines in the literature. We start by
distilling the KAM, the CEK, and the ZINC, and then provide simplified
versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we
also introduce some new machines with global environments. Moreover, we
show that distillation preserves the time complexity of the executions,
i.e. the LSC is a complexity-preserving abstraction of abstract machines.

Comments:63 pagesSubjects:Programming Languages (cs.PL)Cite as:
arXiv:1406.2370 <http://arxiv.org/abs/1406.2370> [cs.PL] (or
arXiv:1406.2370v1 <http://arxiv.org/abs/1406.2370v1> [cs.PL] for this
version)

http://arxiv.org/abs/1406.2370
-------------- next part --------------
HTML attachment scrubbed and removed