# First order linear logic and tensor type calculus for categorial grammars

Sergey Slavnov
National Research University Higher School of Economics
<EMAIL_ADDRESS>

###### 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.

##  1 Introduction

The best known examples of categorial grammars are Lambek grammars, which are
based on Lambek calculus (LC) [5], i.e. noncommutative intuitionistic linear
logic (for background on linear logic see [2],[3]). These, however, have
somewhat limited expressive power, and a lot of extensions/variations have
been proposed, using discontinuous tuples of strings and $\lambda$-terms,
commutative and non-commutative logical operations, modalities etc, let us
mention displacement grammars [9], abstract categorial grammars (also called
$\lambda$-grammars and linear grammars) [1], [10], [11] and hybrid type
logical categorial grammars [4].

It has been known for a while (starting from the seminal work [8]) that
different grammatical formalisms, such as those just mentioned, can all be
represented using simple and familiar commutative system of first order
multiplicative intuitionistic linear logic (MILL1) [6], [7]. In fact, not the
whole of MILL1 is used: it can be noted that translations of different
categorial grammars usually fit into some small fragment, which, therefore,
can be given linguistic interpretation. Unfortunately, we do not have any
deductive system intrinsic to this fragment. Typically, when deriving the
MILL1 translation of an LC sequent in sequent calculus or natural deduction,
one might have to use at intermediate steps sequents and derivations which are
not translations of anything and have no linguistic meaning at all (as it
seems).

Extended tensor type calculus (ETTC), a system extending propositional
(classical) multiplicative linear logic (MLL), recently proposed by the author
[13] (elaborating on [12]), was directly designed for linguistic
interpretation in terms of bipartite graphs whose edges are labeled with
words. It has been shown that tensor grammars based on ETTC include both
Lambek grammars and abstract categorial grammars as conservative fragments,
with representation very similar to that in MILL1. However, unlike the case of
MILL1, in ETTC derivations each rule corresponds to a concrete operation on
strings, so that formal language generation is decomposed into elementary
steps, which, moreover, can be conveniently visualized in the pictorial
setting of labeled graphs.

In this work we identify a fragment (we call it strictly balanced fragment) of
first order linear logic, which is sufficient for linguistic constructions of
[6], [7], and show that there are mutually inverse translations to and from
ETTC. Thus ETTC turns out to be an alternative syntax for the relevant
fragment of MILL1, equipped with an intrinsic deductive system and intuitive
pictorial representation.

We also introduce a natural deduction formulation for ETTC in this work, which
might be more convenient in some situations than the sequent calculus
formulation of [13].

##  2 Background: systems of linear logic

The language of multiplicative intuitionistic logic (MILL1) is summarized in
Figure 1(a). We assume that we are given a set $Pred$ of predicate symbols
with assigned arities, a countable set $Var$ of individual variables and a set
$Const$ of constants. The set of first order atomic formulas is denoted as
$At$, and the set of all first order linear intuitionistic formulas is denoted
as $Fm$. The binary connectives $\otimes$, $\multimap$ are called respectively
tensor (also times) and linear implication. A context $\Gamma$ is a finite
multiset of formulas; as usual, we denote formulas with Latin letters and
contexts with Greek letters. The set of free variables in the context $\Gamma$
is denoted as $FV(\Gamma)$. The sequent calculus for MILL1 is shown in Figure
1(b).

$At=\\{p(e_{1},\ldots,e_{n})|~{}e_{1},\ldots,e_{n}\in Var\cup Const,~{}p\in
Pred,~{}arity(p)=n\\}$, $Fm::=At|(Fm\multimap Fm)|(Fm\otimes Fm)|\forall
xFm|\exists xFm,~{}x\in Var$.

(a) MILL1 language

$A\vdash A,~{}A\in At~{}{\rm{(Id)}}\quad\cfrac{\Gamma\vdash A\quad
A,\Theta\vdash C}{\Gamma,\Theta\vdash C}~{}{\rm{(Cut)}}$
$\cfrac{\Gamma,A,B\vdash C}{\Gamma,A\otimes B\vdash C}~{}{\rm{(\otimes
L)}}\quad\cfrac{\Gamma\vdash A\quad\Theta\vdash B}{\Gamma,\Theta\vdash
A\otimes B}~{}{\rm{(\otimes R)}}$
$\cfrac{\Gamma\vdash A\quad B,\Theta\vdash C}{\Gamma,A\multimap B,\Theta\vdash
C}~{}{\rm{(\multimap L)}}~{}\cfrac{\Gamma,A\vdash B}{\Gamma\vdash A\multimap
B}~{}{\rm{(\multimap R)}}$
$\cfrac{\Gamma,A\vdash C}{\Gamma,\exists xA\vdash C},~{}x\not\in
FV(\Gamma,C)~{}{\rm{(\exists L)}}$
$\quad\cfrac{\Gamma\vdash A}{\Gamma\vdash\forall xA},~{}x\not\in
FV(\Gamma)~{}{\rm{(\forall R)}}$
$\quad\cfrac{\Gamma\vdash A[x:=t]}{\Gamma\vdash\exists xA}~{}{\rm{(\exists
R)}}~{}\cfrac{\Gamma,A[x:=t]\vdash C}{\Gamma,\forall xA\vdash C}{\rm{(\forall
L)}}$

(b) MILL1 sequent calculus

$Pred_{-}=\\{\overline{p}|~{}p\in Pred_{+}\\},\quad
arity({\overline{p}})=arity({p}),\quad Pred=Pred_{+}\cup Pred_{-}$.
$Fm::=At|(Fm\otimes Fm)|(Fm\parr Fm)|\forall xFm|\exists xFm,~{}x\in Var$
$\overline{p(e_{1},\ldots,e_{n})}=\overline{p}(e_{n},\ldots,e_{1}),\quad\overline{\overline{p(e_{1},\ldots,e_{n})}}=p(e_{n},\ldots,e_{1})\mbox{
for }P\in N_{+},$ $\overline{A\otimes
B}=\overline{B}\parr\overline{A},\quad\overline{A\parr
B}=\overline{B}\otimes\overline{A},\quad\overline{\forall xA}=\exists
x(\overline{A}),\quad\overline{\exists xA}=\forall x(\overline{A})$.

(c) MLL1 language

${\vdash\overline{A},A},~{}A\in
At~{}(\mbox{Id})\quad\cfrac{\vdash\Gamma,A\quad\vdash\overline{A},\Theta}{\vdash\Gamma,\Theta}~{}(\mbox{Cut})$
$\cfrac{\vdash\Gamma,A,B}{\vdash\Gamma,A\parr
B}~{}(\parr)\quad\cfrac{\vdash\Gamma,A\quad\vdash
B,\Theta}{\vdash\Gamma,A\otimes B,\Theta}~{}{}(\otimes)$
$\cfrac{\vdash\Gamma A}{\vdash\Gamma,\forall xA},~{}x\not\in
FV(\Gamma)~{}(\forall)$
$\cfrac{\vdash\Gamma A[x:=e]}{\vdash\Gamma,\exists xA},~{}x\not\in
FV(\Gamma)~{}(\exists)$.

(d) MLL1 sequent calculus

$A\multimap B=B\parr\overline{A}$.
$\quad\begin{array}[]{rcl}A_{1},\ldots,A_{n}\vdash_{\bf
MILL1}B&\Longleftrightarrow&\vdash_{\bf
MLL1}B,\overline{A_{n}},\ldots,\overline{A_{1}}.\end{array}$

(e) Translating MILL1 to MILL1

$Fm::=Prop|(Fm\backslash Fm)|(Fm/FM)|(Fm\bullet Fm)$

