First order linear logic and tensor type calculus for categorial grammars

TL;DR

This paper explores the connection between first order multiplicative linear logic and tensor type calculus, proposing an alternative syntax and geometric interpretation for categorial grammars.

Contribution

It identifies a fragment of MLL1 suitable for grammar representations and establishes a correspondence with ETTC, offering a new deductive and geometric framework.

Findings

Established a correspondence between MLL1 fragment and ETTC

Provided a natural deduction formulation of ETTC

Presented a geometric representation for the calculus

Abstract

We study relationship between first order multiplicative linear logic (MLL1), which has been known to provide representations to different categorial grammars, and the recently introduced extended tensor type calculus (ETTC). We identify a fragment of MLL1, which seems sufficient for many grammar representations, and establish a correspondence between ETTC and this fragment. The system ETTC, thus, can be seen as an alternative syntax and intrinsic deductive system together with a geometric representation for the latter. We also give a natural deduction formulation of ETTC, which might be convenient.