<figure><img src="image_1.png" /></figure>

HAL
open science

Proof-theoretic aspects of NL$\lambda$

Richard Moot

► To cite this version:

Richard Moot. Proof-theoretic aspects of NL$\lambda$. 2020. lirmm-02973980

HAL Id: lirmm-02973980

https://hal-lirmm.ccsd.cnrs.fr/lirmm-02973980

Preprint submitted on 21 Oct 2020

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Proof-theoretic aspects of NL_λ

Richard Moot

October 21, 2020

# 1 Introduction

In this paper, we present a proof-theoretic analysis of the logic NL_λ (Barker & Shan 2014, Barker 2019). We notably introduce a novel calculus of proof nets and prove it is sound and complete with respect to the sequent calculus for the logic. We study decidability and complexity of the logic using this new calculus, proving a new upper bound for complexity of the logic (showing it is in NP) and a new lower bound for the class of formal language generated by the formalism (mildly context-sensitive languages extended with a permutation closure operation). Finally, thanks to this new calculus, we present a novel comparison between NL_λ and the hybrid type-logical grammars of Kubota & Levine (2020). We show there is an unexpected convergence of the natural language analyses proposed in the two formalism. In addition to studying the proof-theoretic properties of NL_λ, we greatly extends its linguistic coverage.

# 2 Sequent calculus for NL_λ

The logic NL_λ, introduced by Chris Barker and Chung-Chieh Shan (Barker & Shan 2014, Barker 2019), is in many ways a standard multimodal logic in the tradition of type-logical grammars (Moortgat 1997). It uses two families of connectives:

1. the connectives { \, , • , / } of the non-associative Lambek calculus NL and the corresponding structural connective ‘o’, used for the standard composition operations, and

2. the continuation mode connectives { ⋀ , ⊙ , ⋱ } and corresponding structural connective ‘⊙’, used for scope taking and other discontinuous phenomena.

What makes the logic unusual is its main structural rule, stipulated as shown in Equation 1.

$$ \Gamma[\Delta] \Leftrightarrow \Delta \odot \lambda x.\Gamma[x] \qquad (1) $$

In the equation ‘⊙’ is the structural connective for the scope taking mode. When using Equation 1 from left to right, x must be a fresh variable, not
Identity group

$$ \overline{A \vdash A} Ax \qquad \frac{\Delta \vdash A \quad \Gamma[A] \vdash C}{\Gamma[\Delta] \vdash C} \text{ Cut} $$

Logical rules for the unit

$$ \frac{\Gamma[1] \vdash D}{\Gamma[t] \vdash D} tL \qquad \overline{1 \vdash t} tR $$

Logical rules for NL

$$ \frac{\Delta \vdash B \quad \Gamma[C] \vdash D}{\Gamma[(C / B \circ \Delta)] \vdash D} /L \qquad \frac{(\Gamma \circ B) \vdash C}{\Gamma \vdash C / B} /R $$

$$ \frac{\Delta \vdash C \quad \Gamma[C] \vdash D}{\Gamma[(\Delta \circ A \setminus C)] \vdash D} \setminus L \qquad \frac{(A \circ \Gamma) \vdash C}{\Gamma \vdash A \setminus C} \setminus R $$

$$ \frac{\Gamma[(A \circ B)] \vdash D}{\Gamma[A \bullet B] \vdash D} \bullet L \qquad \frac{\Gamma \vdash A \quad \Delta \vdash B}{(\Gamma \circ \Delta) \vdash A \bullet B} \bullet R $$

Logical rules for continuation connectives

$$ \frac{\Delta \vdash B \quad \Gamma[C] \vdash D}{\Gamma[(C \llbracket B \circ \Delta \rrbracket) \vdash D] \llbracket L \rrbracket} \qquad \frac{(\Gamma \circ B) \vdash C}{\Gamma \vdash C \llbracket B \rrbracket} \llbracket R \rrbracket $$

$$ \frac{\Delta \vdash C \quad \Gamma[C] \vdash D}{\Gamma[(\Delta \circ A \llbracket C \rrbracket) \vdash D] \llbracket R \rrbracket} \qquad \frac{(A \circ \Gamma) \vdash C}{\Gamma \vdash A \llbracket C \rrbracket} \llbracket R \rrbracket $$

$$ \frac{\Gamma[(A \circ B)] \vdash D}{\Gamma[A \circ B] \vdash D} \circ L \qquad \frac{\Gamma \vdash A \quad \Delta \vdash B}{(\Gamma \circ \Delta) \vdash A \circ B} \circ R $$

<caption>Table 1: The sequent calculus rules for NL<sub>λ</sub>: logical rules</caption>

occurring in the context Γ[] or in the structure Δ. When seeing ‘∘’ as a type of application (with the right daughter the function and the left daughter its argument) then reading the equation from right to left corresponds to a type of beta reduction, and the other direction to a form of beta expansion. We also adopt a principle similar to alpha equivalence in the lambda calculus, by treating proof as equivalent if they differ only in the name of abstracted variables.

Tables 1 and 2 show the sequent calculus rules for NL<sub>λ</sub>, with the logical rules in Table 1 and the structural rules in Table 2.

As a simple example, we assign “John” the formula np (that is, “John” functions as a noun phrase), and “saw” the formula (np \ s) / np (that is, “saw” combines first with a noun phrase np to its right, then with a noun phrase np to its left to produce a sentence s).

