2005/05/27 by Gian Luca Cattani, Glynn Winskel · 1 citation
Computer Science · Mathematics · #Algebra over a field #Bisimulation #Computer science #Discrete mathematics #Functor #Homotopy and Cohomology in Algebraic Topology #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Programming language #Pure mathematics #Semantics (computer science)
paper · doi:10.1017/s0960129505004718
openalex publication_date 2005/05/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
This paper studies fundamental connections between profunctors (that is, distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) preserves open maps and open map bisimulation. Consequently, the composition of profunctors preserves open maps as 2-cells. A guiding idea is the view that profunctors, and colimit preserving functors, are linear maps in a model of classical linear logic. But profunctors, and colimit preserving functors, as linear maps, are too restrictive for many applications. This leads to a study of a range of pseudo-comonads and of how non-linear maps in their co-Kleisli bicategories preserve open maps and bisimulation. The pseudo-comonads considered are based on finite colimit completion, ‘lifting’, and indexed families. The paper includes an appendix summarising the key results on coends, left Kan extensions and the preservation of colimits. One motivation for this work is that it provides a mathematical framework for extending domain theory and denotational semantics of programming languages to the more intricate models, languages and equivalences found in concurrent computation, but the results are likely to have more general applicability because of the ubiquitous nature of profunctors.