一句话:用字符串重写与合流性刻画 monad 与伴随,简化 monad 复合验证。
本文关注范畴论构造,尤其是 monad 复合的验证问题。Eklund 等人曾提出图形化技巧来简化此类验证;作者转而采用字符串重写方法,将自然变换视为重写规则。论文证明:三元组 (T, μ, η) 构成 monad 当且仅当 T 是某个由字符串与重写规则构成的范畴中的终对象,并且这一事实可通过证明重写系统的合流性来建立。作者用 monad 复合问题说明该技术,并给出用重写范畴刻画伴随(adjunction)的方式。工作以理论证明和示例展示为主,未报告实现或实验评估。
Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.