一句话：提出单子重写的关系理论，识别弱笛卡尔单子与线性方程条件，并给出带代数效应的 CBV λ 演算的标准化与合流定理。
本文研究带效应程序语言的计算与重写语义：将归约本身视为具有单子效应的重写，提出单子重写系统的关系理论。作者指出，对分布、幂集、reader、全局状态等单子，直接定义有意义的重写并不平凡，因此追问何种条件下单子重写可行。方法上，他们识别出弱笛卡尔单子可保证单子重写具有良好性质；当单子由等式理论（如代数效应）给出时，证明所有等式线性是充分条件。最后将该抽象理论应用于带代数效应的 CBV λ 演算，得到带效应的表面标准化与合流定理。
Motivated by the study of effectful programming languages and computations, we introduce a relational theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, where effects are modelled as monads. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining meaningful notions of monadic rewriting turns out to problematic for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible. We answer that question by identifying a class of monads, known as weakly cartesian monads, that guarantee monadic rewriting to be well-behaved. In case monads are given as equational theories, as it is the case for algebraic effects, we also show that a sufficient condition to have a well-behaved notion of monadic rewriting is that all equations in the theory are linear. Finally, we apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining effectful (surface) standardisation and confluence theorems.