**Semantics 2 (Excerpt from the operational semantics of rewriting
with the on-demand E-strategy).**
** ceq** *eval*(*T*,
TRS) = *T* **if** *eval?*(*T*) .
** ceq** *eval*(*T*,
TRS) = *reduce*(*T*, *strat*(*T*, *sig*(*TRS*)),
*TRS*)
**if** *not* *eval?*(*T*) .
** eq** *reduce*(*T*,
*nil*,
*TRS*)
= *setEFlag*(*T*) .
** eq** *reduce*(*T*,
(0 *LS*), *TRS*) = *reduce2*(match(rules(*TRS*), *T*,
*TRS*),
*LS*,
*TRS*) .
** eq** *reduce*(*T*,
(*PI* *LS*), *TRS*) = *reduce*(*evalArg*(*T*,
*PI*,
*TRS*),
*LS*, *TRS*) .
** ceq** *reduce*(*T*,
(*NI* *LS*), *TRS*) = *reduce*(*upODF*(*T*,
(- *NI*)), *LS*, *TRS*) **if** *NI*
< 0 .
** eq** *reduce2*(`<`*trueT*
`>`, *LS*, *TRS*) = *eval*(*T*,
*TRS*)
.
** eq** *reduce2*(`<`*falseT*
`>`, *LS*, *TRS*) = *reduce*(*T*,
*LS*,
*TRS*)
.

Clearly the only difference between Semantics1
and Semantics2 is the fourth equation for
*reduce*
of Semantics2. If the top of the local strategy
given to a term
**T** is a negative integer *NI*, the operator
*upODF*
marks an on-demand flag on each subterm in the -*NI*th argument of
*T*. In Semantics1, if there is no rewrite
rule whose left side matches with a term, the second element of the pair
returned by *match* is exactly the same as the term passed to *match*
as its second argument. In Semantics2, however,
the second element of the pair returned by *match* might be different
from the term passed to *match* as its second argument because some
subterms in the term might be rewritten while *match* tries to match
the term with the left sides of rewrite rules.

Since terms might be rewritten while *match* tries to match them
with the left sides of rewrite rules, we should write the operational semantics
of pattern matching (i.e. *match*) in more detail in order to specify
the operational semantics of rewriting with the on-demand E-strategy more
precisely. Therefore we present the operational semantics of *match*.

**Semantics 3 (Operational semantics of match).**
** eq** *match*(*nil*,
*T*,
*TRS*) = `<` *false* *T* `>` .
** eq** *match*((*RRRRs*),
*T*, *TRS*) = *match2*(*pm*(*T*,
*lhs*(*RR*),
*TRS*), (*RR* *RRs*), *TRS*) .
** eq** *match2*(`<`*true*
*S* *T* `>`, (*RR* *RRs*), *TRS*) = `<`
*true* *instantiate*(*rhs*(*RR*), *S*)
`>`
.
** eq** *match2*(`<`*false*
*S* *T* `>`, (*RR* *RRs*), *TRS*) = *match*(*RRs*,
*T*, *TRS*) .

The operator *match* takes a list of rewrite rules, a term that
is tried to be matched with the left sides, and a TRS. It returns the pair
of
*true* and a contractum if there exists a rewrite rule whose left
side can match with the term, or otherwise it returns the pair of *false*
and the term passed to *match* as its second argument that might be
rewritten. The operator *pm* actually tries to match a term with the
left side of a rewrite rule. It takes a term, the left side of a rewrite
rule and a TRS, and returns the triple of *true*, the substitution
obtained through the pattern match and the term that might be rewritten
if the term can match with the left side, or otherwise it returns the triple
of *false*, a dummy substitution and the term that might be rewritten.
The auxiliary operator *match2* returns the pair of *true* and
the corresponding instance of the right side (i.e. the contractum) if the
term can match with the left side of the rewrite rule, or otherwise it
calls *match* in order to try to match the term with the remainder
of the rewrite rules. We present the operational semantics of *pm*
that tries to match a term with the left side of a rewrite rule.

