Just-in-time : on strategy annotations

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.