Infinite Traces by Finality: a Sheaf-Theoretic Approach

Abstract

Kleisli categories have long been recognised as a setting for modelling the linear behaviour of various types of systems. However, the final coalgebra in such settings does not, in general, correspond to a fixed notion of linear semantics. While there are well-understood conditions under which final coalgebras capture finite trace semantics, a general account of infinite trace semantics via finality has remained elusive. In this work, we present a sheaf-theoretic framework for infinite trace semantics in Kleisli categories that systematically constructs final coalgebras capturing infinite traces. Our approach combines Kleisli categories, sheaves over ordinals, and guarded (co)recursion, enabling infinite behaviours to emerge from coherent families of finite approximations via amalgamation. We introduce the notion of guarded behavioural functor and show that, under mild conditions, their final coalgebras directly characterise infinite traces.