Vito Michele Abrusci
email: abrusci@uniroma3.it

Roberto Maieli
email: maieli@uniroma3.it

Cyclic multiplicative-additive proof nets of linear logic with an application to language parsing

This paper concerns a logical approach to natural language parsing based on proof nets (PNs), i.e. de-sequentialized proofs, of linear logic (LL). In particular, it presents a syntax for PNs of the cyclic multiplicative and additive fragment of linear logic (CyMALL). Any proof structure (PS), in Girards style, is weighted by boolean monomial weights, moreover, its conclusions Γ (a sequence of formulas occurrences) are endowed with a cyclic order σ, i.e., σ(Γ). Naively, a CyMALL PS π with conclusions σ(Γ) is correct if, for any slice ϕ(π) (obtained by a boolean valuation ϕ of π) there exists an additive resolution (i.e. a multiplicative refinement of ϕ(π)) that is a CyMLL PN with conclusions σ(Γr), where Γr is an additive resolution of Γ (i.e. a choice of an additive subformula for each formula of Γ). In its turn, the correctness criterion for CyMLL PNs can be considered as the non-commutative counterpart of the famous Danos-Regnier (DR) criterion for PNs of the pure multiplicative fragment (MLL) of LL. The main intuition relies on the fact that any DR-switching (i.e. any correction or test graph for a given PN) can be naturally viewed as a seaweed, i.e. a rootless planar tree inducing a cyclic order on the conclusions of the given PN. Dislike the most part of current syntaxes for non-commutative PNs our syntax allows a sequentialization for the full class of CyMLL PNs, without requiring these latter must be cut-free. Moreover, we give a characterization of CyMALL PNs for the extended (MALL) Lambek Calculus and thus a geometrical (non inductive) way to parse phrases or sentences. In particular additive Lambek PNs allow to parse phrases containing words with syntactical ambiguity (i.e. words with polymorphic type).

Introduction

Proof nets (PNs) are one of the most innovative inventions of linear logic (LL, [Gir1987]): they are used to represent demonstrations in a geometric (i.e., non inductive) way, abstracting away from the technical bureaucracy of sequential proofs. Proof nets quotient classes of derivations that are equivalent up to some irrelevant permutations of inference rules instances.

Following this spirit, we present a syntax for PNs of the cyclic multiplicative and additive fragment of linear logic (CyMALL, Sections 1.1). This syntax, like the original Girard's one [Gir1996], is based on weighted (by boolean monomials) proof structures with explicit binary contraction links (Section 3). The conclusions Γ (a sequence of formulas occurrences) of a PS π are endowed with a cyclic order σ on Γ. Naively, a CyMALL PS π with conclusions σ(Γ) is correct if, for any slice ϕ(π) (obtained by a boolean valuation ϕ of π) there exists an additive resolution (a slight deformation of ϕ(π)) that is a CyMLL PN with conclusion σ(Γ r ), where Γ r is an additive resolution of Γ (i.e. a choice of an additive sub-formula for each formula of Γ). In its turn, correctness criterion for CyMLL PNs can be considered as the non-commutative counterpart of the famous Danos-Regnier criterion for proof nets of linear logic (see [DR1989] and [Dan1990]). The main intuition relies on the fact that any DR-switching for a PS (i.e. any correction or test graph, obtained by mutilating one premise of each disjunction -link) can be naturally viewed as a rootless planar tree, called seaweed, inducing a cyclic ternary relation on the conclusions of the given proof structure (Section 2.1).

Dislike some previous syntaxes for non-commutative logic, like e.g., [AR2000] and [Mai2003], this new syntax admits a sequentialization (i.e., a correspondence with sequential proofs) for the full class of CyMLL PNs including those ones with cuts (see Sections 2.2 and 2.3). Actually, unlike what happens in the standard (commutative) MLL case, the presence of cut links is "rather tricky" in the non-commutative case, since cut links are not equivalent, from a topological point of view, to tensor links; these latter make appear new conclusions that may disrupt the original (i.e., in presence of cut links) order of conclusions.

Moreover, CyMALL PNs satisfy both a simple convergent cut-elimination procedure in Laurent-Maieli's style [LM2008] (Section 3.2) and a sequentialization, in Girard's style (Section 3.3), stable under cut-reduction.

CyMALL can be considered as a conservative classical extension of Lambek Calculus (LC, see [Lam1958], [Abr2002] and [MR2012]) one of the ancestors of LL. The LC represents the first attempt of the so called parsing as deduction, i.e., parsing of natural language by means of a logical system. Following [AP1991], in LC parsing is interpreted as type checking in the form of theorem proving of Gentzen sequents. Types (i.e. propositional formulas) are associated to words in the lexicon; when a string w 1 ...w n is tested for grammaticality, the types t 1 , ..., t n associated with the words are retrieved from the lexicon and then parsing reduces to proving the derivability of a one-sided sequent of the form t ⊥ n , ..., t ⊥ 1 , s, where s is the type associated with sentences. Moreover, forcing constraints on the Exchange rule, by e.g. allowing only cyclic permutations over sequents of formulas, gives the required computational control needed to view theorem proving as parsing in Lambek Categorial Grammar style. Anyway, LC parsing presents some syntactical ambiguity problems; actually, there may be:

1. (non canonical proofs) more than one cut-free proof for the same sequent; 2. (lexical polymorphism) more than one type associated with a single word.

Proof nets are commonly considered an elegant solution to the first problem of representing canonical proofs; in this sense, in Section 4, we give an embedding of extened MALL Lambek Calculus into Cyclic MALL PNs.

In Section 5 we propose a parsing approach based on CyMALL PNs that could be considered a step towards a proof-theoretical solution to the problem of lexical polymorphism; technically speaking, CyMALL proof nets allow to manage formulas (types) superposition (polymorphism) by means of the additive links & and ⊕. Following [Moo2002], we propose a parsing, by means of Lambek CyMALL PNs, of some sentences which make use of polymorphic words; naively, when a word has two possible formulas A and B assigned then we can combine (or super-pose) these into a single additive formula A&B.

Cyclic MALL

We briefly recall the necessary background of the Cyclic MALL fragment of LL, denoted CyMALL, without units (see [Abr2002]). We arbitrarily assume literals a, a ⊥ , b, b ⊥ , ... with a polarity: positive (+) for atoms, a, b, ... and negative (-) a ⊥ , b ⊥ ... for their duals. A formula is built from literals by means of the two groups of connectives: negative, ("par") and & ("with") and positive, ("tensor") and ⊕ ("plus"). For these connectives we have the following De Morgan laws:

(A B) ⊥ = B ⊥ A ⊥ , (A B) ⊥ = B ⊥ A ⊥ , (A&B) ⊥ = B ⊥ ⊕ A ⊥ , (A ⊕ B) ⊥ = B ⊥ &A ⊥ . A CyMALL (resp.
, CyMLL) proof is any derivation tree built by the following (resp., only multiplicative) inference rules where sequents Γ, ∆ are sequences of formulas occurrences endowed with a total cyclic order (lists with cyclic permutation) (see Definition 1):

identity: id A, A ⊥ Γ, A A ⊥ ∆ cut Γ, ∆ multiplicatives: Γ, A B, ∆ Γ, A B, ∆ Γ, A, B Γ, A B additives: Γ, A Γ, B Γ, A B Γ, A i ⊕ i=1,2 Γ, A 1 ⊕ i A 2
Naively, a total cyclic order can be thought as follows; consider a set of points of an oriented circle; the orientation induces a total order on these points as follows: if a, b and c are three distinct points, then b is either between a and c (a < b < c) or between c and a (c < b < a). Moreover, a < b < c is equivalent to b < c < a or c < a < b.

Definition 1 (total cyclic order) A total cyclic order is a pair (X, σ) where X is a set and σ is a ternary relation over X satisfying the following properties:

1. ∀a, b, c ∈ X, σ(a, b, c) → σ(b, c, a) (cyclic); 2. ∀a, b ∈ X, ¬σ(a, a, b) (anti-reflexive); 3. ∀a, b, c, d ∈ X, σ(a, b, c) ∧ σ(c, d, a) → σ(b, c, d) (transitive); 4. ∀a, b, c ∈ X, σ(a, b, c) ∨ σ(c, b, a) (total).
Negative (or asynchronous) connectives correspond to true determinism in the way we apply bottom-up their corresponding inference rules. In particular, observe that Γ must appear as the same context (with same order) in both the premises the &-rule. Vice-versa, positive (or synchronous) connectives correspond to true non-determinism in the way we apply bottom-up their corresponding rules; in particular, there is not deterministic the way to split the context into Γ, ∆ in the rule, as well there not exist a deterministic choice in the way we apply bottom up ⊕ 1 or ⊕ 2 rules.

Cyclic MLL proof structures

Definition 2 (CyMLL proof structure) A CyMLL proof structure (PS) is an oriented graph π, in which edges are labeled by formulas and nodes are labeled by connectives of CyMLL, built by juxtaposing the following special graphs, called links, in which incident (resp., emergent) edges are called premises (resp., conclusions):

ax A A ⊥ A cut A B A B A B A B A ⊥
In a PS π each premise (resp., conclusion) of a link must be conclusion (resp., premise) of exactly (resp., at most) one link of π. We call conclusion of π any emergent edge that is not premises of any link.

Correctness

We characterize those proof structures that are images of proofs. Actually, there exist several syntaxes for CyMLL proof nets, like those ones of [AR2000] and [Mai2003]; for sequentialization reasons we prefer the latter one.

Definition 3 (switchings and seaweeds) Assume π is a CyMLL PS with conclusions Γ.

• A Danos-Regnier switching S for π, denoted S(π), is the non oriented graph built on nodes and edges of π with the modification that for each -node we take only one premise, that is called left or right -switch.

• Let S(π) be an acyclic an connected switching for π; S(π) is the rootless planar tree whose nodes are labeled by -nodes, and whose leaves X 1 , ..., X n are the terminal (pending) edges of S(π); S(π) is a ternary relation, called seaweed, with support X 1 , ..., X n ; an ordered triple (X i , X j , X k ) belongs to the seaweed S(π) iff:

the intersection of the three paths X i X j , X j X k and X k X i is the node l ;

the three paths X i l , X j l and X k l are in this cyclic order while moving anti-clockwise around the -node as below

X k X j X i l
If A is an edge of the seaweed S(π), then S i (π) ↓ A is the restriction of the seaweed S(π), that is, the sub-graph of S(π) obtained as follows:

1. disconnect the graph below (w.r.t. the orientation of π) the edge A; 2. delete the graph not containing A.

