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.