It is illustrative to first show how to derive “everyone saw John” in NL (that
Structural rules for unit

$$ \frac{\Gamma[(\Delta \circ 1)] \vdash D}{\Gamma[\Delta] \vdash D} \circ 1 \qquad \frac{\Gamma[\Delta] \vdash D}{\Gamma[(\Delta \circ 1)] \vdash D} \circ 1^{-1} $$

$$ \frac{\Gamma[(1 \circ \Delta)] \vdash D}{\Gamma[\Delta] \vdash D} 1 \circ \qquad \frac{\Gamma[\Delta] \vdash D}{\Gamma[(1 \circ \Delta)] \vdash D} 1 \circ^{-1} $$

Structural rules for continuations

$$ \frac{\Xi[(\Delta \circled{\lambda x} \Gamma[x]) \vdash D}{\Xi[\Gamma[\Delta]] \vdash D} \beta \qquad \frac{\Xi[\Gamma[\Delta]] \vdash D}{\Xi[(\Delta \circled{\lambda x} \Gamma[x]) \vdash D]} \beta^{-1} $$

<caption>Table 2: The sequent calculus rules for NL_λ: structural rules</caption>

is, the non-associative Lambek calculus, without any structural rules). When we assign “everyone” the NL formula $s / (np \setminus s)$ we obtain the following proof.

$$ \frac{\frac{\frac{\overline{np \vdash np} Ax}{np \vdash np} \quad \frac{\overline{np \vdash np} Ax}{np \circ (np \setminus s) \vdash s} \quad \overline{\setminus L}}{np \circ ((np \setminus s) / np \circ np) \vdash s} / L}{\frac{\overline{\setminus R} Ax}{s / (np \setminus s) \circ ((np \setminus s) / np \circ np) \vdash s}} / L $$

We see that the `/L` and `\R` rules combine to replace the quantifier formula $s / (np \setminus s)$ by the formula $np$, and we complete the proof by having the transitive verb select its two arguments.

The problem with the proof above is that it only works when the quantifier formula $s / (np \setminus s)$ is the leftmost formula in the sentence in which it takes its scope. We would like a quantifier to have the possibility to take scope from anywhere in the sentence in which it occurs. When we assign “everyone” the NL_λ formula $s \frown(np \setminus s)$, we can derive “John saw everyone” as type $s$ as follows.

$$ \frac{\frac{\frac{\vdots}{np \circ ((np \setminus s) / np \circ np) \vdash s} \beta^{-1}}{np \circ \lambda x. np \circ ((np \setminus s) / np \circ x) \vdash s \quad \overline{\setminus R} \quad \overline{s \vdash s} / \frown L} \qquad \frac{\overline{\setminus R} Ax}{s \frown(np \setminus s) \circ \lambda x. np \circ ((np \setminus s) / np \circ x) \vdash s} \beta $$

Comparing this proof to the previous one, we see that the $\beta$ rule allows us to move the quantifier to the leftmost position, with the continuation mode `\circled{0}` and with the $\lambda$ binder marking the original position of the quantifier. Then, the `\frown L` and `\frown R` rules combine to replace the quantifier by an $np$ formula (as the `/L` and `\R` rules did in the NL proof), and finally, the $\beta^{-1}$ rule moves this $np$ back
to the position of the original quantifier. The proof then continues as before, with the transitive verb selecting its two arguments.

NL_λ has a unit 't', which is a 0-ary logical connective corresponding to the identity element '1' for the Lambek mode. The structural rules for the unit show that '1' functions as a two-sided identity element for the Lambek structural connective 'o'. Lambek calculi are generally defined in a way which excludes empty antecedent derivations. The classic linguistic example against empty antecedent derivations in Lambek calculi is the standard analysis of phrases like "very interesting book", where "book" is assigned to formula n, "interesting" the formula n / n, and "very" the formula (n / n) / (n / n). The problem with allowing empty antecedent derivations is that 1 ⊢ n / n is derivable, and therefore we not only predict that "very interesting book" is grammatically a noun, but also "very book", by the following derivation.

$$ \frac{\frac{\frac{Ax}{\frac{1 \circ n \vdash n}{1 \vdash n / n}} 1 \circ^{-1}}{I} \frac{Ax}{\frac{n \vdash n}{n / n \circ n \vdash n}} \frac{Ax}{E}}{\frac{((n / n) / (n / n)) \circ 1) \circ n \vdash n}{((n / n) / (n / n)) \circ n \vdash n}} \circ 1 $$

Barker & Shan (2014, Section 16.6) and Barker (2019) allow empty antecedent derivations in their logic. However, it is possible to exclude empty antecedent derivations by simply removing the $\circ 1^{-1}$ and $1 \circ^{-1}$ structural rules from Table 2. This blocks the crucial subproof of $1 \vdash n / n$ in the proof above. In addition to being linguistically desirable, I will argue in Section 4 that removing these two structural rules has formal and computational advantages. However, the results for the proof net calculus in the next section and the decidability result of Section 4 hold irrespective of the presence or absence of empty antecedent derivations.

NL_λ requires its end-sequents to contain only the NL structural connective 'o'; the continuation mode '⊙', variables, and abstracted antecedent structures can only appear as intermediate structures.

## 3 Proof nets

Proof nets can be seen either as a parallelised version of the sequent calculus, which abstracts away from inessential rule permutations, or as a multi-conclusion version of natural deduction. The main advantage of proof nets is that different proof nets corresponds to proofs which differ for interesting reasons. In the linguistic context, this means that different proof nets corresponds to different lambda terms, that is, different readings of the sentence<fnref n="1" />.

<footnote n="1">¹There is a caveat here: while different proof nets will produce different derivational semantics, after lexical substitution, some of these readings can become equivalent.</footnote>
Although it is not hard to give an inductive definition of proof nets, we prefer to give the standard presentation using proof structures and a correctness condition. This way of presenting proof nets can easily be turned into an algorithm for proof search.

1. Unfold the formulas, essentially writing down the tree structure of the formula, until we reach the atomic formulas.

2. Connect atomic occurrences of hypotheses to conclusions, producing a proof structure.

3. Check correctness of the proof structure using a correctness condition. We will use a correctness condition in the form of graph rewriting.

## 3.1 Proof structures

The basic building block of proof structures (and the abstract proof structures introduced below) is the link. In a proof structure, a link connects a complex formula to its immediate subformulas.

**Definition 1** A link is tuple consisting of a type (tensor or par), a family (indicating the family of connectives is belongs to), a list of premisses, a list of conclusions, and possibly a main node (either one of the conclusions or one of the premisses).

A link is essentially a labelled hyperedge connecting a number of vertices in a hypergraph. The premisses of a link are drawn left-to-right above the central node, whereas the conclusions are drawn left-to-right below the central node. A par link displays the central node as a filled circle, whereas a tensor uses an open circle. The non-associative Lambek calculus family of connectives ($\lambda$, $\bullet$, $/$) uses a single circle for its links, whereas the continuation family ($\coloneqq$, $\circ$, $\nolimits$) uses links with double circles. For the binary connectives, this is a normal multimodal setup with two modes, where the modes are visually distinguished by single/double circles in the links rather than mode labels in the centre. The unit $t$ is treated as a 0-ary connective instead of an atomic formula with special properties (this is rather standard in many logics, and in our case it simplifies the proof net calculus, see Appendix A for discussion). Table 3 shows the links for $NL_\lambda$ proof structures.

Each connective has two links: one for where it occurs as a hypothesis (its left link) and one for where it occurs as a conclusion (its right link). The left link and the right link for a connective are up-down symmetric and exactly one of them is a par link (with a filled center) and the other is a tensor link (with an empty center).

From Table 3 it is clear that the binary par links have one premiss and two conclusions, whereas the binary tensor links have two premisses and one conclusion (we will see a tensor link with one premiss and two conclusions later). Par links have an arrow pointing to the main formula of the link. Although the
<figure><img src="image_3.png" /><figcaption>Table 3: Links for NL<sub>Λ</sub> proof structures</figcaption></figure>

main formula of a tensor link can be determined from the formula labels, tensor
links do not have a main node.

The basic idea is that tensor links *build* structure, whereas par links *remove* it. This is clear when we compare the links to the logical rules with which they share their label. For example, the `/L` rule of the sequent calculus, read from top to bottom, creates as new structure with the connective ‘o’ whereas the `/R` rule removes a structural connective ‘o’. The same holds for the other connectives, with the tensor rule adding an occurrence of the structural connective of the corresponding family (‘o’ or ‘⊙’) and the par rule removing one.

**Definition 2** A proof structure is a tuple `(F, L)`, where F is a set of formula occurrences and L is a set of the links shown in Table 3 where each local neighbourhood respects the formulas shown in the table and such that:

* each formula is at most once the premiss of a link,

* each formula is at most once the conclusion of a link.
<figure><img src="image_4.png" /><figcaption>Figure 1: Formula unfolding for “John saw everyone”.</figcaption></figure>

The formulas which are not a conclusion of any link in a proof structure are its hypotheses. The formulas which are not a premiss of any link in a proof structure are its conclusions. Formulas which are both a premiss and a conclusion of a link are internal nodes of the proof structure.

We say a proof structure with hypotheses Γ and conclusions Δ is a proof structure of Γ ⊢ Δ, overloading the ⊢ symbol.

As an example, Figure 1 shows the formula unfolding of “John saw everyone”, with “John” assigned np, “saw” (np \ s) / np, and “everyone” s // (np ⧸ s) with goal formula s. Given that this sentence is grammatical, we want to construct a proof net of np, (np \ s) / np, s // (np ⧸ s) ⊢ s, for some structured antecedent Γ which has the formulas in the indicated left-to-right order. However, Figure 1 shows a proof structure with the following hypotheses and conclusions.

$$np, np, (np \setminus s) / np, np, s // (np \setminus s), s \vdash np, s, s, np, s$$

The problem with the proof structure of Figure 1 is that it has too many atomic formulas, both as hypotheses and as conclusions. For example, the leftmost isolated np, corresponding to the formula unfolding of “John”, is — as it should be — a hypothesis of the proof structure. However, it is also a conclusion of the proof structure and our goal is to construct a proof structure with unique conclusion s (the rightmost isolated s node). Identifying the np corresponding to “John” with the leftmost np of the subgraph corresponding to “saw” will “cancel out” one premiss against a conclusion atomic formula (the rightmost np of “saw” would also be a possibility, but would produce sentences containing “saw John” rather than “John saw”). Figure 2 shows one possibility of connecting the atomic formulas to produce a proof structure of the sequent we are trying to prove.

$$np, (np \setminus s) / np, s // (np \setminus s) \vdash s$$

There are four possible proof structures (we have two choices for the np atoms and two for the s atoms). It will turn out that two of these possibilities are proof nets, one of them — the one following the connections shown in Figure 2 — corresponding to a proof of “John saw everyone” and the other to a proof of “Everyone saw John”.
<figure><img src="image_5.png" /><figcaption>Figure 2: Formula unfolding for “John saw everyone” with identifications of atomic formulas.</figcaption></figure>

Figure 3 shows (on the left hand side) the proof structure after node identifications. The *np* conclusion of the ⋀I link is drawn with an arc to arrive at the object *np* of the transitive verb. Essentially, this is a visual representation of the coindexation used for the introduction rules for the implications in natural deduction. However, we still need a mechanism to ensure the ⋀R rule (corresponding to the par link) has been correctly applied. The premiss of this particular instance of the ⋀R rule requires a proof of *np* ⊙ Γ ⊢ *s* (for some Γ; this is just the ⋀R rule of Table 1 for *A* = *np* and *C* = *s*, and where the *np* in this structure is the one which is the leftmost conclusion of the par link), and we are not in the required structure.

Checking correctness will therefore require us to add two types of operations
to our structures:

1. operations which correspond to the removal of a structural connective (tensor link) by a par link, exactly like the par rules of the sequent calculus,

2. operations which correspond to changing the structure of a connected group of tensor links, exactly like the structural rules of the sequent calculus change the antecedent.

**3.2 Abstract proof structures**

Given a proof structure, we obtain an abstract proof structure by erasing the
formulas for all internal nodes of the proof structure: only the hypotheses and
the conclusions of an abstract proof structure are assigned a formula. Given a
proof structure Π, we denote the underlying abstract proof structure by *A*(Π).

**Definition 3** An abstract proof structure *A* is a tuple <*V*, *L*, *h*, *c*> where *V* is a set of vertices, *L* is a set of the links shown in Table 4 connecting the vertices
<figure><img src="image_6.png" /><figcaption>Figure 3: Proof structure (left) and abstract proof structure (right) for “John saw everyone”.</figcaption></figure>

of V, *h* is a function from the hypothesis vertices of A to formulas, and *c* is a function from the conclusion vertices of A to formulas (a hypothesis vertex is a vertex which is not the conclusion of any link in L, and a conclusion vertex is a vertex which is not the premiss of any link in L).

The links for abstract proof structures are shown in Table 4. The top row shows the links for the 0-ary connective $t$, the second row shows the binary tensor links, the third row shows the par links for the Lambek connectives, and the bottom row shows the par links for the continuation connectives.

The $\lambda$ tensor link is the only non-standard link. Even though it has the same shape as the link for the Grishin connectives of Moortgat & Moot (2013), it is used in a rather different way. The $\lambda$ tensor link does not correspond to a logical connective in $NL_{\lambda}$. Rather, it corresponds to the $\lambda$ constructor in $NL_{\lambda}$ antecedent terms. As in multimodal proof nets, where tensor trees correspond to sequents, here tensor graphs correspond to sequents.

Figure 3 shows how the proof structure on the left hand side is transformed into an abstract proof structure on the right hand side. The procedure consists simply of removing all formulas on the internal nodes. Vertices which are hypotheses of the abstract proof structure have the corresponding formula written above the vertex, whereas vertices which are conclusions have the corresponding formula written below them.

**Definition 4** We say a proof structure, an abstract proof structure or one of their substructures, is a tensor tree iff it is a tree containing only tensor links.
<figure><img src="image_7.png" /><figcaption>Table 4: Links for $NL_\lambda$ abstract proof structures</figcaption></figure>

We say a substructure of a proof structure or of an abstract proof structure is a component *iff* it is a maximal, connected substructure containing only tensor links.

An abstract proof structure or one of its substructures is, is a tensor graph *iff* it is a connected graph of tensor links such that:

1. removing the connection between all $\lambda$ links and their leftmost conclusions produces a tree (we call this the underlying tree of a tensor graph),

2. for each $\lambda$ link in the graph, the leftmost conclusion of this $\lambda$ link is an ancestor of the premiss of the link in this graph.

We call a connected graph of tensor links cyclic (resp. disconnected), if removing the between the lambda link and their leftmost conclusion according to item 1 produces a cyclic (resp. disconnected) structure.

Tensor graphs are graphical representations of the antecedent structure in $NL_\lambda$. The conditions on tensor graphs ensure that each $\lambda$ binder in the abstract proof structure binds exactly one hypothesis in its scope.

## 3.3 Contractions and structural coversions

To check correctness of a proof structure, we have two types of graph rewrite operations on its underlying abstract proof structure. The first are the contractions, shown in Table 5. Each contraction has the condition that the vertex
<figure><img src="image_8.png" /><figcaption>Table 5: Contractions for NL<sub>λ</sub>.</figcaption></figure>

labeled *h* (which is possibly a hypothesis of the abstract proof structure) and
the vertex labeled *c* (which is possibly a conclusion of the abstract proof struc-
ture) are distinct. The contractions replace the displayed pair of links by a
single vertex (deleting the two links and any internal nodes, while identifying
the nodes *h* and *c*).

The contractions are essentially a way of verifying the antecedent is in the
right configuration for the application of the corresponding sequent rule. In this
way the par link for ⋀R and the contraction for ⋀R work together to emulate
the ⋀R rule of the sequent calculus.

Graphically, we can see that the configurations which allow us to perform
a contraction all connect a par link to a tensor link (respecting the left/right
distinction) by the tentacles of the par link which do not have the arrow. Each
contraction removes the two links (and the two internal nodes) while performing
a vertex contraction on the two external vertices.

The contraction for [tL] looks a bit strange, but it is essentially the [•L]
contraction with the two branches removed (*t* is a 0-ary connective, whereas •
is a binary one). It therefore creates a new connection while identifying *h* and
*c*.

Figure 4 shows a ‘sugared’ version of the conversion for the $\beta$ and $\beta^{-1}$ rules for abstract proof structures. The left hand side is a graphical representation of $x \odot \lambda v.\Gamma[v]$ and the right hand side of $\Gamma[x]$, where $x$ can represent any complex structure $\Delta$. Like the corresponding structural rules, $\beta^{-1}$ moves the constituent $x$ out and marks its position using a lambda binder, whereas $\beta$ moves $x$ back to
<figure><img src="image_9.png" /><figcaption>Figure 4: Structural rule for $NL_\lambda$, ‘sugared’ version.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Table 6: Structural rules for $NL_\lambda$.</figcaption></figure>

the placed marked by the abstracted variable. The two rewrites have the side condition that the path through $\Gamma$ (from $x$ to $z$ on the left hand side and from the anonymous nodes at the top and bottom of $\Gamma$ at the right hand side) does not pass through any par links. Table 6 shows the full set of structural rules. The side conditions on the $\beta$ and $\beta^{-1}$ rules are that the node labeled $c_1$ is a
descendant of the node labeled $h_2$ through a path not passing through any par
links — the side condition can be seen as a way of avoiding ‘accidental capture’
of variables by the lambda binder, and it guarantees that all rewrites occur in
a single component (essential for correctness).

**Definition 5** *The size of an NL$_{λ}$ proof structure or abstract proof structure with *p* par links and *t* tensor links is equal to 2*p* + *t*.*

**Definition 6** *We say a graph rewrite is expanding whenever the size of right hand side of the rule is larger than the size of the left hand side, and reducing whenever the size of the right hand side of the rule is smaller than the size of the left hand side.*

The contactions of Table 5 are all reducing (they all reduce the size of the
structure by 3, removing one par link and one tensor link). The structural
rewrites of Table 6 are reducing in their left to right application but expanding
in the right to left application. The reducing structural rules are also the rewrites
which shorten some of the paths in the abstract proof structure.

**3.4 Proof nets**

**Definition 7** *A proof structure is a proof net iff its abstract proof structure contracts to a tensor graph using the contractions of Table 5 and the structural conversions of Table 6.*

As an illustration, Figure 5 shows how we can take the abstract proof struc-
ture of Figure 3 and apply the $\beta^{-1}$ rule to produce the abstract proof structure
shown in Figure 5 on the right. This produces a redex for the $\llcorner$ contraction.
Figure 6 shows the result of applying the contraction and how applying the $\beta$
rule then produces the required tree structure. We have therefore shown that
our example proof structure is a proof net, as it should be.

The end-sequents in NL_λ are required to contain only the Lambek struc-
tural connective ‘o’. However, our intermediate structures can contain the ‘⊙’
connective and the λ binder, and we therefore need to consider them for our
inductive proofs.

**Theorem 8** $\Gamma \vdash C$ is derivable using the sequent calculus rules of Tables 1 and 2 if and only if there is a proof net contracting to the tensor graph $\Gamma \vdash C$.

**Proof** This is a trivial adaptation of the proofs of Moot & Puite (2002) and Moot & Stevens-Guille (2019).

⇒ From sequent proofs to proof nets, we proceed by induction on the
depth of the proof. Only the axiom rule and the tR rule have depth 1.

The axiom $A \vdash A$ corresponds to the single vertex proof structure $A$, shown below on the left, which produces the abstract proof structure of $A \vdash A$, shown below on the right.
<figure><img src="image_11.png" /><figcaption>Figure 5: Abstract proof structure of Figure 3 before and after the $\beta^{-1}$ structural conversion.</figcaption></figure>

$$A \xrightarrow{A} \overset{A}{\cdot} \overset{A}{\cdot}$$

For the $tR$ rule, we unfold the conclusion formula $t$ to obtain the proof structure shown below on the left, and it corresponds immediately to the abstract proof structure of $1 \vdash t$, as required.

$$\begin{tikzpicture}[baseline=(tunktikz.center)]
\node (t) at (0,0) {$\bullet$};
\node (t1) at (1,0) {$\bullet$};
\draw[->] (t) -- (t1);
\node at (0.5,-0.3) {t};
\node at (0.5,0.3) {t1};
\node at (1.5,-0.3) {};
\node at (1.5,0.3) {};
\node at (0.5,-0.5) {};
\node at (0.5,0.5) {};
\end{tikzpicture} \quad \begin{tikzpicture}[baseline=(tunktikz.center)]
\node (t) at (0,0) {$\bullet$};
\node (t1) at (1,0) {$\bullet$};
\draw[->] (t) -- (t1);
\node at (0.5,-0.3) {$\rightarrow A$};
\node at (0.5,0.3) {};
\node at (1.5,-0.3) {};
\node at (1.5,0.3) {};
\node at (0.5,-0.5) {};
\node at (0.5,0.5) {};
\end{tikzpicture}$$

For the inductive cases, we use the induction hypothesis to obtain proof nets (and rewrite sequences) for the immediate subproofs, add the appropriate link (for the logical rules of the connectives), extend the rewrite sequence with the appropriate conversion (a contraction whenever we add a par link, and a structural conversion for the structural rules).

We show only the $tL$, $\not\not\not R$ and $\beta^{-1}$ cases, the other cases are similar.

**$tL$** For the $tL$ rule, induction hypothesis gives us a proof net of $\Gamma[1] \vdash D$. That means we have a way to construct a proof structure $\Pi$ with the formulas
<figure><img src="image_12.png" /><figcaption>Figure 6: Abstract proof structure of Figure 5 after the $\mathcal{V}$ contraction.</figcaption></figure>

of $\Gamma$ as its hypotheses, $D$ as its conclusion, and a rewrite sequence $\rho$ converting the abstract proof structure corresponding to $\Pi$ into $\Gamma[1] \vdash D$. Graphically, we are therefore in the following situation (where we tacitly convert proof structure $\Pi$ to its corresponding abstract proof structure $\mathcal{A}(\Pi)$ before applying the conversions in $\rho$).

<figure><img src="image_13.png" /></figure>

We need to produce a proof net of $\Gamma[t] \vdash D$. The proof net therefore needs to have an additional $t$ hypothesis, and in the final structure this hypothesis needs to be at the position where 1 was in the proof net obtained by induction hypothesis. We add a $t$ as the hypothesis of a $tL$ link. We then apply the rewrites in $\rho$ as before and end with the $tL$ contraction to produce a proof net of $\Gamma[t] \vdash D$ as follows.
<figure><img src="image_14.png" /></figure>

R The case for $\mathcal{R}$ gives us a proof net of $\Gamma \odot B \vdash C$ by induction hypothesis. The means we have the proof structure $\Pi$ shown below on the left and a conversion sequence $\rho$ producing the antecedent structure $\Gamma \odot B$.

<figure><img src="image_15.png" /></figure>

To produce a proof net of $\Gamma \vdash C \mathcal{R} B$, we attach the par link for $\mathcal{R}$ to the proof net given by induction hypothesis, and extend the conversion sequence $\rho$ with the $\mathcal{R}$ contraction. This produces a proof net of $\Gamma \vdash C \mathcal{R} B$ as shown below.

<figure><img src="image_16.png" /></figure>

$\beta^{-1}$ When the last rule is the $\beta^{-1}$ rule, induction hypothesis gives us a proof net of $\Xi[\Gamma[\Delta]] \vdash D$; in other words, a proof structure $\Pi$ and a rewrite sequence $\rho$ converting the corresponding abstract proof structure $\mathcal{A}(\Pi)$ into $\Xi[\Gamma[\Delta]] \vdash D$. We can extend this conversion sequence with the $\beta^{-1}$ conversion to produce a proof net of $\Xi[\Delta \odot \lambda x.\Gamma[x]] \vdash D$.
<figure><img src="image_17.png" /></figure>

The sequentialisation part of the proof, showing that for each proof net we can construct a corresponding sequent proof, is generally the difficult part of the proof. Given that we have a proof net, we know that we have a proof structure and a conversion sequence producing the abstract proof structure representing $\Gamma \vdash D$.

We proceed first by induction on the length *l* of the conversion sequence. If *l* = 0, there are no conversions, and as a consequence there can be no par links and no lambda links (par links require a contraction to produce a tensor graph, whereas lambda links can only be produced by a structural conversion), our tensor graph must therefore be a tensor tree.

We proceed by induction on the number of tensor links in the abstract proof structure. In the base case, *t* = 0 there are no tensor links and the proof structure and abstract proof structure both consists of a single node, which is an *A* hypothesis and an *A* conclusion, corresponding to the axiom *A* ⊢ *A*. For the inductive case, *t* > 0, take any tensor link in the tensor tree. We look at only one binary case (they are all similar) and at the 0-ary case.

In the case for the binary `[L]`, we have the following proof net, which is a tensor tree.

<figure><img src="image_18.png" /></figure>

Removing the tensor link produces three smaller trees, and the induction hy-
pothesis therefore gives us three proofs, $\delta_1$ of $\Gamma \vdash A$, $\delta_2$ of $\Delta \vdash A \Vdash C$, and $\delta_3$ of $\Xi[C] \vdash D$. We combine these three proofs as follows to produce a proof of $\Xi[\Gamma \odot \Delta] \vdash D$ as required.

$$ \frac{\frac{\vdots \quad \delta_2 \quad \Gamma \vdash A \quad \overline{C \vdash C} \quad Ax}{\Delta \vdash A \Vdash C \quad \Gamma \odot A \Vdash C \vdash C} \quad \text{Cut} \quad \overline{\Vdash L} \quad \vdots \quad \delta_3}{\Xi[\Gamma \odot \Delta] \vdash D} \quad \text{Cut} $$

In the case for $[tR]$, we have the following proof structure and abstract proof structure.

<figure><img src="image_19.png" /></figure>

We remove the $[tR]$ tensor link from the abstract proof structure and apply the induction hypothesis to obtain a proof $\delta$ of $\Gamma[t] \vdash D$ (removing the $[tR]$ link leaves a $t$ hypothesis). We can then produce a proof of $\Gamma[1] \vdash D$ as follows.

$$ \frac{\overline{1 \vdash t} \quad tR \quad \vdots \quad \delta}{\Gamma[t] \vdash D} \quad \text{Cut} $$

This concludes the proof of the base case, where there sequence of conversions on the abstract proof structure is empty. We now look at the inductive case, where there are $l > 0$ conversions. We look at the last conversion in the sequence.

The key case is when the last conversion is the contraction of a par link. We only look at the cases for $tL$ and $\Vdash R$. The structural rules correspond rather directly to the structural conversion of the same name, and we only show the $\beta^{-1}$ case.

**$tL$** When the last contraction is a $tL$ contraction, we are in the following situation.
<figure><img src="image_20.png" /></figure>

The general idea of the proof is that the par link corresponding to the last contraction forms a 'barrier' forcing all other conversions before it to be on one or the other side of it. This allows us to remove the par link and end up with two proof nets.

Suppose a conversion operates on both sides of the par link simultaneously, this means that, after the conversions in $\rho$, $\Gamma[1]$ and $\Delta$ must be the same component (since they share at least a vertex), and the $tL$ contraction connects two vertices which were already connected in this component. But then $\Gamma[\Delta]$ cannot be a tensor graph, since it contains a cycle.

We can therefore remove the par link, and divide the conversions in $\rho$ into two subsequences, $\rho_1$ transforming the substructure $\Pi_1$ into $\Delta \vdash t$ and $\rho_2$ transforming the substructure $\Pi_2$ into $\Gamma[1] \vdash D$ as follows.

<figure><img src="image_21.png" /></figure>

These two substructures are therefore proof nets, and since the total number of conversions in the two sequences sums to $l-1$ (we started with $l$ conversions and removed the final $tL$ contraction), we can apply the induction hypothesis to obtain proofs $\delta_1$ of $\Delta \vdash t$ and $\delta_2$ of $\Gamma[1] \vdash D$. We
can combine these to produce the required proof of $\Gamma[\Delta] \vdash D$ as follows.

$$ \frac{\vdots \delta_1 \quad \frac{\Gamma[1] \vdash D}{\Gamma[t] \vdash D} tL \\ \Delta \vdash t \quad \Gamma[\Delta] \vdash D}{\Gamma[\Delta] \vdash D} \text{Cut} $$

### $\parallel R$
When the last contraction is a $\parallel R$ contraction, we are in the following situation.

<figure><img src="image_22.png" /></figure>

As in the previous case, we remove the par link and divide the conversions in $\rho$ depending on the 'side' of the par link where they applied. This gives the following two proof nets, each with a shorter conversion sequence (since the final contraction has been removed).

<figure><img src="image_23.png" /></figure>

Induction hypothesis gives us a proof $\delta_1$ of $\Delta \odot B \vdash C$ and a proof $\delta_2$ of $\Gamma[C \parallel B] \vdash D$. We combine these into the required proof of $\Gamma[\Delta] \vdash D$ as
follows.

$$ \frac{\frac{\Delta \odot B \vdash C}{\Delta \vdash C \llbracket B \rrbracket} \circled{R} \frac{\delta_2}{\Gamma[C \llbracket B \rrbracket] \vdash D}}{\Gamma[\Delta] \vdash D} \text{ Cut} $$

The other contractions for the binary connectives are treated similarly.

$\beta^{-1}$ If the last conversion is a $\beta^{-1}$ conversion, we are schematically in the following case.

<figure><img src="image_24.png" /></figure>

Removing the final $\beta^{-1}$ conversion produces a shorter conversion sequence and we can therefore apply the induction hypothesis to obtain a proof $\delta$ of $\Xi[\Gamma[\Delta]] \vdash D$. We can extend this proof as follows to produce the required proof.

$$ \frac{\vdots \delta}{\Xi[\Gamma[\Delta]] \vdash D \qquad \Xi[(\Delta \odot \lambda x.\Gamma[x])] \vdash D} \beta^{-1} $$

The variables $x$ in the conclusion of the proof is chosen to not appear elsewhere in $\Gamma$ or $\Delta$. The other structural rules are similar.

□

## 3.5 Extending NL$_{\lambda}$

One advantage of the proof net calculus presented in this section is that it is easy to adapt when extending the logic. For example, we can add an associative mode to NL$_{\lambda}$ with the corresponding structural rules. This would give this
extended logic an easy treatment of phenomena like right-node raising which
are a known problem for non-associative logics.

In general, we can import the entire multimodal setup of (Moot & Puite
2002) — modes, unary connectives, structural rules — into NL_λ with the fol-
lowing proviso: all structural rules must be confluent with respect to the β
redex (see also Section 4.1). Well-behavedness with respect to beta reduction is
a standard restriction from the literature on adding rewrite rules or equations
to the lambda calculus (Barendregt 1981, Chapter 4).

The simplest way to enforce this is to ensure a $\beta$ redex cannot be part of a
critical pair with another structural rewrite, by prohibiting structural rules other
than $\beta^{-1}$ and $\beta$ (plus, eventually, an $\eta$ reduction as discussed in Section 4.1) to
modify ‘$\odot$’ and ‘$\lambda$’ links.

# 4 Decidability and Complexity

For decidability, we essentially follow the argument of Barker (2019), with the
minor modification that decidability for proof nets corresponds to forward chain-
ing proof search, as opposed to the backward chaining proof search of the se-
quent calculus used by Barker. The advantage of a forward chaining proof
search strategy is that we compute the antecedent structure as output, rather
than requiring it as part of the input.

Looking at the rewrite rules for abstract proof structures, the only rules
which increase the size of the structure are the right-to-left versions of the
structural conversions on Table 6, the expanding conversions $\beta^{-1}$, $1^{\circ-1}$ and
$\circ 1^{-1}$. This is a potential problem for decidability, since these rules can be used
to add links to the abstract proof structure (at least in principle) without limit.
However, for each of these conversions, we can restrict their application in such
a way that the size of the structure no longer increases. This is easiest for the
1 rules. We can assume, without loss of generality, that we always remove the
occurrences of 1 as much as possible (given that the end-sequent is required
to only contain the NL structural connective ‘$\circ$’, with ‘1’ its identity element,
removal of 1 is only impossible when the antecedent is itself identical to 1). Now
from inspection of the rewrite rules, the only rule which could require one of
the $1^{-1}$ rules are the following contractions.

1. $tL$ can require either the $1^{\circ-1}$ or the $\circ 1^{-1}$ rewrite,

2. $\R$ can require the $\circ 1^{-1}$ rewrite,

3. $/R$ can require the $1^{\circ-1}$ rewrite.

We can combine the rewrites of $1^{\circ-1}$ and $tL$ as shown in Figure 7. Doing this
rewrite in a single step, reduces the size of the structure (given that Definition 5
counts par links as 2 but tensor links as 1, the size of the structure is reduced
by 1). The combination of $\circ 1^{-1}$ with $tL$ is left-right symmetric with Figure 7.

We can combine the rewrites of $\circ 1^{-1}$ and $\R$ as shown in Figure 8. Adding
a new rule transforming the left hand side of the figure directly to the right
<figure><img src="image_25.png" /><figcaption>Figure 7: Combination of the $1 \circ^{-1}$ and $tL$ graph rewrites.</figcaption></figure>

<figure><img src="image_26.png" /><figcaption>Figure 8: Combination of the 1 and $\setminus$ graph rewrites.</figcaption></figure>

hand side ensures that the size of the structure decreases. A similar strategy can be used for the combination of the $1 \circ^{-1}$ rule with the $R$ rule (it is left-right symmetric with Figure 8).

For the $\beta^{-1}$ case, we again use essentially the same argument as **Barker** (2019) to show decidability. In a proof net and its reduction sequence, the only ways to introduce a $\odot$ tensor link are the $\otimes L$, $\text{\textbackslash} L$ and $\odot R$ links, and the $\beta^{-1}$ structural rule. The only ways to remove a $\odot$ tensor link are the $\otimes$, $\text{\textbackslash}$ and $\odot$ contractions and the $\beta$ structural rule.

We can remove cases where a $\odot$ link is introduced by a $\beta^{-1}$ structural rule and removed by a $\beta$ one, since in that case both structural rules can be removed.

This leaves us with the cases where the $\odot$ link is introduced by a $\beta^{-1}$ but removed by a contraction. However, looking at the shape of the contractions, this can only be a $\text{\textbackslash} R$ contraction, because the $\beta^{-1}$ rule introduces a $\odot$ link connected by its rightmost premiss to a $\lambda$ link, leaving only the conclusion and leftmost premiss free for connection to a par link and thereby excluding the $\otimes R$ and $\odot L$ contractions (which both require the rightmost premiss to be connected to their par link instead of to the $\lambda$ link; although the reducing structural conversions can shorten a path, a $\lambda$ link can only be removed together with its paired $\odot$ link).

Figure 9 shows what happens when the $\beta$ structural rule is combined with the $\text{\textbackslash} R$ contraction. When we combine the two contractions, the size of the structure no longer increases.

To conclude, we can provide a decidable calculus by removing the expanding rules (the right to left versions of the rules in Table 6, that is, the $\beta^{-1}$, $1 \circ^{-1}$
<figure><img src="image_27.png" /><figcaption>Figure 9: Combination of the $\beta^{-1}$ rule and the $\otimes_R$ contraction.</figcaption></figure>

<figure><img src="image_28.png" /><figcaption>Table 7: Derived rules for $NL_\lambda$.</figcaption></figure>

and $\circ 1^{-1}$ rewrite) and replacing them by the rewrite rules of Table 7. Each of the derived rules reduces the number of par links and is therefore bounded in its number of applications. The $\beta^{-1}\otimes_R$ rewrite rule has the side condition that there is a path from node $c_1$ to node $h$ which passes only through tensor links (this is the standard condition on the $\beta^{-1}$ rule).

Given that each of the rules reduces the size of the abstract proof structure (according to Definition 5, replacing a par link by a tensor links amounts to a
size reduction) showing decidability is easy. However, we can do a bit better than just showing decidability. We first define the size of words in the lexicon.

**Definition 9** The size of of word $w$ from the lexicon is the sum of the sizes (according to Definition 5) of all words assigned to it in the lexicon. The size of a set of goal formulas $G$ is the sum of the sizes of all formulas $g \in G$

**Lemma 10** $NL_\lambda$ is decidable in non-deterministic linear space.

**Proof** We only present a proof sketch, abstracting away from the actual coding of graphs as strings on the tape of a Turing machine.

Given a sentence and an $NL_\lambda$ grammar, specified by a lexicon and a set of goal formulas, the input space is the sum of the sizes for all words, plus the sum of the sizes for all goal formulas. Non-deterministically do lexical lookup (erasing all but one of the possible formulas for each word), non-deterministically enumerate all proof structures, then non-deterministically enumerate the rewrite sequences (each rewrite reducing the size). Finally, check whether the result is a tree.

We also note that the proof of Theorem 1 of Barker (2019) already implicitly establishes a linear space bound on proof search. □

## 4.1 Confluence

While replacing the expanding structural rules by the derived rules of Table 7 makes the rewrite system decidable, it is unfortunately not confluent. This is not a defect of the derived rules, but of $NL_\lambda$ itself: for example, there is a divergence between the $\beta^{-1}$ and $\overline{\beta}R$ conversions, and between multiple $tL$ redexes (one $tL$ link can reduces with different 0-ary tensor links, and this is aggravated by the fact that the expanding rewrites for 1 can introduce these tensor links anywhere in the structure).

Confluence is not a standard property for proof nets in the style of Moot & Puite (2002), at least not in the presence of structural rules. Generally, a proof structure represents a potential reading of a given sentence, and absence of confluence corresponds to the possibility that different structures and different word orders can correspond to the same meaning, something which the method of proof nets by graph rewriting is designed to accommodate. However, from the point of view of rewriting, confluence is extremely desirable and in this section we will look at some conditions on the rewrite rule which entail confluence for the rewriting component of $NL_\lambda$ proof nets.

**The unit** The $1 \circ t$ and $\circ 1t$ rewrites of Table 7 are not confluent: we can choose any vertex for the $h_1/c$ or $h_2/c$ node, with different vertices producing different structures not convertible to a common structure. A similar argument can be used when rewriting the same vertices using a $1 \circ t$ and a $\circ 1t$ rewrite, which produces structures with the left and right subtree swapped, and not reducible to a common structure (given a non-commutative logic).
The tL link introduces quite a bit of proof combinatorics: given that t is the formula equivalent of the empty string, a t formula can in principle be inserted anywhere in the antecedent (that is, to the left or to the right of any other node). It seems that — at least for the examples used in natural language grammars — we can restrict the tL contraction to its eta expansion case, where it only combines with a tR link present in the proof structure (and not introduced by a structural rule in the abstract proof structure). This reduces a lot of the combinatorics and keeps the meaning assignment by means of Curry-Howard terms simple (see Appendix B for discussion about the term assignment for the unit: it is not clear that the term constructor for tE is ever useful outside of occurrences which can be directly reduced). When we require that a tL link must be matched with a tR link from the lexicon (that is, both links correspond to the logical connective t; the tR link is not introduced by a structural rule), we can eliminate the 1 ◦ t and ◦ 1t conversions entirely.

At the same time, the derived contractions ◦ 1 − $^{1}$\ and 1 ◦ − 1 / correspond to empty antecedent derivations for the Lambek calculus connectives. Although logically unproblematic, these are generally disallowed for linguistic reasons, as discussed at the end of Section 2 — even though Barker & Shan (2014, Sec- tion 16.6) admit them. So a more drastic solution would be to restrict the application of the structural rules for the identity element to only those which reduce the structure, by removing the 1 ◦ − 1 and ◦ 1 − 1 structural rewrites (and the corresponding structural rules from the sequent calculus). This would make the derived rules of Table 7 mentioning 1 superfluous and only keep the β − $^{1}$\ rewrite.

Even though from an algebraic point of view it is preferable to have ‘1’ function as a true identity element for ‘o’, it makes sense to apply the struc- tural rules for the unit only in one direction, both from a term/graph rewrite perspective and from a linguistic perspective. In the term- and graph rewrite literature, it is fairly standard to give equivalences an orientation towards the simpler terms/graphs, and, linguistically, orienting the equations for the iden- tity element gives an easy way to solve the problems with empty antecedent derivations.

**The β − $^{1}$\ rule** The β − $^{1}$\ rewrite rule is not confluent either. Figure 10 shows the simplest example of this critical pair. It is a proof net of A \ B ⊢ A \ B, and following the topmost path and applying the \ R contraction produces a proof net, but applying the β − $^{1}$\ rewrite instead produces another structure to which no further rewrites apply (assuming only the derived rules and simplification structural rules apply).

From the perspective of the lambda calculus, we have produced an η redex. One solution would therefore be to add the equivalent of the η rule to NL$_{λ}$, which corresponds to Equation 2 below.

$$
\Gamma \Leftrightarrow \lambda x.(x \odot \Gamma) \qquad (2)
$$

The two proof nets in Figure 10 correspond to the following two sequent
<figure><img src="image_29.png" /><figcaption>Figure 10: Failure of confluence: a conflict between the $\beta^{-1}\otimes$ and the $\otimes R$ contraction.</figcaption></figure>

proofs, and under the $\eta$ rule, these two proofs are equivalent.

$$ \frac{\overline{A \vdash A} \quad \overline{Ax} \quad \overline{B \vdash B} \quad \overline{Ax}}{A \odot A \otimes B \vdash B} \otimes L \quad \overline{\beta^{-1}} \quad \overline{Ax} \otimes L \\ \equiv_{\eta} \overline{\frac{A \vdash A \quad Ax \quad B \vdash B}{A \odot A \otimes B \vdash B}} \otimes R $$

At the level of proof nets, adding the $\eta$ reduction rule means adding the conversion labeled $\eta$ in Figure 10.

If adding an $\eta$ equivalence rule to $NL_{\lambda}$ is undesirable — the logics of Barker & Shan (2014) and Barker (2019) do not have such a rule after all — then we can instead apply a greedy conversion strategy, as we discuss in the next paragraph.

**A confluent fragment** We now present a confluent fragment of the proof net calculus for $NL_{\lambda}$. It deviates from the calculus $NL_{\lambda}$ of Barker (2019) only in requiring each $tL$ to be matched with a $tR$ rule, which amounts to removing the $1 \circ t$ and $\circ 1t$ rewrites. Depending on whether or not we want to allow empty antecedent derivations, the $\circ 1^{-1} \setminus$ and $1 \circ^{-1} /$ rewrites can be either present or absent; this does not affect confluence.

**Definition 11** An extended axiom linking for a proof structure is:

1. a 1-1 matching between atomic hypothesis formulas and atomic conclusion formulas,

2. a 1-1 matching between $tL$ and $tR$ links.

In the absence of the $1 \circ t$ and $\circ 1t$ rewrites, we can treat the logical rules for $t$ as a sort of axiom links (see Appendix A for discussion). The notion of extended axiom link makes this explicit.
**Lemma 12** *Given a proof structure Π, an extended axiom linking e, the con- tractions of Table 5, the reducing structural rules of Table 6 and the derived ◦1⁻¹\, 1 ◦⁻¹ /, and β⁻¹\ rules of Table 7, reductions of the corresponding abstract proof structure are confluent modulo eager reductions.*

**Proof** We have essentially used brute force to remove all critical pairs.

• the critical pairs between a $tL$ link and two $tR$ links has been removed by item 2 of the definition of extended axiom links (Definition 11),

• the critical pairs between $\beta^{-1}\}$ and $\mathcal{R}$, between $\circ 1^{-1}$ and $/R$, and between $1\circ^{-1}$ and $\mathcal{R}$ have been removed by the rule ordering, removing the potential deadlocks.