Fact 1 (seaweeds as cyclic orders) Any seaweed S(π) can be viewed as a cyclic total order (Definition 1) on its support X 1 , ..., X n ; in other words, if a triple (X i , X j , X k ) ∈ S(π), then X i < X j < X k are in cyclic order.

Intuitively, we may contract a seaweed (by associating the -nodes) until it collapses into single n-ary -node with n pending edges (its support), as follows: 1. π is a standard MLL PN, that is, any switching S(π) is a connected and acyclic graph (therefore, a seaweed);

for any -link A B

A B the triple (A, B, C) must occur in this cyclic order in any seaweed S(π) restricted to A, B, i.e., (A, B, C) ∈ S(π) ↓ (A,B) , where C is any pending leave (if it exists) in the support of the restricted seaweed.

Example 1 We give an instance of CyMLL proof net π 1 with, in particular, the two restricted seaweeds, S 1 (π 1 ) ↓ (B1,B ⊥ 2 ) and S 2 (π 1 ) ↓ (B1,B ⊥ 2 ) , both satisfying condition 2 of Definition 4.

B 1 ax ax cut ax B ⊥ 2 B 2 B 2 B ⊥ 1 π 1 B 1 B ⊥ 2 B 3 B ⊥ 3 B ⊥ 3 B 3 B ⊥ 1 B 1 ax ax cut B 2 ax B ⊥ 3 B 3 B ⊥ 3 B 3 B ⊥ 1 B ⊥ 2 S 1 (π 1 ) ↓ (B1,B ⊥ 2 ) B 2 B ⊥ 1 B 1 ax ax cut B 2 ax B 3 B ⊥ 1 B ⊥ 2 B ⊥ 3 S 2 (π 1 ) ↓ (B1,B ⊥ 2 ) B 2 B ⊥ 1 B 3 B ⊥ 3
Vice-versa, the following instance of proof structures π 2 is not correct (it is not a proof net), since condition 2 of Definition 4 is violated: there exists a -link

B1 B ⊥ 2 B1 B ⊥ 2 and a seaweed S 1 (π 2 ) s.t. ¬∀C pending, (B 1 , B ⊥ 2 , C) ∈ S 1 (π 2 ) ↓ (B1,B ⊥ 2 ) ; actually, if we take C = B ⊥ 3 then (B 1 , C, B ⊥ 2 ) ∈ S 1 (π 2 ) ↓ (B1,B ⊥ 2 ) as follows B 1 cut ax ax ax B 2 B ⊥ 2 B ⊥ 1 B ⊥ 1 B 2 B 1 B ⊥ 2 π 2 B 3 B ⊥ 3 B ⊥ 3 B 3 B 1 cut ax ax B 2 B ⊥ 2 B ⊥ 1 B ⊥ 1 B 2 ax B 3 B ⊥ 3 B ⊥ 3 B 3 S 1 (π 2 ) ↓ (B1,B ⊥ 2 )

Cut reduction

Definition 5 (multiplicative cut reduction) Let L be a cut link in a proof net π whose premises A and A ⊥ are, resp., conclusions of links L , L . Then we define the result π (called reductum) of reducing this cut in π (called redex), as follows:

Ax-cut: if L (resp., L ) is an axiom link then π is obtained by removing in π both formulas A, A ⊥ (as well as L) and giving as new conclusion to L (resp., L ) the other conclusion of L (resp., L ). ( / )-cut: if L is a -link with premises B and C and L is a -link with premises C ⊥ and B ⊥ , then π is obtained by removing in π the formulas A and A ⊥ as well as cut link L with L and L and by adding two new cut links with, resp., premises B, B ⊥ and C, C ⊥ , as follows: , resulting from the cut reduction, otherwise π would already be violating condition 2 of Definition 4; so, assume path B goes through cut 1 and path A goes through cut 2 , like in the next left hand side picture

cut cut π π B C B C cut C ⊥ B ⊥ w w w C ⊥ B ⊥
A B X Y Y ⊥ X ⊥ C cut 2 cut 1 π A B cut X Y Y ⊥ X ⊥ C π
This means there exist a seaweed S (π), a link Y ⊥ X ⊥ and a triple (Y

⊥ , C, X ⊥ ) s.t. (Y ⊥ , C, X ⊥ ) ∈ S (π) ↓ (Y ⊥ ,X ⊥ )
, violating condition 2 and so contradicting correctness of π (see the right hand side picture given before; observe that, since any switching of π is acyclic, deleting the subgraph below Y ⊥ X ⊥ does not make disappear C).

The remaining case when path C goes through cut 1 (resp., through cut 2 ) and either path A or path B goes through cut 2 (resp., through cut 2 ) is treated similarly and so omitted.

Example 2 Observe that w.r.t. Example 1, π 1 reduces to π 1 and so π 1 to π 1 below; both π 1 and π 1 are correct since condition 2 of Definition 4 is void in both π 1 and π 1 :

B 1 ax ax cut ax B ⊥ 2 B 2 B 1 B ⊥ 2 B ⊥ 3 B 3 B ⊥ 1 cut π 1 ax B B ⊥ B B ⊥ π 1
Moreover, w.r.t. Example 1, π 2 is a non correct PS that reduces to a correct one, π 2 , after a cut reduction step (see the left hand side picture below); this is an already well known phenomenon in the standard MLL case where we can easily find non correct MLL PSs that become correct after cut reduction, like that one on the right hand side below:

B 1 cut ax ax ax B 2 B ⊥ 2 B ⊥ 1 B 1 B ⊥ 2 B 3 B ⊥ 3 π 2 cut ax ⊗ cut A ⊥ A A ⊥ A A ⊥ A ax ax ax A A ⊥ We use indexed formulas B 1 , B 2 , B 3 to distinguish different occurrences of B.
Cut reduction if trivially convergent (i.e., terminating and confluent).

Sequentialization

We show a correspondence (sequentialization) between PNs and sequential proofs.

Lemma 1 (splitting) Let π be a CyMLL PN with at least a -link or cut-link and with conclusions Γ not containing any terminal -link (so, we say π is in splitting condition); then, there must exist a -link A B A B (resp., a cut-link A A ⊥ ) that splits π in two CyMLL PNs, π A and π B (resp., π A and π A ⊥ ).

Proof -Assume π is a CyMLL PN in splitting condition, then by the Splitting Lemma for standard commutative MLL PNs ([Gir1987]) π must split either at a -link or a cut-link. We reason according these two cases.

Assume π splits at A B

A B in two components π A and π B ; we know that both components satisfy condition 1 (they eare MLL PNs); assume by absurdum π A is not a CyMLL PN, i.e., π A violates condition 2 of Definition 4. This means there exists a X Y X Y and a restricted seaweed S(π A ) ↓ (X,Y ) containing the triple X, A, Y in the wrong order, i.e., (X, A, Y ) ∈ S(π A ) ↓ (X,Y ) like in Case 1 of next figure. But then there exists a restricted seaweed S(π) ↓ (X,Y ) containing X, Y and C (where C = A B) in the wrong cyclic order, i.e., (X, C, Y ) ∈ S(π) ↓ (X,Y ) , contradicting the correctness of π.

Assume π splits at the cut link

A A ⊥
in two components π A and π A ⊥ ; assume by absurdum π A is not a CyMLL PN, hence π A must be violating condition 2 of Definition 4. Moreover, assume π is such a minimal PN in cut-splitting condition whose subproof π A is not a CyMLL PN. This means, as before, there exists a X Y X Y and a restricted seaweed S(π A ) ↓ (X,Y ) containing the triple X, A, Y in the wrong order, i.e., (X, A, Y ) ∈ S(π A ) ↓ (X,Y ) like in Case 2 of next figure. Then, by correctness π, π A ⊥ must have A ⊥ as unique conclusion, otherwise we can find a restricted seaweed for π, S(π) ↓ (X,Y ) , containing a triple X, C, Y with wrong order for a conclusion C = A ⊥ ; moreover, π A ⊥ cannot contain any cut, otherwise, by Theorem 1, we could replace in π the redex π A ⊥ by its reductum π A ⊥ , contradicting the minimality of π. Now, observe the equality -= 1, relating the number of -nodes with the number of -nodes, holds for any cut free proof net with an unique conclusion. Therefore, π A ⊥ must contains at least a -link, let us say Z T Z T . But then we can easily find a restricted seaweed for π, S(π) ↓ (X,Y ) , and a triple (X, Z, Y ) occurring in S(π) ↓ (X,Y ) with the wrong cyclic order, contradicting the correctness of π, like like in Case 2 of the picture below:

Y X C A B π A π B π Case 1 Y X A π A cut Case 2 π A ⊥ Z T π A ⊥
Lemma 2 (PN cyclic order conclusions) Let π be a CyMLL PN with conclusions Γ, then all seaweeds S i (π) ↓ Γ , restricted to Γ, induce the same cyclic order σ on Γ, denoted σ(Γ) and called the (cyclic) order of the conclusions of π.

Proof -By induction on the size of π, i.e. edges, vertexes 1 .

1. If π is reduced to an axiom link, then obvious.

2. π contains at least a conclusion A B, then Γ = Γ , A B; by hypothesis of induction the sub-proof net π with conclusion Γ , A, B has cyclic order σ(Γ , A, B), and so, by condition 2 of Definition 4 applied to π, we know that each restricted seaweed S i (π) ↓ (Γ ,A,B) induces the same cyclic order σ(Γ , A, B); finally, by substituting

[A/A B] (resp., [B/A B]) in the restriction S i (π) ↓ (Γ ,A) (resp., S i (π) ↓ (Γ ,B
) ), we get that each seaweed S i (π) ↓ (Γ ,A B) induces the same cyclic order σ(Γ , A B).

3. Otherwise π must contain a terminal splitting or cut link. Assume π contains a splitting -link, A B A B , and assume by absurdum that π is such a minimal (w.r.t. the size) PN with at least two seaweeds S i (π) and S j (π) s.t. (X, Y, Z) ∈ S i (π) and (X, Y, Z) ∈ S j (π). We reason according the following two sub-cases.

(a) It cannot be the case X = B, Y = A and Z = C otherwise, by definition of seaweeds, S i (π) and S j (π) will be as follows:

S i (π) ↓ (Γ 1 ,A B,Γ 2 ) = S i (π A ) ↓ (Γ 1 ,A) S i (π B ) ↓ (B,Γ 2 ) S j (π) ↓ (Γ 1 ,A B,Γ 2 ) = S j (π A ) ↓ (Γ 1 ,A) S j (π B ) ↓ (B,Γ 2 ) Γ1 Γ2 Si(πA) Sj(πB) A = Y B = X (A B) = Z
Now, by hypothesis of induction, all seaweeds on π A (resp., all seaweeds on π B ) induce the same order on Γ 1 , A (resp., Γ 2 , B), then in particular,

