IMLL上的弱型Boehm定理
Weak Typed Boehm Theorem on IMLL
摘要：
在克里特岛的Boehm定理研讨会上，Zoran Petric称Statman的“典型模糊性定理”为Boehm定理。此外，他还基于简单类型的λ演算的集合理论模型给出了该定理的新证明。在本文中，我们研究的线性版本的类型Boehm定理的直觉线性逻辑的一个片段。证明了在不含乘法单位1的直觉线性逻辑的乘法片段（简称IMLL）中弱型Boehm定理成立。IMLL系统完全对应于线性λ演算没有指数，添加剂和逻辑常数。IMLL系统也恰好对应于没有单位对象的自由对称monoidal闭范畴。据我们所知，我们的分离结果是第一个关于这些系统在一个纯粹的语法方式。
英文摘要：
In the Boehm theorem workshop on Crete island, Zoran Petric called Statman's ``Typical Ambiguity theorem'' typed Boehm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Boehm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit 1 (for short IMLL) weak typed Boehm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus without exponentials, additives and logical constants. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
