Categorical models of Linear Logic with fixed points of formulas
Categorical models of Linear Logic with fixed points of formulas
复制标题
具有公式不动点的线性逻辑分类模型
DOI：
10.1109/lics52264.2021.9470664
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Farzad Jafarrahmani
中科院分区：
文献类型：
--
作者：
T. Ehrhard;Farzad Jafarrahmani
我们开发了一个类别语义的μLL，一个版本的命题线性逻辑的最小和最大不动点扩展大卫Baelde的命题μMALL指数。我们的一般范畴设置是基于西利范畴和强函子对他们的作用。我们展示两个简单的例子，这种设置。在第一个，这是基于类别的集合和关系，最小和最大的不动点是以同样的方式解释。在第二种情况下，基于配备了整体概念（非一致整体空间）和保持它的关系的集合类别，最小和最大不动点有不同的解释。后一个模型表明，µLL享有证明规范化的指称形式。
We develop a categorical semantics of µLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde’s propositional µMALL with exponentials. Our general categorical setting is based on Seely categories and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving it, least and greatest fixed points have distinct interpretations. This latter model shows that µLL enjoys a denotational form of normalization of proofs.