Richard Moot

Laura Kallmeyer

Paola Monachesi

Gerald Penn

Filtering Axiom Links for Proof Nets

Keywords: categorial grammar, proof nets, proof search, Lambek calculus

An important problem for proving statements in multimodal categorial grammar is that even when using proof nets -which improve upon proof search in natural deduction and sequent calculus by identifying all equivalent proofs -the number of possible axiom links to consider is still enormous. We will propose several efficient strategies to reduce the number of axiom links and will evaluate the resulting combined strategy against a large number of random, provable Lambek calculus statements and find that we eliminate 97.92% of the planar axiom links which do not correspond to any proof net.

Introduction

The multimodal Lambek calculus [START_REF] Moortgat | Categorial type logics[END_REF]) is a powerful and flexible grammar framework. Unfortunately, it has some sublogicslike the associative Lambek calculus L or the associative, commutative Lambek-Van Benthem calculus LP -which are known to be NP complete [START_REF] Pentus | Lambek calculus is NP-complete[END_REF][START_REF] Kanovich | The multiplicative fragment of linear logic is NPcomplete[END_REF].

In this article we will look at proof nets for the multimodal Lambek calculus and investigate ways to reduce the number of axiom links we need to perform in order to decide whether a statement Γ ⊢ C is derivable or not.

We will then evaluate the effect of these reductions on a large number of randomly generated Lambek calculus sequents and find that the combined filtering strategies filter our the large majority of the incorrect axiom links, that is, those axiom links which are not part of any proof net, showing that -in spite of the theoretical complexity -in practice we can parse Lambek grammar while making just a small percentage of incorrect axiom links.

The rest of this paper is structured as follows. Section 1.2 will give a short introduction to parsing statements of the multimodal Lambek calculus using proof nets. Section 1.3 will discuss four strategies for reducing the total number of axioms links. The first two: acyclicity and connectedness (Section 1.3.1) and first-order approximation (Section 1.3.2) are fairly well-known and I will touch upon them only briefly. The final two strategies are new. We will show how to compute the relations between pairs of unary connectives using a context free grammar in Section 1.3.3 and how to eliminate axiom links which cannot be part of a total linking using methods from constraint logic programming in Section 1.3.4. Section 1.4 will evaluate the combined algorithm against a set of derivable Lambek calculus sequents.

Proof nets

We will follow [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF] in our presentation of proof nets in this section. Constructing a proof structure for a statement in the multimodal Lambek calculus is done in three phases:

1. decompose the lexical formulas as well as the goal formula, 2. connect positive and negative atomic formulas, 3. decide whether the resulting proof structure is a proof net, using a correctness criterion.

We will look at each of the three phases in turn. Decomposing the lexical formulas is deterministic and linear in the number of connectives in the statement. Depending on whether a complex formula is a hypothesis (antecedent formula) or a conclusion (succedent formula), only one link can apply and we can simply descend the formula tree until we reach the leaves, which are the atomic formulas.

The full set of links is shown in Table 1. There are two links for every connective: one for when it occurs as a hypothesis (portrayed at the bottom; antecedents formulas start their unfolding here) and one for when it occurs as a conclusion (portrayed at the top; the goal formula starts its unfolding here).

The rule for B\ i A as a hypothesis is simply the modus ponens rule, saying it combines with a B on its left to form an A. The rule for B\ i A as a conclusion is its exact opposite: it allows us to use a B hypothesis to prove an A. Of course, we'll need to check that the B occurs as the Filtering Axiom Links for Proof Nets / 3 June 29, 2007

A•iB A B i i A B B\iA I i A A/iB B 3jA A j 6 j A 2 ↓ j A ? i A•iB A B A B B\iA i A A/iB B i ? j 3jA A A 2 ↓ j A j TABLE 1
Logical links for the multimodal Lambek calculus leftmost sister of the A node and this is where the contractions will come in later. Figure 1 shows an example unfolding of the sequent np, (np\s)/np, ((np\s)/np)\(np\s) ⊢ s which would be a lexical lookup for a sentence like 'Robin wet himself'. The numbers on the atomic formulas are not a part of the proof structure, they serve only to help us refer to the different formulas later. This is a slightly simplified version of the abstract proof structures of [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF]. We have suppressed as much information as possible: the information on the internal nodes, the lexical formula (both of them can be uniquely reconstructed from the unfolding) and the premiss/conclusion distinction of the individual nodes in Figure 1 as well (since we need it only when there is just a single antecedent formula).

The second part of constructing a proof net is identifying the axiomatic formulas: we select a positive and a negative atomic formula of the same type and identify their vertices, thereby connecting different parts of the graph. For this second step, there are potentially many solutions and the main part of this paper will focus on strategies for reducing these possibilities as much as possible.

Figure 1 shows the possibilities for the axioms links by portraying them in a grid: every row represents the axiom link possibilities for a negative formula, whereas every column represents the axiom link possibilities for a positive formula. A full axiom linking corresponds to putting exactly one mark in every row and column. In graph theory, this is usually called a perfect matching.

I 0 np 3 0 s 3 np 2 himself 0 s 2 np 6 0 np 1 Robin wet np 5 0 s 1 np 4 0 Goal s 4 np 1 np 2 np 3 np 4 np 5 np 6 s 1 s 2 s 3 s 4 FIGURE 1
Formula unfolding and axiom link possibilities for np, (np\s)/np, ((np\s

)/np)\(np\s) ⊢ s i ? i τ 2 τ 1 → τ 2 τ 1 i i τ 2 τ 1 → τ 2 τ 1 TABLE 2 Graph contractions
The final step is checking if the resulting graph is a proof net, by contracting all par links, drawn with the black center, as shown in Table 2. When all par links have been contracted, the result will be a tree with the lexical entries used as its leaves.

In case it is impossible to contract a par link, the proof structure we are dealing with is not a proof net and therefore, we know there is no proof of the corresponding sequent.

Filtering Axiom Links

Simple combinatorics shows that there are n! possible axiom linkings for 2n atomic formulas. In Figure 1, there are therefore 2 possibilities for s and 6 possibilities for np. This makes exhaustive search prohibitive

I 0 np 3 0 s 3 np 2 himself 0 s 2 np 6 0 np 1 Robin wet np 5 0 s 1 np 4 0 Goal s 4 np 1 np 2 np 3 np 4 np 5 np 6 0,1 c,W 2,d X,1 2,Y V,W X,Y V,3 c,d 0,3 s 1 s 2 s 3 s 4
First-order constraint

Acyclicity and connectedness

Both FIGURE 2 Links excluded by the acyclicity and connectedness condition for all but the most trivial statements. However, there are several possibilities to rule out axiom links which can never contribute to a contractible proof structure. We discuss some known and some new strategies in the following sections. [START_REF] Danos | The structure of multiplicatives[END_REF] introduce the acyclicity and connectedness criterion for proof nets of multiplicative linear logic. Give that the categorial logics we work with are all sublogics of multiplicative linear logic (in the sense that any derivable sequent in multimodal categorial grammar has a derivable image in multiplicative linear logic) we can use the fact that anything underivable in MLL is underivable in categorial grammar as well. [START_REF] Moot | Graph algorithms for improving type-logical proof search[END_REF] shows how an adaptation of the Floyd-Warshall algorithm can be used to select from the total set of possible axiom links those that produce acyclic and connected proof structures. The complexity of this application of the Floyd-Warshall algorithm is O(n 4 ).

Acyclicity and Connectedness

Figure 2 shows, in dark gray and black, the links which are excluded when we use this condition. We remark that this leaves just one possibility for linking the s formulas.

First-order Approximation and Word Order

Even though the acyclicity and connectedness check is an effective test, it is based on the 'worst case' scenario of a fully associative and commutative logic. A second strategy for removing axiom links which cannot contribute to constructing a proof net is to use first-order approximation to take constraints on word order into account. This has been used at least since LLoré and Morrill (1995) (though in a slightly different context). [START_REF] Moot | Linguistic applications of first order multiplicative linear logic[END_REF] propose an embedding of the Lambek calculus using first-order quantifiers and show how several linguistic phenomena like quantifier scope ambiguities, wh extraction and island constraints -for which there is no satisfactory treatment in the Lambek calculus -can be given an analysis using first-order quantifiers as well.

As long as we make sure that the structural rules permit a subset of the word order possibilities allowed by the first order variables, this strategy is correct.

Figure 2 shows the first-order labels assigned to the atomic formulas of our example sequent and -in light grey and black -the axiom links which are excluded using the first order constraints for L, which is justified given that we have a sequent which is derivable even in the non-associative Lambek calculus. In the figure, the numbers 0, 1, . . . correspond to constants referring to string positions, lower-case letters c, d, . . . to constants introduced by the par links and upper-case letters X, Y, . . . correspond to variables.

However, we can assign slightly more subtle first-order variables and constants. An example for the treatment of extraction is shown in Figure 3. Here, we simply use the solution of [START_REF] Moot | Linguistic applications of first order multiplicative linear logic[END_REF] for wh words. The first-order variables indicate that the word 'which', when it occurs between string positions 1 and 2, is looking for an n starting at some position X directly to its left and an s ending at position Y directly to its right. Inside this s we can use an np which can take up any position. The final result will then be an n between X (the leftmost position of the n argument) and Y (the rightmost position of the s argument). Note that we still need to add the appropriate structural rules to our grammar in order to derive medial extraction cases (see Moortgat, 1997, for a solution).

Given that we can check the first order constraints simply by unification of variables and constants, meaning O(1) per cell in the axiom matrix, the total complexity of the first-order constraints is O(n 2 ) for 2n atomic formulas.

The Unary Connectives

The unary connectives are a powerful addition to the multimodal Lambek calculus. They can be used to license structural rules but the relations between the logical formulas they induce can be used to encode linguistic features, as done, for example by [START_REF] Heylen | Types and Sorts: Resource Logic for Feature Checking[END_REF], or to restrict

I s np which n n X, Y X, 1 2, Y Z, Z FIGURE 3 First order variables for 'which' ⊢ ⊢ ⊢ ⊢ ⊢ ⊢ ⊢ ⊢ 3322A 32A 3223A A 2332A 23A 2233A FIGURE 4
Derivability relations using the unary logical rules scope possibilities, as done, for example by [START_REF] Bernardi | Generalized quantifiers in declarative and interrogative sentences[END_REF].