S i (π A ) ↓ (Γ1,A) = S j (π A ) ↓ (Γ1,A) and S i (π B ) ↓ (B,Γ2) = S j (π B ) ↓ (B,Γ2) but this implies S i (π) ↓ (Γ1,A B,Γ2) = S j (π) ↓ (Γ1,A B,Γ2) .
(b) So, assume both X and Y belong to π A (resp., π B ) and Z belongs to π B (resp., π A ); moreover, assume for some i, j, (X, Y, Z) ∈ S i (π) ↓ (Γ1,Z,Γ2) and (X, Y, Z) ∈ S j (π) ↓ (Γ1,Z,Γ2) ; by Splitting Lemma 1, each seaweed for π must appear as follows, in particular S i (π) and S j (π):

Y X A B Z S i (π A ) ↓ Γ1,A S i (π B ) ↓ B,Γ2 A B Γ 1 Γ 2 (X, Y, Z) ∈ S i (π) ↓ Γ1,A B,Γ2 Y X A B Z A B S j (π B ) ↓ B,Γ2 (X, Y, Z) ∈ S j (π) ↓ Γ1,A B,Γ2) S j (π A ) ↓ Γ1,A Γ 2 Γ 1
then, by restriction on seaweeds, (X, Y, A) ∈ S i (π A ) ↓ Γ1,A and (X, Y, A) ∈ S j (π A ) ↓ Γ1,A , contradicting the assumption (by minimality) that π A is a correct PN with a cyclic order on its conclusions Γ 1 , X, Y, A = Γ 1 , A.

The remaining case, π contains a splitting cut, is similar and so omitted.

Next Corollary states that Lemma 2 is preserved by cut reduction.

Corollary 1 (stability of PN order conclusions under cut reduction) If π, with conclusions σ(Γ), reduces in one step of cut reduction to π , then also π has conclusions σ(Γ).

1 Number of edges and number of vertexes.

Theorem 2 (adequacy of CyMLL PNs) Any CyMLL proof of a sequent σ(Γ) de-sequentializes into a CyMLL PN with same conclusions σ(Γ).

Proof -By induction on the hight of the given sequent proof of σ(Γ).

Theorem 3 (sequentialization of CyMLL PNs) Any CyMLL PN with conclusions σ(Γ) sequentializes into a CyMLL sequent proof with same cyclic conclusions σ(Γ).

Proof -by induction on the size of the given proof net π via Lemmas 1 and 2.

