Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Making first order linear logic a generating grammar

Sergey Slavnov

TL;DR

The paper establishes that the linguistically relevant fragment of first-order linear logic (MLL1) is precisely equivalent to an enriched extended tensor type calculus (ETTC), which encodes strings as labeled bipartite graphs via tensor terms. It provides a self-contained intrinsic deductive system for this fragment through a cut-free sequent calculus and a natural deduction variant, along with a geometric intuition for derivations. The work introduces a rich tensor-term formalism, binding operators, and a first-order translation that bridges ETTC with MILL1 and LC, thereby offering a generating-grammar perspective on the linguistic fragment. This framework clarifies the relationship between surface representations of grammars and deductive derivations, enabling more transparent analyses and potential extensions beyond the standard first-order fragment.

Abstract

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.

Making first order linear logic a generating grammar

TL;DR

The paper establishes that the linguistically relevant fragment of first-order linear logic (MLL1) is precisely equivalent to an enriched extended tensor type calculus (ETTC), which encodes strings as labeled bipartite graphs via tensor terms. It provides a self-contained intrinsic deductive system for this fragment through a cut-free sequent calculus and a natural deduction variant, along with a geometric intuition for derivations. The work introduces a rich tensor-term formalism, binding operators, and a first-order translation that bridges ETTC with MILL1 and LC, thereby offering a generating-grammar perspective on the linguistic fragment. This framework clarifies the relationship between surface representations of grammars and deductive derivations, enabling more transparent analyses and potential extensions beyond the standard first-order fragment.

Abstract

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.
Paper Structure (20 sections, 7 theorems, 14 equations, 9 figures)

This paper contains 20 sections, 7 theorems, 14 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Background: systems of linear logic
  3. MILL1 grammars and linguistic fragment
  4. MILL1 grammars
  5. Linguistic fragment
  6. Occurrence nets
  7. Linguistic derivations
  8. Tensor type calculus
  9. Tensor terms
  10. Geometric representation
  11. Remarks on binding and multiplication
  12. Tensor formulas and types
  13. Sequents and typing judgements
  14. Geometric representation
  15. Sequent calculus
  16. ...and 5 more sections

Key Result

Proposition 3.4

Any cut-free derivation of a linguistically marked MLL1 sequent is linguistically marked. $\Box$

Figures (9)

  • Figure 1: Systems of linear logic
  • Figure 2: Occurrence net example
  • Figure 3: Meaning of $\beta$-reductions
  • Figure 4: ETTC Language
  • Figure 5: Tensor sequent
  • ...and 4 more figures

Theorems & Definitions (30)

  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Proposition 3.4
  • Definition 3.5
  • Definition 3.6
  • Proposition 3.7
  • proof
  • Proposition 3.8
  • proof
  • ...and 20 more