In certain cases, we use the unary modalities just for the derivability relations between the different types. Figure 4 summarizes the different relations between unary prefixes of up to four. Note that 3232A and 2323A are not displayed, given that they are equivalent to 32A and 23A respectively 1 .

By extending the unary prefixes further we can generate an intricate hierarchy of formulas, but for many applications the seven formula recipes in Figure 4 suffice. However, even for the formulas we've shown here it's not directly clear which pairs of them are derivable.

Fortunately, there is a simply way to check the contractibility of a sequence of unary formulas. First, we convert this sequence to a string as follows (with ǫ being the empty string and . the concatenation operation) Definition 1 Let A and B be two formulas which are the identical up 1 Technically the graph of Figure 4 is the transitive reduction of the derivability relation where all equivalent formulas (which would correspond to cycles in the unreduced graph) have been replaced by their smallest element.

to their unary prefixes. σ(A ⊢ B), the string corresponding to A ⊢ B, is defined as A -. B + , where the positive and negative formula are translated as follows.

3B + = B + .m 3A -= l. A - 2B + = B + .r 2A -= m. A - B + = ǫ otherwise A -= ǫ otherwise
The easiest way to see the correspondence between a sequence of unary modes and a string is by turning a page with a formula unfolding 90 degrees to the right and realizing that every arrow pointing left will produce an l, while every arrow pointing right will produce an r. Now, given that we have produced a string corresponding to the two sequences of unary connectives, we can check contractibility of these unary modes using the following context free grammar.

S → ǫ (1) | l S m S (2) | m S r S (3)
Rule (1) corresponds to the fact that it is possible not to have any unary connectives in front of a formula at all. Rule (2) corresponds to the 3 contraction and rule (3) to the 2 contraction.

Proposition 1 A ⊢ B contracts to a single vertex using the unary contractions iff S → σ(A ⊢ B).

Proof (sketch) ⇒ Induction on the number of contractions c. If c = 0 we use rule (1). If c > 0 there we look at the point where the first link is contracted. In order for this contraction to be valid the links between the two contracted links need to contract to a single node and in order for the entire sequence to contract everything after the second link needs to contract to a single node as well. Induction hypothesis allows us to combine these smaller proof nets using either rule ( 2 correspond to mlmrrm is underivable simply because we cannot match the final m: there is no r to its right and if we would match it to the single l we would need to derive mrr, the symbols in between, but this is impossible given that it has an odd number of symbols.

The context free grammar is easily extended to the multimodal case, simply by adding different symbols l i , m i and r i to the grammar and adding two new grammar rules for each of the new symbols.

There are limitations to using this system, however. First of all, it requires us to remove all unary branches from the final tree, though we could overcome this limitation by adding the following rule S → m S to our grammar. Secondly, we cannot use this strategy if some of the structural rules for the unary modes we're interested in are incompatible with the formula to string translation. Examples would be any inclusion rules between unary modes (though adding grammar rules would again be an option here) or structural rules which move unary modes up or down the tree, like the K, K1 and K2 structural rules of [START_REF] Moortgat | Categorial type logics[END_REF], which would require changing the translation function.

Given that parsing a context free grammar is O(n 3 ) and we would have to perform this calculation for all n 2 possible axiom links, the total O(n 5 ) complexity is somewhat high. So for grammars which use the unary connectives extensively, it can be beneficial to pre-compute the relations between all sequences of unary connectives occurring in the grammar, after which we can do a simple table lookup to see if contraction is possible. This would reduce the total complexity to O(n 2 ).

Régin's Algorithm

Even with all the previous constraints on axiom links in place, we sometimes fail to exclude some axiom links which cannot belong to a total matching. This is in part because an axiom link is regarded more or less in isolation, meaning that we don't exploit the fact the we need to find a total matching. [START_REF] Régin | A filtering algorithm for constraints of difference in CSPs[END_REF] proposes an algorithm for the slightly more general problem of finding solutions for 'all different' constraints in constraint logic programming. His algorithm separates the possible axiom links (in our case) into three categories: those which must be a part of any linking, those who are only part of some linkings and those which do not belong to any linking.

As an trivial example of Régin's algorithm, it would reduce a graph as shown in Figure 5 on the left (which we would obtain using the

np 1 np 2 np 3 np 4 np 5 np 6 np 1 np 2 np 3 np 4 np 5 np 6 FIGURE 5
A trivial application of Régins algorithm acyclicity and connectedness constraint after linking both s formulas of Figure 2) to the more logical structure on the right, simply because the unique solution left for np 6 would prevent np 1 from being used for any other axiom links.

Even though a smart axiom linking strategy (like always linking the atomic formula with the least possibilities first) would not benefit a lot from the reduction in this example, there are cases where it will exploit information like the absence of a total matching to fail directly.

The total complexity for Régin's algorithm is O(s 2 d 2 ) where s is the number of source nodes and d is the number of destination nodes. Given that in our application both of these are n (for 2n atomic formulas), the complexity will be O(n 4 ) which means the total complexity for filtering all constraints is O(n 4 ) as well.

Evaluation

In order to evaluate the combined filtering strategies, we have tested the axiom constraints on randomly generated derivable statements of the Lambek calculus. These statements have been generated using the inductive definition of Lambek calculus proof nets where all duplicate statements have been removed. To make the task as difficult as possible, only a single atomic formula a without unary prefixes has been used. Unfortunately, underivable statements don't have such an easy inductive characterization.

Figure 6 shows the amount of statements by the number of atomic formulas per sequent in the sample set, as well as the number of sequents by the number of connectives.

Out of 15.946 possible planar axiom links and 61.524 total possible axiom links, 2.546 correspond to different proofs. Therefore, there are 13.400 planar axioms links and 58.978 total axiom links which do not belong to any proof. Of these, the combined filtering algorithm excludes all but 279, for a total of 2.825 axiom links performed.

This means we eliminated 97.92% of the incorrect planar axiom links and 99.53% of the total number of incorrect axiom links. The distribution of the total number of atomic formulas and the total number of connectives in the randomly generated derivable statements perspective of the correct axiom links, we perform only 10.96% more links than a 'perfect' linking strategy -which through some unknown method would only find links corresponding to proofs in an NP complete logic.

Conclusions and Future Work

We have seen that in spite of the computational complexity of computing all axiom links for a given statement, a combination of constraints on the possible axiom links can reduce the total number of axiom links to just a bit over the optimal number of axiom links to be performed. Some important questions remain unresolved. For example, are there conditions where the filtered axiom links correspond exactly to the axiom links which belong to a proof net? This would mean that after the filtering algorithm has done its job, the resulting axiom matrix would contain all and only those links which would be used for a proof net. In that case, the axiom possibilities would form a sort of shared representation of all proofs for a statement and moreover, it would be computed in O(n 4 ) time. However, analyzing the incorrect axiom links of our experiment doesn't seem to give an easily identifiable handle on the subclasses of multimodal categorial grammar which would have this property.

Another interesting line of research would be to evaluate the current algorithms against a large corpus of categorial grammar sentences, such as those of [START_REF] Hockenmaier | Data and Models for Statistical Parsing with Combinatory Categorial Grammar[END_REF] and [START_REF] Moot | Automated extraction of type-logical supertags from the spoken dutch corpus[END_REF] and see how well the proposed linking strategy scales up to real-world applications.

  ) or (3). ⇐ Induction on the length of the CFG derivation. 2 To give an illustration of how to use the context free grammar, we show how the derivable sequent 3223A ⊢ 23A translates to lmmlmr, which we can derive as shown below. S → l S m S → l m S → l m m S r S → l m m S r → l m m l S m S r → l m m l m S r → l m m l m r We can show the inverse statement 23A ⊢ 3223A which would Filtering Axiom Links for Proof Nets / 9 June 29, 2007

  FIGURE6 The distribution of the total number of atomic formulas and the total number of connectives in the randomly generated derivable statements

June 29, 2007


Richard Moot

Type-Logical and Hyperedge Replacement Grammars Draft

CHAPTER 1 INTRODUCTION

Type-logical grammars [START_REF] Moortgat | Categorial type logics[END_REF][START_REF] Morrill | Type Logical Grammar: Categorial Logic of Signs[END_REF]) are a family of logical calculi -with, as the name suggests, a strong relation to the theory of types -for natural language analysis and natural language semantics. Type-logical grammars were introduced by [START_REF] Lambek | The mathematics of sentence structure[END_REF], who extends the work of [START_REF] Ajdukiewicz | Die syntaktische Konnexität[END_REF] and [START_REF] Bar-Hillel | Language and Information. Selected Essays on their Theory and Application[END_REF] -which have only elimination rules -by adding the corresponding introduction rules and giving cut-elimination and decidability proofs. The addition of the introduction rules, besides being desirable from a logical point of view has descriptive advantages as well, permitting a treatment of wh extraction (at least in peripheral cases) and quantifier scope ambiguities (again with some limitations).

Given that it has long been suspected that Lambek grammars generate only context-free grammars -though this was proved only in [START_REF] Pentus | Product-free Lambek calculus and context-free grammars[END_REF]) -different extensions to the Lambek calculus have been proposed in the literature, notably to deal with linguistic phenomena for which no satisfactory Lambek calculus treatment exists, such as medial extraction or the crossing dependencies of Dutch subordinate clauses. These additions are the use of modes to distinguish different modes of composition each with their own family of connectives. The addition of structural rules to allow more flexibe compisition of categories and the addition of unary control operators. The resulting logic takes the non-associative Lambek calculus NL as a base, adds modes and unary control operators and a set of structural rules R, a small set of structural rules fixed for a grammar. The resulting logic is called NL3 R , or, when R = ∅, just NL3.

