Stable Profunctors and Matrix Representation

Takeshi Tsukada , Kazuyuki Asada , Kengo Hirata

Abstract

The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for profunctors definable by λ-terms. The mathematical reason behind this phenomenon, however, was not understood.

This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor’s work and further developed by Fiore et al. All λ-definable profunctors are known to be stable, and we show that the matrix representation behaves well for stable profunctors. We prove that the matrix representation defines a functor from stable profunctors to matrices that preserves the linear logic structures.