From Outermost Reduction Semantics to Abstract Machine

Research output: Book/anthology/dissertation/reportReportResearch

Reduction semantics is a popular format for small-step operational semantics of deterministic programming languages with computational effects.
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 machine 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 reduction 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.
Original languageEnglish
PublisherDepartment of Computer Science, University of Aarhus
Number of pages23
ISBN (Print)978-87-7507-311-5
DOIs
Publication statusPublished - 2015

See relations at Aarhus University Citationformats

ID: 86781884