Making first order linear logic a generating grammar

要約

さまざまなカテゴリ文法が一次乗算線形論理 (MLL1) のフラグメントで表面表現を持つことが知られています。
我々は、対象のフラグメントが最近導入された拡張テンソル型計算 (ETTC) と同等であることを示します。
ETTC は特定の型付き項の計算であり、文字列のタプル、より正確には文字列で装飾された 2 部グラフを表します。
型は線形論理式から導出され、ルールはこれらの文字列ラベル付きグラフ上の具体的な操作に対応するため、視覚化が容易になります。
これにより、言語モデリングに関連する上記の 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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google