Only the conflict between $\beta^{-1}\}$ and $\mathcal{R}$ requires a bit of reflection, since
the other critical pairs are confluent. Suppose we are in a situation where
the $\mathcal{R}$ contraction (and not the $\beta^{-1}\}$ conversion) must apply at some point.
Look at the path between the $\mathcal{R}$ par link and the $\oplus$ tensor link with which
it contracts. Given that the $\mathcal{R}$ contraction is necessary by assumption, the
only conversions which can apply between the two links are any of the logical
contractions (reducing the size by 3) and any of the $\circ 1$, $1\circ$, and $\beta$ conversions
(reducing the size by 2). Since the $\beta^{-1}\}$ reduces the size by only 1, greedy
reduction will be guaranteed to produce the required $\mathcal{R}$ redex and contract it
before considering the $\beta^{-1}\}$ conversion.
□

## 4.2 Time complexity

The decidability result of Lemma 10 gave only an upper bound for the space complexity of parsing and proof search in $NL_\lambda$. Given the confluence result of Lemma 12, we can now give a time complexity as well.

**Lemma 13** *Parsing for $NL_\lambda$, when excluding $1 \circ t$ and $\circ 1t$ conversions, is in $NP$.*

**Proof** To show the problem is in NP, it suffices to show that we can verify whether a proof candidate is a proof in polynomial time. Given a sentence and a set of goal formulas, non-deterministically select one of the goal formulas and, for each of the words in the sentence, one of the formulas the lexicon assigns to it. Non-deterministically compute the extended axiom linking to the given proof structure to produce an abstract proof structure. Reduce the resulting abstract proof structure using the eager rewrite system. Each rewrite involves scanning the abstract proof structure for redexes, noting the size reduction of the conversion, then performing one of the reductions which maximally decreases the size; each rewrite can be performed in time linear to the size of the abstract proof structure. Since each rewrite reduces the size, only a number of conversions
linear in the size of the abstract proof structure have to be performed. Finally, check whether the result is a Lambek tree with the correct yield. □

