Global State（ストレージ）を特徴付ける7つの公理

http://hal.inria.fr/docs/00/70/20/65/PDF/segal.pdf より、

• 1. annihilation lookup - update:
  reading the value of a location loc and then updating the location loc with the obtained value is just like doing nothing.
• 2. interaction lookup - lookup:
  reading twice the same location loc is the same as reading it once.
• 3. interaction update - update:
  storing a value val and then a value val' at the same location loc is just like storing the value val' in the location.
• 4. interaction update - lookup:
  when one stores a value val in a location loc and then reads the location loc, one gets the value val.
• 5. commutation lookup - lookup:
  The order of reading two different locations loc and loc' does not matter.
• 6. commutation update - update: the order of storing in two different locations loc and loc' does not matter.
• 7. commutation update - lookup:
  the order of storing in a location loc and reading in a location loc' does not matter.

Gordon Plotkin and John Power "Notions of Computation Determine Monads" （http://homepages.inf.ed.ac.uk/gdp/publications/Comp_Eff_Monads.pdf）の7ページに等式的にまとめてある。が、この等式系は分かりにくいと思う。