Semantics of Rules

By induction on R , we define the update set = Updates(D, R, S) generated by a rule R at an appropriate state S under a declaration D that covers R . To fire R at S under D , fire .

We stipulate that an arbitrary rule R is equivalent, for given D and S , to a (D,S) -perspicuous rule R' obtained from R by renaming the bound variables. The equivalence means that Updates(D, R, S) = Updates(D, R', S).

It remains to define = Updates(D, R, S). in the case when R is (D,S) -perspicuous.

If D is not empty, then is the union of Updates(, R, S'), where S' ranges over expansions of S such that Fun(S') = Fun(S) Var(D) and S' is consistent with D (so that the values of D variables are within their ranges in S' ). Notice that if the range of any D variable is empty.

Suppose D = . If R is an update instruction then = Updates(R, S). If R is a sequence of rules , ..., , then is the union of the update sets Updates(, , S). Suppose that R is the conditional rule with clauses (,), ... , (,). . Since R is covered by the empty declaration, the guards have no free variables. We have two cases as usual. If all guards fail in S , then is empty, and if is the first guard that holds in S then = NUpdates (, , S). Finally, if R is a declaration rule with declaration d and body R' then = Updates(d, R', S).

• Remark