${A\vdash A}~{}(\mbox{Id})~{}\cfrac{\Gamma\vdash
A\quad\Theta_{1},A,\Theta_{2}\vdash B}{\Theta_{1},\Gamma,\Theta_{2}\vdash
B}~{}(\rm{Cut})$
$\cfrac{\Gamma,A\vdash B}{\Gamma\vdash B/A}~{}(/\rm{R})~{}\cfrac{\Gamma\vdash
A\quad\Theta_{1},B,\Theta_{2}\vdash C}{\Theta_{1},B/A,\Gamma,\Theta_{2}\vdash
C}~{}(/\rm{L})$
$\cfrac{\Theta_{1}\vdash A\quad\Theta_{2}\vdash B}{\Theta_{1},\Theta_{2}\vdash
A\bullet B}~{}(\bullet\rm{R})~{}\cfrac{\Theta_{1},A,B,\Theta_{2}\vdash
C}{\Theta_{1},A\bullet B,\Theta_{2}\vdash C}~{}(\bullet\rm{L})$
$\cfrac{A,\Gamma\vdash B}{\Gamma\vdash A\backslash
B}~{}(\backslash\rm{R})~{}\cfrac{\Gamma\vdash
A\quad\Theta_{1},B,\Theta_{2}\vdash C}{\Theta_{1},\Gamma,A\backslash
B,\Theta_{2}\vdash C}~{}(\backslash\rm{L})$

(f) LC language and sequent rules

$||p||^{(l,r)}=p(l,r)\mbox{ for }p\in Prop$,
$||A\bullet B||^{(l,r)}=\exists x||A||^{(l,x)}\otimes||B||^{(x,r)}$,
$||B/A||^{(l,r)}=\forall x||A||^{(r,x)}\multimap||B||^{(l,x)}$,
$||A\backslash B||^{(l,r)}=\forall x||A||^{(x,l)}\multimap||B||^{(x,r)}$.

$\begin{array}[]{rcl}A_{1},\ldots,A_{n}\vdash_{\bf
LC}B&\Longleftrightarrow&||A_{1}||^{(c_{0},c_{1})},\ldots,||A_{n}||^{(c_{n-1},c_{n})}\vdash_{\bf
MILL1}||B||^{(c_{0},c_{n})}.\end{array}$

(g) Translating LC to MILL1

Figure 1: Systems of linear logic

We will use notation $\Gamma\vdash_{\bf MILL1}C$ to indicate that the sequent
$\Gamma\vdash C$ is derivable in MILL1 and a similar convention for other
systems considered in this work.

The language of classical first order multiplicative linear logic (MLL1) is
summarized in Figure 1(c). We assume that we are given a set $Pred_{+}$ of
positive predicate symbols with assigned arities, and sets $Var$ and $Const$
of variables and constants. Then the set $Pred_{-}$ of negative predicate
symbols and the set $Pred$ of all predicate symbols are defined. Atomic
formulas are defined same as for MILL1. Formulas are built from the binary
connectives $\otimes$, $\parr$ and quantifiers, the connective $\parr$ is
called cotensor (also par). Linear negation $\overline{(.)}$ is not a
connective, but is definable by induction on formula construction, as in
Figure 1(c). Note that, somewhat non-traditionally, we follow the convention
that negation flips tensor/cotensor factors, typical for noncommutative
systems. This does not change the logic (the formulas $A\otimes B$ and
$B\otimes A$ are provably equivalent), but is more consistent with our
intended geometric interpretation.

Contexts are defined same as for MILL1. The sequent calculus for ${\bf MLL1}$
is shown in Figure 1(d). Translation in Figure 1(e) identifies MILL1 as a
conservative fragment of MLL1.

The language and sequent calculus formulation of Lambek calculus (LC) are
summarised in Figure 1(f). Formulas are built from a set $Prop$ of
propositional symbols, and contexts are sequences, rather than multisets, of
formulas.

Given two variables or constants $l,r$, the first order translation
$||F||^{(l,r)}$ of an LC formula $F$ parameterized by $l,r$ is shown in Figure
1(g) (LC propositional symbols are treated as binary predicate symbols). This
embeds LC into MILL1 as a conservative fragment [8]

##  3 MILL1 grammars and strictly balanced fragment

Translation from LC suggests defining MILL1 grammars similar to Lambek
grammars.

Let a finite alphabet $T$ of terminal symbols be given. Assume also that our
first order language contains all integer constants and two special constants
$l,r$.

Let us say that a MILL1 lexical entry is a pair $(w,A)$, where $w\in T^{*}$ is
nonempty, and $A$ is a MILL1 formula with one occurrence of $l$ and one
occurrence of $r$ and no other constants or free variables. For the formula
$A$ occurring in a simple lexical entry we will write
$A[x;y]=A[l:=x_{1},r:=y_{1}]$ (so that $A=A[l;r]$).

A MILL1 grammar $G$ is a pair $(Lex,S)$, where $Lex$ is a finite set of MILL1
lexical entries, and $S$ is a binary predicate symbol. The language $L(G)$
generated by $G$ or, simply, the language of $G$ is defined as

$L(G)=\\{w_{1}\ldots w_{n}|~{}(w_{1},A_{1}),\ldots,(w_{m},A_{n})\in
Lex,~{}A_{1}[0;1],\ldots,A_{n}[{n-1};n]\vdash_{\bf MILL1}S(0,n)\\}.$

It seems clear that, under such a definition, Lambek grammars translate to
MILL1 grammars generating the same language.

It has been shown [6], [7] that MILL1 allows representing more complex systems
such as displacement calculus, abstract categorial grammars, hybrid type-
logical grammars. This suggests that the above definition should be
generalized to allow more complex lexical entries, corresponding to word
tuples rather than just words. On the other hand, it seems evident that in
translations from grammatical formalisms we may restrict to smaller fragments
of MILL1.

###  3.1 Balanced sequents

We equip the first order language with an extra structure. We say that the
language is balanced if each $n$-ary predicate symbol $p$ is equipped with a
valency, which is a pair $(k,m)$ of nonnegative integers with $k+m=n$. We
indicate it in notation by writing corresponding atomic formulas as
$p(x_{1},\ldots,x_{k};y_{1},\ldots,y_{m})$, with first $k$ entries separated
by a semicolon. In this setting, we say that $x_{1},\ldots,x_{k}$ are left
occurrences, or have left polarity, notation $sgn(x_{i})=-1$, and
$y_{1},\ldots,y_{m}$ are right occurrences, $sgn(y_{i})=+1$. We extend the
notion of occurrence polarity to compound formulas and sequents by induction.

In the intuitionistic language the definition is as follows. For an occurrence
$x$ in an immediate subformula $A$ of a compound formula $F$, the polarity
$sgn_{F}(x)$ of $x$ in $F$ is defined by $sgn_{F}(x)=-sgn_{A}(x)$ if
$F=A\multimap B$ and $sgn_{F}(x)=sgn_{A}(x)$ otherwise. For an occurrence $x$
in a formula $F$ of a sequent $\Gamma\vdash C$, the polarity
$sgn_{\Gamma\vdash C}(x)$ of $x$ in the sequent is defined by
$sgn_{\Gamma\vdash C}(x)=-sgn_{F}(x)$, if $F\in\Gamma$, and $sgn_{\Gamma\vdash
C}(x)=sgn_{F}(x)$ if $F=C$.

In the case of MLL1 we require that valencies of dual predicate symbols be
consistent, so that
$\overline{p(x_{1},\ldots,x_{k};y_{1},\ldots,y_{m})}=\overline{p}(y_{m},\ldots,y_{1};x_{k},\ldots,x_{1})$.
Then the polarity of an occurrence in a formula or a sequent is just the same
as its polarity in the corresponding atomic formula. Obviously, the embedding
of MILL1 to MLL1 preserves polarities.

We say that a first order formula (context, sequent) is balanced if every
quantifier binds exactly one left and one right variable occurrence. A
balanced formula (context, sequent) is strictly balanced if, furthermore, it
has at most one left and at most one right occurrence of any free variable or
constant. It is immediate that if a strictly balanced sequent is derivable (in
MILL1 or MLL1 ) then every free variable or constant occurring in it has
exactly one occurrence of each polarity. We will say that a MILL1 grammar is
balanced if the formula in every lexical entry is strictly balanced, with
constants $l$ and $r$ occurring with left and right polarity respectively.

It is immediate that if we treat LC propositional symbols as predicate symbols
of valency $(1,1)$, then the translation in Figure 1(g) indeed uses only the
strictly balanced fragment. Similar observations apply to translations in [6],
[7].

###  3.2 Occurrence nets

Below we are discussing derivations of balanced and strictly balanced sequents
in MLL1. The discussion can be adapted to the intuitionistic case using the
standard embedding. In the following we will say simply occurrence meaning
occurrence of a variable or a constant.

