逆、迭代与双刃并用之道

不起眼的$\dagger$（“dagger”）在范畴论中用于表示两种不同的运算：取态射的伴随（在dagger范畴中）与求泛函的最小不动点（在由域富集的范畴中）。尽管这两种运算通常被视为彼此独立，但可逆计算概念的出现表明有必要考量二者应当如何相互作用。在本文中，我们同时挥舞这两把dagger，考察由域富集的dagger范畴。我们发展了单调dagger结构的概念，作为一种相对于富集表现良好的dagger结构，并证明此类结构会带来由此产生的不动点所具有的良好逆性质。值得注意的是，此类结构保证了不动点伴随的存在，我们证明它们与富集中一个典范对合幺半结构所产生的共轭密切相关。最后，我们将这些结果关联到可逆编程语言设计与语义中的应用。