It may be possible to sharpen Lemma 13 to remove the restriction on empty antecedent derivations, or otherwise to directly refine the decidability proof of Barker (2019, Theorem 1) (or the decidability proof of Lemma 10) for this purpose. We will leave this for further research.

Given that $NL_λ$ uses a non-associative base, we cannot apply the NP-completeness result for the associative Lambek calculus (Pentus 2006) to show NP completeness of $NL_λ$. However, I conjecture that it is possible to use the $NL_λ$ mechanisms for scope and extraction to prove NP completeness for parsing.

# 5 $NL_λ$ and hybrid type-logical grammars

Hybrid type-logical grammars (Kubota & Levine 2020) are a logic combining the Lambek calculus implications with the lexical lambda term assignments of lambda grammars (Oehrle 1994). At first sight, the similarities between hybrid type-logical grammars (HTLG) and $NL_λ$ seem superficial: both have the Lambek calculus slashes<fnref n="2" />, both have a $λ$ operator to build structures, but the logical foundations appear rather different: HTLG uses lambda term assignments for its lexical entries, which $NL_λ$ doesn't, and $NL_λ$ uses a second mode which is a standard residuated connective, unlike the linear implication of HTLG. However, there is a surprising amount of overlap between the links and conversions of $NL_λ$ in this paper and the links and conversions used for proof nets for HTLG (Moot & Stevens-Guille 2019).