$\vdash a(e;t),\overline{a}(t;e)\otimes a(e;s),\overline{a}(s;e)$
$(\exists)$$\Longrightarrow$$\vdash a(e;t),\exists x(\overline{a}(t;x)\otimes
a(x;s)),\overline{a}(s;e)$ Figure 2: Occurrence nets example

An occurrence net of a balanced MLL1 sequent $\vdash\Gamma$ is a perfect
matching $\sigma$ between left and right free occurrences in $\Gamma$, such
that each pair (link) in $\sigma$ consists of occurrences of the same variable
(constant). Note that for a strictly balanced sequent there is only one
occurrence net possible. Basically, occurrence nets are rudiments of proof-
nets. To each cut-free derivation $\pi$ of $\vdash\Gamma$ we assign by
induction an occurrence net $\sigma(\pi)$.

For an axiom $\vdash\overline{X},X$, where $X={p}(e_{1},\ldots,e_{n})$, the
net is defined by matching an occurrence $e_{i}$ in $X$ with the occurrence
$e_{i}$ in $\overline{X}=\overline{p}(e_{n},\ldots,e_{1})$. For $\pi$ obtained
from a derivation $\pi^{\prime}$ by the $(\parr)$ rule, we put
$\sigma(\pi)=\sigma(\pi^{\prime})$ For $\pi$ obtained from derivations
$\pi_{1}$, $\pi_{2}$ by the $(\otimes)$ rule,
$\sigma(\pi)=\sigma(\pi_{1})\cup\sigma(\pi_{2})$. If $\pi$ is obtained from
some $\pi^{\prime}$ by the $(\forall)$ rule introducing a formula $\forall
xA$, then the variable $x$ has no free occurrences in the premise other than
those in $A$, and, since the sequent is balanced, there is precisely one left
and one right occurrence of $x$ in $A$, say, $x_{l}$ and $x_{r}$. It follows
that $(x_{l},x_{r})\in\sigma(\pi^{\prime})$ and we put
$\sigma(\pi)=\sigma(\pi^{\prime})\setminus\\{(x_{l},x_{r})\\}$. The rule
erases the link $(x_{l},x_{r})$ from the occurrence net.

Finally, let $\pi$ be obtained from $\pi^{\prime}$ by the $(\exists)$ rule
applied to a formula $A^{\prime}=A[x:=e]$ and introducing the formula $\exists
xA$. Since the sequent is balanced, there is exactly one left and one right
occurrence of $x$ in $A$, and to them correspond a left and a right occurrence
of $e$ in $A^{\prime}$, say $e_{l}$ and $e_{r}$. There are two cases.

If $(e_{l},e_{r})\in\sigma(\pi^{\prime})$, put
$\sigma(\pi)=\sigma(\pi^{\prime})\setminus\\{(e_{l},e_{r})\\}$. The rule
erases a link. Otherwise let $e_{l}^{\prime}$, $e_{r}^{\prime}$ be such that
$(e_{l}^{\prime},e_{r}),(e_{l},e_{r}^{\prime})\in\sigma(\pi^{\prime})$. Put
$\sigma(\pi)=\sigma(\pi^{\prime})\setminus\\{(e_{l}^{\prime},e_{r}),(e_{l},e_{r}^{\prime})\\}\cup\\{(e_{l}^{\prime},e_{r}^{\prime})\\}$.
The rule glues two links into one. An example for the latter case is shown in
Figure 2.

The following is easily proved by induction on derivation.

###### Proposition 3.1

Let $\pi$ be a cut-free derivation of a balanced sequent $\vdash\Gamma$, and
assume that $(e_{l},e_{r})\in\sigma(\pi)$. Let $e^{\prime}$ be a fresh
variable or constant and $\Gamma^{\prime}=\Gamma[e_{l},e_{r}:=e]$.

Then $\vdash\Gamma^{\prime}$ is derivable in MLL1 with a derivation
$\pi^{\prime}$ of the same size as $\pi$ and
$\sigma(\pi^{\prime})=\sigma(\pi)\setminus\\{(e_{l},e_{r})\\}\cup\\{(e_{l}^{\prime},e_{r}^{\prime})\\}$.
$\Box$

###  3.3 Strictly balanced derivations

Note that for all sequent rules except $(\exists)$, if the conclusion is
strictly balanced so are the premises. We will supply an admissible rule
$(\exists^{\prime})$, alternative to $(\exists)$, which applies to strictly
balanced sequents only and, therefore, satisfies the same property.

So assume that we have a derivable strictly balanced sequent $\vdash\Theta$,
where $\Theta=\Gamma,A$. Assume that $A$ has a left free occurrence $s_{l}$
and a right free occurrence $t_{r}$ of a variable (constant) $s,t$
respectively, with $s\not=t$. Let $e$ be a fresh variable or constant. Let
$\Theta^{\prime}=\Theta[s,t:=e]$. By Proposition 3.1 the sequent
$\vdash\Theta^{\prime}$ is derivable.

Now, let us write $\Theta^{\prime}=\Gamma^{\prime}A^{\prime}$, where
$A^{\prime}$ is the image of $A$ in $\Theta^{\prime}$. Let $e_{l}$, $e_{r}$ be
the occurrences of $e$ in $A^{\prime}$ that replace $s_{l}$ and $t_{r}$
respectively. Then the strictly balanced sequent
$\vdash\Theta^{\prime\prime}$, where
$\Theta^{\prime\prime}=\Gamma^{\prime},\exists xA^{\prime}[e_{l},e_{r}:=x]$,
is derivable from $\vdash\Theta^{\prime}$ by the $(\exists)$ rule.

We say that $\vdash\Theta^{\prime\prime}$ is obtained from $\vdash\Theta$ by
the $(\exists^{\prime})$ rule. Note that, on the level of occurrence nets,
seen as bipartite graphs, the $(\exists^{\prime})$ rule does the same gluing
as $(\exists)$; only vertex labels are changed.

We will say that derivations of strictly balanced sequents using rules of MLL1
and the $(\exists^{\prime})$ rule and involving only strictly balanced
sequents are strictly balanced derivations.

###### Lemma 3.2

A strictly balanced sequent $\vdash\Theta$ derivable in MLL1 is derivable with
a strictly balanced derivation.

Proof by induction on a cut-free derivation. If $\vdash\Theta$ is the
conclusion of the $(\exists)$ rule applied to non-strictly balanced premise,
then, using Proposition 3.1, we replace the premise with a strictly balanced
sequent and obtain $\vdash\Theta$ by the $(\exists^{\prime})$ rule. $\Box$

Thus, adding the $(\exists^{\prime})$ rule, we obtain a kind of intrinsic
deductive system for the strictly balanced fragment. It seems though that the
usual syntax of first order sequent calculus is not very natural for such a
system, and some other representation might be desirable.

##  4 Tensor type calculus

###  4.1 Tensor terms

We assume that we are given an infinite set $\mathit{Ind}$ of indices. They
will be used in all syntactic objects (terms, types, typing judgements) that
we consider.

Let $T$ be an alphabet of terminal symbols. The set $\widetilde{TmEx}$ of
provisional tensor term expressions is the free commutative monoid generated
by the set

$\\{[w]^{i}_{j}|~{}i,j\in\mathit{Ind},w\in T^{*}\\}\cup\\{[w]|~{}w\in
T^{*}\\},$ (1)

and the set $\widetilde{Tm}$ of provisional tensor terms is the quotient of
$\widetilde{TmEx}$ by the relations

$[u]^{j}_{i}\cdot[v]^{k}_{j}=[uv]^{k}_{i},\quad[w]^{i}_{i}=[w],\quad[a_{1}\ldots
a_{n}]=[a_{n}a_{1}\ldots a_{n-1}]\mbox{ for }a_{1},\ldots,a_{n}\in T$ (2)

(we write the monoid operation multiplicatively and the monoid unit as $1$). A
tensor term expression is a provisional tensor term expression in which any
index has at most one occurrence as an upper one and at most one occurrence as
a lower one. The set $Tm$ of tensor terms is the image of the set $TmEx$ of
term expressions in $\widetilde{Tm}$ under the quotient map. (The adjective
“tensor” will often be omitted in the following.)

Elements of generating set (1) are elementary term expressions. Elementary
expressions of the form $[w]^{j}_{i}$ with $i\not=j$ are regular term
expressions. A tensor term is regular if it is the image of the product of
regular term expression. Otherwise the term is singular.

