imperative language: denotate assignment

Requirements

Assignment is only possible with some way to persist the name-value binding. We can do this via a store.

When we perform assignment, the new store is no longer the same as the previous store, so we denote it as such:

∑ -> ∑'
   ^-------- assignment occurs, e.g. x=1

As such we preserve referential transparency laws:

  1. Any name in a given environment (inclusive of store, ∑) evaluates to the same value.
  2. Any expression in a given environment (inclusive of store, ∑) evaluates to the same value.
logo