For reasons of space, we will not give a complete introduction to proof nets for hybrid type-logical grammars in this section. Instead, we will introduce the logical calculus by emphasising the similarity with the proof net calculus for $NL_λ$. The reader interested in the full details of proof nets for HTLG is invited to read the paper by Moot & Stevens-Guille (2019).

Hybrid type-logical grammars allow lexical entries to provide lexical lambda terms which specify how the strings should be formed.

If we return to our previous example “John saw everyone”, a possible HTLG lexicon for this same sentence would be the following.

<table><thead><tr><th>Word</th><th>Syntactic type</th><th>Prosodic type</th><th>Prosodic term</th></tr></thead><tbody><tr><td>John</td><td>np</td><td>s</td><td>John<sup>s</sup></td></tr><tr><td>saw</td><td>np &rarr; (np &rarr; s)</td><td>s &rarr; (s &rarr; s)</td><td>&lambda;y<sup>s</sup>&lambda;x<sup>s</sup>. x + saw + y</td></tr><tr><td>everyone</td><td>(np &rarr; s) &rarr; s</td><td>(s &rarr; s) &rarr; s</td><td>&lambda;P.(P everyone)</td></tr></tbody></table>

“John” is simply assigned the formula $np$ and the prosodic term $John$, a string. The lexical entry for “saw” is a function from two noun phrases to a

<footnote n="2">²The standard definition of $NL_λ$, as presented here, is as a non-associative logic, whereas hybrid type-logical grammars are generally presented as an associative logic. However, we can add or remove associativity (at least for the Lambek connectives) in either system. In what follows, we will compare $NL_λ$ to non-associative hybrid type-logical grammars.</footnote>
<figure><img src="image_30.png" /><figcaption>Figure 11: Proof structure, abstract proof structure and $\beta$-reduced abstract proof structure for a quantifier in HTLG.</figcaption></figure>

sentence at the syntactic level and a function from two strings to a string at the prosodic level<fnref n="3" />. The prosodic term uses concatenation ‘+’ to concatenate the string *x* (corresponding to the subject) to the string *saw* followed by the string *y* (corresponding to the object noun phrase).

The key entry is the lexical entry for “everyone”. It is assigned the linear logic formula ($np \to o s \to s$). Syntactically, it takes a sentence missing a noun phrase as an argument to produce a sentence. Prosodically it is a function of type ($s \to s \to s$), which we assign the term $\lambda P.(P everyone)$. This means it takes a function from strings to strings as an argument (in this particular case the string of a sentence missing a noun phrase string) and fills this position with the word *everyone*.

## 5.1 Translations of links and rewrites

We begin by a simple illustration to make the similarities immediate.

Unfolding the HTLG lexical entry for *everyone* with syntactic type ($np \to o s \to s$ and prosodic type $\lambda P.(P everyone)$) produces the proof structure shown on the left of Figure 11. As usual, tensor nodes are drawn with an open central circle whereas par nodes are drawn with a filled central circle; the mode of the link is indicated by an index (for binary links the indices are ‘+’ for Lambek calculus links, and ‘@’ and ‘$\lambda$’ for lambda grammar links, respectively corresponding to application and abstraction at the term level).

The corresponding abstract proof structure is shown in the middle of Figure 11. As usual, the $\mathcal{A}$ arrow denotes the conversion of a proof structure to an abstract proof structure. It removes formula information from internal nodes and replaces the lexical leaf ($np \to o s \to s$) by a graphical representation of

<footnote n="3">³HTLG also allows us to assign “saw” the lexical entry ($np \setminus s / np$, which is provably equivalent to the given entry).</footnote>
<figure><img src="image_31.png" /><figcaption>Figure 12: Proof structure and abstract proof structure for a quantifier in NL_λ.</figcaption></figure>

the lambda term $\lambda P.(P \text{ everyone})$, where the binding of P is indicated by the curved edge from the lambda tensor node to the left premiss of the @ tensor node — just like the lambda abstractor link for NL_λ proof nets indicates its bound variable, although the order of the conclusions differs between HTLG and NL_λ proof nets. Using a partial evaluation strategy — introduced in the context of Lambek calculus semantics by Morrill (1999) and by de Groote & Retoré (1996) — we can then reduce the beta redex in this abstract proof structure to produce the structure on the right, as indicated by the $\beta$ arrow.

For the quantifier in NL_λ, which is assigned the formula $s \llbracket (np \llbracket s) \rrbracket$, we produce the proof structure shown on the left of Figure 12 and the abstract proof structure shown on the right of the figure.

The two abstract proof structures are left-right symmetric. This is a consequence the different notational choices: the ‘functor’ of an ‘application’ is on the right for Barker (2019) and the left for Kubota & Levine (2020). This left-right symmetry applies only for the continuation connectives, the Lambek calculus connective of both calculi are identical.

The translation between the quantifier lexical entries is no accident. There is a simple equivalence between many of the links and rewrites in both logics. Table 8 shows the translations between HTLG and NL_λ. Elements of one logic which have no direct translation in the other are marked as ‘???’ in the logic where this element is missing.

The $\lambda$ tensor link (used to represent the prosodic lambda terms from the lexicon, as shown, for example, in the abstract proof structure in the middle of Figure 11) does not have a direct translation into NL_λ formulas: in NL_λ, the $\lambda$ tensor link appears only in antecedent terms (however, it appears that we can emulate most and maybe even all of this functionality judiciously using atomic formulas and the $\llbracket R \rrbracket$ rule to simulate extraction; see Section 5.4 for examples and discussion). Inversely, the par links for $\llbracket \circ \rrbracket$ and $\odot$ in NL_λ (and their logical contractions) have no direct translation into HTLG.

However, there are many similarities. Besides the shared links and contractions for the Lambek calculus implications, the key element of similarity is the presence of the $\beta$ rewrite in both logics and the fact that the $\lambda$ par rewrite in
<table><caption>Table 8: Translations between HTLG and NL<sub>λ</sub>.</caption><thead><tr><th>HTLG</th><th>NL<sub>λ</sub></th></tr></thead><tbody><tr><td>+ link</td><td>↔ ◦ link</td></tr><tr><td>@ with premisses p<sub>1</sub> - p<sub>2</sub></td><td>↔ ◦ with premisses p<sub>2</sub> - p<sub>1</sub></td></tr><tr><td>λ tensor (lexicon)</td><td>↔ ???</td></tr><tr><td>λ par with conclusions c<sub>1</sub> - c<sub>2</sub></td><td>↔ ⋀ par with conclusions c<sub>2</sub> - c<sub>1</sub></td></tr><tr><td>???</td><td>t, ⏸, ◦ par links</td></tr><tr><td>contractions for /, \</td><td>↔ contractions for /, \</td></tr><tr><td>???</td><td>contraction for •</td></tr><tr><td>λ par rewrite</td><td>↔ β<sup>-1</sup> rewrite</td></tr><tr><td>β rewrite</td><td>↔ β rewrite</td></tr><tr><td>η rewrite</td><td>↔ contraction for ⋀</td></tr><tr><td>???</td><td>contractions for t, ⏸, ◦</td></tr></tbody></table>

