一句话：证明范畴语法所在的 MLL1 片段等价于扩展张量类型演算 ETTC，并给出无切矢列演算与自然演绎。
范畴语法可在一阶乘法线性逻辑（MLL1）的某片段中获得表层表示，但该片段此前缺少内在演绎系统。本文证明这一片段等价于新近提出的扩展张量类型演算（ETTC）。ETTC 以特定类型项表示字符串元组，更准确地说，表示用字符串装饰的二部图；类型来自线性逻辑公式，规则对应字符串标记图上的具体操作，因而便于可视化。作者采用记号更丰富的 ETTC 变体，使计算更简洁透明，并给出无切矢列演算与自然演绎两种形式。该工作为面向语言建模的 MLL1 片段提供了替代语法、几何表示和演绎系统。
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.