Syntactic Theories in Practice
Olivier Danvy, Lasse R. Nielsen · Electronic Notes in Theoretical Computer Science · 2001
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 result 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, and illustrate the method with an interpreter for the call-by-value λ-calculus and a transformation into continuation-passing style (CPS). In particular, we mechanically change the time complexity of this CPS transformation from potentially quadratic to linear. An extended version is available as the technical report BRICS RS-01-03 [4].