# How to prove a property of the Lawvere theory for global state

In the field of algebraic computational effects, there is a Lawvere theory for global binary state (taking value either $0$ or $1$) which is generated by three operations

• $get: 2 \to 1$
• $put_0: 1 \to 1$
• $put_1: 1 \to 1$

subject to three natural equations which are specified in Notions of Computation Determine Monads. (I am only considering one store location and a binary variable, so my equations are fewer and simpler than in that paper.) The equations are more conveniently drawn than written:

It is more natural to interpret the equations from bottom to top. Respectively, they specify that

• putting $b$ and then putting $a$ is the same as just putting $a$
• getting the state, then putting $0$ if it was $0$, and $1$ if it was $1$ (before continuing along a joint path) is the same as doing nothing
• getting the state, and then getting the state again, is the same as just getting the state (and you can't get $0$ followed by $1$ or vice versa).

I can prove some simple and natural properties of this Lawvere theory, such as "getting the state, then putting $0$ if it was $0$, and $1$ if it was $1$ before continuing along a separate paths is the same as just getting the state". However I cannot prove equality between the two following diagrams:

This is roughy interpreted as "putting $0$ (resp. $1$) followed by getting" is the same as just "putting $0$ (resp. $1$) and following the left path (resp. right path)".

This seems to me an obvious relation in the theory for state, but I cannot manage to prove it! One of the following must hold

• I have misinterpreted the equations for state
• I have misinterpreted the true meaning of the equation I am trying to prove
• I am missing a simple trick for proving the equation from the state axioms

Can someone help me out? Thanks!

-
I assume you're referring to axioms (1-7) on page 7? I think that there are four axioms (1-4) relevant to you, not 3. Their axiom 1 is your second equation. Axiom 2 is your third equation. Axiom 3 is your first equation, and Axiom 4 is an equation that roughly says "Putting 0 (resp 1) then getting and branching on the result" is the same as "Putting 0 (resp 1) and following the left (resp right) path". – Chris Taylor Jul 28 '12 at 13:57
Chris, you're absolutely right! Thanks for that. – Tom Ellis Jul 28 '12 at 17:44