Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement

For a programming language, there are two kinds of term rewriting: run-time rewriting ("evaluation") and compile-time rewriting ("refinement"). Whereas refinement resembles general term rewriting, evaluation is commonly constrained by Felleisen's evaluation contexts. While evaluation specifies a programming language, refinement models optimisation and should be validated with respect to evaluation. Such validation can be given by Sands' notion of contextual improvement. We formulate evaluation in a term-rewriting-theoretic manner for the first time, and introduce Term Evaluation and Refinement Systems (TERS). We then identify sufficient conditions for contextual improvement, and provide critical pair analysis for local coherence that is the key sufficient condition. As case studies, we prove contextual improvement for a computational lambda-calculus and its extension with effect handlers.