nextupprevious
Next:Operational Semantics as Up:The On-demand E-strategyPrevious:Example Using the

Operational Semantics of the On-demand E-strategy

The following is an excerpt from the operational semantics of rewriting with the on-demand E-strategy in CafeOBJ.

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, TRSif  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 -NIth 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, TRSif top(T) == Sym .
        ceq pm(T, Sym{Ps, TRS) = pm(eval(downODF(T), TRS), Sym{Ps, TRSif 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, TRSif 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 Nth 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.
 


nextupprevious
Next:Operational Semantics as Up:The On-demand E-strategyPrevious:Example Using the


 


Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999