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


Dyk ned i forskningsemnerne om 'From Outermost Reduction Semantics to Abstract Machine'. Sammen danner de et unikt fingeraftryk.