We think of regular terms as bipartite graphs whose vertices are labeled with
indices and edges with words, and direction of edges is from lower indices to
upper ones. Singular terms such as $[w]^{i}_{i}=[w]$ correspond to closed
loops (with no vertices) labeled with cyclic words (this explains the last
relation in (2)). Thus, a regular term expression $[w]_{i}^{j}$, $i\not=j$,
corresponds to a single edge from $i$ to $j$ labeled with $w$, the product of
two term expressions without common indices is the disjoint union of the
corresponding graphs, and a term expression with repeated indices corresponds
to a graph obtained by gluing edges along matching vertices. The monoidal unit
$1$ corresponds to the empty graph. As for singular terms, they arise when
edges are glued cyclically.

We say that an index occurring in a term expression $t$ is free in $t$, if it
occurs in $t$ once. Otherwise we say that the index is bound. We say that a
term expression is normal if it has no bound indices. The sets of free upper
and lower indices of a term expression are invariant under the quotient map to
$Tm$, so they are well-defined for terms as well. We denote the set of free
upper, respectively lower, indices of a tensor term $t$ as $FSup(t)$,
respectively $FSub(t)$.

The geometric representation makes especially obvious that any tensor term $t$
is the image of a normal term expression and can be written as the product
$t=reg(t)\cdot t^{\prime}$, where $reg(t)$ is regular and $t^{\prime}$ is $1$
or the product of elementary singular expressions. We say that $reg(t)$ is the
regular part of $t$.

Especially important are terms of the form
$\delta^{j}_{i}=[\epsilon]^{j}_{i}$, where $\epsilon$ denotes the empty word.
We will also use the notation $\delta^{i_{1}\ldots i_{n}}_{j_{1}\ldots
j_{n}}=\delta^{i_{1}}_{j_{1}}\cdots\delta^{i_{n}}_{j_{n}}$.

We call terms of the above format Kronecker deltas. We will adopt the
convention that capital Latin letters stand for sequences of indices and small
Latin letters stand for individual indices. Typically, a Kreoneker delta will
be written concisely as $\delta^{I}_{J}$.

Multiplication by Kronecker deltas amounts to renaming indices. If $t$ is a
tensor term expression with $i\in FSup(t)$, $j\in FSub(t)$, and
$i^{\prime},j^{\prime}\not\in\mathit{Ind}(t)$, then
$\delta_{i}^{i^{\prime}}\cdot t$ is the term $t$ with $i$ changed to
$i^{\prime}$, and $\delta_{j^{\prime}}^{j}\cdot t$ is $t$ with $j$ changed to
$j^{\prime}$.

There is also a “divergent” delta $\delta=\delta^{i}_{i}=[\epsilon]$ that
corresponds to a closed loop with no label.

###  4.2 Tensor types

Our goal is to assign types to tensor terms.

The set $\widetilde{Tp}$ of provisional tensor types is built according to the
grammar in Figure 3(a). We assume that we are given a set $Lit_{+}$ of
positive atomic type symbols or positive literals, and every element $p\in
Lit_{+}$ is assigned a valency $v(p)\in\mathbb{N}^{2}$. Then the set $Lit_{-}$
of negative atomic type symbols and the set $Lit$ of all atomic type symbols
are defined. The convention for negative atomic symbols is that
$v(\overline{p})=(m,n)$ if $v(p)=(n,m)$. Duality $\overline{(.)}$ is not a
connective or operator but is definable.

The symbols $\nabla,\Delta$ are binding operators. These bind indices exactly
in the same way as quantifiers bind variables. The operator
$Q\in\\{\nabla,\Delta\\}$ in front of an expression $Q^{i}_{j}A$ has $A$ as
its scope and binds all lower, respectively, upper occurrences of $i$,
respectively, $j$ in $A$ that are not already bound by some other operator. A
tensor type is a provisional tensor type in which any index has at most one
free occurrence (no matter, upper or lower) and every binding operator binds
exactly one lower and one upper index occurrence. We will denote the set of
upper, free upper, lower, free lower indices occurring in a type $A$ as
$Sup(A)$, $FSup(A)$, $Sub(A)$, $FSub(A)$ respectively. We say that tensor
types are $\alpha$-equivalent if they differ by renaming bound indices in a
usual way.

$Lit_{-}=\\{\overline{p}|~{}p\in Lit_{+}\\}$, $\quad\overline{\overline{p}}=p$
for $p\in Lit_{+}$, $\quad Lit=Lit_{+}\cup Lit_{-}$.
$\widetilde{At}=\\{p_{j_{1}\ldots j_{n}}^{i_{1}\ldots i_{m}}|~{}p\in
Lit,v(p)=(m,n),i_{1},\ldots,i_{m},j_{1},\ldots,j_{n}\in\mathit{Ind}\\}$.
$\widetilde{Tp}::=\widetilde{At}|(\widetilde{Tp}\otimes\widetilde{Tp})|(\widetilde{Tp}\parr\widetilde{Tp})|\nabla^{i}_{j}\widetilde{Tp}|\Delta^{i}_{j}\widetilde{Tp},~{}i,j\in\mathit{Ind},~{}i\not=j$.
$\overline{p^{I}_{J}}=\overline{p}^{\overline{J}}_{\overline{I}}\mbox{ for
}p\in Lit$, where $\overline{I}=({i_{n}},\ldots,{i_{1}})$ for
$I=(i_{1},\ldots,i_{n})$.
$\overline{A\otimes B}=\overline{B}\wp\overline{A},\quad\overline{A\wp
B}=\overline{B}\otimes\overline{A},\quad\overline{\nabla_{i}^{j}A}=\triangle^{i}_{j}\overline{A},\quad\overline{\triangle_{i}^{j}A}=\nabla^{i}_{j}\overline{A}.$

(a) Language

$\begin{array}[]{rl}\delta^{I^{\prime}\overline{J}}_{\overline{I}J^{\prime}}\vdash{p}^{I}_{J},\overline{p}_{I^{\prime}}^{J^{\prime}},~{}p\in
Lit~{}({\rm{Id}})&\cfrac{t\vdash\Gamma,A\quad
s\vdash\overline{A},\Theta}{ts\vdash\Gamma,\Theta}~{}({\rm{Cut}})\\\
\cfrac{t\vdash\Gamma,A,B}{t\vdash\Gamma,A\parr
B}~{}(\parr)~{}\cfrac{t\vdash\Gamma,A\quad s\vdash
B,\Theta}{ts\vdash\Gamma,A\otimes
B,\Theta}~{}(\otimes)&\cfrac{\delta_{\beta}^{\alpha}\cdot
t\vdash\Gamma,A}{t\vdash\Gamma,\nabla^{\alpha}_{\beta}A}~{}(\nabla)~{}\cfrac{t\vdash\Gamma,A}{\delta^{\beta}_{\alpha}\cdot
t\vdash\Gamma,\triangle_{\beta}^{\alpha}A}~{}(\triangle).\end{array}$

(b) ETTC typing rules

xyba$i$$j$$k$$l$$r$$s$$\Leftrightarrow$$[xy]_{s}^{i}\cdot[ba]_{j}^{l}\cdot[\delta]_{r}^{k}\vdash
a_{i}\otimes b^{j}_{kl},c^{rs}$ (c) Picture for a typing judgement

${I}$($\delta_{I^{\prime}\overline{J}}^{\overline{I}J^{\prime}}\vdash\overline{p}^{I^{\prime}}_{J^{\prime}},p_{I}^{J}$)$\overline{p}$${J}$$J^{\prime}$${p}$$I^{\prime}$
(d) Picture for an axiom

$t$$s$$\Gamma$$a$$\Delta$$\overline{a}$$\Rightarrow$$t$$\Gamma$$s$$\Delta$$(\mbox{cut})$
(e) Picture for a cut

$t$$\Gamma$$a$$\beta$$\alpha$$\Rightarrow$$t$$\Gamma$$\nabla_{\beta}^{\alpha}a$
(f) Picture for a $(\nabla)$ rule

$t$$\Gamma$$a$$\beta$$\alpha$$\Rightarrow$$t$$\Gamma$$\triangle_{\beta}^{\alpha}a$
(g) Picture for a $(\triangle)$ rule

