From Outermost Reduction Semantics to Abstract Machine

Forfattere

Olivier Danvy
Jacob Johannsen
Department of Computer Science, Aarhus University

Synopsis

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.

Forsidebillede til From Outermost Reduction Semantics to Abstract Machine
Publiceret
januar 27, 2015

Detaljer om denne monografi

ISBN-13 (15)
978-87-7507-311-5
Date of first publication (11)
2015-01-27
doi
10.7146/aul.3.2