Example 3 (Mellies's proof structure) Observe that, dislike what happens in the commutative MLL case, the presence of cut links is "quite tricky" in the non-commutative case, since cut links are not equivalent, from a topological point of view, to tensor links: these latter make appear new conclusions that may disrupt the original (i.e., in presence of cut links) order of conclusions. By the way, unlike the most part of correctness criteria for non-commutative proof nets, our syntax enjoys a sequentialization for the full class of CyMLL PNs without assuming these must be cut-free. In particular the following Mellies's proof structure2 , given a page 224 of [MR2012], Observe, Mellies's PS becomes correct (and so sequentializable) after cut reduction. Our criterion satisfies, indeed, all four requirements that, according to page 223 of [MR2012], any "satisfactory" criterion should enjoy.

Cyclic MALL proof structures

Definition 6 (CyMALL proof structure) A CyMALL proof structure (PS) is an oriented graph π, in which edges are labeled by formulas while nodes are labeled by connectives of MALL, built by juxtaposing the following special graphs, called link, in which incident (resp., emergent) edges are called premises (resp., conclusions):

& C A&B A A B A A B B A B A A A A ⊥ cut ax A A ⊥ ⊕ 1 ⊕ 2 A ⊕ B A ⊕ B A B A B
In a PS π each premise (resp., conclusion) of a link must be conclusion (resp., premise) of exactly (resp., at most) one link of π. Finally, we call conclusion of π any emergent edge that is not premises of any link.

Definition 7 (Girard CyMALL proof structure) A Girard proof structure (GPS) is a PS with weights associated as follows (weights assignment):

1. first we associate a boolean variable, called eigen weight p, to each &-node (eigen weights are supposed to be different);

2. then we associate a weight, a product of (negation of ) boolean variables (p, p, q, q...) to each node, with the constraint that two nodes have the same weight if they have a common edge, except when the edge is the premise of a & or C-node, in these cases we do like below:

if p does not occur in w w w.p w.p with w 1 .w 2 = 0

w 1 w 2 w = w 1 + w 2 C v 2 v 1 v 2 v 1 & p

a conclusion node has weight 1;

4. if w is the weight of a &-node, with eigen weight p, and w is a weight depending on p and appearing in the proof structure then w ≤ w (we say that a weight w depends on p when p or p occurs in w).

Finally we say that:

• a node L with weight w depends on the eigen weight p if w depends on p or L is a C-node and one of the weights just above it depends on p;

• the signature of a weight w is the set of variables occurring in w; e.g., the following weights have the same signature {p, q}: pq, pq, pq and pq.

Remark 1 Observe that:

1. -since the weights associated to a PS are products (monomials) of the Boolean algebra generated by the eigen weights associated to a proof structure, then, for each weight w associated to a binary contraction node, there exists a unique eigen weight p that splits w into w 1 = wp and w 2 = wp. We sometimes index a C-link with its splitting variable p, like in the left hand side picture below;

2. -the graph π 1 is not a GPS since it violates condition 4 of Definition 7; actually, if w = q is the weight of the & p -link and w = p is a weight depending on p and appearing in the proof-structure then p ≤ q.

Correctness

Definition 8 (slices, switchings, resolutions) Let π be a CyMALL GPS.

• A valuation ϕ of π is a function from the set of all weights of π into {0, 1}.

• Fixed a valuation ϕ for π, the slice ϕ(π) is the graph obtained from π by keeping only those nodes with weight 1 together with its incident edges.

• Fixed a slice ϕ(π) an additive switching is a multiplicative switching of the slice ϕ(π), denoted S ϕ (π), in which for each & p -node we erase the (unique) premise in ϕ(π) and we add an oriented edge, called jump, from the & p -node to an L-node whose weight depends on the eigen weight p of the & p -node.

• An additive resolution ϕ r (π) for a slice ϕ(π) is the graph obtained by replacing in ϕ(π) each unary link L (a link that after the valuation has a single premise) by a single edge labeled by the formula labeling the unique premise of L. In particular, each conclusion of ϕ r (π) is labeled by a multiplicative formula.

We call additive resolution of a CyMALL sequent Γ what remains of Γ after erasing one subformula in each additive formula occurrence of Γ.. Definition 9 (CyMALL proof net) We call correct (or proof net (GPN)) any CyMALL GPS π whose conclusions Γ are endowed with a cyclic order σ(Γ) and s.t. for any valuation ϕ of π:

1. each additive switching S ϕ (π) is an acyclic and connected graph (ACC); 2. there exists an additive resolution ϕ r (π) for ϕ(π) that is a CyMLL PN with cyclic order conclusions σ(Γ r ), where Γ r is an additive resolution of Γ.

Example 4 Observe, the proof structure π on the left hand side below is not correct: actually, fixed a valuation ϕ s.t. ϕ(p) = 1, there exists an additive switching S ϕ (π) (with a jump) that is not ACC (see the middle side figure). Nevertheless, any slice ϕ(π) is ACC; indeed, for each slice ϕ(π) there exists an additive resolution ϕ r (π) that is a CyMLL PN like that one, on the rightmost hand side, with conclusion C A, A ⊥ C ⊥ that is an additive resolution of the sequent

(B&C) A, (A ⊥ C ⊥ ) ⊕ (A ⊥ B ⊥ ).
(A ⊥ C ⊥ ) ⊕ (A ⊥ B ⊥ ) 1 1 (B&C) A C C ⊕ &p ax ax p p 1 1 p (A ⊥ C ⊥ ) ⊕ (A ⊥ B ⊥ ) 1 (B&C) A p Sϕ(π) ax ax A ⊥ C ⊥ C A ax ax ϕr(π)

Cut reduction

Ready cut reduction

Definition 10 (additive ready cut reduction) Let L be a cut in a proof net π whose premises A and A ⊥ are the respective conclusions of links L , L both different from the contraction C. Then we define the result π (reductum) of reducing this additive ready cut in π (redex), as follows:

(&/⊕)-cut: if L is a & p -link with premises B and C and L is a ⊕ 1 -link (resp., a ⊕ 2 -link) with premise B ⊥ (resp., C ⊥ ), then π is obtained in three steps: first remove in π both formulas A, A ⊥ as well as the cut link L with L and L , then replace the eigen weight p by 1 (resp., bt 0) and keep only those links (vertexes and edges) that still have nonzero weight; finally we add a cut between B and B ⊥ (resp., between C and C ⊥ ).

cut & p cut B C B B ⊥ w wp wp w π π [p/1] B ⊥ ⊕ 2
Theorem 4 (stability of GPN under ready cut reduction) Assume π is GPN that reduces to π in one step of multiplicative (Definition 5) or additive (Definition 10) ready cut reduction, then π is GPN too.

Proof -Stability of multiplicative ready cut reduction (Definition 5) follows by Theorem 1. Stability of additive ready cut reduction (Definition 10) is immediate. Trivially, conditions 1 and 2 of Definition 9 are preserved by additive ready cut reduction steps.

Commutative cut reduction

(The confluence problem). In general, reducing a cut involving a contraction link as (at least) one of its premises from a proof structure π may lead to several solutions, depending on which subgraph of π we decide to duplicate. For instance, as illustrated in the following picture, reducing the commutative cut of π of may lead to solution π 1 as well solution π 2 , depending on which additive box (& q or & p ) we decide to duplicate. Of course these two resulting proof nets are different and there is no a-priori way to make them equal. Girard does not give in [Gir1996] a solution to this problem which has been proposed later by Laurent and Maieli in [LM2008]. In the following we present a commutative cut reduction that simplify this latter. • dependency graph of p w.r.t. π, denoted E p , is the (possibly disconnected) subgraph of π made by all links depending on p.

• the spreading of w over π, denoted by w.

[π], is the product of w for π, i.e., π where we replaced each weight v with the product of weights vw.

Lemma 3 (dependency graph) If a & p -node belongs to the dependency graph E q , then E(p) ⊆ E(q).

Proof -If the & p -node belongs to E q then the weight w of the & p -node depends on q (i.e., w = w q or w = w q) then trivially, by the dependency condition 4 of Definition 7, each node v whose weight depends on p will also depends on q.

Definition 12 (commutative cut reduction) Let L be cut link in a proof net π whose premises A and A ⊥ are the respective conclusions of links L and L s. t. at least one of them is a contraction link C. Then we define the result π (reductum) of reducing this commutative cut L in π (redex), as follows:

(C/ )-cut: if L is a C-link
C ⊥ B ⊥ B C B C
(C/C)-cut: if both L and L are both C-links, then there are two cases:

1. either the weight w of both L and L splits on a same p variable, then π reduces in one (C p /C p ) step to π as follows

cut cut π π cut A A A ⊥ A ⊥ A A A ⊥ A ⊥
C ⊥ B ⊥ B ⊕ C cut B ⊕ C & p & p wq C ⊥ B ⊥ C ⊥ B ⊥ cut q.[E p ] q.[E p ] C C ... ... ... A 1 A n χ w n w 1 q w n q w n q w 1
w 1 q wq with the assumptions that graphs q.[E p ] and q.[E p ] are obtained as follows:

1. we take two copies, E p and E p , of the dependency graph of p, E p ;

2. we replace in E p (resp., in E p ) the variable p with a new p (resp., p ); 3. we spread q (resp., q) over E p (resp., over E p ).

Stability of correctness under cut reduction

Theorem 5 (stability under commutative cut reduction: I part) If π is a proof net s.t. it reduces to π in one step of commutative cut reduction that is different from the C/&-case, then π is still a proof net.

Proof -(sketch) All cases are more or less immediate consequences of the Euler-Poicaré Property 1. Trivially, conditions 1 and 2 of Definition 9 are preserved by these commutative cut reduction steps.

Lemma 4 (conservative/extensive switching) Assume π is a proof net that reduces to π in one step of commutative cut reduction C q /& p . We say that a switching S for π is extensive (resp., conservative) w.r.t. q if there exists (resp., there do not exist) in S at least a jump going from the & q -node to a node that was not depending on q in π. Then, for any extensive (resp., conservative) switching for π that is not ACC we can find a corresponding switching for π that is not ACC too.

Proof -(sketch) Assume π reduce to π after a commutative cut reduction C q /& p and assume there exists a cycle in an extensive switching S (π ) like the left hand side picture below This cycle goes through a node ν that depends on both variables p and q, where p is a fresh variable copying p of π, according to the definition C q /& p cut reduction step. Then we can easily find a switching for S(π) with a cycle like the blue-black one of the following picture: replace in π, the fresh variable p of π with the original one p. Similarly, if we assume that S (π ) is not connected.

Lemma 5 (separation) Assume π is a proof net containing two nodes, & p and & p , with weights, resp., w q and w q, for some eigen weight q of π. Then, there cannot exist in π a node whose weight depends both on p and on p .

Proof -By absurdum, assume a node v whose weight w depends both on p and p ; let's say, for instance, w = w 1 .p .p . Now fix an evaluation ϕ for π s.t. ϕ(w) = 1, then by the dependency condition 4 of Definition 7, we have both w 1 .p .p ≤ w q and w 1 .p .p ≤ w q; this is only possible when ϕ(w) = 0, contradicting ϕ(w) = 1.

Theorem 6 (stability under commutative cut reduction: II part) If π is a proof net that reduces to π in one step of cut reduction C/&, then π is a proof net too.

Proof -(sketch) First observe that each cut reduction step C q /& p preserves the property of being a proof structure. This follows by construction of π . In particular Lemmas 3 and 5, ensure that we can safely rename the sets of eigen weights in E and E and get still a proof structure.

Moreover, by Lemma 4 it is enough to only verify that all the extensive switchings, w.r.t. q, for π are ACC. In the rest of proof, whenever it is not explicitly declared, each switching for π is meant to be extensive w.r.t. q.

Connectedness -Assume by absurdum there exists a switching S (π ) that is disconnected. Then there exists at least a node v j occurring in a connected component γ 1 that is separated from the component γ 2 that contains the & q -node together with the jump ν directed to a node v i , like in the next left hand side picture where γ 1 and γ 2 are separated by dotted lines (in S (π ) there is no path from v j to v i ).

γ 2 w j v i v j ν w S (π ) γ 1 & q w i q γ 2 w j v j w γ 1 v h ν v i S (π ) & q w i q w h q
Now let S (π ) be an other switching that is a copy of S (π ) except for the jump ν from the & q -node to a v h node that was already depending on q in π (in other words, S is a conservative switching, w.r.t. q, which differs from S only for the jump ν, like in the previous right hand picture). Clearly in S (π ) there is no connection path between v i and v j , otherwise this path would go through the ν-jump (and so through the & q -node) contradicting the assumption that the & q -node and v j were disconnected in S (π ). But this contradicts, by Lemma 4, the hypothesis that π was correct.

Acyclicity -Assume there exists a cycle in S (π ) going through a jump ν from the & q -node to a node v i whose weight w i depends on q as follows

w v i ν S (π ) γ & q w i p q
where γ is the path in S (π ) from the conclusion of the & q -node to v i . Now, the new variable p or its negation (resp., p or its negation) occurs by definition of C q /& p -cut reduction step in the weight w i : let us say w i = w i p q. So, by condition 4 of Definition 7 and by connectedness of S (π ) showed before, the & p -node (resp., the & p -node) and the node v i must be connected in S (π ) in two possible ways:

1. either by a path going through the & q -node without crossing γ, like path γ 1 of the next left hand side picture;

2. or by a path γ 2 not going through the & q -node (and possibly crossing γ as γ 2 ) like in the left hand side picture below:

v i w p & q & p w i p q w ν S (π ) γ γ 1 γ 2 γ 2 v i & q & p v j w γ 1 γ γ 2 γ 2 w i p q w p ν A ⊥ A cut S (π )
In both cases we can set a conservative switching S (π ) that is identical to S (π ) except for the jump ν going from the & q -node to the node v j whose conclusion A ⊥ is the premise of the cut link of π obtained after reducing the cut C q /& p in π (see the right hand side picture above). Then we get a cycle, contradicting, by Lemma 4, the hypothesis that π is correct.

Strong cut-elimination

Technical details of proofs of next Theorems 7 and 8 can be found in [Mai2008].

Theorem 7 (termination) We can always reduces a proof net π in to a proof net π that is cut-free, by iterating the reduction steps of Definition 5 and 12.

Theorem 8 (confluence) Assume π is proof net s.t. it reduces in one step α to π (π α π ) and it reduces in an other step β to π (π β π ); then, there exists a proof net σ such that π reduces, in a certain number of steps, to σ (π * σ) and π reduces, in a certain number of steps, to σ (π * σ).

Sequentialization

Theorem 9 (sequentialization) A CyMALL GPN of Γ can be sequentialized into a CyMALL sequent proof with same cyclic conclusions σ(Γ) and vice-versa (de-sequentialization).

Proof -Sequentialization-part: any CyMALL proof net π can be sequentialized into a proof Π, by induction on the number of slices (or, equivalently, by the number of & links). The base of induction corresponds to the sequentialization of the CyMLL proof nets (Theorem 3). The induction step follows from the sequentialization of standard MALL PNs (see [Gir1996]). The only novelty is to show that whenever a PN π contains a terminal &-link L, then π ca be toggled3 at L in two sub-proof nets preserving conditions 1 and 2 of Definition 9.

De-sequentialization-part: any CyMALL proof Π of σ(Γ) can be de-sequentialized into a PN π of σ(Γ), by induction of the height of Π derivation.

Example 5 In general, there may exist different GPNs to denote the same sequential proof. Although π 2 and π 3 below are both correct proof structures with same conclusions, π 3 quotients "more" sequential proofs than π 2 . Vice-versa, π 4 and π 5 are both correct proof structures (with same conclusions) that sequentialize into the same proof, although π 4 is not the de-sequentialization of any proof. 1. A is a pure Lambek formula (PLF) if it is a CyMLL formula recursively built according to the following grammar

A := + atoms | A A | A ⊥ A | A A ⊥ .

2.

A is an additive Lambek formula (ALF or simply LF) if it is a CyMALL formula recursively built according to the following grammar

A := a PLF | A&A | A ⊕ A. 3. S is a Lambek sequent of CyMALL iff S = (Γ) ⊥ , A
where A is a non void LF and (Γ) ⊥ is a possibly empty finite sequence of negations of LFs (i.e., Γ is a possibly empty sequence of LFs and (Γ) ⊥ is obtained by taking the negation of each formula in Γ). Proof -Consequence of Theorems 4, 5 and 6. Trivially, each reduction step preserves the property that each edge of the reductum is labeled by a Lambek formula or the negation of a Lambek formula.

A

Theorem 10 (de-sequentialization of Lambek CyMALL proofs) Any proof of a CyMALL Lambek sequent σ(Γ ⊥ , A) can be de-sequentialized in to a Lambek CyMALL PN with conclusions σ(Γ ⊥ , A).

Proof -By induction on the hight of the given sequent proof (similarly to the de-sequentialization part of Theorem 9).

Theorem 11 (sequentialization of pure Lambek CyMALL PNs) Any Lambek CyMALL PN of σ(Γ ⊥ , A) sequentializes into a Lambek CyMALL proof of the sequent σ(Γ ⊥ , A).

Proof -Sequentialization follows by induction on the number of &-links of the given PN. The base of induction follows from next Theorem 12.

Theorem 12 (sequentialization of Lambek CyMLL PNs) Any Lambek CyMLL PN of σ(Γ ⊥ , A) sequentializes into a Lambek CyMLL proof of σ(Γ ⊥ , A).

Proof -Assume by absurdum there exists a pure Lambek CyMLL proof net π that does not sequentialize into a Lambek CyMLL proof. We can chose π minimal w.r.t. the size. Clearly, π cannot be reduced to an axiom link; moreover π contains neither a negative conclusion of type A ⊥ B ⊥ nor a positive conclusion of type A ⊥ B (resp., A B ⊥ ), otherwise, we could remove this terminal -link and get a strictly smaller (than π) proof net π that is sequentializable, by minimality of π; this implies that also π is sequentializable (last inference rule of the sequent proof will be an instance of -rule) contradicting the assumption. For same reasons (minimality), the unique positive conclusion (e.g. A B) of π cannot be splitting. Therefore, since π is not an axiom link A ⊥ A , by Lemmas 1 and 2, there must exist either a (negative) splitting -link (Case 1) or a splitting cut-link (Case 2). Case 1. Assume a negative splitting conclusion A ⊥ B (resp., A B ⊥ ). By minimality, π must split like in the next left hand side picture (we use A + , resp. A -, to denote positive, resp., negative, LF and Γ -for sequence of negative LFs):

A ⊥ B π 1 B π 2 Γ - 1 A ⊥ P + Γ - 2 π 2 π 1 A ⊥ B π 1 C D ⊥ Γ - 1 C D ⊥ Γ - 1 A ⊥ Γ - 2 B P + π
Now, let us reason on π 1 (reasoning on π 2 is symmetric): by minimality of π, π 1 cannot be reduced to an axiom link (otherwise Γ - 1 would not be negative); moreover, none of Γ - 1 is a (negative) splitting link, like e..g., C D ⊥ , otherwise we could easily restrict to consider the subproof-net π , obtained by erasing from π the sub-proof-net π 1 (with conclusions Γ - 1 , C) together with the C ⊥ D-link, like the graph enclosed in the dashed line above. Clearly, π would be a non sequentializable Lambek proof net strictly smaller than π. In addition, π 1 must be cut-free, otherwise by minimality, after a cut-step reduction we could easily build a non sequentializable reductum PN π , strictly smaller than π, (π will have same conclusions of π). Therefore, there are only two sub-cases:

1. either A ⊥ = C ⊥ D ⊥ , then we can easily get, from the PN π on the l.h.s. below, the non sequentializable PN π , on the r.h.s.; π is strictly smaller than π, contradicting the minimality assumption:

Γ - 1 C ⊥ π 1 D ⊥ B π 2 Γ - 2 P + C ⊥ D ⊥ π : A ⊥ B Γ - 1 C ⊥ D ⊥ B π 2 Γ - 2 P + π 1 π : D ⊥ B
2. or A ⊥ = C ⊥ D, then this C ⊥ D-link must split by Lemma 1, since π 1 is a cut-free PN in splitting condition without other -splitting conclusion in Γ - 1 ; so from π on the l.h.s., we can easily get the non sequentializable PN π on r.h.s.; π is strictly smaller of π, contradicting the minimality assumption:

B π 2 Γ - 2 P + π : π 1 π 1 Γ - 1 Γ - 1 C ⊥ D A ⊥ B C ⊥ D B π 2 Γ - 2 P + π 1 Γ - 1 C ⊥ π : C ⊥ B
Case 2. Assume π contains a splitting cut link, like the leftmost hand side picture below, then we proceed like in Case 1. We reason on π 1 with two sub-cases:

1. either A ⊥ = C ⊥ D ⊥ , then we can easily get, starting from the PN π on the middle side below, a non sequentializable PN π , like the rightmost hand side picture; π is strictly smaller than π, contradicting the minimality assumption:

π 1 π 2 Γ - 1 P + cut (A ⊥ ) -A + Γ - 2 Γ - 1 C ⊥ π 1 D ⊥ π 2 Γ - 2 P + C ⊥ D ⊥ π : cut A Γ - 1 C ⊥ D ⊥ π 2 Γ - 2 P + π 1 π : A D ⊥ A
2. or A ⊥ = C ⊥ D, then this A ⊥ -link must be splitting by Lemma 1, since π 1 is a cut-free PN in splitting condition without any other -splitting conclusion in Γ - 1 ; so, we can easily get, starting from the PN π on the l.h.s., a non sequentializable PN π that is strictly smaller than π (on the r.h.s.), contradicting the minimality assumption.

π 2 Γ - 2 P + π : π 1 π 1 Γ - 1 Γ - 1 C ⊥ D cut A C ⊥ D π 2 Γ - 2 P + π 1 Γ - 1 C ⊥ π : A C ⊥ A
5 Language parsing with Lambek CyMALL PNs

In this section we reformulate, in our syntax, some examples of linguistic parsing suggested by Richard Moot in his PhD thesis [Moo2002]. We use s, np and n as the types expressing, respectively, a sentence, a noun phrase and a common noun. According to the "parsing as deduction style", when a string w 1 ...w n is tested for grammaticality, the types t 1 , ..., t n associated with the words are retrieved from the lexicon and then parsing reduces to proving the derivability of a two-sided sequent of the form t 1 , ..., t n s. Remind that proving a two sided Lambek derivation t 1 , ..., t n s is equivalent to prove the one-sided sequent t ⊥ n , ...t ⊥ 1 , s where t ⊥ i is the dual (i.e., linear negation) of each type t i . Any phase or sentence should be read like in a mirror (with opposite direction).

Assume the next lexicon, where linear implication -• (resp., •-) is traditionally used for expressing types in two-sided sequent parsing:

1. Vito = np; Sollozzo = np; him = np; 2. trusts = (np-•s)•-np = (np ⊥ s) np ⊥ .
Cases of lexical ambiguity follow to words with several possible formulas A and B assigned it. For example, a verb like "to believe" can express a relation between two persons, np's in our interpretation, or between a person and a statement, interpreted as s, as in the following examples: Sollozzo believes Vito.

(1)

Sollozzo believes Vito trusts him.

(2)

We can express this polymorphism by two lexical assignments as follows: Using that, we can move lexical ambiguity into proof net as follows: we give the Lambek CyMALL PN corresponding to the parsing of the additive superposition of sentences (1) and (2). (5 p)

Observe that for slice ϕ p (π) (resp., ϕ p(π)) there exists an additive resolution that is a CyMLL PN corresponding to parsing of sentence (1), see the blue subgraph, (resp., sentence (2); see the red subgraph); these PNs sequentialize as follows:

id 1 np ⊥ ,
(2)

(3)

(5) (4)

6 Conclusions and further works

Stability of sequentialization under cut reduction

Problem: try to give a direct sequentialization avoiding Girard's one.

Proof-structures with explicit n-ary links

Proof-structures with explicit n-ary (& or Contraction) links differ from those one defined in Definition 7 only for the use of n-ary contractions instead of the binary ones, like the next left hand side picture. Then, the notion of slices and switchings (Definitions 8) and proof-nets (Definitions 9) remain unchanged as well the (De-)Sequentialization Theorem 9. Observe that in general the syntax with n-ary contraction or & links is not equivalent to the former one with binary ones. Actually, the picture on the right hand side below shows an example of proof-net with an n-ary contraction (resp., &) link whose monomial sum, pqr+pr+qr+pq+pqr, cannot be factorized in such a way to reduce this n-ary contraction into a sum of only monomial binary sums (contractions). It is not clear whether this new syntax has effects on LambeK proof nets.

Complexity

We aim at studying the class complexity of the CyMALL correctness criterion. What complicate matters from a computational point of view is the fact that, dislike the multiplicative case, we could have chosen different additive proof nets for capturing the polymorphic lexical behavior described by the proof net above.

d

  Definition 4 (CyMLL proof net) A CyMLL PS π is correct, i.e. it is a CyMLL proof net (PN), iff:

  not correct according to our correctness criterion (thus it is not sequentializable) since there exists a A B A B link and a switching S(π) s.t. ¬∀C, (A, B, C) ∈ S(π) ↓ (A,B) , contradicting condition 2 of Definition 4: following the crossing red dotted lines of next figure you can easily verify ∃C, (A, C, B) ∈ S(π) ↓ (A,B) . A, B, C) ∈ S(π) ↓ A.B ∃C, (A, C, B, ) ∈ S(π) ↓ A.B

  empire and spreading) Assume a proof structure π, an eigen weight p and a weight w, then:

  and L is a -link, then π reduces in one (C/ ) step to π (the (C/ ) step is analogous) as follows:

  the weight w of L , resp., L , is split by two different variables, p and q, then π reduces in one (C p /C q ) step to π , like follows ⊕ i )-cut: if L is a C-link and L a ⊕ i=1,2 -link, then π reduces in one (C/⊕) step to π , as follows &)-cut: if L is a C-link and L a & p -link, then π reduces in one (C/&) step to π , like follows

