From Outermost Reduction Semantics to Abstract Machine

Publikation: Bog/antologi/afhandling/rapportRapportForskning

Reduction semantics is a popular format for small-step operational seman-
tics of deterministic programming languages with computational eects.
Each reduction semantics gives rise to a reduction-based normalization
function where the reduction sequence is enumerated. Refocusing is a
practical way to transform a reduction-based normalization function into
a reduction-free one where the reduction sequence is not enumerated. This
reduction-free normalization function takes the form of an abstract ma-
chine that navigates from one redex site to the next without systematically
detouring via the root of the term to enumerate the reduction sequence,
in contrast to the reduction-based normalization function.
We have discovered that refocusing does not apply as readily for re-
duction semantics that use an outermost reduction strategy and have
overlapping rules where a contractum can be a proper subpart of a redex.
In this article, we consider such an outermost reduction semantics with
backward-overlapping rules, and we investigate how to apply refocusing
to still obtain a reduction-free normalization function in the form of an
abstract machine.
ForlagDepartment of Computer Science, University of Aarhus
Antal sider23
ISBN (Trykt)978-87-7507-311-5
StatusUdgivet - 2015

Bibliografisk note

Extended version of:
Olivier Danvy and Jacob Johannsen. From outermost reduction semantics
to abstract machine. In Gopal Gupta and Ricardo Pe~na, editors, Logic
Based Program Synthesis and Transformation, 23rd International Sym-
posium, LOPSTR 2013, revised selected papers, number 8901 in Lecture
Notes in Computer Science, pages 91{108, Madrid, Spain, September 2013.

Se relationer på Aarhus Universitet Citationsformater

ID: 86781884