Loading ...
Loading ...
From Outermost Reduction Semantics to Abstract Machine

Publication Info

Added 2015-01-27
ISBN-13: 978-87-7507-311-5
Date of first publication: 2015-01-27
doi: 10.7146/aul.3.2

Related categories

From Outermost Reduction Semantics to Abstract Machine

Olivier Danvy, Jacob Johannsen (Author)

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.

About the Author: Olivier Danvy

No biography available at this time.

About the Author: Jacob Johannsen

No biography available at this time.

Open Monograph Press Public Knowledge Project

Aarhus University Library/State and University Library - AU Library Scholarly Publishing Services - E-books