Finally, π 6

 6 is not a correct proof structure: you can easily get an additive switching with a cycle like that one in dashed line. Calculus into CyMALL PNs Definition 13 (Lambek formulas and sequents of CyMALL) Assume A and S are, respectively, a formula and a sequent of CyMALL.

3

  . believes = (np-•s)•-np = (np ⊥ s) np ⊥ ; 4. believes = (np-•s)•-s = (np ⊥ s) s ⊥ .Typically, additives are used for capturing cases of lexical ambiguity. When a word has two possible formulas A and B assigned it, we can combine these into a single additive formula A&B (resp., A ⊕ B). Thus, we can collapse assignments 3 and 4 into a single additive formula assignment as follow:5. believes = ((np-•s)•-np)&((np-•s)•-s) = ((np ⊥ s) np ⊥ )&((np ⊥ s) s ⊥ ).

wqp

  j (with 1 ≤ i, j ≤ n) w i .w j = 0 Fully local cut reduction and parsing contraction Problem: try to define a retraction system stable under a strongly normalizing cut reduction that implements a commutative cut elimination step & p /C that does not duplicate the empire E p as follows Observe that, dislike the C/& cut reduction step given before, this new C/& cut reduction step breaks the monomial condition GPS. This problem has been formulated and solved in[LM2008].

  Theorem 1 (stability of PNs under cut reduction) If π is a CyMLL PN that reduces to π in one step of cut reduction, π π , then π is a CyMLL PN.

	Proof -Observe that w.r.t. Definition 4 condition 1 follows as an almost immediate conse-
	quences of the next graph theoretical property ([Gir2006], pages 250-251):
	Property 1 (Euler-Poicaré invariance) Given a graph G, then ( CC -Cy) = ( V -E),
	where CC, Cy, V and E denotes the number of, respectively, connected components, cycles,
	vertexes and edges of G.
	Condition 2 of Definition 4 follows by calculation. Assume π reduces to π after the reduction of
	a cut between (X Y ) and (Y ⊥ X ⊥ ) and assume, by absurdum, there exist a -link labeled
	by a formula A B s.t. the triple (A, C, B) occurs in this wrong cyclic order in a seaweed S(π )
	restricted to A, B, S(π ) ↓ (A,B) , for a pending leave C occurring in this restriction, i.e., (A, C, B) ∈
	S(π ) ↓ (A,B) . Then, two of the three paths A , B and C must go through (i.e., they must
	contain) the two (sub)cut-links, cut 1	X X ⊥	and cut 2	Y Y ⊥

  Lambek proof is any derivation built by means of the CyMALL inference rules whose premise(s) and conclusions are CyMALL Lambek sequents. Definition 14 (Lambek CyMALL proof net) We call Lambek CyMALL proof net any Cy-MALL PN whose edges are labeled by LFs or negation of LFs and whose conclusions are a Lambek sequent. Corollary 2 Any Lambek CyMALL proof net π is stable under cut reduction, i.e., if π reduces in one step to π , then π is a Lambek CyMALL proof net too.

  np id 2 s ⊥ , s id 3 np, np ⊥ s ⊥ np, np ⊥ , s np ⊥ , np (s ⊥ np), np ⊥ , s ⊥ id 3 np, np ⊥ s ⊥ np, np ⊥ , s np ⊥ , np (s ⊥ np), np ⊥ , s id 4 s, s ⊥ id 5 np, np ⊥ s ⊥ np, np ⊥ , s np ⊥ , np (s ⊥ np), np ⊥ , s (s ⊥ np), np ⊥ , s np ⊥ (np (s ⊥ np)), np ⊥ , s (s ⊥ np), np ⊥ , s (np ⊥ (np (s ⊥ np))) np ⊥ , s (s ⊥ np), np ⊥ , s

	np ⊥ , np him id 1 np ⊥	id 2 np him trusts Vito np trusts Vito s, s s ⊥	np ⊥	s	believes s ⊥	np ⊥ Vito np	(1)	s ⊥ believes np (2) Sollozzo np ⊥	np s	np ⊥ Sollozzo (3)	s

