A simple kind of strategy annotations is investigated, giving rise to a class of strategies, including leftmost-innermost. It is shown that under certain restrictions, an interpreter can be written which computes the normal form of a term in a bottom-up traversal. The main contribution is a correctness proof of this interpreter. Furthermore, a default strategy is provided, called just-in-time, which satisfies the criteria for the interpreter. The just-in-time strategy has a better termination behaviour than innermost rewriting for many interesting examples.

, , ,
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

van de Pol, J. (2001). Just-in-time : on strategy annotations. Software Engineering [SEN]. CWI.