arXiv 1402.04742014-02-03cs.LOcs.FL

部分可换乘法线性逻辑Lambek与PCMLL的正规化及子公式性质

Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic

Maxime Amblard, Christian Retoré

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文建立了直觉主义非交换逻辑的自然演绎或λ演算公式的规范化--它同时涉及交换和非交换连接词。这种演算首先介绍了德格罗特，而不是经典版本的Abrusci和Ruet承认充分熵，允许为了放宽到任何suborder。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。对于全熵的直觉非交换逻辑，至今没有一个证明网语法;对于语言应用，与自然演绎或多或少等价的逻辑演算由于缺乏标准的Curry-Howard同构而不方便。

英文摘要：

This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non commutative connectives. This calculus first introduced by de Groote and as opposed to the classical version by Abrusci and Ruet admits a full entropy which allow order to be relaxed into any suborder. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Regarding Intuitionistic Non Commutative Logic with full entropy does not have up to now a proof net syntax, and that for linguistic applications, sequent calculi which are only more or less equivalent to natural deduction, are not convenient because they lack the standard Curry-Howard isomorphism.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Normalization by Evaluation for the Lambek Calculus

The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it has many applications, mostly in formal computational investigations of natural languages. This paper introduces a calculus of beta-eta-long normal forms for derivations in the Lambek calculus with multiplicative unit and conjunction among its logical connectives. Reduction to normal form follows the normalization by evaluation (NbE) strategy: (i) evaluate a derivation in a Kripke model of Lambek calculus; (ii) extrac…

2022-04-14cs.LO

The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill's calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove algorithmic undecidabi…

2020-09-30cs.LOmath.LO

非结合Lambek演算经典扩张的聚焦和相位模型

Focalization and phase models for classical extensions of non-associative Lambek calculus

Lambek的非联想句法演算（NL）在其资源意识方面表现出色：通常的弱化，收缩，交换甚至结合性的结构规则都被丢弃。最近，有人提出了一些保守的扩展，以免除NL对具有单一结论的序列的直觉偏见：De Groote和Lamarche的经典非结合Lambek演算（CNL）和Moortgat及其同事的Lambek-Grishin演算（LG）。我们证明了Andreoli的聚焦属性所述的建议：一个规范化的结果，确定在很大程度上，那些不同的只是由平凡的规则排列的切免费的cirrhosis推导。在这样做的时候，我们从一个“统一的”CCN介绍，通过增加结构规则从LG派生CNL。规范化的证明收益的句法阶段模型的建设，其中每一个“真理”有一个集中的证明，类似于冈田和Herbelin和李的工作。

2011-06-02cs.LO

On the Recognizing Power of the Lambek Calculus with Brackets

Every language recognized by the Lambek calculus with brackets is context-free. This is shown by combining an observation by Jäger with an entirely straightforward adaptation of the method Pentus used for the original Lambek calculus. The case of the variant of the calculus allowing sequents with empty antecedents is slightly more complicated, requiring a restricted use of the multiplicative unit.

2018-04-15cs.LOmath.LO

扩展的Lambek演算与一阶线性逻辑

Extended Lambek calculi and first-order linear logic

CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）

一阶乘法直觉线性逻辑（MILL 1）可以看作是Lambek演算的一个扩展。除了MILL 1的片段对应于Lambek演算（Moot & Piazza 2001），我将展示MILL 1的片段，它们生成多种上下文无关语言，并对应于Morrilll等人的位移演算。

2013-05-27cs.CLcs.LO

From Double Pushout Grammars to Hypergraph Lambek Grammars With and Without Exponential Modality

We study how to relate well-known hypergraph grammars based on the double pushout (DPO) approach and grammars over the hypergraph Lambek calculus HL (called HL-grammars). It turns out that DPO rules can be naturally encoded by types of HL using methods similar to those used by Kanazawa for multiplicative-exponential linear logic. In order to generalize his reasonings we extend the hypergraph Lambek calculus by adding the exponential modality, which results in a new calculus HMEL0; then we prove that any DPO grammar can be converted into an equivalent HMEL0-grammar. We also define the conjuncti…

2023-03-28cs.FLcs.LO

更多相关论文收起更多论文

Dialectica Categories for the Lambek Calculus

We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a κmodality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional proper…

2018-01-21cs.LO

带 Kleene 星的无穷 Lambek 演算的复杂性

Complexity of the Infinitary Lambek Calculus with Kleene Star

本文证明了带 Kleene 星的无穷 Lambek 演算的可推导性问题是 $\Pi_1^0$-困难的，解决了 Buszkowski 的开放问题，并作为副产品证明了不含空词的上下文无关语言可由唯一类型赋值的 Lambek 文法生成。

2020-05-01cs.LOmath.LO

带弱化的完全Lambek演算中的可推演性是HAck完全的

Deducibility in the full Lambek calculus with weakening is HAck-complete

该研究证明带弱化的完全Lambek演算的后承关系判定问题（含乘法片段）为HAck完全，通过有损通道系统可达性归约证下界，结合结构证明论与良拟序理论得上界。

2024-06-21cs.CCcs.LOmath.LO

Language Models for Some Extensions of the Lambek Calculus

We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only no issues with distributivity arise. In contrast, there exists a corollary of the distributivity law in the language with disjunction only which is not derivable in the non-distributive system. Moreover, this d…

2020-07-31cs.LOmath.LO

Comparing and evaluating extended Lambek calculi

CNRS (LaBRI)（法国国家科学研究中心（拉布里实验室））；University of Bordeaux（波尔多大学）

Lambeks Syntactic Calculus, commonly referred to as the Lambek calculus, was innovative in many ways, notably as a precursor of linear logic. But it also showed that we could treat our grammatical framework as a logic (as opposed to a logical theory). However, though it was successful in giving at least a basic treatment of many linguistic phenomena, it was also clear that a slightly more expressive logical calculus was needed for many other cases. Therefore, many extensions and variants of the Lambek calculus have been proposed, since the eighties and up until the present day. As a result, th…

2015-06-18cs.CLcs.LO

线性逻辑及相关系统中的插值

Interpolation in Linear Logic and Related Systems

本文证明了带交换的完整Lambek演算及经典与直觉线性逻辑等存在连续统多个具有演绎插值性质的公理扩张，并指出它们虽不具备Craig插值性质，但均满足受守卫形式的Craig插值。

2023-08-03cs.LOmath.LO

Exponentially Handsome Proof Nets and Their Normalization

Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system…

2021-12-30cs.LO

Pomset logic: the other approach to non commutativity in logic

Thirty years ago, I introduced a non-commutative variant of classical linear logic, called "pomset logic", issued from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a non-commutative connective, "$\triangleleft$" called "before", associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered MultiSET of formulas. Pomset logic enjoys a proof net calculus with cut-elimination…

2023-02-03cs.LOmath.LO

$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclusion natural deduction system and show it is isomorphic to a simple and natural extension of $λ$-calculus with parallelism and communication primitives, called $λ_{\unicode{8523}}$. We shall prove that $λ_{\unicode{8523}}$ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.

2019-07-08cs.LO

基于反证的经典线性λ演算

A Classical Linear $λ$-Calculus based on Contraposition

Universidad Nacional de Quilmes (CONICET)（基尔梅斯国立大学（阿根廷国家科学研究委员会））；Universidad de Buenos Aires（布宜诺斯艾利斯大学）；Stevens Institute of Technology（史蒂文斯理工学院）

本文提出基于反证的经典线性λ演算，通过引入反向替换规则，实现了对MELL的正确性和完备性证明，并展示了其在类型编程语言中的核心属性。

2026-02-02cs.LO

线性逻辑中的最小和最大不动点

Least and Greatest Fixed Points in Linear Logic

MALL（乘法，加法线性逻辑）的一阶理论仅在等式上是一个有趣但弱的逻辑，因为它不能捕获无界（无限）行为。而不是通过增加指数（！和？），我们添加最小和最大不动点算子。由此产生的逻辑，我们称之为muMALL，满足两个基本的证明理论性质：我们建立弱规范化，我们设计了一个集中的证明系统，我们证明完整的。第二个结果提供了一个强范式的无切割证明结构，可用于，例如，帮助自动化证明搜索。我们展示了如何将这些基础应用于直觉逻辑。

2010-11-30cs.LO

Around finite second-order coherence spaces

Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhibit such a finite semantics for a polymorphic purely linear language: more precisely, we show that in Girard's semantics of second-order linear logic using coherence spaces and normal functors, the denotations of multiplicative-additive formulas are finite. This model is also effective, in the sense that the denotations of formulas and proofs are computable, as we show. We also establish analogous results for a second…

2019-05-13cs.CCcs.LOmath.LO