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.

翻译：不动点在计算机科学中无处不在，它们在为递归和循环定义提供语义方面发挥着核心作用。互模拟、行为度量、马尔可夫链和随机博弈的终止概率都是通过最小或最大不动点来定义的。本文表明，我们最近提出的用于检验函数不动点是否为最小（或最大）的技术，在gs-单子范畴的框架下具有自然的范畴论解释。该技术基于一个将函数映射到适当近似值的构造。我们研究了该映射的组合性质，并证明在某些限制下，它可以自然地解释为一个（松弛的）gs-单子函子。这指导了名为UDEfix的工具的开发，该工具允许我们像构建电路一样，用基本构建块来组合函数（及其近似），并随后执行不动点检验。我们还表明，对该理论的轻微推广允许处理一个新的相关案例研究：基于Wasserstein提升的余代数行为度量。