$b$$\overline{a}$string1string2 (h) Picture for $a\multimap b$

$b$$\overline{a}$string (i) $b/a$ inside $a\multimap b$

$b$$\overline{a}$string  (j) $a\backslash b$ inside $a\multimap b$

$a^{I}_{J}\multimap
b^{K}_{L}=b^{K}_{L}\parr\overline{a}^{I}_{J},\quad(b/a)^{i}_{j}=\nabla^{\alpha}_{\beta}(b^{i}_{\alpha}\wp\overline{a}_{j}^{\beta}),\quad(a\backslash
b)^{i}_{j}=\nabla^{\alpha}_{\beta}(\overline{a}_{\alpha}^{i}\wp
b_{j}^{\beta}).$

(k) Encoding different implications in ETTC

Figure 3: ETTC

We also define tensor type symbols as, basically, $\alpha$-equivalence classes
of tensor types with all free indices erased. That is, tensor type symbol is
an equivalence class for the smallest equivalence relation on tensor types
that identifies any two $\alpha$-equivalent types and any two types obtained
from each other by renaming a free index. Valency $v(a)$ of a type symbol $a$
is a pair $(n,m)$, where $n$ and $m$ are the numbers of, respectively, free
upper and free lower indices in corresponding types.

Usually we will denote types with capital letters and type symbols with small
letters. A tensor type, up to $\alpha$-equivalence, can be recovered from its
symbol by specifying the sequences of its upper and lower free indices.
Accordingly, we will write $A=a^{I}_{J}$ to indicate that $A$ is a type whose
symbol is $a$, and sequences of free upper and lower indices are $I$ and $J$
respectively. Sometimes we will have enumerations of type symbols, such as
$a_{(1)},\ldots,a_{(n)}$. In such cases we will put brackets around subscripts
in order to avoid confusion with tensor type indices.

A tensor type context is a finite set of tensor types whose elements have no
common free indices. We extend the notation for sets of upper, free upper,
lower and free lower indices from types to type contexts in the obvious way
and write $Sup(\Gamma)=\bigcup\limits_{A\in\Gamma}Sup(A)$ etc.

###  4.3 Typing judgements and rules

A tensor typing judgement is a pair $(t,\Gamma)$, written as $t\vdash\Gamma$,
where $\Gamma$ is a tensor type context, and $t$ is a tensor term, such that
$FSup(t)=FSub(\Gamma)$, $FSub(t)=FSup(\Gamma)$.

Typing judgements are derived using the rules of extended tensor type calculus
(ETTC) [13] in Figure 3(b). (The title “extended” refers in [13] to usage of
binding operators, which extend plain types of MLL.)

It is implicit in the rules that all typing judgements are well defined, i.e.
there are no index collisions. In the $(\nabla)$ and $(\Delta)$ rules it is
required that $\alpha\in FSub(A)$, $\beta\in FSup(A)$. Note that the term $t$
in the premise of the $(\triangle)$ rule must have free occurrences of
$\alpha$ and $\beta$ (as an upper and a lower index respectively). In the
conclusion, the term $\delta^{\beta}_{\alpha}\cdot t$ has these occurrences
bound. Thus free indices to the left and to the right of the turnstile do
match, and the typing judgement is well defined.

It is not hard to see that ETTC is cut-free [13]. Note also that the system
does not use any terminal alphabet. Terminal symbols will appear in nonlogical
axioms, i.e. lexical entries of formal grammars.

Let us define $\alpha$-equivalence of tensor typing judgements as the smallest
equivalence relation identifying typing judgements that can be obtained from
each other by renaming bound indices in types or, for a free index, by
replacing both its occurrences to the right and to the left of the turnstile
with a fresh one. Then, obviously, derivable typing judgements are closed
under $\alpha$-equivalence. $\alpha$-Equivalent typing judgements are
essentially “the same”; nothing is lost even if we identify them as in [13].

####  4.3.1 Geometric representation and meaning

While tensor terms have a natural interpretation as edge-labeled graphs,
tensor typing judgements suggest some particular pictorial representation for
such graphs. A type to the right of the turnstile can be seen as inducing an
ordering on the set of free indices, for example, from left to right, from top
to bottom, and this can be seen as an ordering of vertices in a picture. Thus,
a typing judgement $t\vdash F$ can be depicted as the graph representing the
term $t$ with vertices aligned, say, horizontally according to the ordering
induced by $F$. (Bound indices of $F$ are not in the picture.) An example of a
concrete typing judgement representation is given in Figure 3(c). Note that
such a representation identifies $\alpha$-equivalent judgements, and the
indices usually become redundant, at least, in the absence of binding
operators.

Some schematic pictures corresponding to rules of ETTC are shown in Figure 3.
The $(\triangle)$ rule simply glues together two bound indices/vertices. On
the other hand, the $(\nabla)$ rule is applicable only in the case when the
corresponding indices/vertices are connected with an edge carrying no label.
Then this edge (together with its endpoints) is erased from the picture
completely. The information about the erased edge is stored in the introduced
type.

Thus, terms of type $\nabla^{\alpha}_{\beta}A$ encode the subtype of $A$
consisting of terms/graphs with that specific form: vertices corresponding to
$\alpha$ and $\beta$ are connected with an edge, and the connecting edge
carries no label. It can be observed that we have the admissible rule
$\cfrac{t\vdash\Gamma,\nabla^{\alpha}_{\beta}A}{\delta^{\alpha}_{\beta}\cdot
t\vdash\Gamma,A}~{}(\nabla{\rm{E}})$, so that “decoding” from
$\nabla^{\alpha}_{\beta}A$ to $A$ is always possible.

Let $a$, $b$ be type symbols of valency $(1,1)$, so that regular elements of
the corresponding types are strings. The implication type symbol $a\multimap
b=b\wp\overline{a}$ has valency $(2,2)$, and elements of the corresponding
type can be interpreted as pairs of strings, as Figure 3(h) suggests. Now,
there are two subtypes consisting of elements of the forms respectively
$[u]_{l}^{i}\cdot\delta_{k}^{j}$ and $[u]_{k}^{j}\cdot\delta_{l}^{i}$
corresponding to Figures 3(i), 3(j). It is easily computed that elements of
the first form act (by means of the Cut rule) on elements of $a_{k}^{l}$ by
multiplication (concatenation) on the left, and elements of the second form,
by multiplication on the right. The two formats identify two subtypes of the
implicational tensor type that correspond to two implicational types of Lambek
calculus. Which suggests that the implicational types of Lambek calculus
should be translated to ETTC as in Figure 3(k) (compare with Figure 1(g)).

###  4.4 Relation with first order logic

Given a balanced first order language, we identify predicate symbols with
atomic type symbols of the same valencies. For an MLL1 strictly balanced
context $\Gamma$, let $X$ be the set variables and constants occurring in
$\Gamma$ (not necessarily freely) and choose non-intersecting subsets
$I,J\subset\mathit{Ind}$ together with a pair of bijections $\pi:X\to I$,
$\rho:X\to J$. Translation of subformulas of $\Gamma$ to tensor types is given
by

$||a(x_{1},\ldots,x_{n};y_{1},\ldots,y_{m})||^{\rho}_{\pi}=a^{\rho(x_{1})\ldots\rho(x_{n})}_{\pi(y_{1})\ldots\pi(y_{m})}\mbox{
for }a\in N,$ $||\forall
xA||^{\rho}_{\pi}=\nabla^{\pi(x)}_{\rho(x)}||A||^{\rho}_{\pi},\quad||\exists
xA||^{\rho}_{\pi}=\Delta^{\pi(x)}_{\rho(x)}||A||^{\rho}_{\pi}$

(with binary connectives obviously translating to themselves).

###### Lemma 4.1

There is a translation assigning to any strictly balanced derivation of
$\vdash\Gamma$ a derivable tensor typing judgement
$\tau\vdash||\Gamma||^{\rho}_{\pi}$, where the regularization $reg(\tau)$ is,
independent of a particular derivation, the product of all Kronecker deltas
$\delta^{\pi(x)}_{\rho(x)}$, where $x$ ranges over all free occurrences in
$\Gamma$. Conversely, any derivable tensor typing judgement is obtained as a
translation of a strictly balanced MLL1 derivation.

