We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints. Interestingly, our nets are untyped: we only rely on the sequentiality of linear logic nets and the dynamics of cut elimination. The paths on which we impose bounds are the switching paths involved in the Danos--Regnier criterion for sequentiality. In order to accommodate multiplicative units and weakenings, our nets come equipped with jumps: each weakening node is connected to some other node. Our constraint can then be summed up as a bound on both the length of switching paths, and the number of weakenings that jump to a common node.


翻译:我们在多复制线性逻辑(MLL)验证网中检查平行切除平行切除的一些组合特性。我们显示,如果我们对一些路径施加限制,我们可以将满足这一限制的所有网的大小捆绑起来,将其缩小为固定的成网。这为无限的加权网数目提供了足够条件,可以将其减为另一网数目,同时保持系数的有限性。我们还表明,我们的制约因素在减少中是稳定的。我们的方法受到线性逻辑定量语义的驱动:许多模型已经提出,其结构反映了多复制的指数性线性逻辑(MELL)验证网的扩展为无限的差别网数目。为了模拟MELL的消除步骤,我们必须减少其扩大的差别网的任意削减数量。结果也适用于差别性网,因为它们的消除基本上是多倍增的。我们还表明,在泰勒扩大的MELL网中出现的差别网数目自动满足了我们的限制因素。有趣的是,我们的网型结构是非型式的:我们仅仅依靠线性逻辑性逻辑网的顺序顺序的顺序,而在每一条线性递减线性线性线性线性线性线性线上的递减线性线性线性线性线性线性调整中,而使不断递减的线性递减。

0
下载
关闭预览

相关内容

【KDD2021】图神经网络,NUS- Xavier Bresson教授
专知会员服务
62+阅读 · 2021年8月20日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
【课程】纽约大学 DS-GA 1003 Machine Learning
专知会员服务
45+阅读 · 2019年10月29日
学习自然语言处理路线图
专知会员服务
137+阅读 · 2019年9月24日
保序最优传输:Order-preserving Optimal Transport
我爱读PAMI
6+阅读 · 2018年9月16日
已删除
将门创投
7+阅读 · 2018年4月25日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】决策树/随机森林深入解析
机器学习研究会
5+阅读 · 2017年9月21日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Logically-Constrained Reinforcement Learning
Arxiv
3+阅读 · 2018年12月6日
VIP会员
相关资讯
保序最优传输:Order-preserving Optimal Transport
我爱读PAMI
6+阅读 · 2018年9月16日
已删除
将门创投
7+阅读 · 2018年4月25日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
【推荐】决策树/随机森林深入解析
机器学习研究会
5+阅读 · 2017年9月21日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员