A reduction strategy is a function that takes a set of rewrite rules and a ground term as arguments, and prescribes which redex in the term has to be rewritten next. Although lazy evaluation is fascinating because it has a better termination behavior than eager evaluation, pure lazy evaluation is not efficiently implementable. Therefore some efficiently implementable compromises between lazy and eager evaluation have been proposed. The on-demand evaluation strategy (abbr. the on-demand E-strategy) is one of them, which is used in CafeOBJ. The on-demand E-strategy is an extension of the evaluation strategy (abbr. the E-strategy) initiated by OBJ2. The E-strategy not only simulates a variant of lazy evaluation such as the functional strategy, but also is flexible because it can control the order in which terms are rewritten by giving a local strategy to each operator (or function symbol). However, it imposes a restriction on constructing rewrite rules: if non-variable terms are put on lazy positions in the left sides, some terms cannot be rewritten as intended. The on-demand E-strategy can remove this restriction of the E-strategy.
We have written the operational semantics of rewriting with the on-demand E-strategy so that we can deeply understand it. The operational semantics has been written in CafeOBJ, an executable algebraic specification language. The reason why we used CafeOBJ to write the operational semantics is that we can confirm the partial correctness of the specification with the CafeOBJ system and can also observe the dynamic behavior of rewriting with the on-demand E-strategy using the operational semantics as an interpreter. We believe that the formal operational semantics of rewriting with the strategy should be useful not only for making sure of what rewriting with the strategy performs, but also as a formal specification that can be used when implementing rewriting with the strategy.
The rest of the paper is organized as follows: Section2 gives a brief introduction to CafeOBJ. Section3 describes the E-strategy and the operational semantics of the E-strategy in CafeOBJ. In Sect.4, the restriction imposed by the E-strategy and the on-demand E-strategy that removes the restriction are first mentioned, and then an example that needs the on-demand E-strategy is given. After that the operational semantics of rewriting with the on-demand E-strategy in CafeOBJ is described and the dynamic behavior of rewriting with the strategy is observed. Section5 presents a hint about specifying local strategies. Section6 discusses the related work. Finally, Section7 gives a conclusion.
We suppose the reader familiar with the basic concepts of term rewriting systems (abbr. TRSs).