经典线性逻辑的线性/生产者/消费者模型
A Linear/Producer/Consumer Model of Classical Linear Logic
摘要：
本文定义了一个新的证明和范畴理论框架的经典线性逻辑，分为一个线性政权和两个持久政权相应的推理！然后呢？由此产生的线性/生产者/消费者（LPC）逻辑将三类命题置于相同的语义基础上，遵循本顿的线性/非线性直觉线性逻辑公式。从语义上讲，LPC对应于一个由反映线性/生产者/消费者结构的概念连接的三个类别的系统。本文的元理论结果包括容许定理的削减和对偶规则，并翻译的LPC逻辑到范畴理论。文中还介绍了LPC模型的几个具体实例。
英文摘要：
This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
