非确定性单子的等式推理：Spark聚合的例子
Equational reasoning for non-determinism monad: the case of Spark aggregation
摘要：
作为作者关于单子程序的等式推理研究的一部分，本文主要研究非确定性单子程序。我们讨论这个单子应该满足什么属性，可以引入什么额外的操作符和符号，以促进关于非确定性的等式推理，并通过在我们的示例问题中证明一些属性来测试它们，这些问题的灵感来自于作者以前的工作证明Spark聚合的属性。
英文摘要：
As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
