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
    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 1166 times.
    This article's PDF has been downloaded 383 times.