一句话:为带最小/最大不动点的命题线性逻辑 μLL 建立范畴语义,给出两个模型,后者展示指称式证明归一化。
论文研究 μLL 的范畴语义。μLL 是带最小与最大不动点的命题线性逻辑,在 Baelde 的命题 μMALL 基础上加入指数。作者以 Seely 范畴及作用于其上的强函子为一般框架,给出该语言的语义解释。文中构造两个实例:第一个基于集合与关系范畴,其中最小与最大不动点被同样解释;第二个基于带完全性概念的集合(非一致完全空间)及其保持完全性的关系范畴,其中两类不动点获得不同解释。后一模型表明 μ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.