Relatively little is known about the exact class of languages generated by NL3 R . [START_REF] Moot | Proof Nets for Linguistic Analysis[END_REF] shows that when we disallow structural rules to increase the total number of unary connectives then NL3 R generates exactly the contextsensitive languages, which implies that the decision problem for NL3 R is PSPACE complete. It is also known that NL3 generates exactly the contextfree languages and polynomial algorithms are known in this case [START_REF] De Groote | The non-associative Lambek calculus with product in polynomial time[END_REF][START_REF] Capelletti | Parsing with Structure-Preserving Categorial Grammars[END_REF]. While these results establish interesting upper and lower bounds, we would like to find fragments of NL3 R which generate a bit more than just the context-free languages, though less than the full class of contextsensitive languages while maintaining a polynomial time parsable formalism. The class of mildly context-sensitive grammar formalisms appears to be a good compromise between parsing complexity and language classes generated.

In order to indentify mildly context-sensitive and polynomially parsable fragments of NL3 R , we will related two classes of (hyper-)graph languages: hyperedge replacement grammars and proof nets a graph-like representation of proofs in NL3 R .

Hyperedge replacement grammars (introduced in Chapter 2) are a type of context-free graph grammar where we replace a hyperedge by a hypergraph [START_REF] Engelfriet | Context-free graph grammars[END_REF]. Hyperedge replacement grammars have been well-studied in the context of theoretical computer science and many results about the classes of string languages, tree languages and graph languages generated are known [START_REF] Engelfriet | Context-free graph grammars[END_REF], Drewes, Habel & Kreowski 1997, both give good overviews of many of the results for hyperedge replacement grammars).

Proof nets (introduced in Chapter 3) are a graph-like presentation which has several advantages over the other calculi. They are redundancy-free, in the sense that different proof nets correspond to different lambda-term semantics, much like natural deduction for the (→, ∧) fragment of intuitionistic logic. In addition, they have been shown to share some proporties with human sentence processing [START_REF] Morrill | Incremental processing and acceptability[END_REF][START_REF] Johnson | Proof nets and the complexity of processing centerembedded constructions[END_REF].

In Chapter 4, I will relate hyperedge replacement grammars to type-logical proof nets. In particular, I will give hyperedge replacement grammars for several different, commonly used but restricted, Lambek calculi, NL3, NL3 R (for several instances of R) and LG and show that for each of these systems there is a strongly equivalent hyperedge replacement grammar.

This has several important consequences: first of all it gives a characterization of the tree languages generated by type-logical grammars, which is exactly the class of tree languages generated by tree adjoining grammars. Secondly, it gives us new polynomial parsing algorithms for several restricted fragments of type-logical grammars and opens the door for the treatment other fragments.

CHAPTER 2 HYPEREDGE REPLACEMENT GRAMMARS

Hypergraphs

A hypergraph generalises the notion of graph by allowing the edges, called hyperedges, to connect not just two but any number of nodes. Hypergraphs will de the data structure used both for type-logical proof nets and for hyperedge replacment grammars. There are slight differences between authors on the definition of hypergraphs. In the current paper, I will follow [START_REF] Engelfriet | Context-free graph grammars[END_REF], but use σ instead of Σ for the alphabet of selectors, reserving Σ for the alphabet of non-terminal word labels later.

Definition 2.1 Let Γ be an alphabet of edge labels and let σ be an alphabet of selectors. A hypergraph over Γ and σ is a tuple V, E, lab, nod, ext , where V is the finite set of vertices, E is the finite set of hyperedges disjoint with V , lab is the labeling function, from E to Γ, assigning an edge label to each hyperedge, nod is the incidence function that associates with each edge e ∈ E a partial function nod(e) : σ → V , that is, it selects a vertex for every selector σ of the edge.

ext is the external function, a partial function from σ to V , that is, for every selector σ of the hypergraph it select a vertex.

Definition 2.2

The type of a hypergraph H is the domain of the external function, type(H) = dom(ext). The type of an edge e is the domain of the incidence fuction type(e) = dom(nod(e)).

• • • t t f i • p i o (i) (o) Figure 2.1: Hypergraph of a flowchart
To simplify the results and discussion which follow, we will assume that edge labels are (σ-)typed, that is to say that every edge e with label lab(e) will always appear with the same set of selectors.

The external nodes are special nodes in the graph which are identified by the selectors. Their goal is to define the embedding mechanism of hyperedge replacement grammars, where we will replace a hyperedge of a certain type by a hypergraph of the same type. [START_REF] Habel | May we introduce to you: Hyperedge replacement[END_REF], Figure 2.1 gives a hypergraph representing the flowchart of a very simple program. The selector alphabet σ has member i (input), o (output), t (true) and f (false). The complete hypergraph has one input, the external vertex labeled (i) and one output, the external vertex labeled (o). The hyperedge t is of type {i, t, f }. It represents a boolean test with a false branch exiting this piece of code immediately and a true branch executing a basic program p (of type {i, o}) then returning to the boolean test. As should be clear from the intended meaning of this hypergraph, it is an abstract representation of a while loop.

Example 2.3 As an example, inspired by

Hyperedge Replacement

The operation of hyperedge replacement replaces a hyperedge by a hypergraph H of the same type. Basically, we delete the hyperedge then add a (disjoint copy of) H and finally we identify each external node of H with the node adjacent to the same selector of the deleted hyperedge. Formally, this is defined as follows.

Definition 2.4 Let H and K be two disjoint hypergraphs with the same set of edge labels Γ and the same set of selectors σ. Let e be an edge of H such that type(e) = type(K). The hyperedge replacement of e by G, H[e := G] = V, E, lab, nod, ext is defined as follows.

V = V H ∪ V K E = (E H -e) ∪ E k • • • B t f i • p i o (i) (o) H • • • t 1 t f i • • • t 2 t f i (i) (t) (f ) K • • • t 1 t f i • • • t 2 t f i • p i o (i) (o)
H[e := K] It is well-known that hyperedge replacement is both confluent and associative [START_REF] Courcelle | An axiomatic definition of context-free rewriting and its application to NLC graph grammars[END_REF][START_REF] Lautemann | The complexity of graph languages generated by hyperedge replacement[END_REF]). Confluent in this context means that whenever we have a hypergraph H with two distinct hyperedges e 1 and e 2 then H[e

1 := K 1 ][e 2 := K 2 ] = H[e 2 := K 2 ][e 1 := K 1 ].
That is to say we can change the order of the replacement of two distinct hyperedges without changing the resulting hypergraph.

In this context, associative means that when we have a hyperedge e 1 of H and a hyperedge e

2 of K 1 , then H[e 1 := K 1 ][e 2 := K 2 ] = H[e 1 := K 1 [e 2 := K 2 ]].
That is to say we can perform a substitution ...

Hyperedge Replacement Grammars

Hyperedge replacement grammars were introduced by [START_REF] Bauderon | Graph expressions and graph rewritings[END_REF] and [START_REF] Habel | May we introduce to you: Hyperedge replacement[END_REF] and have been applied to ... [START_REF] Engelfriet | Context-free graph grammars[END_REF] gives an overview of hyperedge and node replacement grammars and several of the resuls obtained for them. Definition 2.6 A hyperedge replacement grammar (or HR grammar) is a tuple G = N, T, σ, P, S such that. T is the disjoint alphabet of terminal edge labels.

• • S o i → • • p n o i (i) (o) | • • S o i • • S o i (i) (o) | • • • B t f i • S i o (i) (o) | • • • B t f i • S i • S i • o o (i) (o)
σ is the alphabet of selectors.

P is the finite set of productions. The notation of derivation and of languages generated generalize easily from those of context-free string languages. Definition 2.8 Let G be a hyperedge replacement grammar and H a hypergraph. We say that G derives H iff there is a sequence S → . . . → H such that S is the start symbol of the grammar and every step in the derivation corresponds to a hyperedge replacement according to a production in P

• • • B i t f → • • • t n i t f (i) (t) (f ) | • • • B t f i • • • B t f i (i) (t) (f ) | • • • B t f i • • • B t f i (i) (t) (f )
Figure 2.4: Hyperedge replacement grammar for flowcharts -booleans Definition 2.9 Let G be a hyperedge replacement grammar. The language generate by G is the set of hypergraphs without hyperedges labeled by nonterminal edge labels derivable from S.

Basic Results for Hyperedge Replacement Grammars

As attested by the aforementioned overviews [START_REF] Engelfriet | Context-free graph grammars[END_REF][START_REF] Drewes | Hyperedge replacement graph grammars[END_REF], hyperedge replacement grammars have are an area of active research with many results. In this section, I will provide an admittedly ecclectic selection of results which will prove useful later.

Definition 2.10 The rank of a terminal or nonterminal symbol is the number of its tentacles.

The rank of a hyperedge replacement grammar is the maximum rank of a nonterminal symbol in the grammar.

Given that each additional tentacle permits us to have access to an additional vertex in the hypergraph, it should come as no surprise that increasing the rank of a hyperedge replacement grammar increases the language generated by the grammar.

It will often be convenient to look at hyperedge replacement grammars where we require all tentacles to reach distinct vertices and where we require all external vertices to be distinct. This last condition corresponds to not allowing a nonterminal to rewrite to the empty string in context-free string grammars.

Definition 2.11 Let g be a hyperedge replacement grammar and H the right hand side of a rule in g.

• g is loop-free iff for every nonterminal e of every right hand side H of a rules in g and for all s 1 , s 2 ∈ type(e) whenever nod H (e, s 1 ) = nod H (e, s 2 ) then s 1 = s 2 .

• g is identification-free iff for every right hand side H of a rule in g and for all s 1 , s 2 ∈ type(H) whenever ext H (s 1 ) = ext H (s 2 ) then s 1 = s 2 .

