Infinite Traces by Finality: a Sheaf-Theoretic Approach

TL;DR

This paper introduces a sheaf-theoretic framework within Kleisli categories to systematically model infinite trace semantics, capturing infinite behaviours through finite approximations and guarded recursion.

Contribution

It develops a novel sheaf-theoretic approach for infinite trace semantics in Kleisli categories, unifying finite approximations and infinite behaviours via guarded (co)recursion.

Findings

Constructs final coalgebras for infinite traces

Uses sheaves over ordinals to model infinite behaviours

Provides conditions for characterising infinite traces

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.