Proof The translation is by induction on strictly balanced derivation. The
regular part $reg(\tau)$ encodes the unique occurrence net of $\Gamma$. Axioms
and propositional rules translate to themselves. The $(\forall)$ rule
translates to the $(\nabla)$ rule, while the $(\exists)$ and
$(\exists^{\prime})$ rules translate as the $(\Delta)$ rule. An interesting
case is that of the $(\exists)$ rule. When applied to a strictly balanced
sequent, it erases a link from the occurrence net, just as the $(\forall)$
rule. As for the $(\Delta)$ rule in this case, it glues together the
corresponding link endpoints, producing a closed loop, divergent $\delta$. The
link is removed from the regular part, but not from the term entirely. The
second claim of the lemma is proven by induction on ETTC derivations. $\Box$

We observe that, in general, the tensor translation does indeed depend on the
derivation, only the regular part of the term is completely determined by the
sequent.

##  5 Tensor natural deduction and grammars

In order to give a natural deduction formulation for ETTC we need to allow
variables standing for tensor terms. Thus we introduce a countable set of
tensor variable symbols of different valencies (where valency, as usual, is a
pair of nonnegative integers) and the convention that if $x$ is a variable
symbol of valency $(m,n)$ and $i_{1},\ldots,i_{m}$, $j_{1},\ldots,j_{m}$ are
pairwise distinct indices, then $x^{i_{1}\ldots i_{n}}_{j_{1}\ldots j_{m}}$ is
a tensor variable. Similarly to types and type symbols, we will use small
letters for variable symbols and capital letters for variables; typically, we
will write $X=x^{I}_{J}$.

Natural deduction tensor term expressions and terms are defined from
provisional term expressions exactly as in Section 4.1, with the modification
that we add to generators (1) of the provisional monoid $\widetilde{TmEx}$ all
tensor variables, and to defining relations (2) all possible equations

$\delta^{i}_{j}x_{IiJ}^{K}=x_{IjJ}^{K},\quad\delta^{i}_{j}x^{IjJ}_{K}=x^{IiJ}_{K}.$

In the following we abbreviate the title “natural deduction” as “n.d.”.

An n. d. tensor typing judgement is an expression of the form $t:A$, where $t$
is a natural deduction term and $A$ is a tensor type, with $Fsup(t)=Fsub(A)$,
$Fsub(t)=Fsup(A)$ (basically, we use a colon instead of a turnstile). A
variable declaration is a typing judgement with a tensor variable to the left
of the colon, and an n.d. typing context is a finite set of variable
declarations which have no common variable symbols. An n.d. tensor sequent is
an expression of the form $\Gamma\vdash\sigma$, where $\Gamma$ is an n.d.
typing context and $\sigma$ is an n.d. typing judgement. Natural deduction
system of ETTC is given by the rules in Figure 4(a).

$X:A\vdash X:A~{}(\rm{Id})\quad\quad\quad\quad\quad\quad\quad\quad$
$\begin{array}[]{rl}\cfrac{\Gamma,x^{I}_{J}:a^{J}_{I}\vdash x^{K}_{L}\cdot
t:B}{\Gamma\vdash
t\cdot\delta^{J^{\prime}\overline{K}}_{\overline{L}I^{\prime}}:B\parr\overline{a}^{{I^{\prime}}}_{{J^{\prime}}}}~{}(\parr{\rm{I}})&\cfrac{\Gamma\vdash
s:B\parr\overline{A}\quad\Theta\vdash t:{A}}{\Gamma,\Theta\vdash
st:B}~{}(\parr{\rm{E}})\\\ \cfrac{\Gamma\vdash t:A\quad\Theta\vdash
s:B}{\Gamma,\Theta\vdash ts:A\otimes
B}~{}(\otimes{\rm{I}})&\cfrac{\Gamma\vdash t:A\otimes B\quad
X:A,Y:B,\Theta\vdash X\cdot Y\cdot s:C}{\Gamma,\Theta\vdash
ts:C}~{}(\otimes{\rm{E}})\\\ \cfrac{\Gamma\vdash\delta^{\alpha}_{\beta}\cdot
t:A}{\Gamma\vdash
t:\nabla^{\alpha}_{\beta}A}~{}(\nabla{\rm{I}})&\cfrac{\Gamma\vdash
t:\nabla^{\alpha}_{\beta}A}{\Gamma\vdash\delta^{\alpha}_{\beta}\cdot
t:A}~{}(\nabla{\rm{E}})\\\ \cfrac{\Gamma\vdash
t:A}{\Gamma\vdash\delta_{\alpha}^{\beta}\cdot
t:\Delta^{\alpha}_{\beta}A}~{}(\Delta{\rm{I}})&\cfrac{\Gamma\vdash
t:\Delta^{\alpha}_{\beta}A\quad X:A,\Theta\vdash\delta_{\alpha}^{\beta}\cdot
X\cdot s:B}{\Gamma,\Theta\vdash ts:B}~{}(\Delta{\rm{E}}).\end{array}$

(a) Rules

$\Gamma$$a$$b$$\Longrightarrow$$(\parr{\rm{I}})$$\Gamma$$\overline{a}$$b$

(b) Picture for the $(\parr{\rm{I}})$ rule

$a$$\Theta$$\overline{a}$$b$$\Gamma$$\Longrightarrow$$(\parr{\rm{E}})$$\Theta$$b$$\Gamma$

(c) Picture for the $(\parr{\rm{E}})$ rule

Figure 4: Natural deduction for ETTC

Again, it is implicit that types and typing judgements in Figure 4(a) are well
defined. In particular, in the $(\parr{\rm{I}})$ rule we need pairwise
disjoint sequences $I^{\prime},J^{\prime}$ of pairwise distinct fresh indices,
in the $(\parr{\rm{E}})$ rule the contexts $\Gamma,\Theta$ have no common
tensor variable symbols etc. The $(\nabla{\rm{I}})$ and $(\Delta{\rm{I}})$
rules are same as in the sequent calculus and use the same convention:
$\alpha\in Fsup(A)$, $\beta\in Fsub(A)$.

Let us say that a n.d. term is closed if it contains no tensor variables. A
closed term is pure if it contains no terminal symbols. A closed term is
lexical if, on the contrary, it cannot be written as a normal term expression
of the form $\delta^{i}_{j}\cdot t^{\prime}$ (in a geometric language, all
edges of the corresponding graph have nonempty labels). A typing judgement
$t:A$ is lexicalized if the term $t$ is lexical.

It is easily seen that any sequent derivable in natural deduction of ETTC can
be written in the form

$X_{(1)}:(a_{(1)})^{I_{1}}_{J_{1}},\ldots,X_{(n)}:(a_{(n)})^{I_{n}}_{J_{n}}\vdash
X_{(1)}\cdots X_{(n)}\cdot t:B,$ (3)

where the term $t$ is pure. (In the case of the $({\rm{Id}})$ axiom we put
$t=1$.) The following is completely standard.

######  Lemma 5.1 (“Deduction theorem”)

Let $\Xi$ be a finite set of lexicalized typing judgements,
$\Xi=\\{\tau_{(1)}:(a_{(1)})^{I_{1}}_{J_{1}},\ldots,\tau_{(n)}:(a_{(n)})^{I_{n}}_{J_{n}}\\}$.

A natural deduction sequent of the form $\vdash\sigma:B$ is derivable from
$\Xi$ using each element of $\Xi$ exactly once iff there is a natural
deduction sequent of the form (3) derivable without nonlogical axioms such
that $t\cdot\tau_{(1)}\ldots\tau_{(n)}=\sigma$. $\Box$

We define the sequent calculus translation of (3) as the tensor typing
judgement

$\delta^{I_{n}^{\prime}\overline{J_{n}}}_{\overline{I_{n}}{J_{n}^{\prime}}}\cdots\delta^{I_{1}^{\prime}\overline{J_{1}}}_{\overline{I_{1}}{J_{1}^{\prime}}}\cdot
t\vdash
B,\overline{(a_{(n)})}^{J_{n}^{\prime}}_{I_{n}^{\prime}},\ldots,\overline{(a_{(1)})}^{J_{1}^{\prime}}_{I_{1}^{\prime}},$
(4)

