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 {\bf ETTC}, which allows more concise and transparent computations. We present both a cut-free sequent calculus and a natural deduction formalism.
翻译:已知不同的范畴语法在一阶乘法线性逻辑(MLL1)的一个片段中具有表层表示。我们证明该相关片段等价于最近引入的扩展张量类型演算(ETTC)。ETTC是一种特定类型项的演算,表示字符串元组,更确切地说,是带有字符串标记的二部图。类型源自线性逻辑公式,规则对应于这些字符串标记图的具体操作,从而可以方便地可视化。这不仅为上述与语言建模相关的MLL1片段提供了替代语法和直观的几何表示,还赋予其此前缺失的内在演绎系统。在本文中,我们对先前引入的{\bf ETTC}进行了一项非平凡的符号化增强变体研究,该变体允许更简洁透明的计算。我们同时给出了无切割矢列演算和自然演绎形式化。