一句话：从 gs-monoidal 范畴视角解释不动点检查技术，刻画其组合性并实现工具 UDEfix。
本文研究如何判定递归与循环定义所产生的不动点是否为最小或最大不动点，该问题普遍存在于互模拟、行为度量、马尔可夫链与随机博弈的终止概率等场景。作者将此前提出的“函数到近似”的不动点检查技术纳入范畴论框架，证明其可自然地用 gs-monoidal 范畴解释；进一步研究该映射的组合性，并在一定限制下将其解释为（lax）gs-monoidal 函子。基于该理论开发了工具 UDEfix，支持像搭电路一样由基本构件构造函数及其近似，并执行不动点检查。最后，通过轻微推广该理论，处理了基于 Wasserstein 提升的余代数行为度量这一新案例。
Fixpoints are ubiquitous in computer science as they play a central role in providing a meaning to recursive and cyclic definitions. Bisimilarity, behavioural metrics, termination probabilities for Markov chains and stochastic games are defined in terms of least or greatest fixpoints. Here we show that our recent work which proposes a technique for checking whether the fixpoint of a function is the least (or the largest) admits a natural categorical interpretation in terms of gs-monoidal categories. The technique is based on a construction that maps a function to a suitable approximation. We study the compositionality properties of this mapping and show that under some restrictions it can naturally be interpreted as a (lax) gs-monoidal functor. This guides the development of a tool, called UDEfix that allows us to build functions (and their approximations) like a circuit out of basic building blocks and subsequently perform the fixpoints checks. We also show that a slight generalisation of the theory allows one to treat a new relevant case study: coalgebraic behavioural metrics based on Wasserstein liftings.
@article{paperbot3397,
title = {A Monoidal View on Fixpoint Checks},
author = {Paolo Baldan and Richard Eggert and Barbara König and Timo Matt and Tommaso Padoan},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:5)2025}
}