Lemma 2.12 ((Engelfriet & Heyker 1992)) For every hyperedge replacement grammar g there is a hyperedge replacement grammar g ′ which is loop-free and identificationfree and which generates the language L(g ′ ) = {H ∈ L(g)|His identification-free.

I will not consider loops in the current paper and therefore make the quiet assumption that all tentacles with different labels will reach different nodes. However, it is sometimes convenient to allow rules in our grammar to identify nodes. Even though by Lemma 2.12 they can be removed from the hyperedge replacement grammars I propose -and for parsing the hyperedge replacement grammars in this article it is generally necessary that they are -in the interest of keeping the grammars as compact as possible, I will use hyperedge replacement rules which identify nodes.

CHAPTER 3 PROOF NETS FOR TYPE-LOGICAL GRAMMARS

Proof nets are a way of representing proofs in linear logic introduced by [START_REF] Girard | Linear logic[END_REF]. Proof nets naturally factor out the 'bureaucratic' rule permutations which are possible in the sequent calculus and natural deduction formulations of linear logic.

Proof nets are usually described in three steps: first, we start with a more general set of structures which includes all provable statements but also some non-provable statements. These structures are proof structures. For the second step, we 'forget' about a lot of the information of the proof structures. For example, for the Danos-Regnier switching criterion [START_REF] Danos | The structure of multiplicatives[END_REF] we forget about the actual formulas in the proof structure and obtain just a set of graphs, the correction graphs. Similarly, we obtain abstract proof structures by forgetting about the internal formulas of a proof structure and by forgetting most of the names of the logical rules used. Finally, we state a correctness condition such that any proof structure of which the underlying abstract structure satisfies this condition is a proof net. For the Danos-Regnier criterion we verify that all correction graphs are acyclic and connected. For the type-logical proof nets, we use a contraction criterion in the style of [START_REF] Danos | La Logique Linéaire Appliquée à l'étude de Divers Processus de Normalisation (Principalement du λ-Calcul)[END_REF].

For the description of proof nets in the current chapter, I follow [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF] but define the proof structures in terms of hypergraphs to make the equivalence proof with hyperedge replacement grammars simpler.

Proof Structures

Definition 3.1 A proof structure P is a tuple H, V, A, frm, pre, con such that H is a hypergraphwith selectors σ = {s1, s2, t}1 and edge labels.

h, c

of type {s1} a + , a - of type {s1} for all a ∈ A L3, R3, L2, R2 of type {s1, t} L/, R/, L•, R•, L\, R\ of type {s1, s2, t} and the empty set of external nodes.

V is the set of vertices in the hypergraph.

A is the set of atomic formulas. As shown above, each atomic formula a ∈ A induces a positive hyperedge a + as well as a negative hyperedge a -.

frm is a function from vertices to formulas such that for all v ∈ V , frm(v) is a member of the set of formulas F , such that the neighborhood of every hyperedge is of one of the forms shown in Figure 3.1.

con and pre are functions from edge labels Γ to lists of selectors, such that for an edge e with label lab(e) = l , pre(l) ∈ σ * . That is, the function pre returns is a list of selectors indicating the list of premisses of the edges with label l: if selector s is a member of pre(l), then for an edge e with this label, the vertex nod(e, s) is a premiss of the edge and if selector s 1 precedes selector s 2 in pre(l) then vertex nod(e, s 1 ) occurs to the left of vertex nod(e, s 2 ). The function con(l) is a list of selectors indicating the list of conclusions of the edge.

For every edge label l of type t, pre(l) and con(l) partition the set t into two disjoint subsets: every member of t occurs exactly once in either pre(l) or con(l).

Every vertex is incident to exactly two hyperedges: once as a premiss and once as a conclusion.

Table 3.1 shows the value of the premisses and the conclusions for the different link types. Remark the following:

• In Figure 3.1 the premisses are drawn from left to right above the edge whereas the conclusions are drawn from left to right below it. Note, however, than only the labels are important and that sometimes it will be convenient when drawing a graph to abandon this convention.

• The left and right link of a connective are inverse to eachother with respect to premisses and conclusions, that is to say for any connective c we have pre(Lc) = con(Rc) and con(Lc) = pre(Rc). These are the symmetries of our logical calculus.

All vertices which are incident to an h edge are called the hypotheses of the proof structure. All vertices which are incident to a c edge are called the conclusions of the proof structure.

There are few graphical and notational differences with the proof structures of Moot & Puite. I will discuss each of them in turn.

I use special h and c hyperedges to indicate the hypotheses and conclu-

sions of the proof structure. This makes our proof structures more regular in that every formula is now the premiss exactly one link and the conclusion of exactly one link.

target selector and arrow leaving it, which is the way the links are presented in [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF])

A/B B A • • • L/ t s2 s1 A B A • B • • • R• s1 s2 t B\A B A • • • L\ s1 t s2 2A A • • L2 s1 t 3A A • • R3 t s1 A/B B A • • • R/ t s2 s1 A B A • B • • • L• s1 s2 t B\A B A • • • R\ s1 t s2 2A A • • R2 t s1 3A A • • L3 s1 t Figure 3.1: Hyperedges for NL3 proof structures pre(h) =[] con(h) =[s1] pre(c) =[s1] con(c) =[] pre(L3) =[t] con(L3) =[s1] pre(R3)=[s1] con(R3)=[t] pre(L2) =[t] con(L2) =[s1] pre(R2)=[s1] con(R2)=[t] pre(L/) =[t, s2] con(L/) =[s1] pre(R/) =[s1] con(R/) =[t, s2] pre(L•) =[s1, s2] con(L•) =[t] pre(R•) =[t] con(R•) =[s1, s2] pre(L\) =[s1, t] con(L\) =[s2] pre(R\) =[s2] con(R\) =[s1, t]
Table 3.1: The functions pre and con for proof structures 2. I use explicit hyperedges corresponding to the positive and negative atomic formulas, the axiom/cut rule discussed below allows us to eliminate a postive and negative atomic hyperedge by identifying the vertices which are incident to the two links.

3. The list of premisses and list of conclusions of links are replaced by the functions pre and con.

4. The main formula of a link is the vertex which is reached by the t selector, the active formulas are the vertices reached by the s1 and s2 selectors. Definition 3.2 If a vertex is incident to two selectors ∈ {s1, s2}, we will call it an axiomatic vertex, if it is incident to one s and one t selector we will call it a flow vertex and if it is incident to two t selectors we will call it a cut vertex.

Proof nets for intuitionistic logic often use a notion of polarity to distinguish negative (antecedent) formulas from positive (succedent) formulas. It is possible to assign polarities to the vertices in proof structures here as well, but we need to keep in mind that axiom and cut formulas perform the role of both a positive and a negative formula. The way to see this is that an axiom is a negative formula with respect to the hyperedge of which it is a conclusion and a positive formula with respect to the hyperedge of which it is a premiss.

Figure 3.2 shows the different types of vertices. In all cases, the vertex is a conclusion of the hyperedge with the tentacle connecting it from above and a premiss of the hyperedge with the tentacle connecting it at the bottom.

The hyperedges corresponding to positive and negative atomic formulas are eliminated by means of the axiom or cut rule, shown in Figure 3.3. This rule allows us to connect two arbitrary formulas of opposite polarity; they need not be disjoint as suggested by the figure. The grey lines indicate a possibility for the axiom identifications, the result of which is the proof structure shown in Figure 3.5.

• h s1 • n - s1 book n • • • L\ s1 t s2 • • • L/ t s2 s1 • • • R/ t s2 s1 • • L3 s1 t • • L2 s1 t • h s1 • s + s1 • n + s1 • n - s1 • np - s1 which (n\n)/(s/32np) • h s1 • np - s1 Jim np • h s1 • np + s1 • np + s1 • s - s1 • • • L\ s1 t s2 • • • L/ t s2 s1 read (np\s)/np • n + s1 • c s1
In the example above, all identifications are of atomic formulas and they result in axiomatic vertices in the resulting proof structure. Connecting an axiomatic vertex with a flow vertex will simply result in a new flow vertex, whereas connective two flow vertices will result in a cut vertex. Given that the axiom hyperedges are of type {s1}, these are the only possibilities.

Though the cut vertices don't present any problems for the proof net calculus, they can be eliminated without problem giving a shorter conversion sequence to the final tensor tree [START_REF] Moot | Proof nets for the multimodal Lambek calculus[END_REF]. From the point of view of proof search, we therefore want to look at cut-free proof nets. Indeed, we can see that cut elimination is immediate for the cases where the axiom/cut rule produces an axiomatic or flow vertex, it corresponds simply to a composition of proofs similar to what we have in natural deduction.

Figure 3.5 shows an example of a proof structure corresponding to the sequent n, (n\n)/(s/32np), np, (np\s)/np ⊢ n on the left of the figure. The five axiomatic vertices in the proof structure have been circled. The only positive vertex, a premiss of the [R/] link by the t selector and a conclusion of the [L/] link by the s2 selector has a grey color. All other vertices are negative flow vertices. Remark that I have rotated the [R/] link, displaying the s2-selected vertex above the node label instead of below it, in spite of it being a conclusion of the link. Similarly, the s2-selected vertex of the topmost [L/] link is portray below the node label, even though it is a premiss of its link.

Abstract Proof Structures

An abstract proof structure erases some of the distinctions made by proof structures. For example, the different tensor links with the same number of tentacles are no longer distinguished and the formula function is no longer defined for all vertices but only for the hypotheses and conclusions of the structure.

We keep the different par links, but because the tensor links are now indistinguishable, we lose nearly all information about axiom, flow and cut vertices. Definition 3.5 An abstract proof structure is a tuple H, V, frm, pre, con such that H is a hypergraph with selectors {1, 2, 3} and edge labels

h, c of type {1} of type {1, 2} • of type {1, 2, 3} L3, R2 of type {1, 2} R/, L•, R\ of type {1, 2, 3}
such that every vertex is incident to exactly two hyperedges, once as a premiss and once as a conclusion. pre and con are the premiss and conclusion functions as before, but with the definitions for the edge labels of abstract proof structures as shown in Table 3.2.

The formula function frm is a partial function from edges to formulas. frm(e) is defined iff e is an h or c edge.

• • • L\ s1 t s2 • • • L/ t s2 s1 • • • R/ s1 s2 t • • • L\ s1 t s2 • • L3 t s1 • • • L/ s1 s2 t • • L2 t s1 • h s1 • h s1 • h s1 • h s1 • c s1 • • • • • • 1 2 3 • • • • 1 2 3 • • • R/ 3 2 1 • • • • 1 2 3 • • L3 2 1 • • • • 3 2 1 • • 1 2 • h 1 • h 1 • h 1 • h 1 • c 1 Figure 3.5:
An example proof structure and the corresponding abstract proof structure Definition 3.6 Let P be a proof structure. The abstract proof structure corresponding to P, A = aps(P) is defined as follows.

