|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'502'364
Articles rated: 2609
23 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Retracing some paths in categorical semantics: From process-propositions-as-types to categorified real numbers and monoidal computers | | Dusko Pavlovic
; | | Date: |
20 Jul 2020 | | 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 emph{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. | | Source: | arXiv, 2007.10057 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER