Context-sensitive rewriting techniques for programs with strategy annotations

Author

Salvador Lucas

Abstract

Strategy annotations have been used in a number of programming languages and rewriting-based systems (e.g., OBJ2, OBJ3, CafeOBJ, Maude, JITty, ...) for improving the termination behavior and avoiding useless computations. They also accomplish the important task of providing a simple interface for understanding and eventually modifying the execution of programs. They have been given different formats and operational interpretations: a recent classification distinguishes between E-strategies, just-in-time style, and laziness annotations. In all these cases, context-sensitive rewriting (CSR) provides a framework for analyzing and ensuring essential computational properties such as termination, correctness and completeness (regarding the usual semantics: head-normalization, normalization, functional evaluation, and infinitary normalization). Thus, CSR and its associated techniques provide a useful tool for the programmers and designers of software systems aimed at supporting the practical use of such programming languages and rewriting-based systems. In this paper, we summarize the main results and techniques regarding CSR, and exemplify their use with programs using strategy annotations.