Guarded Multi-updates

A multi-update instruction is a sequence of update instructions. A guarded update instruction (respectively, guarded multi-update instruction) is a rule of the form

if g then R endif

where R is an update (respectively, a multi-update) instruction.

Lemma 3.1 For every rule R, there is a sequence R' of guarded updates such that Fun(R') = Fun(R) and Updates(R',S) = Updates(R,S) for all appropriate states S.

For example, the rule

if FirstChild(c) <> undef then c := FirstChild(c)
elseif NextSib(c) <> undef then c := NextSib(c)
elseif Parent(c) <> undef then c := Parent(c)
endif

converts to the following sequence of guarded updates:

if FirstChild(c) <> undef then c := FirstChild(c) endif
if FirstChild(c) = undef and NextSib(c) <> undef
    then c := NextSib(c) 
endif
if FirstChild(c) = undef and NextSib(c) = undef and Parent(c) <> undef
    then c := Parent(c) 
endif

The Lemma suggests a simpler definition of rules. The reason for choosing the recursive definition is pragmatic. It is too tedious to write rules as sequences of guarded updates. It is feasible to write them as sequences of guarded multi-updates but it is more convenient and practical to use elseif clauses and nest conditionals. The pragmatic Occam's razor does not cut as much as the original Occam's razor would.

• Remark