Paolo Baldan ; Richard Eggert ; Barbara König ; Timo Matt ; Tommaso Padoan - A Monoidal View on Fixpoint Checks

lmcs:12875 - Logical Methods in Computer Science, July 22, 2025, Volume 21, Issue 3 - https://doi.org/10.46298/lmcs-21(3:5)2025
A Monoidal View on Fixpoint ChecksArticle

Authors: Paolo Baldan ; Richard Eggert ; Barbara König ; Timo Matt ; Tommaso Padoan

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.


Volume: Volume 21, Issue 3
Secondary volumes: Selected Papers of the 16th International Conference on Graph Transformation (ICGT 2023)
Published on: July 22, 2025
Accepted on: April 21, 2025
Submitted on: January 17, 2024
Keywords: Logic in Computer Science

Consultation statistics

This page has been seen 1446 times.
This article's PDF has been downloaded 482 times.