• V A = V P .

• E A = tr(E P ), where tr is the edge translation function shown in Figures 3.6 and 3.7.

• frm A = frm P (nod(e, s1)) for all e ∈ e P such that lab(e) = h or lab(e) = c and undefined in all other cases.

On the right of Figure 3.5 we see the conversion of the example proof structure into its abstract proof structure.

From the definition of the translation function it is clear that we can still recover some of the active and main vertices of an abstract proof structure: for

pre(h) =[] con(h) =[1] pre(c) =[1] con(c) =[] pre( ) =[1] con( ) =[2] pre(•) =[1, 2] con(•) =[3] pre(L3)=[1] con(L3)=[2] pre(R2)=[1] con(R2)=[2] pre(R/) =[3] con(R/) =[1, 2] pre(L•) =[3] con(L•) =[1, 2] pre(R\) =[3] con(R\) =[1, 2]
Table 3.2: The functions pre and con for abstract proof structures a R/ link, the main formula is the one incident to 1, for a R\ link it is incident to 2 and for a L• link it is incident to 3. Similary, the main formula of a R2 link is incident to 1 and the main formula of a L3 link is incident to 2.

Lemma 3.7 If P is a proof structure then A = aps(P) is an abstract proof structure.

Proof This is fairly trivial. It amounts to verifying is all cases that the incidence function reaches the same vertices with the renamed selector and that the hypotheses and conclusions of a hyperedge are the same list of vertices in each case. Since the translation is a simple renaming, this is trivial. The formula function frm has the required property of assigning a formula to all and only the h and c edges by construction.

2 Definition 3.8 A tensor tree T is an abstract proof structure containing only edges with labels h, c, and •.

Contractions and Structural Rules

For abstract proof structures, we define the contraction operation as follows.

The configurations we contract are shown in Figure 3.8: in all cases a tensor link and a par link are connected to eachother by all tentacles of the two links which have the same selector except one and the difference between the par links is the tentacle chosen to be 'external', that is, pointing to the top and bottom vertices in the Figure.

Definition 3.9 If a hypergraph H contains a subgraph of one of the forms shown in Figure 3.8, a contraction in one step is H → H ′ is obtained by deleting the two links as well as the vertices which are incident to both links, then identifing the two exterior vertices.

We will say H → * H ′ or H contracts to H ′ by taking the → * to be the reflexitive, transitive closure of →.

• • • • 1 2 3 → • • • R• s1 s2 t (1) (2) (3) | • • • L/ t s2 s1 (1) (2) (3) | • • • L\ s1 t s2 (1) (2)
(3)

• • 2 1 → • • R3 s1 t (1)
(2)

| • • L2 t s1 (1)
(2)

Figure 3.6: Converting a PS to an APS: tensor cases

• • • L• 1 2 3 → • • • L• s1 s2 t (1) (2)
(3)

• • • R\ 1 2 3 → • • • R\ s1 t s2 (1) (2)
(3)

• • • R/ 1 2 3 → • • • R/ t s1 s2 (1) (2)
(3)

• • L3 2 1 → • • L3 t s1 (1)
(2)

• • R2 2 1 → • • R2 s1 t (1)
(2) Proof Take H = E, v, frm, pre, con to be an abstract proof structure and e 1 and e 2 to be two hyperedges such that their neighbourhood is as shown in

• • • • 1 2 3 • • • L• 1 2 3 • • • R\ 1 3 2 • • • • 1 3 2 • • • R/ 3 2 1 • • • • 3 2 1 • • 2 1 • • L3 1 2 • • R2 1 2 • • 2 1 Figure 3
.8: Contractions for NL3 abstract proof structures Figure 3.8, with v 1 and v 2 being the two internal vertices and v h the vertex which is a hypothesis of its link -and therefore the conclusion of another link -and v c the vertex which is a conclusion of its link -and therefore the hypothesis of another link. To obtain H we delete hyperedges e 1 and e 2 and vertices v 1 and v 2 . Furthermore we identify the two nodes v c and v h , making it a vertex which is a conclusion of one link and a premiss of one link. Given that no hyperedges labeled h or c can disappear frm remains the same, whereas pre and con are the natural restriction of the same functions of H to the hyperedges of H ′ . 2

In addition to the contractions, which are a fixed component of all instantiations of NL3 R , a logic can specify a (finite and typically quite small) set of structural rules R. These structural rules rewrite a tensor tree into another tensor tree, with the requirement that both tensor trees have the same set of distinct leaves, though we are allowed to change the order of the leaves. I will present some structural rules which have been used very frequently in the literature on multimodal categorial grammars [START_REF] Moortgat | Logical parameters and linguistic variation. Lecture notes on categorial grammar[END_REF][START_REF] Moortgat | Adjacency, dependency and order[END_REF][START_REF] Moortgat | Categorial type logics[END_REF][START_REF] Moortgat | Constraints and Resources in Natural Language Syntax and Semantics[END_REF][START_REF] Vermaat | The Logic of Variation. A cross-linguistic account of whquestion formation[END_REF].

One of the first sets of structural rules used to extend the descriptive power of the non-associative Lambek calculus are the mixed associativity and mixed commutativity postulates. Figure 3.9 shows these postulates in their extraction formulation (the arrows pointing towards the central graph) as well as in their infixation formulation (the arrows pointing away from the central graph). In all cases, there is an interaction between a mode 0 and a mode 1 where the same

• • • • 0 1 2 3 • • • • 1 1 2 3 x y z v • • • • 1 1 2 3 • • • • 0 1 2 3 x y z v • • • • 0 1 2 3 • • • • 1 1 2 3 y x z v ← P 2 → P 1 → P 2 ′ ← P 1 ′ Figure 3
.9: Mixed associativity and mixed commutativity -left branch Another possibility for expressing controlled associativity and commutativty in a multimodal calculus is by using unary control. This time we have just a single binary mode interacting with a single unary mode. The unary mode marks the element which licenses the restructuring operations. In Figure 3.11 this is the element x (compare this figure with the version of these structural rules without unary control in Figure 3.9). There is again the possibility to specify these structural rules in the form of infixation and in the form of extraction rules.

• • • • 0 1 2 3 • • • • 1 1 2 3 x y z v • • • • 1 1 2 3 • • • • 0 1 2 3 x y z v • • • • 0 1 2 3 • • • • 1 1 2 3 y x z v ← P 4 → P 3 → P 4 ′ ← P 3 ′
Figure 3.12 displays a version of the right branch extraction and infixation rules of Figure 3.10 with unary control. In both cases the z node moves from one right branch to another. Definition 3.11 Let H be a hypergraph which is an abstract proof structure for some logic NL3 R with a set of structural rules R, a conversion in one step is • performing a contraction,

H → R H ′ • • • • 0 1 2 3 • • • • 0 1 2 3 • • 0 2 1 x y z v • • • • 0 1 2 3 • • • • 0 1 2 3 • • 0 2 1 x y z v • • • • 0 1 2 3 • • • • 0 1 2 3 y x z v • • 0 2 1 ← U2 → U1 → U2 ′ ← U1 ′
• • • • 0 1 2 3 • • • • 0 1 2 3 x y z v • • 0 2 1 • • • • 0 1 2 3 • • • • 0 1 2 3 x y z v • • 0 2 1 • • • • 0 1 2 3 • • • • 0 1 2 3 y x z v • • 0 2 1 ← U4 → U3 → U4 ′ ← U3 ′
• given a rule r ∈ R which is of the form T → T ′ such that T is a subgraph of H and H ′ is H with the subgraph T of H replaced by T ′ .

We will say

H → * R H ′ or H converts to H ′ by taking → * R to be the reflexitive, transitive closure of → R . Lemma 3.12 If H → R H ′ then H is an NL3 R abstract proof structure iff H ′ is an abstract proof structure.
Proof This is a trivial extension of the previous lemma. For every structural rule, the internal nodes are a premiss and a conclusion of a link, as required. For the external nodes: the leaves which are premisses of the links of the structural rule on both the left hand side and the right hand side of the rule and therefore all the conclusion of some other link. Given structural rules preserve the leaves, the situation doesn't change from left hand side to the right hand side of a rule of vice verse. For the conclusion, we can make the same argument. It is a conclusion of a link in the structural rule and therefore a hypothesis of another link in the abstract proof structure before a structural conversion iff it is the hypothesis of this same link after the structural conversion. 2

The Lambek-Grishin Calculus

The Lambek-Grishin calculus LG was introduced by [START_REF] Grishin | On a generalization of the Ajdukiewics-Lambek system[END_REF]. It adds symmetric connectives to the Lambek calculus: reversing the left hand and right hand side of the turnstile, or, in our proof net case, adding up-down symmetric connectives, which turn each premiss into a conclusion and each conclusion into a premiss. In addition, Grishin explores the possible interaction principles between the connectives. [START_REF] Bernardi | Continuation semantics for symmetric categorial grammar[END_REF] explore the possiblities of using the Lambek-Grishin calculus, giving an analysis of quantifier scope using Grishin's interaction principles and an interpretation of the scope possiblities in terms of continuation semantics. Grishin has proposed a number of interaction principles for LG divided into four classes. Class I and class IV will interest us here since they concern the interaction between a Lambek connector '•' and an inverse Grishin connector ';'.

Figures 3.14 and 3.15 show all structural rules in Grishin classes I and IV. The inward pointing arrows, with the primed rule names, correspond to the structural rules of class I, whereas the outward pointing arrows correspond to the structural rules of class IV.

Let me take a moment to point out the similarity between Figure 3.14 and Figure 3.9 and between Figure 3.15 and Figure 3.10. Apart from the fact that v is a conclusion of the rule in Figure 3.14 and that x is a hypothesis of the rule in Figure 3.9 the two figures display the same configuration up to a relabeling of the selectors and hyperedges. The easiest way to see this is to rotate the ';' hyperedge to the right in such a way that v is displayed at the top of the hyperedge.

Similarly, in Figure 3.15, when we abstract away of the fact that one vertex

