Syntactic Theories in Practice

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 result in the context. Directly implementing this evaluation function therefore yields an interpreter with a quadratic time factor over its input. We present sufficient conditions over a syntactic theory to circumvent this quadratic factor, and illustrate the method with two programming-language interpreters and a transformation into continuation-passing style (CPS). In particular, we mechanically change the time complexity of this CPS transformation from quadratic to linear.