|
Syntactic Theories in Practice
Olivier Danvy
January 2002 |
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 Available as PostScript, PDF, DVI. |