A Profunctorial Scott Semantics
A Profunctorial Scott Semantics
复制标题
口语斯科特语义学
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Z. Galal
中科院分区：
文献类型：
--
作者：
Z. Galal
本文研究了具有自由有限余积伪余单子的前函子的双范畴，并证明了它构成了推广Scott模型的线性逻辑模型。我们将两个模型之间的联系形式化为丰富类别的基的变化，这引起了一个伪函子，保留了所有的线性逻辑结构。我们证明了在co-Kleisli双范畴中的态射对应于预层范畴之间的强有限函子（筛余极限保持函子）的概念。我们进一步表明，该模型提供了解决方案的递归型方程，提供了2维模型的纯lambda演算，我们还展示了一个不动点算子的条款。2012年ACM学科分类计算理论→线性逻辑;计算理论→范畴语义学
In this paper, we study the bicategory of profunctors with the free finite coproduct pseudo-comonad and show that it constitutes a model of linear logic that generalizes the Scott model. We formalize the connection between the two models as a change of base for enriched categories which induces a pseudo-functor that preserves all the linear logic structure. We prove that morphisms in the co-Kleisli bicategory correspond to the concept of strongly finitary functors (sifted colimits preserving functors) between presheaf categories. We further show that this model provides solutions of recursive type equations which provides 2-dimensional models of the pure lambda calculus and we also exhibit a fixed point operator on terms. 2012 ACM Subject Classification Theory of computation → Linear logic; Theory of computation → Categorical semantics