where $I_{1}^{\prime},\ldots,I_{n}^{\prime}$,
$J_{1}^{\prime},\ldots,J_{n}^{\prime}$ are pairwise disjoint sequences of
pairwise distinct indices, all disjoint from ${FSup}(B)$, ${FSup}(B)$.
Translation (4) provides for equivalence of natural deduction and sequent
calculus formulation of ETTC, which is proven in a routine way familiar from
the case of, say, MILL1.

###### Lemma 5.2

Sequent (3) is derivable in the natural deduction formulation of ETTC iff its
translation (4) is derivable in the sequent calculus formulation. $\Box$

###  5.1 Geometric representation and example

Translating to the sequent calculus allows geometric representation of natural
deduction derivations as operations on bipartite graphs with indices
corresponding to vertices. It is natural to depict indices occurring to the
left and to the right of the turnstile as vertices aligned on two parallel
lines (continuously deforming the graph of translation (4), where all vertices
are on one line). Also, it should be clear from formula (4) that different
occurrences of the same index in a natural deduction sequent correspond to
distinct indices in the translation and to distinct vertices in the picture.
In Figures 4(b), 4(c), 5(b) we align vertices vertically. With such a
convention, the geometric representation for the $(\parr)$ rules can be shown
schematically as in Figures 4(b), 4(c). The $(\parr{\rm{I}})$ rule does not
change the graph, but changes its pictorial representation by a continuous
deformation.

Figure 5(a) shows a derivation of a tensor sequent corresponding under the
translation in Figure 3(k) to a sequent derivable in LC. Figure 5(b) gives a
geometric representation of the derivation.

$y^{j}_{m}:\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}^{i}_{j})\vdash
y^{j}_{m}:\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}^{i}_{j})$
$(\nabla{\rm{E}})$
$\mathord{y^{j}_{m}:\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}^{i}_{j})}\
\vdash\
\mathord{}$$\delta^{k}_{i}y^{j}_{m}:b^{m}_{k}\parr\overline{a}^{i}_{j}$ $(=)$
$\mathord{y^{j}_{m}:(b/a)^{m}_{j}}\ \vdash\
\mathord{}$$\delta^{k}_{i}y^{j}_{m}:b^{m}_{k}\parr\overline{a}^{i}_{j}$
$x^{i}_{j}:a^{j}_{i}\vdash x^{i}_{j}:a^{j}_{i}$ $(\parr{\rm{E}})$
$\mathord{y^{j}_{m}:(b/a)^{m}_{j},x^{u}_{v}:a^{v}_{u}}\ \vdash\
\mathord{}$$\delta^{k}_{i}y^{j}_{m}x^{i}_{j}:b^{m}_{k}$ $(=)$
$\mathord{y^{j}_{m}:(b/a)^{m}_{j},x^{u}_{v}:a^{v}_{u}}\ \vdash\
\mathord{}$$y^{j}_{m}x^{k}_{j}:b^{m}_{k}$

(a) Derivation

$j$$j$$i$$i$$a^{j}_{i}$$a^{j}_{i}$$m$$m$$j$$j$$\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}_{i}^{j})$$\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}_{i}^{j})$$\Longrightarrow$$(\nabla{\rm{E}})$$j$$j$$i$$i$$a^{j}_{i}$$a^{j}_{i}$$m$$m$$k$$i$$j$$j$$\nabla^{k}_{i}(b^{m}_{k}\parr\overline{a}^{i}_{j})$$b^{m}_{k}$$\overline{a}^{i}_{j}$$=$$a$$a$$b/a$$b$$\overline{a}$$\Longrightarrow$$(\parr{\rm{E}})$$a$$b/a$$b$$=$$a$$b/a$$b$
(b) Geometric representation

Figure 5: Example for natural deduction

###  5.2 Grammars

$\cfrac{\Gamma,x^{I}_{J}:a^{J}_{I}\vdash x^{K}_{L}\cdot t:B}{\Gamma\vdash
t\cdot\delta^{\overline{K}J^{\prime}}_{I^{\prime}\overline{L}}:{a}^{{I^{\prime}}}_{{J^{\prime}}}\multimap
B}~{}(\multimap{\rm{I}})\quad\cfrac{\Gamma\vdash s:A\multimap
B\quad\Theta\vdash t:{A}}{\Gamma,\Theta\vdash st:B}~{}(\multimap{\rm{E}})$
$\cfrac{\Gamma\vdash t:(b/a)^{i}_{j}\quad\Theta\vdash
s:a^{j}_{k}}{\Gamma,\Theta\vdash
ts:b^{i}_{k}}(/{\rm{E}})\quad\cfrac{\Gamma\vdash s:a^{j}_{k}\quad\Theta\vdash
t:(a\backslash b)^{i}_{j}}{\Gamma,\Theta\vdash
st:b^{i}_{k}}(\backslash{\rm{E}})$

(a) Admissible rules

$[{\rm{Mary}}]^{i}_{j}:np,~{}[{\rm{John}}]^{i}_{j}:np,~{}[{\rm{loves}}]^{i}_{j}:(np\backslash
s)/np,$

$[{\rm{madly}}]^{i}_{j}:((np\backslash
s)\backslash(np\backslash)),~{}[{\rm{who}}]^{i}_{j}:(np\backslash
np)/\Delta^{u}_{t}(np^{t}_{u}\multimap s).$

(b) Axioms

$\vdash$ $[{\rm{loves}}]^{k}_{l}:(np\backslash s)/np$
$\mathord{x^{j}_{k}:np}\mbox{\ $\vdash$\ }\mathord{}$$x^{j}_{k}:np$
$(/{\rm{E}})$ $\mathord{x^{j}_{k}:np}\mbox{\ $\vdash$\
}\mathord{}$$[{\rm{loves}}]^{k}_{l}x^{j}_{k}:np\backslash s$ $\vdash$
$[{\rm{madly}}]^{i}_{j}:(np\backslash s)\backslash(np\backslash s)$
$(\backslash{\rm{E}})$ $\mathord{x^{j}_{k}:np}\mbox{\ $\vdash$\
}\mathord{}$$[{\rm{loves}}]^{k}_{l}x^{j}_{k}[{\rm{madly}}]^{i}_{j}:np\backslash
s$

$\vdash$ $[{\rm{John}}]^{l}_{m}:np$ $\mathord{x^{j}_{k}:np}\mbox{\ $\vdash$\
}\mathord{}$$[{\rm{loves}}]^{k}_{l}x^{j}_{k}[{\rm{madly}}]^{i}_{j}:np\backslash
s$ $(\backslash{\rm{E}})$ $\mathord{x^{j}_{k}:np}\mbox{\ $\vdash$\
}\mathord{}$$[{\rm{John}}\mbox{
}{\rm{loves}}]^{k}_{m}x^{j}_{k}[{\rm{madly}}]^{i}_{j}:s_{i}^{m}$
$(\multimap{\rm{I}})$ $\vdash$ $[{\rm{John}}\mbox{
}{\rm{loves}}]^{k}_{m}x^{j}_{k}[{\rm{madly}}]^{i}_{j}\delta^{j\alpha}_{\beta
k}:np^{\beta}_{\alpha}\multimap s_{i}^{m}$ $(=)$ $\vdash$ $[{\rm{John}}\mbox{
}{\rm{loves}}]^{\alpha}_{m}\cdot[{\rm{madly}}]^{i}_{\beta}:np^{\beta}_{\alpha}\multimap
s_{i}^{m}$ $(\Delta{\rm{I}})$ $\vdash$
$\delta_{\alpha}^{\beta}\cdot[{\rm{John}}\mbox{
}{\rm{loves}}]^{\alpha}_{m}\cdot[{\rm{madly}}]^{i}_{\beta}:\Delta^{\alpha}_{\beta}(np^{\beta}_{\alpha}\multimap
s_{i}^{m})$ $(=)$ $\vdash$ $[{\rm{John}}\mbox{ }{\rm{loves}}\mbox{
}{\rm{madly}}]^{i}_{m}:\Delta^{\alpha}_{\beta}(np^{\beta}_{\alpha}\multimap
s)$

$\vdash$ $[{\rm{who}}]_{i}^{j}:(np\backslash
np)/\Delta^{\beta}_{\alpha}(np^{\alpha}_{\beta}\multimap s)$ $\vdash$
$[{\rm{John}}~{}{\rm{loves}}~{}{\rm{madly}}]^{i}_{n}:\Delta^{\alpha}_{\beta}(np^{\beta}_{\alpha}\multimap
s)$ $(/{\rm{E}})$ $\vdash$ $[{\rm{who}}\mbox{ }{\rm{John}}\mbox{
}{\rm{loves}}\mbox{ }{\rm{madly}}]^{j}_{n}:np\backslash np$