HTLG is equivalent to the $β^{-1} \between$ rewrite of Table 7, with identical constraints on the rule application.

**Lemma 14** When NL<sub>λ</sub> and (non-associative) HTLG lexical entries reduce to isomorphic (with respect to left-right symmetry of the continuation/linear links) abstract proof structures and require only the $β, β^{-1} \between / \to I, 1 \circ, \circ 1, \between R/η, \between R, \between R$ rewrites, then these lexical entries are logically equivalent.

The same equivalence holds between NL<sub>λ</sub> with added associativity (L<sub>λ</sub>) and standard, associative HTLG, when adding the associativity rewrites to both proof net calculi.

**Proof** Given that we produce isomorphic structures by assumption and that all the rewrite rules which can apply are equivalent as well, this is trivial. □

As a consequence of Lemma 14, many of the signature linguistic analyses proposed in the respective formalisms can be translated between the formalisms with ease. For each of these cases, we not only have equivalence at the level of the abstract proof structures, but also at level of the graph rewrites which apply to them. So in spite of the difference in logical foundations, the analyses proposed for these two logics converge in many interesting cases.

## 5.2 Gapping

Gapping is a phenomenon which has received a lot of attention in the categorial grammar literature (Hendriks 1995, Morrill et al. 2011, Kubota & Levine 2012). The basic idea is that sentences like the following can be analysed as a type of coordination.

(1) John studies logic, and Charles phonetics.

In the sentence above, the intended meaning is equivalent to the meaning of
<figure><img src="image_32.png" /><figcaption>Figure 13: Abstract proof structure of the lexical entry for gapping from Kubota & Levine (2020), before and after $\beta$ reductions.</figcaption></figure>

"John studies logic and Charles *studies* phonetics", with the word "studies" missing syntactically from the second conjunct.

Kubota & Levine (2012, 2020) propose the formula $(tv \dashv \alpha s) \dashv (tv \dashv \alpha s) \dashv tv \dashv \alpha s$ with prosodic term $\lambda Q.\lambda P.\lambda v.(P v) + and + (Q \epsilon)$ for the coordinator "and" in gapping constructions (where $tv$ is short for $(np\backslash s)/np$). The idea of this lexical entry is that it selects two sentences, each missing a transitive verb $tv$, then selects a transitive verb and inserts it in the leftmost sentence, whereas in the rightmost sentence the missing transitive verb is assigned the empty string at the term level. The advantage of such an analysis is that it is now easy to get the desired semantics of the sentence.

Looking at this lexical entry in terms of proof nets, the abstract proof structure
ture corresponding to this formula and its assigned term is shown in Figure 13 (the occurrences of *tv* have not been unfolded). The three $\lambda$ links correspond to the abstractions over $Q$ (corresponding to the rightmost sentence missing a transitive verb), $P$ (corresponding to the leftmost one) and $v$ (corresponding to the transitive verb). This is again just a graphical way to represent the lambda term assigned to the lexical entry. The unfolding of the lexical formula and its prosodic term has again produced an abstract proof structure which can be further reduced by beta reduction. After performing the three beta reductions, we obtain the abstract proof structure shown below on the right.

We can obtain the NL$_{\lambda}$ formula corresponding to this abstract proof structure by first mirroring the premisses of the @ links and the conclusions of the $\lambda$ par links, then taking as the main formula of each link the vertex closest to the lexical leaf “and”. This entails that the two @ links become continuation product formulas in NL$_{\lambda}$. Completing the computations produces the formula $((tv \odot (tv \sqcup s)) \setminus s)/(t \odot (tv \sqcup s))$. Although it is rather similar to the analysis of Morrill (1994, Section 3.4), this formula doesn’t look like a typical coordination formula. Compared to the HTLG formula and the formula of Morrill et al. (2011, Section 3.2.6), it uses a form of de-Currying on the last two arguments $((tv \sqcup s)$ and $tv$) (although this is not a *derivable* form of de-Currying since it mixes the Lambek and continuation modes).

## 5.3 Parasitic scope: “same” and “different”

Words like “same” and “different” allow what Barker & Shan (2014) call ‘parasitic scope’. Take the following sentences, for example.

(2) Everyone read the same book.

(3) Everyone read different books.

(4) No one read the same book.

(5) The same waiter served everyone.

The reading of Sentence (2) is that everyone read some books, and that there is one specific book read by everyone. Sentence (3), on the other hand, has the meaning that everyone read some set of books, but that these sets of books are all disjoint. Sentences (3) and (4) have essentially the same meaning. Sentence (5) shows that the same type on phenomenon is possible with “same” occurring in the subject and when “everyone” is the object.

Barker & Shan (2014) propose the formula $(np \sqcup s) \not\frown ((n \setminus n) \sqcup (np \sqcup s))$ for the word “same” to get the required semantic readings. It is an adjective $n \setminus n$ lifted with respect to the formula $np \sqcup s$ using the continuation mode. This allows it to function locally as an adjective, while taking scope over the same $np \sqcup s$ formula as selected by a quantifier. A fully worked out example with “same” can be found in Appendix C.

Unfolding this formula produces the proof structure and abstract proof structure shown respectively on the left and right of Figure 14. To reduce complexity,
<figure><img src="image_33.png" /><figcaption>Figure 14: Proof structure and abstract proof structure of the word “same” according to the analysis of Barker & Shan (2014)</figcaption></figure>

the subformula $n \setminus n$ has been not unfolded.

Translating the formula to HTLG produces the following formula.

$$((n \setminus n) \to np \to s) \to np \to s$$

By its structure, we know the prosodic type should be $(s \to s \to s) \to s \to s$. Given a constant ‘same’ of type $s$, there are two linear lambda terms of this type (slightly more when we add constants ‘+’ and ‘ε’). In general, there can be many choices for the linear lambda term and choosing the correct one (to obtain a given abstract proof structure) can be tricky. This is because it is easier to evaluate a program (i.e. reduce a lambda term) than to construct one given its output.

In this case, it is easy to see the prosodic term should be $\lambda P.\lambda x.((P \ same) x)$. The abstract proof structure for this lexical entry is shown on the left of Figure 15. Performing the two beta reductions produces the abstract proof structure shown on the right of the figure.

The abstract proof structure on the right of Figure 15 is again the left-right symmetric version of the abstract proof structure for “same” in $NL_{\lambda}$ shown in Figure 14.

## 5.4 Dutch verb clusters

One well-studied topic in linguistics and formal language theory are the crossed dependencies which occur for verb clusters and their objects in Dutch relative clauses. The complexity of the phenomenon is illustrated by the famous ‘hip-popotamus’ sentences such as the following.
<figure><img src="image_34.png" /><figcaption>Figure 15: The analysis of “same” from Barker & Shan (2014) translated into HTLG.</figcaption></figure>

(6) (dat) Jan Marie de nijlpaarden zag voeren
(that) Jan Marie the hippopotami saw feed
‘(That) John saw Marie feed the hippopotami’

(7) (dat) Jan Henk Marie de nijlpaarden zag helpen voeren
(that) Jan Henk Marie the hippopotami saw help feed
‘(That) John saw Henk help Marie feed the hippopotami’

The key point of Sentence (7) is the “de nijlpaarden” (the hippopotami) is the object of “voeren” (feed), “Marie” the object of “helpen” (help), and “Henk” the object of “zag” (saw), leading to ‘crossed’ dependencies between the verbs and their objects, which is essential to produce the right meaning under the standard (minimal) type-logical assumptions of the syntax-semantic interface.

Unlike the previous cases, we cannot directly apply Lemma 14 here: the
HTLG lexical items shown below crucially use lexical lambda terms which can-
not be reduced directly in the abstract proof structures corresponding to the
lexical unfolding.

However, there is a work-around for this problem. Given the following NL<sub>λ</sub>
lexicon, we generate exactly the correct readings.

<table>
  <tr>
    <td>dat</td>
    <td>s<sub>that</sub> / s<sub>sub</sub></td>
  </tr>
  <tr>
    <td>Jan</td>
    <td>np</td>
  </tr>
  <tr>
    <td>Henk</td>
    <td>np</td>
  </tr>
  <tr>
    <td>Marie</td>
    <td>np</td>
  </tr>
  <tr>
    <td>de</td>
    <td>np / n</td>
  </tr>
  <tr>
    <td>nijlpaarden</td>
    <td>n</td>
  </tr>
  <tr>
    <td>zag</td>
    <td>(np \ (np \ s<sub>sub</sub>)) ⌜(j ⌜ inf)</td>
  </tr>
  <tr>
    <td>helpen</td>
    <td>j \ ((np \ inf) ⌜(j ⌜ inf))</td>
  </tr>
  <tr>
    <td>voeren</td>
    <td>j \ (np \ inf)</td>
  </tr>
</table>

The key property is that we use a special atomic formula *j* to mark a point for future extraction. In the lexical entry for “voeren”, when combined with all its arguments will produce the structure (*de* ◦ *nijlpaarden*) ◦ (*j* ◦ *voeren*) with *j* the left sister of *voeren*. The following proof shows how we combine this phrase with “Marie” and “helpen” (to save space, we have abbreviated (*de* ◦ *nijlpaarden*) by *dn*).

$$
\[
\frac{
  \begin{array}{@{}c@{\quad}c@{}}
    \begin{array}{@{}c@{}} \vdots \\ j \vdash j \end{array}
    &
    \begin{array}{@{}c@{}} \frac{\displaystyle dn \circ (j \circ \text{voeren}) \vdash \text{inf}}{j \odot \lambda x.dn \circ (x \circ \text{voeren})} \beta^{-1} \quad \vdots \quad \frac{\displaystyle \lambda x.dn \circ (x \circ \text{voeren}) \vdash j \unrhd \text{inf}}{\lambda x.dn \circ ((np \unrhd \text{inf}) \unrhd (j \unrhd \text{inf})) \odot \lambda x.dn \circ (x \circ \text{voeren})} \vdash \text{inf} \quad \unrhd_L \frac{\displaystyle \text{Marie} \circ ((j \circ \text{helpen}) \odot \lambda x.dn \circ (x \circ \text{voeren})) \vdash \text{inf}}{\text{Marie} \circ (dn \circ ((j \circ \text{helpen}) \circ \text{voeren})) \vdash \text{inf}} \beta
  \end{array}
}{Ax}
\]
$$

We can see that “Marie” is concatenated before “de nijlpaarden” whereas the
insertion point ‘*j*’ is replaced by “*j* ◦ *helpen*”, effectively putting “helpen” before
“voeren” and creating a new insertion point before “helpen”.

Reading the proof as backward chaining proof search, we start by moving (*j* ◦ *helpen*) between “Marie” and “de nijlpaarden”. We then use the \L rule to combine “helpen” with its *j* argument. This produces the subproof *j* ⊢ *j* and replaces (*j* ◦ *helpen*) by ((np \ inf) ⌜(*j* ⌜ inf)) in the other proof branch. In that branch, we can immediately apply the ⌜L rule. The right branch is a trivial NL derivation. The left branch uses the standard combination of ⌜R and *β* to move the *j* formula in the place from where we moved out (*j* ◦ *helpen*) at the start of the proof. We can then complete the proof using the NL rules.

Figure 16 shows the only abstract proof structure for Example (7) (at least the only one which produces the correct noun phrase order). We leave the reader to verify that two applications of the $\beta^{-1} \unrhd$ conversion and two applications of the $\beta$ conversion produce a tree with the right yield.

This analysis is extremely close to the Displacement calculus analysis of
Morrill et al. (2011, Section 3.2.8) when we translate $A \unrhd (j \unrhd B)$ by $B \setminus_w A$ and
j by J.

zag inf\_w (np \ (np \ s_{sub}))

helpen J \ (inf\_w (np \ inf))

voeren J \ (np \ inf)

The key logical rule which makes this analysis work is the following<fnref n="4" />.

