重溯范畴语义学中的若干路径：从过程-命题即类型到范畴化实数与计算机
Retracing some paths in categorical semantics: From process-propositions-as-types to categorified reals and computers
AI总结：
本文从逻辑视角系统梳理交互范畴谱系，区分计算建模与一般过程刻画，并通过余归纳构造出以极化互模拟为态射的实数紧致范畴，最终勾勒可计算片段的结构特征。
摘要：
命题联结词与类型构造子之间的逻辑对应关系不仅限于谓词的静态领域，还延伸至过程的动态领域。理解过程命题与动态类型之间的逻辑对应关系，曾是计算语义学的核心问题之一，尽管这一点并不总是清晰或明确。这一关系在Samson Abramsky的早期工作中变得清晰起来，其中指称语义学与进程演算的核心思想被汇聚在一起，并通过范畴工具加以分析，例如交互范畴的结构。虽然一些源于计算动态性的逻辑结构立即开始显现，但另一些则不得不等待，原因可能是其背后的逻辑原理（主要是由余归纳产生的那些原理）尚未得到充分理解，或者仅仅是因为研究界对其他语义学任务更感兴趣。回顾过去，早期语义学努力所揭示的过程逻辑似乎可能仍处于刚刚开始显现的阶段，而在此期间获得的大量结果可能只是冰山一角。在本文中，我试图对交互范畴的全谱系提供一个逻辑性概述，并区分那些对计算进行建模的交互范畴与那些刻画一般过程的交互范畴。主要的余归纳构造被证明属于后一类，这一点在本文末尾通过一个紧致范畴加以说明，该范畴将所有实数（包括可计算与不可计算的实数）作为过程，并以极化互模拟作为态射。实数的加法作为双积出现，实向量空间是丰富双完备化，线性代数则源于丰富Kan扩张。在最后一步，我勾勒出一个刻画范畴语义学中可计算片段的结构。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
