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.

Functional programming and lambda calculus (msc 68N18), Grammars and rewriting systems (msc 68Q42), Abstract data types; algebraic specification (msc 68Q65), Symbolic computation and algebraic computation (msc 68W30)
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

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