Shin-Cheng Mu. Tech. Report TR-IIS-19-002, Institute of Information Science, Academia Sinica, June 2019.
As part of the author’s studies on equational reasoning for monadic programs, this report focus on nondeterminism monad. We discuss what properties this monad should satisfy, what additional operators and
notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author’s previous work on proving properties of Spark aggregation.