通过抽象重写系统实现部分单子作用的全球化

我们研究了通过关联重写系统 $(X_M^+,\to)$ 对单子 $M$ 在半群 $X$ 上强部分作用 $\alpha$ 的全球化问题。我们证明 $(X_M^+,\to)$ 的局部合一性足以保证 $\alpha$ 的可全局化，但与群的情况不同，此条件并非必要。聚焦于单子 $M=G^0$（其中 $G$ 为群），我们得到 $\alpha$ 可全局化以及 $(X_M^+,\to)$ 局部合一的显式判据。此外，本文给出了若干应用：关于单子 $M=\{0,1\}$ 在半群和代数上的强部分作用，以及关于任意单子 $M$ 在左零和空半群上的强部分作用的可全局化结果。