Transition Rules: Semantics

An import commands chooses an element of the reserve and removes it from the reserve. To clarify our intentions, we note that the non-perspicuous rule

import v
     Parent(v) := CurrentNode
endimport
import v
     Parent(v) := CurrentNode
endimport

creates two children of CurrentNode. In general, different choices from the reserve produce different elements.

For each rule R and every state S appropriate for R , we define an update set Updates(R,S) over S ; to fire R at S , fire Updates(R,S).

First, we consider the case of when R is S -perspicuous. Fix an injective map from Bound(R) to the reserve of the given S . (The injectivity means that assigns different elements to different bound variables.) By induction on subrule R' of R we define sets Updates(R',S',) where S' is an expansion of S appropriate for R' and such that R' is S'-perspicuous. (Recall that S' is an expansion of S if and only if the reduct of S' to Fun(S) equals S .) Let = Fun(S').

The cases of update instructions, sequence rules and conditional rules are treated as above. (Variables in are treated as nullary functions.) Suppose that R' is an import rule with main existential variable v and body . Let a = (v) and be the expansion of S' to the auxiliary vocabulary ' {v} where v is interpreted as a . Recall that variables are not subjects of update instructions. Thus Updates(, , ) is an update set over S' . Set Updates(R',S',) = { ( (Reserve,a), false)} Updates(, , ). Finally Updates(R,S) = Updates(R,S,). Of course, Updates(R,S) is not defined uniquely, because it depends on . It is easy to see, however, the resulting state is unique up to isomorphism.

Second, we stipulate that an arbitrary rule R is equivalent, over the given appropriate state S , to an S -perspicuous rule R' obtained from R by renaming the bound variables. (The desired R' can be obtained by iterating the following transformation: Select an innermost import subrule whose main existential variable v occurs in the rest of the rule or in Fun(S), and replace v with a fresh variable in .) The stipulation means the following: To fire R at S , fire R' at S .

• Discarding Elements from Universes