Hostname: page-component-6bf8c574d5-2jptb Total loading time: 0 Render date: 2025-02-21T04:38:16.827Z Has data issue: false hasContentIssue false

Profunctors, open maps and bisimulation

Published online by Cambridge University Press:  27 May 2005

GIAN LUCA CATTANI
Affiliation:
DS Data Systems S.p.A., Via Ugozzolo 121/A, I-43100 Parma, Italy. Email: cattanil@dsdata.it.
GLYNN WINSKEL
Affiliation:
University of Cambridge Computer Laboratory, Cambridge CB3 0FD, England. Email: gw104@cl.cam.ac.uk.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Paper
Copyright
2005 Cambridge University Press