$$ \frac{\Delta_1, J, \Delta_2 \vdash A \quad \Gamma_1, C, \Gamma_2 \vdash C}{\Gamma_1, \Delta_1, A \setminus_w C, \Delta_2, \Gamma_2 \vdash C} L\_w $$

The $L\_w$ rule allows a formula $A\_w C$ to select the $\Delta_1$ and $\Delta_2$ structures which surround it, while marking the separation between the two with $J$. In the Displacement calculus, the $NL_\lambda$ proof above looks as follows.

$$ \frac{\vdots}{J \vdash J} Ax \quad \frac{\begin{array}{l} dn, J, \text{voeren} \vdash \text{inf} \quad \text{Marie, np} \setminus \text{inf} \vdash \text{inf} \\ \text{Marie, dn, inf} \setminus_w (np \setminus \text{inf}), \text{voeren} \vdash \text{inf} \end{array}}{\text{Marie, dn, J, helpen, voeren} \vdash \text{inf}} L\_w \setminus L $$

The comparison with hybrid type-logical grammars is also instructive. The following lexicon allows HTLG to analyse the Dutch verbs (the other lexical entries stay the same). The atomic type `inf` is assigned the complex prosodic type $s \to s$. The abstracted variable $v$ plays the same role as the $j$ atomic formula in $NL_\lambda$ and as the $J$ formula in the Displacement calculus.

<table><thead><tr><th>Word</th><th>Syntactic type</th><th>Prosodic term</th></tr></thead><tbody><tr><td>zag</td><td>inf &rarr; np &rarr; np &rarr; s</td><td>&lambda;P<sup>s&rarr;s</sup> &lambda;x<sup>s</sup> &lambda;y<sup>s</sup>.x + y + (P zag)</td></tr><tr><td>helpen</td><td>inf &rarr; (np &rarr; inf)</td><td>&lambda;P<sup>s&rarr;s</sup> &lambda;x<sup>s</sup>.&lambda;v<sup>s</sup> x + P(v + helpen)</td></tr><tr><td>voeren</td><td>np &rarr; inf</td><td>&lambda;x&lambda;v.x + v + voeren</td></tr></tbody></table>

With these lexical entries, the phrase “de nijlpaarden voeren” is assigned the term $\lambda v.de + nijlpaarden + v + voeren$. Then giving “helpen” this infinitive and “Marie” as arguments produces a term which normalises to the following.

$$ \lambda v.\text{Marie} + de + nijlpaarden + v + \text{helpen} + \text{voeren} $$

Finally, applying this term and “Jan” and “Henk” to “zag” produces the required string.

Figure 17 shows the HTLG abstract proof structure for “(dat) Jan Henk Marie de nijlpaarden zag helpen voeren”, after some $\beta$ reductions have simplified the structure. We can again see the similarity with the $NL_\lambda$ abstract proof structure of Figure 16: applying the $\beta^{-1}\$ conversion twice to the structure of Figure 16 produces a structure which is equivalent under the now standard left-right symmetry of the ‘$\lambda$’ and ‘@’ links with respect to the corresponding $NL_\lambda$ links.

<footnote n="4">⁴The rule presented here is simplified from the rule of Morrill et al. (2011). However, this simplification does not affect the analysis.</footnote>
<figure><img src="image_35.png" /><figcaption>Figure 16: Abstract proof structure for the NL_λ analysis of “(dat) Jan Henk Marie de nijlpaarden zag helpen voeren”.</figcaption></figure>

However, there is an important difference in the two analyses: the $\beta^{-1}\backslash$ rewrite, which produces the $\lambda$ link in NL$_\lambda$, requires the $\backslash R$ par link (it is produced by the positive $j\backslash inf$ subformula of “zag” and “helpen”; the topmost par link is part of the lexical entry for “helpen” and the bottom par link is part of the lexical entry for “zag”) whereas in the HTLG analysis $\lambda$ links come from the lexicon (the topmost lambda link is part of the lexical entry for “voeren”, the bottom lambda link of the lexical entry for “helpen”). So although the abstract proof structures end up as equivalent, the lexical entries divide the links in different ways.
<figure><img src="image_36.png" /><figcaption>Figure 17: Abstract proof structure for the HTLG analysis of “(dat) Jan Henk Marie de nijlpaarden zag helpen voeren”.</figcaption></figure>

## 5.5 Differences and untranslatables

Having the residuals of the continuation mode (and the formula corresponding to the empty string) allows $NL_{\lambda}$ to have a simple treatment of the across-the-board cases of extraction such as the following.

(8) Which book does Peter like - but Mary hate -?

Sentences like (8) are grammatical only when the two coordinated phrases “Peter like” and “Mary hate” both miss the same material (here, both sentences are
incomplete for a noun phrase). In NL<sub>λ</sub> we can simply use the standard formula
for “and” (X \ X)/X with X = t ⊙ (np ⸥ s). The left rule for the product of the
continuation mode (corresponding to its par link) and the left rule for t (again a
par link) ensure this works correctly. This analysis can therefore not be directly
adapted to HTLG, but unlike the Dutch verb cluster case of Section 5.4, there
doesn’t appear to be a work-around either.

Conversely, lexical entries in HTLG using ‘irreducible’ lambda terms (that is,
lambda terms which cannot be β-reduced at the level of the formula unfolding)
need not allow a reanalysis like the Dutch verb cluster example, and this would
point to an advantage of HTLG over NL<sub>λ</sub>.

One conclusion to draw from all this is that there appears to be a ‘common
core’ to modern type-logical grammars (including HTLG, NL<sub>λ</sub> and the Displace-
ment calculus) which, even though it is a sort of least common denominator,
already handles quite a few sophisticated phenomena.

Where a logic allows for operations outside of this common core, and where
a direct translation is therefore impossible, provides a useful starting point for
discovering potential advantages of one system over another.

Another way to resolve the tension between HTLG and NL<sub>λ</sub> is to *combine* the two logics into a single, convergent framework (a doubly-hybrid type-logical grammar). This would move HTLG into a more standard multimodal setting, where all connectives are part of a residuated triple, and give it an analysis of across-the-board phenomena. From the NL<sub>λ</sub> perspective, this would give NL<sub>λ</sub> access to lambda terms at the level of the lexicon as well, and allow it to use the HTLG analyses from Kubota & Levine (2020) directly.

6 Formal language

We have seen in Section 5.4 how NL<sub>λ</sub> can handle Dutch verb clusters. A natural follow-up question is: what class of formal languages can be generated by NL<sub>λ</sub>. In this section we provide some preliminary answers to this question. We assume the reader has some basic familiarity with mildly context-sensitive formalisms (Joshi et al. 1991, Seki et al. 1991, Kallmeyer 2010).

It is well-known that a wrapping operator as defined for the analysis of crossing
dependencies in Section 5.4 suffices for generating (at least) the simplest class
of the mildly context-sensitive languages (Weir et al. 1986, Joshi et al. 1991) —
the tree adjoining languages or the languages generated by well-nested 2-MCFL
(Joshi et al. 1991, Seki et al. 1991). This means that in addition to giving an
analysis of Dutch verb clusters, we have also shown that NL<sub>λ</sub> generates at least
the weakest class of the mildly context-sensitive languages.

**Lemma 15** *NL*<sub>*λ*</sub> *generates mildly context-sensitive languages*

With enough separation symbols $j_1, \dots, j_n$ the construction of Section 5.4 can be extended to generate the well-nested mildly context-sensitive languages<fnref n="5" />. I am

<footnote n="5">⁵When desired, multiple occurrences of the same symbol $j_i$ can be used to emulate the non-deterministic wrapping operation of Morrill et al. (2011, Section 3.4)</footnote>
**Proof** We can generate $(a_1a_2...a_k)^+$ using the following lexicon.

a_1 ((s / t_k) ... / t_2)
a_1 ((s / t_k) ... / t_2) / s
a_2 t_2
...
a_n t_k

Lemma 17 gives us the permutation closure of this language as required. □

MIX₃ is known to be a mildly context-sensitive language — it is a 2-MCFL (Salvati 2015) but not well-nested (Makoto & Salvati 2012). However, the precise place of the generalised MIX languages in the standard inclusion hierarchy of formal languages used for computational linguistics (Kallmeyer 2010) is not known. There are simple ways to derive them in quite expressive formalisms outside of the mildly context-sensitive classes such as Range Concatenation Grammars (Boullier 1999, Kallmeyer 2010). It therefore appears that the classes of languages generated by NL_λ (and many other type-logical grammars) fall outside the standard language-theoretic classes. For example, the formalisms which can handle the generalised MIX languages also handle the language which, for all n, generates exactly 2ⁿ occurrences of a (Kallmeyer 2010), and this 'exponential' language appears outside of what most type-logical grammars can handle: generating 2ⁿ occurrences of a symbol strongly suggests a formalism-internal mechanism for copying, which contradicts the multiplicative nature of type-logical grammars.

With respect to the formalisms whose language classes do not yet have a precise place in the standard hierarchy, some of the formalisms which provide non-local permutation mechanisms, such as multi-set valued linear indexed grammars and some extensions of tree adjoining grammars (Rambow 1994, Becker 1994) are candidates for formalisms deriving the same language classes as type-logical grammars<fnref n="6" />. This would point to a refinement of the standard picture, possibly adding the presence and absence of permutation closure as a parameter comparable to the presence and absence of well-nestedness. Alternatively, it may turn out that these language classes correspond to one of the classes in the standard hierarchy<fnref n="7" />.

Concluding, although we have shown that NL_λ can generate (well-nested) mildly context-sensitive languages and the permutation closure of any context-free language, these are only lower bounds on the language class generated by the formalism. As with many other type-logical grammars, there is no precise upper bound (other than the context-sensitive languages). A precise formal

<footnote n="6">⁶There are a number of technical difficulties adapting the proof of Pentus (1997) — which shows the Lambek calculus generates exactly the context-free languages — to other type-logical grammars, as discussed by Buszkowski (1997, Section 3.2) and Moot & Retoré (2019, Section 3).</footnote>

<footnote n="7">⁷Extending the proof of Salvati (2015) to the generalised MIX languages would similarly require a solution to many technical difficulties (Nederhof 2016).</footnote>
characterisation of the language classes generated by type-logical grammars re-
mains an important open question.

# 7 Conclusion

We have investigated the proof theoretic aspects of NL_λ by introducing a proof
net calculus for the logic, and proving proof nets are sound and complete with
respect to the standard sequent calculus presentation. Thanks to this proof
net calculus, we have also shown that excluding the empty antecedent means
NL_λ proof search is in NP, an improvement over the previous upper bound. Fi-
nally, we have shown there to be a surprising convergence between the linguistic
analyses in NL_λ and those in hybrid type-logical grammars. This extends the
empirical coverage of NL_λ and gives a first analysis of the logic in terms of the
class of formal languages generated.

A Treating the unit as an atom

In proof theory, there are generally two ways to treat the logical constants like
'⊤' and '⊥' in classical logic and '1' and '⊥' in multiplicative linear logic: we
can treat them as 0-ary connectives, or we can treat them as atomic formulas
with special rules.

In the above, we have treated the unit ‘t’ as a 0-ary connective. In this
section we briefly present what it would entail to treat ‘t’ as an atomic formula.
If *t* is treated as an atomic formula, it neither has its own logical links<sup>8</sup> nor
its own contractions. Formula unfolding would simply stop like for any other
atomic formula. Instead of the contractions, we have the two structural rules
shown below.

<figure><img src="image_37.png" /></figure>

The structural rules simply allow us to rewrite a 't' atomic formula (occurring
as a hypothesis) for its structural connective '1' and vice versa. While this works
as it should, the fact that the t⁻¹ rule introduces a new atomic formula means
that we lose the clear separation of stages: first unfolding the formulas, then
linking the axioms, and finally rewriting. The t⁻¹ can require us to have an
axiom connection as a rewrite step on the abstract proof structure, for example
for the following proof of A ⊢ A / t. We start from the unique abstract proof
structure obtained by unfolding the formulas, identifying the A formulas and
translating the resulting proof structure to its abstract proof structure. The
result is shown below as the leftmost abstract proof structure.