In the related literature, this example is commonly considered a "measure of the satisfiability degree" of correctness criteria of non commutative proof nets. Let us say, a "good" correctness criterion for non-commutative logic should not recognize this structure as a correct proof net.

We say that a conclusion link &p of a GPN π is toggling whenever the restriction of π w.r.t. p and the restriction of π w.r.t. p are both correct GPSs. We call restriction of π w.r.t. p (resp., p) denoted π p (resp., π p), what remains of π when we replace p with 1 (resp., p with 1) and keep only those vertexes and edges whose weights are still non zero (see details in[Gir1996]).


Elixabete Rezabal
email: elixabete.rezabal@polytechnique.edu

Gilles Frison
email: gilles.frison@polytechnique.edu

Estimating π binding energy of N-heterocyclic carbenes: the role of polarisation

Keywords: Density Functional Theory, Energy Decomposition Analysis, Natural Orbitals for Chemical Valence, donor-acceptor interactions

In this work, the tuneability of the π acceptor or donor properties of a set of N-heterocyclic carbenes (NHCs) with a wide spectrum of electronic characteristics is established by means of density functional theory (DFT) and energy decomposition analysis (EDA) tools. Even though the main orbital interaction contribution to the NHC coordination is the σ donation, a significant contribution of the π interactions to the bond is observed. By means of carefully selected coordination sites, different contributions to the π interactions could be identified and isolated. It includes not only the well known back donation and donation interactions, but also the intrafragment polarisation, which has not been considered in previous studies. This can be obtained through the use of the extended transition state method for energy decomposition analysis combined with the natural orbitals for chemical valence (ETS-NOCV) and the constrained space orbital variation (CSOV) analysis. The contributions vary with the position of the heteroatoms and the presence of exocyclic substituents; the donation/backdonation π interactions between NHC and the coordination site can range between 2 and 61 % of the total π orbital interactions, while the rest is owed to intrafragment polarisation. Our results do not only contribute to the understanding of the electronic structure of NHC-based complexes, giving ways to improve their catalytic properties, but also provide comprehension on the modelisation methods used to study their donor-acceptor interactions.

INTRODUCTION

N-heterocyclic carbenes (NHCs) have been successfully used in a variety of applications, as organocatalysts [1][2][3] , or ligands to other species 1,[4][5][6][7] , mainly based on their good σ nucleophilic characteristics [8][9][10][11] . In the last years, growing interest has been focused on their π donor and acceptor properties [12][13][14] , generally as ligands to transition metals (TMs) [15][16][17][18][19][20][21] , observing that NHCs present π basicity or acidity, depending on the electronic structure of the metal 22 , and can vary the catalytic properties of the latter 23 . Works in the literature surprisingly show that even the formal d 0 TMs show a significant amount of π backdonation, around 65% of the total π bonding contribution. This amount increases with increasing the d-electron count and takes on values around 90% for d 10 complexes 22 . In other words, complexes with a low d electron count, show a contribution both from π donation and from π back donation; when species with more d electrons are considered, π back bonding dominates the interaction of the π orbitals of the NHC with the d orbitals of the metal center. This implies that the π interactions modify the population of the d atomic orbitals in the metal center, which can backdonate electron density to the NHC even in formally d 0 TM complexes, or accept electron density in formally d 10 TM complexes. Consequently, the interaction between the partially filled d orbital of the metallic fragment (d yz in the section (a) of Fig 1) and the partially filled π orbital of the NHC gives rise to simultaneous donation and backdonation interactions. This makes difficult the separate study of donation and backdonation interactions, jeopardising to some extent the analysis of the π donor and acceptor properties of NHCs. Different strategies have been used in the literature for estimating separately these two contributions, as the deletion of selected orbitals 22,24 , natural bond orbital (NBO) analysis 25 , or the extended transition state (ETS) method for energy decomposition analysis combined with the natural orbitals for chemical valence (NOCV) theory. 26,27 . Even if these procedures have significantly increased our understanding of the π donor-acceptor interactions, the interpretation of the results is hindered by the limitations of these approaches and the complexity of the systems under study, which prevent to associate accurately each energetic term to a single contribution (vide infra).

In the quest of a more straightforward access to the NHC π interactions, simpler coordi-nation sites establishing the π interaction with atomic orbitals rather than with molecular orbitals are chosen in this work. The coordinating groups bear either empty or doubly occupied atomic orbitals, and therefore can be expected to undergo electron density transfer only in one direction, relying exclusively on NHC π donor or acceptor properties. Most of the research published regarding the π properties of NHCs has been devoted to imidazolylidenes and pyrimidinylidenes. Tuning the π properties of NHCs by manipulating the position of the heteroatoms in the NHCs has yet to be considered in literature, even though, together with the exocyclic substituents, it has been observed to play a major role on these properties 27,29 .

In the present work, the role of endocyclic and exocyclic N atoms in the ring is considered (see Fig. 2). Different positions of the heteroatoms will be considered, giving rise to normal

(1,2 and 3), remote (5 30 ,6 and 7) and mesoionic (4 31 , 5,6 and 7) NHCs.

METHODOLOGY

In this work, the bond between H + , BH 2 + and F + and the NHCs presented in Figure 2 is studied. M06HF/TZVP level, which has been shown to give the best results in terms of binding energy (see ESI) has been used for optimizations and frequency calculations (in order to ensuring the lack of imaginary modes) carried out in all the complexes, together with natural bond orbital (NBO) analysis 32 .

The interaction energy associated to the bond between the carbenes and the cations corresponds to the interaction of two fragments which posses the local equilibrium geometry of the final molecule, and which both have an electronic structure suitable for bond formation.

A partition of this interaction in three terms, namely the electrostatic interaction ∆E elst , the Pauli repulsion ∆E P auli and the orbital interaction energy ∆E oi , is performed by an energy decomposition analysis (EDA), following the well-known Morokuma-like energy partition of the bond using the ADF program (version 2013.01a) 33 .

∆E oi can be further broken down into contributions from the orbital interactions within the various irreproducible representation of the overall symmetry group of the system (see Supporting Information).

The decomposition of the orbital interactions can be extended by performing additional constrained space orbital variation (CSOV) calculations 34,35 , as implemented in ADF. CSOV calculations permit to perform the bond decomposition analysis excluding selected virtual orbitals. Even if the change on the orbital space might lead to a slight deviation in the estimation of interaction energies, it is very valuable in order to understand the fundamentals of the NHC-coordination site interplay.

The extended transition state (ETS) 36,37 method for energy decomposition analysis combined with the natural orbitals for chemical valence (NOCV) [38][39][40] theory, computed at the same level of theory, is used as an alternative approach to decompose the ∆E oi . Within this framework, it is possible to separate the orbital interactions between the NHC and their coordination site into contributions related to the deformation density due to the bonding.

Each individual deformation density contribution is associated with an energy contribution to the total interaction energy. Complementary NOCVs with opposite sign and identical absolute energy eigenvalues can be grouped together to describe charge-transfer channels between the molecular fragments. Visualisation allows the assignment of these NOCV pairs to donating and backdonating processes and the identification of the participating fragment orbitals.

All the compounds studied present a planar ring, therefore resulting in symmetric complexes, with the exception of 5, whose exocyclic heteroatoms are pyramidalized. The electron density decrease on the C carbene , the amount of which is connected to the electronegativity of the coordination site, leads to the enhancement of π delocalisation, mainly from nitrogen atoms to C carbene , and therefore, decrease of C carbene -X,Y distance. A hypothetical π donation from the cation would have the opposite effect, and competition between both donations would take place. In the studied complexes we find that C carbene -X,Y bonds are longest for BH 2 + , followed in decreasing order by H + and F + , as a result of the increasing σ acceptor nature of the coordinating group. Even if we can expect a stronger σ acceptor character of F + as compared to H + , the differences in C carbene -X,Y distances are small, and in some cases, the ordering is reversed, due to the competition between the nitrogen atoms and F + to donate charge to C carbene .

Regarding the cation-NHC bond, H + binds the carbenes at a rather constant bond length of around 1.080 Å. F + forms bonds between 1.289 Å, in the case of NHC 2, and 1.338 Å with the carbene 7. BH 2 + forms the longest bonds, between 1.520 Å in BH 2 + -7 and 1.577 Å in BH 2 + -2, which correspond to the opposite trend compared to F + (vide infra).

Strong correlation is found between the cation interaction energy and the eigenvalues of the NHC σ HOMO lone pair orbital (see Fig. S1), as already observed previously 29,41,42 .

However, lower correlation is found for BH 2 + -NHC complexes (R 2 =0.9012), as compared to that of H + -NHC (R 2 =0.9601) and F + -NHC (R 2 =0.9764) systems; BH 2 + -5 seems particularly interesting on this regard, since it deviates significantly from linearity. This feature can be traced back to an important contribution of π orbital interactions to the BH 2 + total interaction energy (vide infra).

Further insight on the bond nature is obtained by performing EDA analysis on these species, which permits the decomposition of the bond energy into Pauli repulsion (∆E P auli ), electrostatic interaction (∆E elst ) and orbital interaction (∆E oi ) terms (Table S2). The composition of the bond is rather constant for each coordination site through the set of NHCs: 2, which correlates with the large bond length previously observed for this complex.

