Syntactic Theories in Practice

Authors

  • Olivier Danvy
  • Lasse R. Nielsen

DOI:

https://doi.org/10.7146/brics.v9i4.21721

Abstract

The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the contractum in the context. Directly implementing this evaluation function therefore yields an interpreter with a worst-case overhead, for each step, that is linear in the size of the input program. We present sufficient conditions over a syntactic theory to circumvent this overhead, by replacing the composition of (3) plugging and (1) decomposing by a single ``refocusing'' function mapping a contractum and a context into a new context and a new redex, if there are any. We also show how to construct such a refocusing function, we prove its correctness, and we analyze its complexity.

We illustrate refocusing with two examples: a programming-language interpreter and a transformation into continuation-passing style. As a byproduct, the time complexity of this program transformation is mechanically changed from quadratic in the worst case to linear.

Downloads

Published

2002-01-05

How to Cite

Danvy, O., & Nielsen, L. R. (2002). Syntactic Theories in Practice. BRICS Report Series, 9(4). https://doi.org/10.7146/brics.v9i4.21721