Go backward to Example Go up to Top Go forward to Non-Communicating Commands

Retaining Multiple Stores

E[[E₁ + E₂]] = lambda s.E[[E₁]]s plus E[[E₂]]s

• E uses store s in "read only" mode.
• No second store required for implementation.

E[[begin C return E]] =
    lambda s. let s' = C[[C]]s in E[[E]]s'

• Side effects in expression evaluation possible.
• Multiple stores required for implementation.

E[[E₁ + E₂]] = lambda s. let (v',s') = E[[E₁]]s
    (v",s") = E[[E₂]]s'
    in (v' plus v", s")
E[[begin C return E]] =
    lambda s. let s' = C[[C]]s in (E[[E]]s', s')

• Local updates remain in global store.
• Expression evaluation returns new store.