F + relies
The sum of ∆E P auli and ∆E elst gives the term ∆E 0 (see Table S3), which reflects the interaction between both fragments without electron transfer and orbital mixing. A large repulsive ∆E 0 is obtained for F + (between 252.7 and 292.4 kcal/mol), arising from its fully occupied orbitals. Slightly negative or thermoneutral ∆E 0 values are obtained for BH 2 + , except for the case of carbenes 5 and 7 (6.9 kcal/mol and 5.6 kcal/mol, respectively), which can be related to the steric interactions between the cation and the exocyclic substituents.

Finally, H + , due to its lack of Pauli repulsion, presents a ∆E 0 dominated by the attractive electrostatic forces. S2). This term will be further decomposed and analysed in the following section.

Orbital interaction decomposition and analysis

∆E oi can be decomposed into the irreducible representations of the symmetry group of the molecule by performing an EDA analysis. This permits to understand the nature of the bonds, and to identify the interactions that conform it. Due to the symmetry limitations on the chosen compounds, and for the sake of brevity, the complete analysis for NHC 1, which presents C 2v symmetry, is presented here. The energy will be decomposed into a interactions, instead, are less significant for all the coordination sites and account for 3.8, 5.2 and 5.7 %, respectively. Finally, as expected, the contribution of δ interactions to the bond is negligible for any of the cations considered.