$\vdash$ $[{\rm{Mary}}]^{i}_{j}:np$ $\vdash$ $[{\rm{who}}\mbox{
}{\rm{John}}\mbox{ }{\rm{loves}}\mbox{ }{\rm{madly}}]^{j}_{n}:np\backslash np$
$(\backslash{\rm{E}})$ $\vdash$ $[{\rm{Mary}}\mbox{ }{\rm{who}}\mbox{
}{\rm{John}}\mbox{ }{\rm{loves}}\mbox{ }{\rm{madly}}]^{i}_{n}:np$

(c) Derivation

Figure 6: Example with nonlogical axioms

We give a more elaborate, linguistically motivated example of a derivation
from nonlogical axioms in Figure 6. For better readability, we systematically
use notation of LC and MILL understood as in Figure 3(k) and, in concrete
derivations, we omit free indices in types of valency $(1,1)$ (they are
uniquely determined by free indices in terms). In Figure 6(a) we fix
admissible rules corresponding to rules of LC and MILL that we will use.
Figure 6(b) shows our axioms (the lexicon), which we assume closed under
$\alpha$-equivalence of typing judgements, and in Figure 6(c) we derive the
noun phrase “Mary who John loves madly”. It might be entertaining to reproduce
the derivation in the geometric language.

Now let us define a tensor lexical entry as an $\alpha$-equivalence class of
lexicalized typing judgements and a tensor grammar as a pair $(Lex,s)$, where
$Lex$ is a finite set of lexical entries and $s$ is an atomic type symbol of
valency $(1,1)$. For a tensor grammar $G$ we will right $\vdash_{G}\sigma:A$
to indicate that the sequent $\sigma:A$ is derivable in ETTC from elements of
$Lex$. We define two languages generated by $G$. The regular language $L(G)$
and the regularized language $L_{reg}(G)$ of $G$ are, respectively the sets

$L(G)=\\{w|~{}\vdash_{G}[w]^{i}_{j}:s\\},\quad
L_{reg}(G)=\\{w|~{}\vdash_{G}[w]^{i}_{j}\cdot(\delta)^{n}:s\\}.$

(Note that $n$ in the definition of $L_{reg}$ is not an index, but indicates
the $n$-th power.)

Any balanced MILL1 grammar $G$ translates to a tensor grammar $\widetilde{G}$
by writing for every lexical entry $(w,A)$ of $G$ the tensor lexical entry
$[w]_{\rho(r)}^{\pi(l)}:a^{\rho(r)}_{\pi(l)}$, where $a$ is the type symbol of
$||A||^{\rho}_{\pi}$ (the choice of particular bijections $\rho$, $\pi$ is not
important because of closure under $\alpha$-equivalence of typing judgements).

###### Lemma 5.3

In the above setting we have $L(G)=L_{reg}(\widetilde{G})$.

Proof Let $w\in L_{reg}(\widetilde{G})$. Then we have $\vdash_{G}\tau:s$,
where $\tau=[w]^{i}_{j}\cdot(\delta)^{n}$.

Obviously $w$ is the concatenation $w=w_{1}\ldots w_{n}$ of all words
occurring in lexical entries $[w_{\mu}]^{i}_{j}:(a_{(\mu)})_{i}^{j}$,
$\mu=1,\ldots,n$, used to derive $\vdash\tau:S$. By Lemma 5.1 (“Deduction
theorem”) it must be that the we have the derivable n.d. sequent

$(x_{(1)})^{i_{1}}_{j_{1}}:(a_{(1)})_{i_{1}}^{j_{1}},\ldots,(x_{(n)})^{i_{n}}_{j_{n}}:(a_{(n)})_{i_{n}}^{j_{n}}\vdash\delta_{i_{1}}^{j_{2}}\cdots\delta_{i_{n-1}}^{j_{n}}\cdot(\delta)^{n}\cdot(x_{(1)})^{i_{1}}_{j_{1}}\cdots(x_{(n)})^{i_{n}}_{j_{n}}:s_{i_{n}}^{j_{1}},$

which corresponds, by Lemma 5.2, to the derivable typing judgement

$\delta_{i_{0}}^{j_{1}}\cdots\delta_{i_{n}}^{j_{n+1}}\cdot(\delta)^{n}\vdash
s^{i_{0}}_{j_{n+1}},\overline{(a_{(n)})}_{j_{n}}^{i_{n}},\ldots,\overline{(a_{(1)}})_{j_{1}}^{i_{1}}.$
(5)

If we translate MLL1 to ETTC using the prescription $\rho(\mu)=i_{\mu}$,
$\pi(\mu)=i_{\mu+1}$, where $\mu=0,\ldots,n$, then, by Lemma 4.1, we have that
(5) comes from a derivation of the sequent $\vdash
S[0;n],\overline{A_{n}}[n;n-1],\ldots,\overline{A_{1}}[1;0]$. The latter is
identified as the image of an MILL1 sequent expressing, by definition, that
$w\in L(G)$.

The opposite inclusion is similar, just easier. $\Box$

Geometric intuition might suggest that it is the regular, rather than,
regularized, language of a tensor grammar that should be accepted as natural.
In any case, it can be shown directly that in the case of tensor grammars
obtained from Lambek grammars or $\lambda$-grammars there are no additional
words generated “by regularization”: i.e. $L(G)=L_{reg}(G)$.

## References

  * [1] P. de Groote, “Towards Abstract Categorial Grammars”, in , Proceedings of the 39th Annual Meeting on Association for Computational Linguistics, ACL ’01, pp.148-155, 2001.
  * [2] Jean-Yves Girard, “Linear logic”, Theoretical Computer Science, 50:1-102, 1987.
  * [3] Jean-Yves Girard, “Linear logic: its syntax and semantics”, in J.-Y.Girard, Y.Lafont and L.Regnier, eds. Advances in Linear Logic, 1-42, Cambridge University Press, 1995, Proc. of the Workshop on Linear Logic, Ithaca, New York, June, 1993.
  * [4] Y. Kubota, R. Levine, “Gapping as like-category coordination”, in D. Béchet & A. Dikovsky, eds, ‘Logical Aspects of Computational Linguistics’, Vol. 7351 of Lecture Notes in Computer Science, Springer, Nantes, pp. 135-150, 2012.
  * [5] J. Lambek, ”The mathematics of sentence structure”, Amer. Math. Monthly, 65: 154-170, 1958.
  * [6] R. Moot, “Extended Lambek calculi and firsr-order linear logic”. In C. Casadio, B. Coecke, M. Moortgat, and P. Scott, eds., Categories and Types in Logic, Language, and Physics: Essays dedicated to Jim Lambek on the Occasion of this 90th Birthday, No. 8222 in Lecture Notes in Artifficial Intelligence, 2970330, Springer, 2014.
  * [7] R. Moot, “Hybrid type-logical grammars, 1rst-order linear logic and the descriptive inadequacy of lambda grammars”, https://hal.archives-ouvertes.fr/ hal-00996724, 2014.
  * [8] R. Moot and M. Piazza, “Linguistic applications of first order multiplicative linear logic”. Journal of Logic, Language and Information, 10(2):211-232, 2001.
  * [9] G. Morrill, O. Valentín, M. Fadda, “The displacement calculus”, Journal of Logic, Language and Information 20(1), 1-48, 2011.
  * [10] R. Muskens, “Separating syntax and combinatorics in categorial grammar”, Research on Language and Computation 5(3), 267-285, 2007.
  * [11] V. Mihaliček, C. Pollard, “Distinguishing phenogrammar from tectogrammar simplifies the analysis of interrogatives.” In Proceedings of the 15th and 16th International Conference on Formal Grammar (FG’10/FG’11), 130-145. Springer 2012.
  * [12] S. Slavnov, “Cobordisms and commutative categorial grammars”, Journal of Cognitive Science, 22, 68-91, 2021.
  * [13] S. Slavnov, “On embedding Lambek calculus into commutative categorial grammars”, Journal of Logic and Computation, 2021.