Lazy evaluation is fascinating because it often has a better termination behavior than eager evaluation, while it is much more difficult to implement efficiently lazy evaluation than eager evaluation. Therefore some compromises have been proposed. The functional strategy[10] is one of them, which is often used in the field of the implementation of functional languages such as

Kamperman and Walters have proposed a transformation method for TRSs
and terms to be rewritten so that lazy evaluation can be simulated on an
implementation of eager evaluation: *lazy rewriting on eager machinery*[9].
The method concisely expresses the intricate interaction between pattern
matching and lazy evaluation. Our operational semantics concisely expresses
the same thing by the third equation for
*pm* in Semantics4,
viz if the top symbol of a term is not seemingly equal to that of a pattern
but the term has been marked with an on-demand flag, *pm* retries
to match the term with the pattern after evaluating the term.

We introduce two more examples of semantics written in formal languages.
One is the operational semantics of an organic programming language *GAEA*[5]
in *Maude*[3] a specification language
based on rewriting logic[11], and the other
the algebraic semantics of imperative programs in *OBJ3*[6].
Ishikawa et al.[8] have written the operational
semantics of *GAEA* in
*Maude* as an instance through a study
on declarative description of reflective concurrent systems. Goguen and
Malcolm[7] give the algebraic semantics
of imperative programs in *OBJ3* so as to introduce Computing Science
students to formal reasoning about imperative programs. They do not only
write the algebraic semantics of an imperative programming language, but
also prove assertions about the behavior of programs written in the imperative
programming language.

We introduce one more example of semantics written in formal languages.
Goguen and Malcolm[7] give the algebraic
semantics of imperative programs in *OBJ3* so as to introduce Computing
Science students to formal reasoning about imperative programs. They do
not only write the algebraic semantics of an imperative programming language,
but also prove assertions about the behavior of programs written in the
imperative programming language. In future we are going to verify some
properties of rewriting with the on-demand E-strategy with the operational
semantics.