 It is instructive to compare the actions of update semantics to programming statements and their execution. Such a comparison provides a first glimpse into how quantification works within a dynamic setting. Programming statements of imperative languages are interpreted (or “executed”) in the context of a machine state, where machine states can be viewed as allocations of values to registers. Assume the registers are named by variables \(x, y, z\), and that the contents of the registers are natural numbers. Then the following is a machine state: