论文标题
使一阶线性逻辑成为生成语法
Making first order linear logic a generating grammar
论文作者
论文摘要
众所周知，不同的类别语法在一阶乘法线性逻辑（MLL1）的片段中具有表面表示。我们表明，感兴趣的片段等同于最近引入的扩展张量型演算（ETTC）。 ETTC是特定键入术语的演算，它代表字符串的元素，更精确地用字符串装饰。类型来自线性逻辑公式，规则对应于这些字符串标记图上的具体操作，因此可以方便地可视化它们。这提供了上述MLL1的片段，该片段与语言建模相关，不仅与某些替代语法和直观的几何表示形式相关，而且还具有固有的演绎系统。 在这项工作中，我们考虑了先前引入的ETTC的非平凡符号富集变化，该变化允许更简洁和透明的计算。我们既提出了无剪切的序列演算和自然扣除形式主义。
It is known that different categorial grammars have surface representation in a fragment of first order multiplicative linear logic (MLL1). We show that the fragment of interest is equivalent to the recently introduced extended tensor type calculus (ETTC). ETTC is a calculus of specific typed terms, which represent tuples of strings, more precisely bipartite graphs decorated with strings. Types are derived from linear logic formulas, and rules correspond to concrete operations on these string-labeled graphs, so that they can be conveniently visualized. This provides the above mentioned fragment of MLL1 that is relevant for language modeling not only with some alternative syntax and intuitive geometric representation, but also with an intrinsic deductive system, which has been absent. In this work we consider a non-trivial notationally enriched variation of the previously introduced ETTC, which allows more concise and transparent computations. We present both a cut-free sequent calculus and a natural deduction formalism.
