Retracing some paths in categorical semantics: From process-propositions-as-types to categorified reals and computers

Abstract

The logical parallelism of propositional connectives and type constructors extends beyond the static realm of predicates, to the dynamic realm of processes. Understanding the logical parallelism of process propositions and dynamic types was one of the central problems of the semantics of computation, albeit not always clear or explicit. It sprung into clarity through the early work of Samson Abramsky, where the central ideas of denotational semantics and process calculus were brought together and analyzed by categorical tools, e.g. in the structure of interaction categories. While some logical structures borne of dynamics of computation immediately started to emerge, others had to wait, be it because the underlying logical principles (mainly those arising from coinduction) were not yet sufficiently well-understood, or simply because the research community was more interested in other semantical tasks. Looking back, it seems that the process logic uncovered by those early semantical efforts might still be starting to emerge and that the vast field of results that have been obtained in the meantime might be a valley on a tip of an iceberg. In the present paper, I try to provide a logical overview of the gamut of interaction categories and to distinguish those that model computation from those that capture processes in general. The main coinductive constructions turn out to be of this latter kind, as illustrated towards the end of the paper by a compact category of all real numbers as processes, computable and uncomputable, with polarized bisimulations as morphisms. The addition of the reals arises as the biproduct, real vector spaces are the enriched bicompletions, and linear algebra arises from the enriched kan extensions. At the final step, I sketch a structure that characterizes the computable fragment of categorical semantics.