• • • • 1 2 3 • • • L• 1 2 3 • • • R\ 1 3 2 • • • • 1 3 2 • • • R/ 3 2 1 • • • • 3 2 1 • • • R⊙ 1 2 3 • • • ; 1 2 3 • • • ; 1 3 2 • • • L 1 3 2 • • • ; 3 2 1 • • • L⊘ 3 2 1 Figure 3.13: Contractions for LG abstract proof structures • • • • 1 2 3 • • • ; 1 2 3 y z v w • • • ; 1 2 3 • • • • 1 2 3 y z v w • • • • 1 2 3 • • • ; 1 2 3 v z y w ← Gr2 ′ → Gr1 ′ → Gr2 ← Gr1
Figure 3.14: Mixed associativity and mixed commutativity -Lambek-Grishin, left branch is a hypothesis and the other a conclusion, w plays the role of z in Figure 3.10 and a rotation of the ';' hyperedge -to the left this time -again gives an isomorphism of the graphs up to a relabeling of the hyperedges and selectors labels.

• • • • 1 2 3 • • • ; 1 2 3 x y v w • • • ; 1 2 3 • • • • 1 2 3 x y v w • • • • 1 2 3 • • • ; 1 2 3 x y w v ← Gr4 ′ → Gr3 ′ → Gr4 ← Gr3

Proof Nets

We are now in a position to define proof nets. For NL3 a proof net is simply a proof structure where we can convert its abstract proof structure to a tensor tree, that is to say we eliminate all par rules (labeled

[R\], [L•], [R/], [R2] and [L3]
) and the resulting structure is a tree with the leaves labeled by h edges and the root by a c edge. Theorem 3.13 (Moot & Puite) An proof structure S for NL3 is a proof net if and only if its underlying abstract proof structure contracts to a tensor tree.

The result extends naturally when we add any set R of structural rules to NL3 to obtain NL3 R . A structural rule in this context is a rewrite of one tensor tree with n distinct hypotheses as its leaves into another tensor tree with the same n distinct leaves, though not necessarily in the same order. Theorem 3.14 (Moot & Puite) An proof structure S for NL3 R is a proof net if and only if its underlying abstract proof structure converts to a tensor tree using the contractions and the structural rules in R.

Finally, moving to LG not a lot changes. The only change is that interaction principles proposed by Grishin are defined on structures having two conclusions in addition to two hypotheses. Theorem 3.15 (Moot) An proof structure S for LG is a proof net if and only if its underlying abstract proof structure converts to a tensor tree using the contractions and any subset of the Grishin interaction principles.

• • • • 1 2 3 • • • • 1 2 3 • • • R/ 3 2 1 • • L3 2 1 • h 1 • h 1 • h 1 • h 1 • c 1 • • 1 2 • • • • 1 2 3 • • • • 3 2 1 • • • • 1 2 3 • • • • 1 2 3 • • • R/ 3 2 1 • • L3 2 1 • h 1 • h 1 • h 1 • h 1 • c 1 • • 1 2 • • • • 1 2 3 • • • • 3 2 1 Figure 3
.16: Applying a structural conversion to the abstract proof structure of Figure 3.5.

Example 3.16

Everything is now in place to show that the proof structure shown in Figure 3.5 is a proof net, given that we have the structural rules for right branch extraction with unary control shown in Figure 3.12. Figure 3.16 shows the abstract proof structure of Figure 3.5 on the left. There are two possibilities here: either we perform the [L3] contraction -in which case we have a dead end where neither structural rules nor contractions apply -or we perform the single structural rule which is possible in this configuration, moving the unary branch out as shown on the right of Figure 3.16.

To convince yourself that the part of Figure 3.16 marked in gray is just Figure 3.12,

• • • • 1 2 3 • • • • 1 2 3 • • • R/ 3 2 1 • • • • 1 2 3 • • • • 3 2 1 • h 1 • h 1 • h 1 • h 1 • c 1 • • 1 2 • • L3 2 1 • • • • 1 2 3 • • • • 1 2 3 • • • R/ 3 2 1 • • • • 1 2 3 • • • • 3 2 1 • h 1 • h 1 • h 1 • h 1 • c 1 • Figure 3
.17: Applying an L3 contraction to the abstract proof structure of Figure 3.16.

remark that only the selector labels and the nodes connected to the rest of the graph are important. Figure 3.16 has turned the selector 2 of the top '•' node has downward and has inversed the ' ' node, but the gray subgraph on the left is still isomorphic to the graph on the left of Figure 3.12 wheres the gray subgraph on the right is isomorphic to the graph in the middle of Figure 3.12. Figure 3.17 shows repeats the result of the structural conversion at the left. Now the are no other possibilities for applying structural rules since only the extraction structural rules are available. In terms of the contractions, the redex for the [L3] contraction is marked in gray on the left of the figure and it contracts to the single

• • • • 1 2 3 • • • • 1 2 3 • • • • 1 2 3 • h 1 • h 1 • h 1 • h 1 • c 1 • • • R/ 3 2 1 • • • • 3 2 1 • • • • 1 2 3 • • • • 1 2 3 • • • • 1 2 3 • h 1 • h 1 • h 1 • h 1 • c 1 • Figure

Type-logical Grammars

We now have everything in place to define type-logical grammars and the tree and string languages generated by them. In essence, as shown by the following definition, it corresponds to the simple addition of a lexicon to either an instance of NL3 R or an instance of LG. Definition 3.17 A type-logical grammar G is a tuple Σ, A, C, lex, R, S such that.

Σ is the alphabet of non-terminal symbols,

A is a finite set of atomic formulas, C is a set of logical connectives each with an arity, lex is a function from Σ to ℘(F ), that is from non-terminals to sets of formulas. We will assume without loss of generality that lex never assigns the empty set to a member of Σ.

R is a finite set of structural rules.

S ∈ F is a special formula, call the start formula or the goal formula.

The definition above is deliberately vague about the connectives. Moot (2007) lists the possibilities, but for the moment we will only consider the following two instantiations.

• the multimodal categorial grammar vocabulary, consisting of binary connectives {/ i , • i , \ i } for members i of a finite set of binary modes I together with unary connectives {3 j , 2 j } for members j of a finite set of unary modes J.

• the Lambek-Grishin vocabulary consisting of the Lambek connectives {/, •, \} and the Grishin connectives {⊘, ⊙, }.

For the structural rules R, I will only consider subsets of the rules discussed in Section 3.3 for the multimodal vocabulary and I will only consider subsets of the structural rules dicussed in Section 3.4 for the Lambek-Grishin calculus.

Example 3.18 Given a single unary and a single binary mode, the set of structural rules U 3 and U 4 for their combination, the lexical assignments shown in Figure 3.4 and goal formula n we have a (minimal) type-logical grammar G wh for wh extraction in English. Definition 3.19 Given a type-logical grammar G and a sequence of words w 1 , . . . , w n , such that w i ∈ Σ and n > 0, we say that G → w 1 , . . . , w n iff A 1 , . . . , A n ⊢ S where for each i, A i ∈ lex(w i ).

Definition 3.20 Let G be a type-logical grammar. The string language generated by G is the set of sequences of words such that G → w 1 , . . . , w n . The tree language generated by G is the set of tensor trees T such that for each t ∈ T , G ⊢ t.

Analysis of the Structural Rules

The structural rules allow us to rewrite a tensor tree into a tensor tree with the same external nodes. Even with the condition posed in [START_REF] Moot | Proof Nets for Linguistic Analysis[END_REF]) -that the number of unary tensor links on the right hand side of a tensor rules is equal to or less than the number of unary tensr links on the left hand side of a rulethis gives us extactly the context-sensitive languages and a PSPACE decision problem.

As we have seen in Section 2.3, hyperedge replacement grammars are context free graph grammars [START_REF] Engelfriet | Context-free graph grammars[END_REF]): while the right hand side of a rule can be any complex graph of the right type, the left hand side is always a single nonterminal hyperedge. The structural rules, on the other hand, have (typically non-trivial) trees on the left hand side of the rule. In this section we will investigate some very frequently used structural rules and ways to characterize the proof nets generated by using them in a context-free way. Now, let's analyse the combinatorial possibilities of the combinations of the structural rules of Sections 3.3 and 3.4. Some combinations are know to have undesirable side-effects, such as collapse to an associative, commutative system but we will eliminate these combinations after discussing the total combinatorics. We will end up with a number of restrictions on the final grammar permitting us to describe the generated proof nets as a hyperedge replacement grammar while factoring out the structural rules.

The basic assumption we make in this analysis is that the final tensor trees in the grammar have a certain form: in particular, for the multimodal structural rules of Figures 3.9 and 3.10 we assume that mode 1 is grammar-internal and that no hyperedges labeled • 1 occur in the final tensor tree. All ternary hyperedges in the final tensor tree are labeled • 0 using the external mode 0 (we can extend this by adding other external modes without problem, requiring only that such additional modes do not interact with either mode 0 or mode 1).

We deploy a similar restriction to the structural rules with unary control, requiring that all unary branches are eliminated from the final tree and to the structural rules of the Lambek-Grishin calculus, requiring that all Grishin connectives ; are eleminated. Definition 3.21 Given a structural rule r with connectives c 1 , . . . , c n on the left hand side and connectives d 1 , . . . , d n on the right hand side a trace is a bijection associating each element c i with an element of d j . Definition 3.22 Let P be a proof structure, A its corresponding abstract proof structure and ρ be a conversion sequence coverting A. For a hyperedge e of P the trace of e in ρ is defined as the prefix of ρ such that:

• ... Definition 3.23 Let P be a proof net. It is well-bracketed iff there are no two contractions c 1 and c 2 in the conversion sequence of A such that such that on any of the paths between the two traces t 1a and t 1b of c 1 there is just one of the traces of c 2 .

Intuitively, the combination of well-bracketedness and traces guarantee that every path in a proof net can be described by a context free grammar, in much the same way as this is possible for several mildly context-sensitive grammar formalisms (Vijay-Shanker, Weir & Joshi 1987). Lemma 3.24 Any NL3 proof net is well-bracketed. Proof Looking backwards at a conversion sequence ending in a tensor tree, we see that every contraction corresponds to expanding a single vertex into two adjacent hyperedges with the empty path between their traces. All we need to verify is that whenever we apply such an expension the (output) result abstract proof structure is well-bracketed whenever the input was.