**Semantics 4 (Operational semantics of pm)**
** eq** *pm*(*T*,
(*var* *V*), *TRS*) = `<` *true* (`<`(*var*
*V*) *T* `>` *nil*) *T* `>` .
** ceq** *pm*(*T*,
*Sym*{*Ps*, *TRS*) = *pml*(*nil*, 1, *T*,
*Sym*{*Ps*, *TRS*) **if** top(*T*) == *Sym*
.
** ceq** *pm*(*T*,
*Sym*{*Ps*, *TRS*) = *pm*(*eval*(*downODF*(*T*),
*TRS*), *Sym*{*Ps*, *TRS*) **if** *top*(*T*)
=/= *Sym* *and* *upODF?*(*T*) .
** ceq** *pm*(*T*,
*Sym*{*Ps*, *TRS*) = `<` *false* *nil*
*T* `>` **if** *top*(*T*) =/= *Sym*
*and* (*not* *upODF?*(*T*)) .
** ceq** *pml*(*S*,
*N*, *T*, *P*, *TRS*) = *pml2*(*pm*(*arg*(*T*,
*N*), *arg*(*P*, *N*), *TRS*), *S*, *N*,
*T*, *P*, *TRS*) **if** *N* <= *arity*(*T*,
*sig*(*TRS*)) .
** ceq** *pml*(*S*,
*N*, *T*, *P*, *TRS*) = `<` *true* *S*
*T* `>` **if** *N* > *arity*(*T*, *sig*(*TRS*))
.
** eq** *pml2*(`<`
*true* *S1* *T1* `>`, *S*, *N*, *T*,
*P*, *TRS*) = *pml*(*S1* ++ *S*, *N* + 1,
*replace*(*T*, *N*, *T1*), *P*, *TRS*) .
** eq** *pml2*(`<`
*false* *S1* *T1* `>`, *S*, *N*, *T*,
*P*, *TRS*) = `<` *false* *nil* *replace*(*T*,
*N*, *T1*) `>` .

There are two types of constructors *var*_ and _{_} for patterns
(i.e. the left and right sides of rewrite rules). The first constructor
*var*_
is one for variables. It takes a string as its argument that denotes a
variable name, e.g. *var* "X" denotes a variable *X*. The second
constructor _{_} is one for non-variable patterns such as *tp*(*cons*(*X*,
*L*)).
It takes a string and a list of patterns as its first and second arguments.
The string and the list denote the top function symbol name and the arguments
of a pattern, e.g. "tp"{("cons"{(* var* "X") (* var* "L") *nil*})
*nil*} denotes the pattern
*tp*(*cons*(*X*,
*L*)).

If the pattern is a variable *var* *V*, *pm* returns
the triple of
*true*, the pair of the variable and the term *T*
(more precisely the singleton list of the pair denoting a substitution),
and the term. If the pattern is a non-variable one *Sym*{*Ps*},
the situation divides into three cases. If the top function symbol of the
term *T* is equal to
*Sym* the top function symbol of the pattern,
*pml*
tries to match the arguments of the term with those of the pattern. The
next case is the most interesting in rewriting with the on-demand E-strategy.
If the top function symbol of the term is not seemingly equal to *Sym*
but the term has been marked with an on-demand flag, *eval* evaluates
the term after removing the on-demand flag from it, and then *pm*
retries to match the term that might have been rewritten with the pattern.
No removing the on-demand flag may lead to an infinite loop. If the top
function symbol of the term is not equal to *Sym* and the term has
not been marked with an on-demand flag, *pm* returns the triple of
*false*,
the empty substitution *nil* and the term, which means failure in
the pattern match.

The operator *pml* tries to match the arguments of a term with
those of a pattern and returns the triple of *true*, the substitution
obtained through the pattern match and the term that might be rewritten,
which means success in the pattern matching, if each of the arguments of
the term can match with each of them of the pattern. The reason why the
*N*th
argument of the term *T* is replaced by *T1* at the right sides
of the two rewrite rules for *pml2* is that the argument might have
been rewritten through the pattern match.