dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Fix wording

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-29 20:36:51 +01:00
parent 754c3b823e
commit b2eb9334ca
1 changed files with 13 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
thesis.tex
View File

@@ -1226,23 +1226,25 @@ manipulating the state cell.
equations~\cite{Gibbons12}. equations~\cite{Gibbons12}.
% %
\begin{reductions} \begin{reductions}
\slab{Get\textrm{-}get} & \getF\,\Unit \bind (\lambda st. \getF\,\Unit \bind (\lambda st'.k~st~st')) &=& \getF \bind \lambda st.k~st~st\\
\slab{Get\textrm{-}put} & \getF\,\Unit \bind (\lambda st.\putF~st) &=& \Return\;\Unit\\ \slab{Get\textrm{-}put} & \getF\,\Unit \bind (\lambda st.\putF~st) &=& \Return\;\Unit\\
\slab{Put\textrm{-}put} & \putF~st \bind (\lambda st.\putF~st') &=& \putF~st'\\ \slab{Put\textrm{-}get} & \putF~st \bind (\lambda\Unit.\getF\,\Unit \bind (\lambda st.k~st') &=& \putF~st \bind (\lambda \Unit.k~st)\\
\slab{Put\textrm{-}get} & \putF~st \bind (\lambda\Unit.\getF\,\Unit) &=& \putF~st \bind (\lambda \Unit.\Return\;st) \slab{Put\textrm{-}put} & \putF~st \bind (\lambda st.\putF~st') &=& \putF~st' \bind (\lambda\Unit.k~st)
\end{reductions} \end{reductions}
% %
The first equation captures the intuition that getting a value and The first equation states that performing one get after another get
then putting has no observable effect on the state cell. The second is redundant. The second equation captures the intuition that
equation states that only the latter of two consecutive puts is getting a value and then putting has no observable effect on the
observable. The third equation states that performing a get state cell. The third equation states that performing a get
immediately after putting a value is equivalent to returning that immediately after putting a value is equivalent to returning that
value. value. The fourth equation states that only the latter of two
consecutive puts is observable.
\end{definition} \end{definition}
The literature often presents the state monad with a fourth equation, The literature often uses the presentation (or a similar one) with the
which states that $\getF$ is idempotent. However, this equation is four equations above, even though, there exists a smaller presentation
redundant as it is derivable from the first and third in which the first equation is redundant as it is derivable from the
equations~\cite{Mellies14}. second and third equations (c.f. Appendix~\ref{ch:get-get}).
We can implement a monadic variation of the $\incrEven$ function that We can implement a monadic variation of the $\incrEven$ function that
uses the state monad to emulate manipulations of the state cell as uses the state monad to emulate manipulations of the state cell as