Indexed Lawvere theories for local state
John Power · CRM proceedings & lecture notes · 2011
Monads for global state and local state have been used to provide semantics of programming languages for many years. There is a computation- ally natural presentation of an ordinary Lawvere theory that corresponds to the monad on Set for global state, inevitably called the Lawvere theory for global state. Here, we introduce a notion of indexed Lawvere theory and use it to give a Lawvere-style account of local state, extending the theorem for global state to local state. En route, we develop the notion of comodel of a Lawvere theory and exploit a universal characterisation of the category of worlds for local state. Ultimately, we give both syntactic and semantic characterisations of the operation block that allows one to move between worlds and use them to characterise the monad for local state.