• • • • 0 1 2 3 • • • • 1 1 2 3 • L• 1 3 • L• 0 3 1 2 1 2 → • • • • 1 1 2 3 • • • • 0 1 2 3 • • • L• 0 1 2 3 • L• 1 3 1 2
Suppose we have such a well-bracketed input and we apply an expansion. This operation has the effect that all paths passing through the vertex of the input which is expanded will be extended in the output graph, but extended in such a way all paths necessarily pass through both traces of the new hyperedges.

2

Unfortunately, Lemma 3.24 doesn't extend in general to logics with structural rules. Figure 3.19 shows a non-wellbracketed proof net on the left, which we can contract after application of a mixed commutativity rule as shown on the right of the figure.

The configuration shown in Figure 3.19 can easily be adapted to the other binary par links and to the other sets of mixed associativity and mixed commutativity structural rules: those with unary control and the Lambek-Grishin interactions.

In order to provide conditions under which well-bracketing of the contractions can be guaranteed, I will introduce the notion of an inert mode. Definition 3.25 Given a grammar G with a set of structural rules R, a mode m is inert with respect to this grammar and these structural rules if we can appy all its contraction before applying any structural rules.

Proof Nets for Type-logical Grammars

In other words, a mode is inert Definition 3.26 Given a grammar G with a set of modes M a grammar can select a subset E of M the member of which are called the external modes. All other modes are called internal.

The distinction between external and internal modes is implicit in the work of many authors. A typical use of grammar-internal modes is feature-checking, where a unary branch of a certain mode -for example n for nominative case -is introduced. Proposition 3.27 Let P be a proof net. The internal modes of P occur only in pairs of par and tensor links.

Proof This is a direct consequence of the fact the internal modes are not allowed to occur on the final tensor tree and that contractions eliminate a tensor and a par link at the same time.

2

As already suggested by the description I gave of the structural rules in Lemma 3.28 An NL3 R or LG grammar G is well-bracketed if

• all its external modes are inert,

• the structural rules are a subset of one of the following sets

-{P 1, P 2, P 3, P 4} -{P 1 ′ , P 2 ′ } -{P 3 ′ , P 4 ′ } -{Gr1, Gr2, Gr3, Gr4} -{Gr1 ′ , Gr2 ′ } -{Gr3 ′ , Gr4 ′ } • • • • 1 1 2 3 • • • L• 1 1 2 3 P3 ′ | P4 ′ P1 ′ | P2 ′ • • • R\ 1 1 3 2 • • • • 1 1 3 2 P1 | P2 • • • R/ 1 3 2 1 • • • • 1 3 2 1 P3 | P4 Figure 3.20: Generalised contractions for NL3 R abstract proof structures • • • R\ 0 1 3 2 • • • • 0 1 3 2 • • L3 2 1 • • 0 1 2 U1 | U2 • • • R/ 0 3 2 1 • • • • 0 3 2 1 • • L3 2 1 • • 0 1 2 U3 | U4 Figure 3
.21: Generalised contractions for NL3 R abstract proof structures with unary control Given that the data structures used for proof structures and abstract proof structures are both hypergraphs, it makes sense to try to provide hyperedge replacement grammars for both. I will do this in steps, adding more details at each step until the at final result we have a hyperedge replacement grammar for type-logical grammars. As a first step, Section 4.1 presents a hyperedge replacement grammar for abstract proof nets, that is, abstract proof structures which contract to a tensor tree. The second step adds the rules fof converting an abstract proof structure to a proof structures, which are exactly the inverse rules of Section 3.2. Then we add additional information keeping track of the axiomatic, flow and cut formulas in the proof net, which will allow us to tell where we have to split up the proof net. Finally, special hyperedge replacement rules for different sets of structural rules will be discussed.

• • • R⊙ 1 2 3 • • • ; 1 2 3 Gr3 ′ | Gr4 ′ Gr1 ′ | Gr2 ′ • • • ; 1 3 2 • • • L 1 3 2 Gr1 | Gr2 • • • ; 2 3 1 • • • L⊘ 2 3 1 Gr3 | Gr4
The correspondence is very strong: except for the structural rules, which are 'compiled away' we will generate the same sets of hypergraphs using the hyperedge replacement grammars as we doing generating the proof nets.

A Hyperedge Replacement Grammar for Abstract Proof Nets

The hyperedge replacement grammar HR(APN) is defined as follows.

HR(APN) = ({S, T, V }, {h, c, •, , /, •, \, 3, 2}, {s1, s2, t, 1, 2, 3}, P, S)

