ch:dijkstra-monads: Dijkstra monads

Let $P$ be the successful postcondition on $(\mathsf{unit},s_1)$ and $Q$ the exceptional postcondition on $(\mathsf{negative},s_1)$. The program reads $s_0$; if it raises, and otherwise it writes $s_0+1$. Expanding get, bind, raise, and put gives Thus the negative branch requires exactly $Q(\mathsf{negative},s_0)$, retaining the failing state, while the nonnegative branch requires exactly $P(\mathsf{unit},s_0+1)$.

Let $\mathsf{incr}\mathsf{2}$ sequence $\mathsf{incr}$ twice. Two applications of WP-Bind, followed by the get and put clauses, calculate Advertise $$w_a(p)(s_0)=\mathrm{\forall }{s}_2.s_2=s_0+2\Rightarrow p(\mathsf{unit},s_2).$$ Rule WP-Sub asks for $\mathrm{\forall }p,s_0.w_a(p)(s_0)\Rightarrow w_2(p)(s_0)$. Given its antecedent, instantiate $s_2$ with $s_0+2$, use reflexivity of equality, and obtain $p(\mathsf{unit},s_0+2)$, which is the calculated consequent.

Fix a result type $A$, a state $s_0:S$, and a postcondition $p:A\times S\to \mathsf{U}$. For a state transformer $w$, right identity is For $w:{\mathsf{WP}}_{\mathsf{St}}(A)$, $k:A\to {\mathsf{WP}}_{\mathsf{St}}(B)$, and $h:B\to {\mathsf{WP}}_{\mathsf{St}}(C)$, fix $q:C\times S\to \mathsf{U}$. Then Extensionality in $q$ and $s_0$ yields the two transformer equations.

In the state-preserving semantics, $\mathsf{raise}(e)(p)(q)(s_1)=q(e,s_1)$. In the rollback semantics a computation also receives its entry state $s_0$, and failure uses $q(e,s_0)$, discarding the state at the point of failure. Start at zero and run $\mathsf{put}(1);\mathsf{raise}(e)$. The preserving transformer produces $q(e,1)$, while the rollback transformer produces $q(e,0)$. Choose $q(e^{\prime },s):=(e^{\prime }=e\wedge s=1)$. The preserving precondition is true and the rollback precondition is false. Therefore the transformers are not extensionally equal, and the generated bind/catch laws of one semantics cannot be transferred without replacing the failure rule.