Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product
Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product
复制标题
部分交换线性逻辑和兰贝克微积分乘积的自然演绎和归一化
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Christian Retoré
中科院分区：
文献类型：
--
作者：
M. Amblard;Christian Retoré
本文给出了部分可换直觉乘法线性逻辑（PCIMLL）的一个自然演绎系统，并建立了它的规范化和子公式性质。这样一个系统涉及交换和非交换连接词，并处理串并联公式的多集。这calculu- lus是一个由德Groote介绍的扩展提出的二阶建模Petri网的执行，与充分的熵，允许为了放松到任何suborder -而不是非交换逻辑的Abrusci和Ruet。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。到目前为止，全熵的PCIMLL还没有自然演绎。特别是在语言学应用中，这种句法是非常受欢迎的，从句法分析中构建语义表示。1介绍非交换逻辑自然出现在数学的角度和建模的一些真实的世界现象。数学上的非交换性是自然的，无论是从真值语义学的观点（相位语义学，基于可以是非交换的幺半群），还是从一个syn-tactical的观点（序列而不是公式集的微积分，可以有很好的括号公理链接的证明网）。非交换性也出现在真实的世界的应用中，比如并发理论，比如Petri网的并发执行，以及我们最喜欢的应用，计算语言学，这可以追溯到50年代和Lambek演算的出现。我们首先简要介绍了非交换逻辑，然后强调他们的并发性和计算语言学的兴趣。非交换线性逻辑线性逻辑（6）提出了Lambek演算（9）和非交换演算的逻辑观点.在许多年里，字典是整合交换连接词和非交换连接词。第一个解决方案，没有一个长期演算，是庞塞特逻辑，现在研究与扩展的微积分称为微积分的结构（7）。
This paper provides a natural deduction system for Partially Commutative Intuitionistic Multiplicative Linear Logic (PCIMLL) and establishes its normalisation and subformula property. Such a system in- volves both commutative and non commutative connectives and deals with context that are series-parallel multisets of formulae. This calcu- lus is the extension of the one introduced by de Groote presented by the second order for modelling Petri net execution, with a full entropy which allow order to be relaxed into any suborder — as opposed to the Non Commutative Logic of Abrusci and Ruet. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Up to now PCIMLL with full entropy had no natural deduction. In particular for linguistic applications, such a syntax is much welcome to construct semantic representations from syntactic analyses. 1 Presentation Non commutative logics arise naturally both in the mathematical perspective and in the modelling of some real world phenomena. Mathematically non com- mutativity is a natural both from the truth valued semantics viewpoint (phase semantics, based on monoids which can be non commutative) and from a syn- tactical one (sequent calculus with sequences rather than sets of formulae, proof nets which can have well bracketed axiom links). Non commutativity also ap- pears from real world applications such as concurrency theory, like concurrent execution of Petri net, and in our favourite application, computational linguistic, and this goes back to the fifties and the apparition of the Lambek calculus. We first give a brief presentation of non commutative logics and then stress their interest for concurrency and computational linguistics. Non commutative linear logics Linear logic (6) oered a logical view of the Lam- bek calculus (9) and non commutative calculi. During many years, the diculty was to integrate commutative connective and non commutative connectives. A first solution, without a term calculus, was Pomset Logic, now studied with extended sequent calculi callled Calculus of Structures (7).