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 and the compositionality properties of this mapping are naturally interpreted as a gs-monoidal functor. This guides the realisation of a tool, called UDEfix that allows 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提升的余代数行为度量。