<footnote n="8">⁸In the abstract proof structure, we will still have the link for its structural connvective
‘1’.</footnote>
<figure><img src="image_38.png" /></figure>

We expand the $A$ formula to $A \circled{1}$ using the $\circled{1}$ structural rule, then replace the structural 1 by the $t$. This adds a $t$ hypothesis to the abstract proof structure. We then identify the vertices with the $t$ hypothesis and with the $t$ conclusion to produce a redex for the $/R$ contraction, which we perform to complete the proof.

We can modify our proof net calculus to do the connections of atomic formula at the abstract proof structure level instead of at the proof structure level.

For comparison, we show the same proof but with the unit treated as a 0-ary connective. The conversion sequences are quite similar, and the contraction for $tL$ works rather like the axiom connection in the reduction sequence above.

<figure><img src="image_39.png" /></figure>

# B Meaning assignment for the unit

Under the standard term assignments for intuitionistic (linear) logic (Troelstra 1992), we obtain the following term assignment rules for the unit $t$ in $NL_\lambda$.

$$ \frac{\Delta \vdash N^1 : t \quad \Gamma[1] \vdash M^\alpha : C}{\Gamma[\Delta] \vdash E^t(M, N)^\alpha : C} tE $$

As usual, the term assignments are for the natural deduction rules, and we note that the $tE$ rule uses a context formula $C$, requiring permutation conversions for the term assignment rules (confirming it behaves like a 0-ary version of the binary ‘•’).

The term corresponding to the $tI$ rule is the term constant ‘*’ of type **1** (the semantic type corresponding to the unit $t$). The term constructor $E^t$, corresponding to the $tE$ rule, takes a term $M$ of type $\alpha$ (corresponding to the
semantic type of the formula C) and a term N of type 1 (the semantic type corresponding to the unit t), to produce a term of type α.

The η and β conversion steps correspond to the proof normalisations shown, respectively as Equation 3 and 4 below.

$$ \frac{\frac{\overline{1 \vdash * : t^1} \quad tI}{\Gamma[1] \vdash E^t(M, *)^\alpha : C} \quad \vdots \quad \delta}{\Gamma[1] \vdash M^\alpha : C} \quad tE \rightsquigarrow \Gamma[1] \vdash M^\alpha : C \quad (3) $$

$$ \frac{\frac{\vdots \delta}{\Delta \vdash N^1 : t \quad \overline{1 \vdash *^1 : t} \quad tI} \quad tE}{\Delta \vdash E^t(*, N)^1 : t} \rightsquigarrow \Delta \vdash N^1 : t \quad \vdots \quad \delta \quad (4) $$

The corresponding term rewrites are shown as Equations 5 and 6.

$$ E^t(M, *)^\alpha \rightsquigarrow M^\alpha \quad (5) $$

$$ E^t(*, N)^1 \rightsquigarrow N^1 \quad (6) $$

We will not list the full set of commutative conversions which are necessary here: the tE rule can permute with all logical rules<fnref n="9" /> and although the term conversions are fairly standard, there are rather many of them.

## C A more complicated example

As a more complicated example showing how to use proof nets for NL_λ theorem proving, we show how to derive “everyone read the same book”, an example from Section 5.3. We use the following lexical entries.

* everyone $s \llbracket (np \llbracket s) \rrbracket$
* read $(np \setminus s) / np$
* the $np / n$
* same $(np \llbracket s) \rrbracket ((n \setminus n) \llbracket (np \llbracket s) \rrbracket)$
* book $n$

Given the above lexicon, Figure 18 shows the formula unfolding for the sentence “everyone read the same book”. To improve readability of the structure and to save space, the formula of each lexical entry has been replaced by the label of the corresponding word, so, for example, “the” denotes the formula $np / n$.

<footnote n="9">⁹It permutes with the structural rules as well, but these rule permutations do not correspond the term equations.</footnote>
<figure><img src="image_40.png" /><figcaption>Figure 18: Formula unfolding for “everyone read the same book”.</figcaption></figure>

We identify the atomic formulas of the structure to obtain the proof structure shown on the left of Figure 19. The par link of “everyone” forms a redex with the bottom tensor link of “same”, the topmost par link of “same” will ensure that “everyone” appears as the subject, whereas the other par link of “same” has its position determined by the place of the adjective subformula $n/n$, which appears between “the” and “book”, since this is where we want the word “same” to end up.

The corresponding abstract proof structure is shown on the right of Figure 19. This should by now be familiar: all internal formulas have been removed and only the hypotheses and conclusions of the structure are still assigned formulas.

To show this is a valid proof net, we have to convert the abstract proof structure of Figure 19 to a tree of Lambek (singly circled) tensor links, using the contraction rules of Table 5, the structural rules of Table 6. There easiest way to do this, it to use the rewrite rules of Table 6 from left to right only and to use the derived $\beta^{-1}\}$ rule of Table 7, following the discussion in Section 4.

We start with the $\mathbb{R}$ contraction, which produces the abstract proof structure shown on the left of Figure 20. There are no further contractions possible, so we apply the $\beta^{-1}\}$ conversion to the two remaining $\mathbb{R}$ par links to obtain first the structure shown in Figure 20 on the right, then the structure shown in Figure 21 on the left.

We are now in the situation where we can apply the $\beta$ conversion twice in succession, first putting “same” in the right place, , as shown in Figure 21 on the right, then “everyone” as shown in Figure 22. This is a Lambek tree with the required yield “everyone read the same book”. We have therefore shown
<figure><img src="image_41.png" /><figcaption>Figure 19: Proof structure (left) and the corresponding abstract proof structure (right) for “everyone read the same book”.</figcaption></figure>

that the proof structure back in Figure 19 is a proof net.

References

Barendregt, H. (1981), *The Lambda Calculus: Its Syntax and Semantics*, Vol. 103 of *Studies in Logic and The Foundations of Mathematics*, Elsevier. Revised Edition, 1984.
<figure><img src="image_42.png" /><figcaption>Figure 20: The abstract proof structure on the right of Figure 19 after the ⋀R contraction (left) and after the β⁻¹∢ conversion (right).</figcaption></figure>

Barker, C. (2019), ‘NL<sub>λ</sub> as the logic of scope and movement’, *Journal of Logic, Language and Information* **28**(2), 217–237.

Barker, C. & Shan, C. (2014), *Continuations and Natural Language*, Oxford Studies in Theoretical Linguistics, Oxford University Press.

Becker, T. (1994), HyTAG: A New Type of Tree Adjoining Grammars for Hybrid Syntactic Representation of Free Word Order Languages, PhD thesis, Saarland University, Saarbrücken.

Becker, T., Rambow, O. & Niv, M. (1992), The derivational generative power of formal systems or scrambling is beyond LCFRS, Technical Report 38, Institute for Research in Cognitive Science, University of Pennsylvania, Philadelphia.

Boullier, P. (1999), Chinese numbers, MIX, scrambling and range concatenation
<figure><img src="image_43.png" /><figcaption>Figure 21: The abstract proof structure of Figure 20 after the $\beta^{-1}\L$ contraction (left) and the $\beta$ conversion (right).</figcaption></figure>

<figure><img src="image_44.png" /><figcaption>Figure 22: Final tree computed after $\beta$ reduction from the abstract proof structure on the right of Figure 21.</figcaption></figure>
grammars, in 'Proceedings of the European Association of Computational Linguistics EACL'99'.

Buszkowski, W. (1997), Mathematical linguistics and proof theory, in J. van Benthem & A. ter Meulen, eds, 'Handbook of Logic and Language', North-Holland Elsevier, Amsterdam, chapter 12, pp. 683-736.

de Groote, P. & Retoré, C. (1996), On the semantic readings of proof nets, in G.-J. Kruijff, G. Morrill & R. T. Oehrle, eds, 'Formal Grammar', pp. 57-70.

Emms, M. (1993), Extraction covering extensions of the Lambek calculus are not context free, in P. Dekker & M. Stokhof, eds, 'Proceedings 9th Amsterdam Colloquium', pp. 268-286.

Hendriks, P. (1995), Ellipsis and multimodal categorial type logic, in G. Morrill & R. T. Oehrle, eds, 'Proceedings of Formal Grammar 1995', Barcelona, Spain, pp. 107-122.

Hopcroft, J. E. & Ullman, J. D. (1979), *Introduction to Automata Theory, Languages and Computation*, Addison-Wesley, Reading, Massachusetts.

Joshi, A., Shanker, V. & Weir, D. (1991), The convergence of mildly context-sensitive grammar formalisms, in P. Sells, S. Shieber & T. Wasow, eds, 'Foundational Issues in Natural Language Processing', MIT Press, Cambridge, Massachusetts, pp. 31-82.

Kallmeyer, L. (2010), *Parsing Beyond Context-Free Grammars*, Springer.

Kubota, Y. & Levine, R. (2012), 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.

Kubota, Y. & Levine, R. (2020), *Type-Logical Syntax*, MIT Press.

Makoto, K. & Salvati, S. (2012), Mix is not a tree-adjoining language, in 'Proceedings of the 50th Annual Meeting of the Association for Computational Linguistics'.

Moortgat, M. (1997), Categorial type logics, in J. van Benthem & A. ter Meulen, eds, 'Handbook of Logic and Language', Elsevier/MIT Press, chapter 2, pp. 93-177.

Moortgat, M. & Moot, R. (2013), Proof nets for the Lambek-Grishin calculus, in E. Grefenstette, C. Heunen & M. Sadrzadeh, eds, 'Quantum Physics and Linguistics: A Compositional, Diagrammatic Discourse', Oxford University Press, pp. 283-320.

Moot, R. & Puite, Q. (2002), 'Proof nets for the multimodal Lambek calculus', *Studia Logica* **71**(3), 415-442.
Moot, R. & Retoré, C. (2019), ‘Natural language semantics and computability’, *Journal of Logic, Language and Information* **28**, 287–307.

Moot, R. & Stevens-Guille, S.-J. (2019), Proof-theoretic aspects of hybrid type-logical grammars, in *Proceedings of Formal Grammar 2019*, Vol. 11668 of *Lecture Notes in Computer Science*, Springer, pp. 84–100.

Morrill, G. (1994), *Type Logical Grammar*, Kluwer Academic Publishers, Dordrecht.

Morrill, G. (1999), Geometry of lexico-syntactic interaction, in *Proceedings of the Ninth Conference of the European Chapter of the Association for Computational Linguistics*, Bergen, Norway, pp. 61–70.

Morrill, G., Valentín, O. & Fadda, M. (2011), ‘The displacement calculus’, *Journal of Logic, Language and Information* **20**(1), 1–48.

Nederhof, M.-J. (2016), A short proof that o.2 is an MCFL, Technical report, arXiv.

Oehrle, R. T. (1994), ‘Term-labeled categorial type systems’, *Linguistics & Philosophy* **17**(6), 633–678.

Pentus, M. (1997), ‘Product-free Lambek calculus and context-free grammars’, *Journal of Symbolic Logic* **62**, 648–660.

Pentus, M. (2006), ‘Lambek calculus is NP-complete’, *Theoretical Computer Science* **357**(1), 186–201.

Rambow, O. (1994), Formal and Computational Aspects of Natural Language Syntax, PhD thesis, University of Pennsylvania.

Salvati, S. (2015), ‘MIX is a 2-MCFL and the word problem in Z2 is captured by the IO and the OI hierarchies’, *Journal of Computer and System Sciences* **81**(7), 1252–1277.

Seki, H., Matsumura, T., Fujii, M. & Kasami, T. (1991), ‘On multiple context-free grammars’, *Theoretical Computer Science* **88**, 191–229.

Troelstra, A. S. (1992), *Lectures on Linear Logic*, CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California.

Weir, D. J., Vijay-Shanker, K. & Joshi, A. K. (1986), The relationship between tree adjoining grammars and head grammars, in *Proceedings of the 24th Meeting of the Association for Computational Linguistics*.