The set of productions P is shown in The intuition behind the T rules (T for 'tensor tree') shown in Figure 4.2 is that we construct a tensor tree with binary und unary branches (we obtain the tree by interpreting 1 as indicating the left daugter, 2 as indicating the right daughter and 3 as indicating the parent node for binary branches and by interpreting 1 as indicating the single daughter and 2 the parent node for unary branches.

The tree is constructed top-down, that is to say the nonterminal hyperedge connected to the root (conclusion) external node -the external node (2) -is an abstract proof structure contracting to a single vertex, indicated by the V nonterminal. This way, the T rules construct a tree of tensor links where every vertex in the tensor tree is represented by a single V nonterminal.

The V rules are shown in Figure 4.3: again we descend the graph top-down. In order for an abstract proof net to contract to a single vertex, we need to be able to find a 1-1 correspondance between tensor links and par links. Figure 4.3 simply states that an abstract proof structure contracts to a single vertex whenever the two active vertices of a tensor and a par link are connected after contracting any intervening structure, as indicated by the V hyperedges between the active vertices in all grammar rules. Finally, we can have a graph contracting to a single vertex which is followed by another sequence to be contracted (remember that the contraction of the first hyperedge doesn't necessarily occur with the last hyperedge).

The final case contracts the V hyperedge to a single vertex, identifying the two distinct nodes it connected before.

• • T 2 1 → • • V 2 1 • • 2 1 • • T 2 1 (2) (1) | • • • • 1 2 3 • • V 2 1 • • T 2 1 • • T 2 1 • h s1 (2)
(1)

|

(1)

• • V 2 1 (2)

A Hyperedge Replacement Grammar for Proof Nets

The hyperedge replacement grammar HR(PN) is defined as follows.

HR(PN) = ({S, T, V, •, , /, •, \, 3, 2}, {h, c, L/, R/, L•, R•, L\, R\, L3, R3, L2, R2}, {s1, s2, t}, P, S)
where the set of productions P contains -in addition to all the productions of HR(APN) -the following additional productions.

Remember that proof nets are relatively close to abstract proof nets. We have to distinguish the different possible instantiations of the '•' and the ' ' tensor links in the abstract proof structures -as shown in Figure 4.4 -but for the par links this is just a simple matter of relabeling the hyperedges and tentacles.

Soundness and Completeness

With everything in place it is time to prove the main theorem, that the proof nets generated by the hyperedge replacement grammar of the previous section

• • • • 1 2 3 → • • • R• s1 s2 t (1) (2) (3) | • • • L/ t s2 s1 (1) (2) (3) | • • • L\ s1 t s2 (1) (2) (3) • • 2 1 → • • R3 s1 t (1) (2) | • • L2 t s1 (1)
(2)

Figure 4.4: Converting tensor links from abstract proof nets to proof nets

• • • • 1 2 3 → • • • L• s1 s2 t (1) (2)
(3)

• • • \ 1 2 3 → • • • R\ s1 t s2 (1) (2)
(3)

• • • / 1 2 3 → • • • R/ t s1 s2 (1) (2)
(3)

• • 3 2 1 → • • L3 t s1 (1)
(2)

• • 2 2 1 → • • R2 s1 t (1)
(2)

t 0 → . . . → t i → v 0 → . . . → v j → v ′ 0 → . . . → v ′ k
where each t n rewrites a T nonterminal, each v n expands a V nonterminal, i.e. applies on of the V rules except the last one which contracts the V edge, and finally each v ′ n corresponds to a contraction of a V edge.

PN → HR(PN)

Given that S is a proof net, we know that there is a conversion sequence ρ which converts the abstract proof structure A of S to a tensor tree T . We proceed by induction on the length l of ρ. The induction hypothesis is that for every abstract proof structure in the conversion sequence we have a V edge for every vertex in the abstract proof structure which can expand into a pair of links. Starting from the tensor tree at the end of the conversion sequence we move to the beginning of the conversion sequence generating the initial abstract proof net then finally we convert it to the proof net.

In case l = 0, we know that A is a tensor tree. We apply the T rules to obtain the same tensor tree, but where every vertex in this tensor tree is now a V edge.

In case l > 0, we know by the induction hypothesis that the abstract proof structure has a V edge for each of its vertices. The contraction expands a vertex into two edges and we apply the corresponding HR rule to add the two links to the abstract proof structure.

After all contractions have been performed, we have obtained an abstract proof net with some extra V edges. We replace these edges with single nodes to obtain an HR(APN) derivation producing a hypergraph which is isomorphic to the original APN. Finally, using the links of the proof net we extend this HR(APN) derivation to a HR(PN) derivation which is isomorphic to the original proof net.

HR(PN)

→ PN Suppose that d is a HR(PN) derivation in normal form. Let S be the proof structure at the end of the conversion sequence and let A be the abstract proof structure at the end of the subsequence d ′ of d which is a HR(APN) derivation. In order to show that S is a proof net we have to prove that A contracts to a tensor tree, which we do by induction on the number of expansions e in d ′ .

Suppose d ′ contains no expansions, then d ′ ends in a tensor tree we have a proof net.

If d ′ does contain expansions, we look at the last one. Given that there are no further expansions, all V nodes in the rule are converted to vertices to abtain Axiom

A Hyperedge Replacement Grammar for Type-Logical Grammars

The main theorem states that proof nets generated by hyperedge replacement and proof nets conforming to the contraction criterion coincide for NL3. However, we haven't yet taken the axiom connections and the structural rules into account.

In order to add the axiom connections to the hyperedge replacement grammar of the previous sections, we are confronted with the problem that in order to distinguish between cut, flow and axiom vertices we need to know the labels of the two tentacles adjacent to the vertex and the hyperedge replacement rules can distinguish only between hyperedge labels, we cannot rewrite a vertex based on its incident labels. The solution is very simple: since the V hyperedges already correspond to the vertices in the hypergraph of a proof structure, we simply need to distinguish the four different cases (cut, flow up, flow down and axiom) in the hyperedge label. So the hyperedge label V is replaced by a hyperedge label V ij where i, j ∈ {0, 1}. i is 0 in case the vertex is the hypothesis of a link by means of its t tentacle and 1 in case it is its hypothesis by means of an s tentacle. Similarly, j is 0 in case it is the conclusion of a link by means of its t tentacle and 1 in case it is the conclusion by means of an s tentacle. The single T hyperedge labels is likewise replaced by four instances T 11 (axiom), T 01 (flow down), T 10 (flow up) and T 00 (cut).

However, given that these vertex types depend crucially on the instantiations of the •, and ; labels, we need to compile out the different possibilities. This multiplication results in a hyperedge replacement grammar with a bigger number of rules, though it reduces a hyperedge replacement grammar of or-

• • V 2 1 → • • • L• m 1 2 3 • • V 2 1 • • V 2 1 • • • • 1 2 3 • • V 2 1 (2)
(1)

• • V 2 1 • • V 10 2 1 → • • • L• m 1 2 3 • • V 10 2 1 • • V 11 2 1 • • • L/ m 1 2 3 • • V 10 2 1 (2)
(1)

• • V 10 2 1
Figure 4.7: Hyperedge replacement rules with and without separating the different V edges der three to a hyperedge replacement grammar of order two. Figure 4.7 shows how this addition changes the hyperedge replacement rules.

• • • L\ s1 t s2 • • • L/ t s2 s1 • • • R/ s1 s2 t • • • L\ s1 t s2 • • L3 t s1 • • • L/ s1 s2 t • • L2 t s1 • h s1 • h s1 • h s1 • h s1 • c s1 • • • V 11 2 1 • • V 11 2 1 • • V 11 2 1 • • V 11 2 1 • • V 11 1 2 • • • L\ 1 2 3 • • • L/ 1 2 3 • • • R/ 3 2 1 • • • L\ 1 2 3 • • L3 2 1 • • • L/ 3 2 1 • • L2 1 2 • h 1 • h 1 • h 1 • h 1 • c 1
• • V 11 2 1 • • V 11 2 1 • • V 11 2 1 • • V 11 1 2 • • • L\ 1 2 3 • • • L/ 1 2 3 • • • R/ 3 2 1 • • T 10 2 1 • • L3 2 1 • • • L/ 3 2 1 • • L2 1 2 • h 1 • h 1 • h 1 • c 1 • • V 11 2 1 • • V 11 2 1 • • • L\ 1 2 3 • • • L/ 1 2 3 • • T 10 • h 1 • h 1 • h • c 1

Figure 2

 2 Figure 2.2: Hyperedge replacement

Figure 2 . 3 :

 23 Figure 2.3: Hyperedge replacement grammar for flowcharts -statements

  Figure 3.2: Cut, flow and axiom vertices

Figure 3

 3 Figure 3.4: Example lexical graphs and a possible set of axiom connections

Figure 3 . 7 :

 37 Figure 3.7: Converting a PS to an APS: par cases

Figure 3 .

 3 Figure 3.10: Mixed associativity and mixed commutativity -right branch

Figure 3 .

 3 Figure 3.11: Mixed associativity and mixed commutativity -left branch with unary control

Figure 3 .

 3 Figure 3.12: Mixed associativity and mixed commutativity -right branch with unary control

Figure 3 .

 3 13 shows the contractions for proof nets in the Lambek-Grishin calculus. The contractions for Lambek connectives [R\], [L•] and [R/] are the same as before, but note how the Grishin connectives [L ], [L⊙] and [R⊘] are just the up-down symmetric versions of the Lambek connectives, given that ';' is the inverse of '•'.

Figure 3 .

 3 Figure 3.15: Mixed associativity and mixed commutativity -Lambek-Grishin, right branch

  Figure 3.18: Applying an R/ contraction to the abstract proof structure of Figure 3.17.

Figure 3 .

 3 Figure 3.19: A proof net violating the well-bracketing conditions

Figure 3 .

 3 Figure 3.22: Generalised contractions for LG abstract proof structures

Figures

Figure 4 .Figure 4

 44 Figure 4.1: Abstract proof nets: start rule

Figure 4 . 2 :

 42 Figure 4.2: Abstract proof nets: tensor rules

Figure 4 . 5 :

 45 Figure 4.5: Converting par links from abstract proof nets to proof nets

Figure 4

 4 Figure 4.6: Cut, flow and axiom vertices and the corresponding hyperedges

  Figure 4.6 repeats Figure 3.2 while adding the different corresponding V hyperedges.

Figure 4 . 8 :

 48 Figure 4.8: The example structure of Figure 3.5 with the axiom vertices encircled (left) and with explicit axiom hyperedges (right)

Figure

  Figure 4.9: Applying a T 01 rule

  Lemma 4.2 For every HR(APN) derivation d there is a derivation d ′ ending in the same graph which is in normal form. A HR(PN) derivation is in normal form iff it is of the following forma 0 → . . . → a i → p 0 → . . . → p jwhere each the sequence a 0 , . . . a i is an HR(APN) derivation in normal form and the sequence p 0 → . . . → p j contains only HR(PN) rules not in HR(APN). For every HR(PN) derivation d there is a derivation d ′ ending in the same graph which is in normal form. An proof structure S for NL3 is a proof net if an only if it is generated by HR(PN).

	Definition 4.3 Lemma 4.4 Theorem 4.5

The selector labels represent 'source 1', 'source

2' and 'target' respectively: in the notation of[START_REF] Habel | May we introduce to you: Hyperedge replacement[END_REF] the source selector labels would be arrows entering the hyperedge and the

|

(1)

•

(2) This is the full NL3 HR 2 grammar, that is to say it is a hyperedge replacement grammars where all non-terminals have two tentacles. All ternary nonterminals haven been compiled away and the axiom/cut/flow disctintions have been factored in. The non-terminal symbols of the grammar are S, T 00 (tree, cut), T 01 (tree, flow down), T 10 (tree, flow up), T 11 (tree, axiom), V 00 (vertex, cut), V 01 (vertex, flow down), V 10 (vertex, flow up), V 11 (vertex, axiom).

A.1 Start: Initial Axiom

The initial axiom rewrites S to a T 11 (axiom) vertex which is both a hypothesis and a conclusion of the abstract proof net.

A.2 Tensor: Binary

The T binary tensor rules construct the final tensor tree where every vertex in the tensor tree is a V edge.

Complete HR Grammar for NL3

(1)

A.3 Tensor: Unary

The two unary tensor rules and the base case, where we rewrite a tensor tree

|

(1)

A.4 Par: L•

The par rules are all instances of the same schema: a par link is linked to a tensor link by all its tentacles except one, making sure the connecting tentacles have the same selector at both ends.

(1)

A.5 Par: R/

A.6 Par: R\

A.7 Par: L3 53 A.7 Par: L3

Complete HR Grammar for NL3

A.9 End: Cut/Flow/Axiom

These rules end the derivation. Flow up (V 01 ) and flow down (V 10 ) edges are deleted. Axiom and cut edges are separated into their positive and negative parts. To obtain cut-free proof nets, simply erase all rules containing occurrences of either T 00 or V 00 .

•

(2)

APPENDIX B

ADDING STRUCTURAL RULES: HRG FOR NL3 R

B.1 Multimodality

A first extension to NL3 is multimodality. Instead of having a single family of connectives, an NL3 R grammar G can have a set M of modes. For every

In addition there are structural connectives {• m , m } for each mode. Finally, there is a set E ⊆ M of external modes. These are the modes which are allowed to appear as structural connectives on the final tensor tree. The rules of Appendix A already implement the multimodal version of NL3. For every external mode e ∈ E there is a T e tree rule constructing a tree with a structural connective e and for every mode m ∈ M , the internal modes include, there is a V vertex rule contracting a tensor and par link of mode m.

B.2 Mixed Associativity and Mixed Commutativity

Mixed assiociativity and commutativity use an external mode 0 and an internal mode 1.

The case for embedding tree adjoining grammars, using (A/ 1 B) • 1 B uses the following schema. The contraction for mode 0 uses the normal HR rule, while mode 1 next to it differs just in the choice of T instead of V , which permets a tensor tree to insert itself at the place of the vertex in the original rule. To show this rule is correct, we need to show that for any tensor tree T in the position indicate in the contraction the structural rules allow us to rewrite them.

(1)

B.3 Mixed Associativity and Mixed Commutativity With Unary Control

For mixed associativity and mixed commutativity with unary control, we only consider two very restricted cases: either positive occurrences of A/ 0 3 0 2 0 B together with U 1 and U 2 or positive occurences of 3 0 2 0 B\ 0 A together with U 3 and U 4.

B.3 Mixed Associativity and Mixed Commutativity With Unary Control 57

B.4 The K1, K2 interaction rules

The K1 and K2 interaction rules are easy to implement. Given that the unary mode 0 is internal to the grammar, we know that every R3 0 and L2 0 rule must be paired to either an L3 0 or an R2 0 rule.

The grammars of Appendix A and B extend easily to the Lambek-Grishin calculus. We can even incorporate the Grishin class IV interactions in a way similar to the incorporation of mixed associativity and mixed commutativity in Appendix B.2

C.1 Start: Initial Axiom

The initial axiom rewrites S to a T 11 (axiom) vertex which is both a hypothesis and a conclusion of the abstract proof net.

C.2 Tensor: Binary

As usual, the T rules construct the final tensor tree, but we require it consists of Lambek constructors only.

C.4 Par: R⊙

63

C.4 Par: R⊙

(1)

C.5 Par: R\

C.6 Par: L

C.9 End: Cut/Flow/Axiom

The end rules remain unchanged.

(2)

•

C.10 The Class IV Interactions