Surprisingly, interaction between NHC and H + imply π (and to a lower extent π // ) contribution to the bonding, whereas only σ interaction is expected. In order to identify the origin of these contributions, we perform CSOV calculations on these systems by deleting selected vacant orbitals. Deletion of the virtual orbitals of one fragment turns off all donation interactions into its orbitals, which allows to isolate and analyse the different possible interactions: (i) the π donation takes place from the occupied π orbitals of the NHC to the virtual π orbitals of the coordination site, and can be estimated by deleting the virtual orbitals of NHC (right to left arrow in As it has already been discussed in the literature 22,43 , synergic and residual contributions to the orbital interaction energy arise from the different choices of variational space partitioning. Therefore, even if the following discussion based on CSOV data uses the numbers as obtained from the calculations, it must be remembered that these are roughly estimated and attention should rather be focused on the qualitative understanding of the different contributions to the π bond.

For H + -1, the deletion of empty b 1 symmetry orbitals in the NHC depletes almost completely the b 1 term (2.5 kcal/mol in Table 3) happening when all the empty orbitals are available (25.1 kcal/mol) (see Table 3). This difference accounts for 22.6 kcal/mol, and can be assigned to polarisation (or intra fragment electronic reorganization) within NHC, considering that H + has no electronic charge to backdonate to 1, or to polarise. The presence of a positively charged σ acceptor results in the polarisation of the ring π system towards the C carbene , which is included as π interaction in EDA analysis.

BH The occupied p y orbital allow for F + to perform the similar calculation by deleting the empty b 1 symmetry orbitals of the cation. We then obtain throughout this second way a second value, 39.4 kcal/mol, which should originate from the sum of the polarisation in the ring and the backdonation from the cationic moiety, whereas the polarisation within F + is now estimated in 4.1 kcal/mol (43.5-39.4 kcal/mol). As indicated previously, the different number of orbitals used in the estimation of interaction energies in the CSOV method explains the deviation in the different values and limits the use of this tool to a qualitative approximation to the interactions. Nevertheless, this analysis indicates that the π contribution to the bonding is not restrained to π donation and π backdonation, but also includes non negligeable π polarisation within the fragments, which can be estimated from the π contribution in the protonated complexes.

A similar analysis can be done in b 2 symmetry, resulting in a internal in plane ring rearrangement of 8.5 kcal/mol (9.5-1.1), i.e. 14 kcal/mol below the value obtained in b 1 symmetry, and negligible π // donation from NHC to BH 2 + (see Table 3).

ETS-NOCV analysis

The qualitative comprehension of the bond obtained thanks to the CSOV method will be used as a guide for a more quantitative understanding of the interactions, by means of the ETS-NOCV method. The latter will allow to obtain unbiased values for the different contributions and to extend the study to systems without symmetry.

NOCV analysis permits the visualisation of the electron density loss and gain in the system due to the bond formation and to calculate the energy contribution associated to it (see Fig 4). Similar NOCV shapes are found for all the NHCs included in this study (full analysis available in ESI), which can be assigned to recognisable σ, π // and π interactions even in those systems without symmetry, allowing to extend the above analysis to all the NHCs, regardless their geometrical characteristics. Many NOCV pairs are found for each complex;

in this work, we will consider only those related to an interaction energy of more than 1 kcal/mol. Comparing the results of the π interactions to those obtained by EDA analysis (see Tables 2, S4 and S6), very satisfactory agreement is found between the π interaction contributions of both partition schemes. As already observed in the EDA analysis, the σ interactions are the most significant ones (see Table S4), and very similar σ interactions are found for H + and BH 2 + (between 136.5 and 168.6 kcal/mol), while F + results in much larger interactions (from 677.7 to 693.5 kcal/mol).

Even if, as observed by EDA analysis, the bond is dominated by the σ interaction, the ∆E π contribution is not negligible for any of the cations, supposing between 9 and 15 % of the orbital interactions for H + complexes, 13-19% in the case of BH 2 + , 5-6 % in the case of F + . These numbers are not far from those found for TM-carbene bonds 14,16,22 , where the contribution of the π system to the orbital interactions was estimated to be between 10 and 25 %.

The quantitative agreement between EDA and ETS-NOCV may be extended to the specific nature of the interactions. The NOCV analysis of the H + systems shows the π manifold reorganisation in the carbene upon protonation. In addition to this reorganisation, BH 2 + and F + complexes bear interactions of the coordination site with the π system of the ring (Figure 4).

π NOCV pairs denote electron density loss (light grey surfaces on Fig. 4) mainly on the cation in the case of F + and on the carbene ring in the case of BH 2 + . Instead, the electron density gain (black surfaces on Fig. 4) is observed on the cation-NHC bond, for both coordination sites. Electron density gain is observed in F + , in perfect agreement with the CSOV analysis performed above, pointing out to a significant electronic rearrangement of the F + .

The π // charge transfer occurs from the ring and cations to the C carbene . When F + is considered as the coordination site, electron density loss is observed also in the divalent carbon atom and the electron density gain is extended to the p x orbital of the coordination site.

This picture is, overall, in consonance with the description of the bond provided by the CSOV analysis on 1, pointing out to the importance of the intrafragment reorganisation, and the separation of donation or backdonation interactions in the coordination sites chosen.

Furthermore, it is observed that in F + -NHC complexes the C carbene receives electron density from both the ring and the cation, what results in a mitigated reorganisation of the ring.

Considering the CSOV analysis performed above, the different contributions to the π interaction can be extracted from the ETS-NOCV data. The intrafragment reorganisation of NHCs in presence of BH 2 + can be estimated to be equal to the π contribution calculated in protonated systems. Furthermore, we can assume that the additional π interactions found in BH 2 + correspond to the net (BH 2 + ←NHC) π donation. In the case of F + , this difference arises from the net (F + →NHC) π backdonation plus a polarisation in F + . The polarisation within F + , which has been shown to be rather constant in the CSOV analysis, can be roughly estimated to be around 10 kcal/mol for the different NHC complexes, as

shown by the difference between the π interaction for H + (which should be inexistant) and atoms. H + -4, being identical to H + -1, presents a smaller polarisation (19.9 kcal/mol) since in this case the C carbene has only one heteroatom in α position. The protonation of 5 also induces a significant reorganisation within the ring (22.9 kcal/mol), in which both endocyclic and exocyclic donor groups donate π electron density to the divalent carbon atom. 7, which maintains the exocyclic heteroatoms but not the endocyclic ones, undergoes a remarkably weaker reorganisation (16.9 kcal/mol). On the contrary, in the absence of the exocyclic heteroatoms, 6 shows a rearrangement of 19.2 kcal/mol. Therefore, we can conclude that endocyclic N atoms polarise the π system towards the C carbene more efficiently. Finally, H + -3, being the same compound as H + -6, presents a stronger polarisation towards the coordination site (24.1 kcal/mol), since it has a α NH-NH moiety, in agreement with the H + -1/ H + -4 pair, suggesting that the α heteroatoms promote the delocalisation of the π electrons towards the C carbene more efficiently than β heteroatoms.

Besides the ring reorganisation, in BH This significantly large π donation interactions are reflected in their total affinity towards BH 2 + , which is higher than initially suggested by the σ-HOMO eigenvalue (see Fig S1).

Furthermore, it explains the short C carbene -B bond length observed for both 5 and 7 (Table 1 and Figure S9).

The small influence of the -NH-NH-bridge on the π donating capacity of 5 is confirmed by deleting the exocyclic substituents, which results in a net donation of only 8.3 kcal/mol in BH 2 + -6. By changing the coordination site to BH 2 + -3, a similar yet slightly lower donation is observed (5.8 kcal/mol). Among those NHCs with no exocyclic substituents, the largest net donation occurs with 4 (10.4 kcal/mol). 1, with an interaction site with two α heteroatoms, presents a lower donation ability (6.8 kcal/mol). Therefore, even if the total π interaction in 1 is higher than in 4 (34.1 vs 30.4 kcal/mol), only 19.9% of it is net donation towards the cation, while it accounts for 34.4% in the latter. In this case, the electronegativity of the CH-CH moiety in 1 improves the donation, as is evidenced by comparing it to 2 (1.1 kcal/mol).

In agreement with the literature 27 , no descriptor could be found for the total ∆E π energy.

Interestingly, the donation energy correlates (R 2 =0.913) with the π-HOMO eigenvalue of the bare NHC (see Figure 6); the higher the energy of the π-HOMO orbital, the better donor capacity is observed for the NHC. The donor capacity of the NHCs is also reflected in the bond distance with the cation, which decreases as higher is the donation energy (see Figure S9).

A similar partition can be done also in F + -NHC complexes, keeping in mind that the NOCV pairs show a smaller reorganisation within the NHCs as compared to H + and BH

CONCLUSIONS

Besides the crucial role of σ interactions in the total orbital interactions, we have observed for various NHCs that the role of π interactions is very significant even in main group element coordination sites. Overall, the contribution of π interactions to the bond is comparable to that found in TM fragments in the literature 22,27 .

The π interactions can be decomposed into intrafragment reorganisation, and backdonation or donation contributions between the fragments. In particular, we have found that the π polarisation within the NHC ring is a significant or even the main contribution (up to 90% ) of the computed π interaction. Consequently, we could postulate that decomposing the interaction only in donation/backdonation contributions results in their unreliable estimation. The scheme usually employed to analyse the TM-NHC π interactions might overestimate both the donation from the NHC and the back donation to the NHC, since it hides a fundamental part of the π contributions, namely the fragment reorganisation.

From this energetic decomposition, it has been observed that MICs show the best donor properties, while normal NHCs have remarkable acceptor properties. Furthermore, it becomes possible for the first time to nicely correlate for example the π donation with the π HOMO eigenvalue of the bare NHC, or the cation-NHC bond length.

We believe that the study presented here will contribute significantly not only to the intimate comprehension of the intrinsic π bonding characteristics of NHCs, but also to the understanding and perfectioning of the computational tools to study metal-ligand interactions. This could facilitate the analysis of experimental quantification of the NHCs electronic properties [44][45][46] , as well as the design of catalytic TM-NHC complexes with the desirable electronic properties.

  Besides H + , which can not induce any π donation or backdonation and has been chosen to give reference interaction energy values brought by the formation of a purely σ bond, two different cationic coordination sites have been chosen: on one hand, the dihydro borenium cation, BH 2 + 28 (see section (b) in Fig 1), with an occupied in plane p x orbital and two empty p orbitals (out of plane, p y , and along the C carbene -cation axis, p z ). In this case, the cation will behave as σ acceptor in the z axis and π acceptor in the y axis, enabling the π donation from NHC. On the other hand, F + (see section (c) in Fig 1) includes an empty p z orbital along the C carbene bond axis and fully occupied p x and p y orbitals. It is expected that F + will interact with the π system of the NHC via backdonation from the doubly occupied p orbitals. While the three coordination sites are σ acceptors, BH 2 + and F + are π acceptor and donor, respectively, and as such, NHCs will behave as π basic or acid moieties upon their binding. Similar description can be achieved for in plane π interactions (noted π // ).

Fig 3 )

 3 ; (ii) the π backdonation occurs from the occupied orbitals of the cationic fragment to the virtual π orbitals of the NHC and can be estimated by deleting the virtual orbitals of the cation (left to right dashed arrow in Fig 3); (iii) the polarisation is ascribed to the reorganisation inside each fragment (blank vertical arrows in Fig 3).

  Analysis of the CSOV values for F + shows a parallel behaviour to that in b 1 symmetry. The sum of the π // backdonation from F + and the NHC π // reorganisation is estimated between 16.4 and 25.3 kcal/mol, once again 14 kcal/mol below the values obtained in b 1 symmetry (30.7 and 39.4 kcal/mol), indicating that π and π // backdonation have apparently the same intensity. Similarly, the π // polarisation within F + amount to between 4.6 and 12.6 kcal/mol, in agreement with the values obtained in the b 1 symmetry (4.1 and 12.8 kcal/mol).

F

  scheme is presented in Fig 5, and full data is provided in ESI. The amount of energy retrieved from the ring electronic density redistribution towards the C carbene (white in Fig 5) changes with the nature of the NHC (16.9 to 27.3 kcal/mol). Nevertheless, it is the principal contribution to the total π interaction in BH 2 + complexes, with the exception of 7-BH 2 + . Highest reorganisation energy is displayed by 1, (27.3 kcal/mol), in which the N atoms in α position donate π electron density to the divalent carbon atom. Instead, 2, also having two heteroatoms in α, results in a weaker reorganisation (21.5 kcal/mol) due to the sp 3 hybridised C atoms, which have worse donor ability than sp 2 hybridised C

2 + 5 .

 25 bound complexes (seeFigures 4 and S1-8 in ESI), and therefore, an overestimation of the reorganisation contribution in this case must be assumed. Similarly, the 10 kcal/mol polarisation within the coordination site is probably overestimated by the CSOV analysis. This uncertainty is denoted by error bars in Figure4.Nevertheless, it can be observed that the electronic reorganisation in the fragments is a noticeable contribution in the total π interaction. The net backdonation provides between 8.3 and 26.7 % of the π interaction, while the rest is due to intrafragment reorganisation. The absence of exocyclic ( 6-F + ) or endocyclic ( 7-F + ) N atoms increases the backdonation to 8.9 and 8.2 kcal/mol, respectively, compared to the low (3.0 kcal/mol) back donation obtained for Changing the binding site from 6-F + to 3-F + results yet in a better backdonation ability, 9.8 kcal/mol. The low backdonation in 1-F + , 7.7 kcal/mol, is increased to 11.1 kcal/mol by the presence of the CH 2 -CH 2 moiety in the ring ( 2-F + ), and by the change in the coordination site to 4-F + (10.9 kcal/mol).

Figure 1 :

 1 Figure 1: Schematic representation of the interactions taking place between a NHC and a metallic fragment (a), BH 2 + (b) and F + (c).

Figure 2 :

 2 Figure 2: NHCs studied in this work.

Figure 3 :Figure 4 : 20 Figure 5 :

 34205 Figure 3: Schematic representation of the different contributions to the π interaction between the coordination site and the NHC

Figure 6 :NHC-BH 2 +

 62 Figure 6: Correlation between the (BH 2 + ←NHC) donation interaction for BH 2 + -NHC complexes and the π-HOMO eigenvalue of the bare NHC. Empty circles denote total ∆E π interactions, solid circles stand for (BH 2 + ←NHC) donation energy.

Table 3 :

 3 CSOV analysis of the contribution of the symmetry groups b 1 and b 2 on the ∆E oi of carbene 1, in kcal/mol. The first column specifies the virtual orbitals that have been deleted for the given fragment.

  mainly on orbital interactions (72.2% in average) with few contribution of electrostatic interactions (around 27.8%), similarly to H + (70.2% and 29.8%, respectively) while BH 2 + depends equally on both (50.8% and 49.2%, respectively).

∆E P auli and ∆E elst contributions are strongest in the case of F + (see Table S2), due to its full p orbitals, and much lower for BH 2 + and H + , in decreasing order, due to the lower electron count. Overall, the electrostatic interactions and Pauli repulsions remain rather constant through the set of NHCs. As an exception, particularly low electrostatic contribution (-159.3 kcal/mol) and Pauli repulsion (158.1 kcal/mol) are observed for BH 2 + -

  1 , a 2 , b 1 , and b 2 contributions (see Table2), which correspond to σ, δ, π and π // interactions, respectively. As expected, the σ interaction provides the largest part of the bond, being one order of magnitude stronger than π and π // interactions. π and π // interactions are, in absolute values, strongest for F + , followed by BH 2

+ and H + , but their contribution to the total orbital interaction is smaller; π interactions represent only the 5.7 % of the F + -1 bond, while this contribution rises to 13.8 and 19.8 % with H + and BH 2 + , respectively. π //

  2 + bears empty p y orbitals able of receiving π electronic density from the NHC, and no occupied orbitals on the same symmetry. Therefore, deleting the b 1 symmetry orbitals of the carbene should lead to pure (BH 2 + but can potentially donate charge to the NHC π system. Deleting the empty b 1 orbitals of the carbene results in a contribution of 12.8 kcal/mol in the b 1 symmetry, significantly lower than the contribution for the complete system (43.5 kcal/mol). Following prior analysis for H + and BH 2 + , this means that NHC π reorganisation and π backdonation from F + contribute 30.7 kcal/mol (43.5-12.8) whereas polarisation within F + accounts for 12.8 kcal/mol. Assuming that the intra fragment electronic reorganisation is similar to that obtained on H + species, we can estimate the net backdonation on 16.7 kcal/mol.

+ ← NHC) π donation. This charge transfer is worth 13.3 kcal/mol for 1. The difference between this number and that accounting for all the empty b 1 orbitals in the system (35.7 kcal/mol) is, in fact, in good agreement with the intra fragment reorganisation previously estimated in H + complex (22.5 kcal/mol vs 22.6 kcal/mol). Consequently we can assume that the π-reorganisation within the NHC is similar for both H + and BH 2 + coordination, and that the π donation from NHC to the BH 2 + coordinating group accounts roughly for a third of the total π contribution.

F + presents a doubly occupied p y orbital which mainly prevents π donation from the NHC to F Therefore, it is observed that, even if the π interaction initially calculated for F + is significantly larger than that taking place with BH 2 + , the net donation to BH 2 + (13.3 kcal/mol) and backdonation from F + (16.7 kcal/mol) interactions are comparable.

  2 + complexes we observe the net π donation from the NHC, which varies between 1.1 kcal/mol and 26.2 kcal/mol, accounting for the 4.9 % and 60.8 % of the π interaction, respectively (see black bars in Fig 5). Our results indicate that mesoionic NHCs (4-7) induce larger π donation than normal NHCs (1-3), in agreement with what has been described previously 8 . Furthermore, net donation towards the cation is highly favoured by the π delocalisation of the lone pair of exocyclic N atoms in BH 2 + 5and BH 2 + -7, accounting for 47.2 and 60.8 % of the π interaction, respectively. In this case, the endocyclic N atoms in 5 result in a weaker net π donation (20.5 vs 26.2 kcal/mol).

Table 1 :

 1 X-C carbene -Y angle (in degrees, X and Y being C or N atoms), C carbene -X,Y and C carbene -Ligand distances (in Å , L being B, H and F atoms) for all the systems studied, computed at the M06HF/TZVP level.

		.6	1.356	-	1.535	105.7	1.339	-	1.076	107.1	1.330	-	1.274	109.3	1.322	-
	2	103.7	1.344	-	1.577	111.5	1.311	-	1.083	112.8	1.306	-	1.273	114.7	1.305	-
	3	101.7	1.325 1.440 1.549	107.3	1.336 1.392 1.079	108.2	1.335 1.382 1.280	109.7	1.340 1.380
	4	100.5	1.390 1.383 1.539	104.5	1.395 1.365 1.076	106.4	1.373 1.358 1.285	108.2	1.374 1.352
	5	98.6	-	1.385 1.508	104.1	-	1.410 1.077	106.0	-	1.387 1.317	108.2	-	1.383
	6	101.4	-	1.393 1.535	105.6	-	1.393 1.076	105.9	-	1.387 1.295	107.4	-	1.384
	7	99.2	-	1.387 1.490	105.7	-	1.407 1.078	105.8	-	1.389 1.320	110.5	-	1.379

Table 2 :

 2 Decomposition of ∆E oi (in kcal/mol) between the NHC 1 and the cationic groups.

ACKNOWLEDGMENTS

This work was granted access to the HPC resources of CINES under the allocation x2014086894 made by GENCI (Grand Equipement National de Calcul Intensif).