Roberto Bonato

Christian Retoré

Learning Lambek grammars from proof frames

In addition to their limpid interface with semantics, categorial grammars enjoy another important property: learnability. This was first noticed by Buskowsky and Penn and further studied by Kanazawa, for Bar-Hillel categorial grammars. What about Lambek categorial grammars? In a previous paper we showed that product free Lambek grammars where learnable from structured sentences, the structures being incomplete natural deductions. These grammars were shown to be unlearnable from strings by Foret and Le Nir. In the present paper we show that Lambek grammars, possibly with product, are learnable from proof frames that are incomplete proof nets. After a short reminder on grammatical inference à la Gold, we provide an algorithm that learns Lambek grammars with product from proof frames and we prove its convergence. We do so for 1-valued also known as rigid Lambek grammars with product, since standard techniques can extend our result to k-valued grammars. Because of the correspondence between cut-free proof nets and normal natural deductions, our initial result on product free Lambek grammars can be recovered. We are sad to dedicate the present paper to Philippe Darondeau, with whom we started to study such questions in Rennes at the beginning of the millennium, and who passed away prematurely. We are glad to dedicate the present paper to Jim Lambek for his 90 birthday: he is the living proof that research is an eternal learning process.

Presentation

Generative grammar exhibited two characteristic properties of the syntax of human languages that distinguish them from other formal languages:

1. Sentences should be easily parsed and generated, since we speak and understand each other in real time. 2. Any human language should be easily learnable, preferably from not so many positive examples, as the study of first language acquisition shows. ⋆ I am deeply indebted to my co-author for having taken up again after so many years our early work on learnability for k-valued Lambek grammars, extended and coherently integrated it into the framework of learnability from proof frames. ⋆⋆ Thanks to CNRS and to IRIT for my sabbatical year, to the Loci ANR project for its intellectual and financial support, to C. Casadio, M. Moortgat for their encouragement and to A. Foret and to the anonymous reviewers for their helpful remarks. Formally, the first point did receive a lot of attention, leading to the class of mildly context sensitive languages [START_REF] Joshi | The convergence of mildly context-sensitive grammar formalisms[END_REF]: they enjoy polynomial parsing but are rich enough to describe natural language syntax. A formal account of learnability was more difficult to find. Furthermore, as soon as a notion of formal learnability was proposed, the first results seemed so negative that the learnability criterion was left out of the design of syntactical formalisms. This negative result can be stated as follows: any class of languages that contains all the regular languages cannot be learnt. It should be explained why this result was considered so negatively. By that time, languages were viewed through the Chomsky hierarchy (see figure 1). Given that regular languages are the simplest class and that human languages were known to go beyond regular languages, it seemed that there could not exist an algorithm that learns a large class as the one of human languages. This pessimistic viewpoint was erroneous for at least two reasons:

-The class of human languages does not include all regular languages and it is likely that it does not even include a single regular language.

The figure 1 gives the present hypothesis on the class of human languages. -The positive examples were thought to be sequences of words, while it has been shown long ago that grammatical rules operate on structured sentences and phrases (that are rather trees or graphs), see e.g. [START_REF] Berwick | Poverty of the stimulus revisited[END_REF] for a recent account. Although we shall recall it more precisely in the first section of the present paper, let us make some comments on Gold's notion of learning a class of languages generated by a class of grammars G. According to Gold, a learning function φ maps a sequence of sentences e1, . . . , en to a grammar Gn = φ(e1, . . . , en) in the class G in such a way that, when the examples (ei) i∈N enumerate a language L(G) of a grammar G in G i.e. L(G) = {ei i ∈ N} there exists an integer N such that for all n > N the grammars Gn are constantly equal to G N which generates the same language i.e. L(Gn) = L(G) = {ei i ∈ N}. The fundamental point is that the function learns a class of languages: the algorithm eventually finds out that the enumerated language cannot be any other language in the class. This means that the very same language can be learnable as a member of a learnable class of languages, and unlearnable as the member of another class of languages. Although surprising at first sight, this notion according to which one learns in a predefined class of languages is rather compatible with our present knowledge of first language acquisition.

Overtaking the pessimistic view of Gold's theorem, Angluin established in the 80s that some large but transversal classes of languages were learnable in Gold's sense. [START_REF] Angluin | Finding patterns common to a set of strings[END_REF] Regarding categorial grammars, Buszkowski and Penn defined in late 80s [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF][START_REF] Buszkowski | Discovery procedures for categorial grammars[END_REF] an algorithm that learns basic categorical grammars from structured sentences, that are called functor-argument structures, and Kanazawa proved in 1994 that their algorithm converges: it actually learns categorial grammar in Gold's sense. [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF][START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF] The result in the present paper is much in the same vein as the ones by Buskowski, Penn and Kanazawa.

Section 2 We first recall the Gold learning paradigm, identification in the limit from positive examples.

Sections 3, 4 Next we briefly present Lambek categorial grammars with product, and define their parsing as the construction of cut-free proof nets. We also introduce the structures we shall learn from, that we call proof frames. Indeed, Lambek grammars (with or without product) ought to be learnt from structured sentences since Foret and Le Nir established that they cannot be learnt from strings [START_REF] Foret | Lambek rigid grammars are not learnable from strings[END_REF]. Informally, proof-frames are name-free parse-structures, i.e. name-free proof-nets, just like functor-argument structures are name-free natural deduction used to learn basic categorial grammars.

Sections 5,6,7 After a reminder on unification in relation to categorial grammars, we present our algorithm that learns rigid Lambek categorial grammars with product from proof frames. We illustrate it on examples involving introduction rules (that are not part of basic categorial grammars) and product rules (that are not part of product free Lambek grammars). We then prove the convergence of this algorithm.

Section 8

We there show that the present result strictly encompasses our initial result [START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF] that learns rigid product-free Lambek grammars from name-free natural deductions. To do so, we give the bijective correspondence between cut-free proof nets for the product-free Lambek calculus and normal natural deduction that are commonly used as parse structures.

In the conclusion, we discuss the merits and limits of the present work. We briefly explain how it can generalise to k-valued Lambek grammars with product and suggest direction for obtaining corpora with proof frame annotations from dependency-annotated corpora.

2 Exact learning à la Gold: a brief reminder

We shall just give a brief overview of the Gold learning model of [START_REF] Gold | Language identification in the limit[END_REF], with some comments, and explain why his famous unlearnability theorem of [START_REF] Gold | Language identification in the limit[END_REF] (theorem 1 below) is not as negative as it first seemed -as the result of [START_REF] Angluin | Finding patterns common to a set of strings[END_REF] and of the present article shows. The principles of first language acquisition as advocated by Chomsky [START_REF]Théories du langage, théories de l'apprentissage -le débat Chomsky Piaget[END_REF] and more recently by Pinker [START_REF] Pinker | Language acquisition[END_REF][START_REF] Pinker | Why the child holded the baby rabbits[END_REF] can be very roughly summarised as follows:

1. One learns from positive examples only: an argument says that in certain civilisations children uttering ungrammatical sentences are never corrected although they learn the grammar just as fast as ours -this can be discussed, since the absence of reaction might be considered as negative evidence, as well as the absence of some sentences in the input. 2. The target language is reached by specialisation, i.e. by restricting word order from tentative languages with a freer word order: rare are the learning algorithms for natural language that proceed by specialisation although, when starting from semantics, there are such algorithms as the one by Tellier [45] 3. Root meaning is learnt first, and as part of this root meaning, the argumental structure (also known as valencies in dependency grammars) are known before the grammar learning process actually starts. This implies that in the learner's utterances exactly all needed words are present, possibly in a non correct order. This enforces the idea that one learns by specialisation -the afore mentioned work by Tellier actually uses argument structures as inputs [START_REF] Tellier | How to split recursive automata[END_REF] 4. The examples that the child is exposed to are not so numerous:

this is known as the Poverty Of Stimulus argument. It has been widely discussed since 2000 in particular for supporting quantitative methods. [START_REF]Théories du langage, théories de l'apprentissage -le débat Chomsky Piaget[END_REF][START_REF] Pullum | Empirical assessment of stimulus poverty arguments[END_REF][START_REF] Reali | Uncovering the richness of the stimulus: Structure dependence and indirect statistical evidence[END_REF][START_REF] Berwick | Poverty of the stimulus revisited[END_REF] In his seminal 1967 paper, Gold introduced a formalisation of the process of the acquisition of one's first language grammar. It strictly follows the first principle stated above, which is the easiest to formalise: the formal question he addressed could be more generally stated as grammatical inference from positive examples. It also should be said that Gold's notion of learning may be used for other purposes, every time one wants to extract some regularity out of sequences observations. It has been applied to genomics (what would be a grammar generating the strings issued from DNA sequences) and diagnosis (what are the regular behaviours of the system, what would be a grammar generating the sequences of normal observations provided by captors for detecting abnormal behaviours). We shall provide only a minimum of information on formal languages and grammars. Let us just say that a language is a subset of an inductive class U. Elements of U usually are finite sequences (a.k.a. strings) of words, or trees whose leaves are labelled by words, or graphs whose vertices are words. 3 A grammar G is a finitely described process gener-ating the objects of a language L(G) ⊂ U. The membership question is said to be decidable for a grammar G when the characteristic function of L(G) in U is computable. The most standard example of U is Σ * the set of finite sequences over some set of symbols (e.g. words) Σ. The phrase structure grammars of Chomsky-Schutzenberger are the most famous grammars producing languages that are parts of Σ * . Lambek categorial grammars and basic categorial grammars are an alternative way to generate sentences as elements of Σ * : they produce the same languages as context-free languages [8,34,30, chapters 2]. Finite labeled trees also are a possible class of objects. For instance a regular tree grammar produces a tree language, whose yields define a context free string language. In the formal study of human languages, U usually consists in strings of words or in trees with words on their leaves. Definition 1 (Gold, 1967, [21]). A learning function for a class of grammars G producing U-objects (L(G) ⊂ U) is a partial function φ that maps any finite sequence of positive examples ex1, ex2, . . . , ex k with exi ∈ U to a grammar Gi = φ(ex1, ex2, . . . , ex k ) of the class of grammars G such that: if (ei) i∈I is any enumeration of a language L(G) ⊂ U with G ∈ G, then there exists an integer N such that:

-

G P = G N for all P ≥ N . -L(G N ) = L(G).
Several interesting properties of learning functions have been considered:

Definition 2.
A learning function φ is said to be effective or computable when φ is recursive. In this case one often speaks of a learning algorithm. In this article, we shall only consider effective learning functions: this is consistent both with language being viewed as a computational process and with applications to computational linguistics. Observe that the learning function does not have to be a total recursive function: it may well be undefined for some sequences of sentences and still be a learning function. conservative if φ(e1, . . . , ep, ep+1) = φ(e1, . . . , ep) whenever ep+1 ∈ L(φ(e1, . . . , ep)). consistent if {e1, . . . , ep} ⊂ L(φ(e1, . . . , ep)) whenever φ(e1, . . . , ep) is defined. set driven if φ(e1, . . . , ep) = φ(e ′ 1 , . . . , e ′ q ) whenever {e1, . . . , ep} = {e ′ 1 , . . . , e ′ q } -neither the order of the examples nor their repetitions matters.

incremental if there exists a binary function Ψ such that φ(e1, . . . , ep, ep+1) = Ψ (φ(e1, . . . , ep), ep+1) responsive if the image φ(e1, . . . , ep) is defined whenever there exists L in the class with {e1, . . . , ep} ⊂ L monotone increasing when φ(e1, . . . , ep, ep+1) ⊂ φ(e1, . . . , ep)

The algorithm for learning Lambek grammars that we propose in this paper enjoys all those properties. All of them seem to be sensible with respect to first language acquisition but the last one: indeed, as said above, children rather learn by specialisation. It should also be observed that the learning algorithm applies to a class of languages. So it is fairly possible that a given language L which both belongs to the classes G1 and G2 can be identified as a member of G1 and not as a member of G2. Learning L in such a setting is nothing more than to be sure, given the examples seen so far, that the language is not any other language in the class. The classical result from the same 1967 paper by Gold [21] that has be over interpreted see e.g. [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF][START_REF] Johnson | Gold's theorem and cognitive science[END_REF] can be stated as follows:

Theorem 1 (Gold, 1967, [21]). If a class Gr of grammars generates languages (Li)i ∈ N with Li ∈ N which are strictly embedded that is Li ⊊ Li+1 for all i ∈ N together with the union of all these languages ∪ i∈N Li ∈ Gr then no function may learn Gr.

Proof. From the definition, we see that a learning function should have guessed the grammar of a language L(G) with G ∈ G after a finite number of examples in the enumeration of L(G). Consequently, for any enumeration of any language in the class, (1) the learning function may only change its mind finitely many times.

Assume that is a learning function φ for the class Gr. Since the Li are nested as stated, we can provide an enumeration of L = ∪Li according to which we firstly see examples x 1 0 , ⋯, x p 0 0 from L0 until φ proposes G0 with LG0 = L0, then we see examples x 1 1 , ⋯, x p 1 in L1 until φ proposes G1 with LG1 = L1, then we see examples x 1 2 , ⋯, x p 2 in L2 until φ proposes G2 with LG2 = L2, etc. In such an enumeration of L the learning function changes its mind infinitely many times, conflicting with [START_REF] Abrusci | Non-commutative logic I: the multiplicative fragment[END_REF]. Thus there cannot exists a learning function for the class Gr.

Gold's theorem above has an easy consequence that was interpreted quite negatively:

Corollary 1. No class containing the regular languages can be learnt. Indeed, by that time the Chomsky hierarchy was so present that no one thought that transverse classes could be of any interest, let alone that they could be learnable. Nowadays, it is assumed that the syntax of human languages contains no regular languages and goes a bit beyond context free languages -as can be seen in figure 1. It does not seem likely that human languages contain a series of strictly embedded languages as well as their unions. Hence Gold's theorem does not prevent large and interesting classes of languages, like human languages, from being learnt. For instance Angluin showed that pattern languages, a transversal class can be learnt by identification in the limit [START_REF] Angluin | Finding patterns common to a set of strings[END_REF] and she also provided a criterion for learnability base on telltale sets: Theorem 2 (Angluin, 1980, [6]). An enumerable family of languages Li with a decidable membership problem is effectively learnable whenever for each i there is a computable finite Ti ⊂ f Li such that if Ti ⊂ Lj then there exists w ∈ (Lj ∖ Li).

As a proof that some interesting classes are learnable, we shall define particular grammars, Lambek categorial grammars with product, and their associated structure languages, before proving that they can be learnt from these structures, named proof frames.

3 Categorial grammars and the LCG p class Given a finite set of words Σ and an inductively defined set of categories C including a special category s and an inductively defined set of derivable sequents ⊢ ⊂ (C * × C) (each of them being written t1, . . . , tn ⊢ t) a categorial grammar G is defined as map lex G from words to finite sets of categories. An important property, as far as learnability is concerned, is the maximal number of categories per word i.e. max w∈Σ lex G (w) . When it is less than k, the categorial grammar G is said to be k-valued and 1-valued categorial grammars are said to be rigid. Some standard family of categorial grammars are:

1 3 -a variant allows empty antecedents. A phrase, that is a sequence of words w1⋯wn, is said to be of category C according to G when, for every i between 1 and p there exists ti ∈ lex G (wi) such that t1, . . . , tn ⊢ C is a derivable sequent. When C is s the phrase is said to be a sentence according to G. The string language generated by a categorial grammar is the subset of Σ * consisting in strings that are of category s i.e. sentences. Any language generated by a grammar in one of the aforementioned classes of categorial grammars is context free. In this paper we focus on Lambek grammars with product (LCGp). The explicit use of product categories in Lambek grammars is not so common. Indeed, one rather sees negative products that can be treated with categorial implication and . For instance a category like (a ⊗ b) c can be viewed as b (a c) so they do not really involve a product. The comma in the left-hand side of the sequent, corresponding to the blanks between words are implicit products, but grammar and parsing of those can be defined without explicitly using the product. Nevertheless, there are cases when the product is appreciated:

The derivable sequents of the Lambek syntactic calculus with product are obtained from the axiom C ⊢ C for any category C and the rules are given below, where A, B are categories and Γ, ∆ finite sequences of categories: (2) Jean donne un livre à Marie et une fleur à Anne.

Γ, B, Γ ′ ⊢ C ∆ ⊢ A h Γ, ∆, A B, Γ ′ ⊢ C A, Γ ⊢ C i Γ ≠ ∅ Γ ⊢ A C Γ, B, Γ ′ ⊢ C ∆ ⊢ A h Γ, B A, ∆, Γ ′ ⊢ C Γ, A ⊢ C i Γ ≠ ∅ Γ ⊢ C A Γ, A, B, Γ ′ ⊢ C ⊗ h Γ, A ⊗ B, Γ ′ ⊢ C ∆ ⊢ A Γ ⊢ B ⊗i ∆, Γ ⊢ A ⊗ B
-According to Glyn Morrill [START_REF] Morrill | Incremental processing and acceptability[END_REF][START_REF] Morrill | Categorial Grammar: Logical Syntax, Semantics, and Processing[END_REF] past participles like "raced " should be assigned the category

((CN CN ) (N (N s-)) ⊗ (N (N s-))
where sis an untensed sentence in sentences like:

(3) The horse raced past the barn fell.

Categorial grammars generating proof frames

The classes of languages that we wish to learn include some proper context free languages [START_REF] Bar-Hillel | On categorial and phrasestructure grammars[END_REF], hence they might be difficult to learn. So we shall learn them from structured sentences, and this section introduces proof frames that we shall use as structured sentences.

A neat natural deduction system for Lambek calculus with product is rather intricate [START_REF] Amblard | Natural deduction and normalisation for partially commutative linear logic and lambek calculus with product[END_REF][START_REF] Amblard | Calculs de représentations sémantiques et syntaxe générative : les grammaires minimalistes catégorielles[END_REF], mainly because the product elimination rules have to be carefully commuted for having a unique normal form. Cut-free sequent calculus proofs neither are fully satisfactory because they are quite redundant and some of their rules can be swapped. As explained in [30, chapter 6] proof nets provide perfect parse structures for Lambek grammars even when they use the product -when the product is not used, cut-free proof nets and normal natural deduction are isomorphic, as we shall show in subsection 8.1. Consequently the structures that we used for learning will be proof frames that are proof nets with missing informations. Let us see how categorial grammars generate such structures, and first let us recall the correspondence between polarised formulae of linear logic and Lambek categories.

Polarised linear formulae and Lambek categories

A Lambek grammar is better described with the usual Lambek categories, while proof nets are better described with linear logic formulae.

Hence we need to recall the correspondence between these two languages as done in [30, chapter 6]. Lambek categories (with product) are C⊗ defined in the previous section 3. Linear formula L are defined by:

L ∶∶= P P ⊥ (L ⊗ L) (L ℘ L)
The negation of linear logic ) ⊥ is only used on propositional variables from P as the De Morgan laws allow:

(A ⊥ ) ⊥ ≡ A (A ℘ B) ⊥ ≡ (B ⊥ ⊗ A ⊥ ) (A ⊗ B) ⊥ ≡ (B ⊥ ℘ A ⊥ )
To translate Lambek categories into linear logic formulae, one has to distinguish the polarised formulae, which are either outputs or positive formulae of L ○ or inputs or negative formulae of

L • with F ∈ L ○ ⇐⇒ F ⊥ ∈ L • and (L ○ ∪ L • ) ⊊ L: L ○ ∶∶= P (L ○ ⊗ L ○ ) (L • ℘ L ○ ) (L ○ ℘ L • ) L • ∶∶= P ⊥ (L • ℘ L • ) (L ○ ⊗ L • ) (L • ⊗ L ○
) Any formulae of the Lambek L calculus can be translated as an output formula +L of multiplicative linear logic while its negation can be translated as an input linear logic formulae -L:

L α ∈ P L = M ⊗ N L = M N L = N M +L α +M ⊗ +N -M ℘ +N +N ℘ -M -L α ⊥
-N ℘ -M -N ⊗ +M +M ⊗ -N Conversely any output formula of linear logic is the translation of a Lambek formula and any input formula of linear logic is the negation of the translation of a Lambek formula. Let (. . .) ○ Lp denotes the inverse bijection of "+", from L ○ to Lp and (. . .) • Lp denotes the inverse bijection of "-" from L • to Lp. These two maps are inductively defined as follows:

F ∈L ○ α∈P (G∈L ○ ) ⊗ (H∈L ○ ) (G∈L • ) ℘ (H∈L ○ ) (G∈L ○ ) ℘ (H∈L • ) F ○ Lp α G ○ Lp ⊗ H ○ Lp G • Lp H ○ Lp G ○ Lp H • Lp F ∈L • α ⊥ ∈P ⊥ (G∈L • ) ℘ (H∈L • ) (G∈L ○ ) ⊗ (H∈L • ) (G∈L • ) ⊗ (H∈L ○ ) F • Lp α H • Lp ⊗ G • Lp H • Lp G ○ Lp H ○ Lp G • Lp 4.

Proof nets

A proof net is a graphical representation of a proof which identifies essentially similar proofs. A cut-free proof net has several conclusions, and it consists of the subformula trees of its conclusions, that possibly stops on a sub formula which is not necessarily a propositional variable (axioms involving complex formulae simplify the learning process).

a cyclic order on these sub formula trees axioms that links two dual leaves F and F ⊥ of these formula subtrees. Such a structure can be represented by a sequence of terms -admittedly easier to typeset than a graph -with indices for axioms. Each index appears exactly twice, once on a formula F (not necessarily a propositional variable) and one on F ⊥ . Here are two proof nets with the same conclusions:

(4) s ⊥1 ⊗ (s 2 ℘ np ⊥3 ), np 3 ⊗ (s ⊥ ⊗ np) 7 , (np ⊥ ℘ s) 7 ⊗ s ⊥2 , s 1 (5) s ⊥1 ⊗ (s 2 ℘ np ⊥3 ), np 3 ⊗ (s ⊥4 ⊗ np 5 ), (np ⊥5 ℘ s 4 ) ⊗ s ⊥2 , s 1
The second one is obtained from the first one by expansing the complex axiom (s ⊥ ⊗ np) 7 , (np ⊥ ℘ s) 7 into two axioms:

(s ⊥4 ⊗ np 5 ), (np ⊥5 ℘ s 4
). Complex axioms always can be expansed into atomic axioms -this is known as η-expansion property. This is the reason why proof nets are often presented with atomic axioms. Nevertheless, we shall substitute propositional variables with complex formula during the learning process, and therefore we need to consider complex axioms as well -see the processing of the example 9 in section 6. No any such structure does correspond to a proof: Definition 3. A proof structure with conclusions C 1 , I 1 1 , . . . , I 1 n is said to be a proof net of the Lambek calculus when it enjoys the correctness criterion defined by the following properties:

1. Acyclic: any cycle contains the two branches of a ℘ link 2. Intuitionistic: exactly one conclusion is an output formula of L ○ , all other conclusions are input formulae of L • 3. Non commutative: no two axioms cross each other 4. Without empty antecedent: there is no sub proof net with a single conclusion

The first point in this definition is not stated precisely but, given that we learn from correct structured sentences, we shall not need a precise definition. The reader interested in the details is referred to [30, chapter 6]. Some articles on proof nets add to the criterion above a form of connectedness but it is not actually needed since this connectedness is a consequence of the first two points see [START_REF] Guerrini | A linear algorithm for mll proof net correctness and sequentialization[END_REF] or [30, section 6.4.8 pages 225-227].

Definition 4. Proof nets for the Lambek calculus can be defined inductively as follows (observe that they contain exactly one output conclusion):

given an output formula F an axiom F, F ⊥ is a proof net with two conclusions F and F ⊥ -we do no require that F is a propositional variable. given a proof net π 1 with conclusions O 1 , I 1 1 , . . . , I 1 n and a proof net π 2 with output formula O 2 , I 2 1 , . . . , I 2 p where O 1 and O 2 are the output conclusions, one can add a ⊗-link between a conclusion of one and a conclusion of the other, at least one of the two being an output conclusion. We thus can obtain a proof net whose conclusions are:

• O 1 ⊗ I 2 k , I 2 k+1 , . . . , I 2 p , O 2 , I 2 1 , I 2 k-1 , I 1 1 , . . . , I 1 n -O 2 being the out- put conclusion • I 1 l ⊗ O 2 , I 2 1 , . . . , I 2 p , I 1 l+1 , . . . , I 1 n , O 1 , I 1 1 , . . . , I 1 l-1 , -O 1 being the output conclusion • O 1 ⊗ O 2 , I 2 1 , . . . , I 2 p , I 1 1 , . . . , I 1 n -O 1 ⊗ O 2 being the output con- clusion.
given a proof net π 1 with conclusions O 1 , I 1 1 , . . . , I 1 n one can add a ℘ link between any two consecutive conclusions, thus obtaining a proof nets with conclusions:

• O 1 , I 1 1 , . . . , Ii ℘ Ii+1, . . . , I 1 n -O 1 being the output conclusion • O 1 ℘ I 1 1 , I 1 2 . . . , I 1 n -O 1 ℘ I 1 1 being the output conclusion • I 1 n ℘ O 1 , I 1 1 . . . , I 1 n-1 -O 1 ℘ I 1 1

being the output conclusion

A key result see e.g. [START_REF] Moot | The logic of categorial grammars: a deductive account of natural language syntax and semantics[END_REF]Theorem 6.28]. is that:

Theorem 3. The inductively defined proof nets of definition 4, i.e. proofs, exactly correspond to the proof nets defined as graphs enjoying the universal properties of the criterion 3

A parse structure for a sentence w 1 , . . . , w p generated by a Lambek grammar G defined by a lexicon lex G is a proof net with conclusions

(c n ) -, . . . , (c 1 ) -, s + with c i ∈ lex(w i
). This replaces the definition of parse structure as normal natural deductions [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] which does not work well when the product is used [START_REF] Amblard | Natural deduction and normalisation for partially commutative linear logic and lambek calculus with product[END_REF][START_REF] Amblard | Calculs de représentations sémantiques et syntaxe générative : les grammaires minimalistes catégorielles[END_REF]. Non-commutative proof-nets were first introduced by Roorda in his thesis [START_REF] Roorda | Resource logic: proof theoretical investigations[END_REF] but he only showed the soundness of the criterion: the inductively defined proof nets enjoys a correctness criterion, namely the Danos Regnier criterion [START_REF] Danos | The structure of multiplicatives[END_REF] augmented with intuitionistic and non-commutative conditions. We provided the first proof of the converse in [START_REF] Retoré | Calcul de Lambek et logique linéaire[END_REF]. There are several equivalent notions of proof nets for cyclic multiplicative intuitionistic linear logic that is Lambek calculus. For instance the proof nets for non commutative linear logic by Abrusci and Ruet [START_REF] Abrusci | Non-commutative logic I: the multiplicative fragment[END_REF], restricted to the non commutative multiplicative connectives and to intuitionistic formulae also are a presentation of proof nets for Lambek calculus. It should be underlined, however that all these notions of proof nets do not properly handle cuts except the one by Melliès [START_REF] Melliès | A topological correctness criterion for multiplicative non commutative logic[END_REF] -see e.g. the discussions in [19, chapters 11 and 18].

Structured sentences to learn from: s proof frames

An s proof frame (sPF) is simple a parse structure of a Lambek grammar i.e. a proof net whose formula names have been erased, except the s on the output conclusion. Regarding axioms, their positive and negative tips are also kept. Such a structure is the analogous of a functor argument structure for AB grammars or of a name free normal natural deduction for Lambek grammars used in [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF][START_REF] Buszkowski | Discovery procedures for categorial grammars[END_REF][START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF] and it can be defined inductively as we did in 4, or by the conditions in definition 3. Definition 5 (s proof frames, sPFs). An s proof frame (sPF) is a normal proof net π such that:

-The output of π is labelled with the propositional constant s -which is necessarily the conclusion of an axiom, the input conclusion of this axiom being labelled s ⊥ .

-The output conclusion of any other axiom in π is O its input conclusion being O ⊥ = I. Given an s proof net π its associated s proof frame π f is obtained by replacing in π the output of any axiom by O (and its dual by I = O ⊥ ) except the s that is the output of π itself which is left unchanged. A given Lambek grammar G is said to generate an sPF ρ whenever there exists a proof net π generated by G such that ρ = π IO . In such a case we write ρ ∈ sPF(G).

The sPFs associated with the two proof nets 4 and 5 above are:

(6) s ⊥1 ⊗ (O 2 ℘ I 3 ), O 3 ⊗ (I 4 ⊗ O 5 ), (O 5 ℘ O 4 ) ⊗ I 2 , s (7) s ⊥1 ⊗ (O 2 ℘ I 3 ), O 3 ⊗ I 7 , O 7 ⊗ I 2 , s
Are proof frames related to partial proof nets or modules that first appeared in [START_REF] Girard | Multiplicatives. Rendiconti del Seminario dell[END_REF]? They only partly are! Indeed, modules are name-free parts of proof-nets and generalised such structures that can be combined to obtained real multiplicatives proof nets. Here we only consider name-free complete proof nets, and as far as proof net surgery is concerned, we only replace some axioms with their η-expansion as explained in [19, chapter 11].

Unification, proof frames and categorial grammars

In this section, we shall briefly describe how categories, and more generally categorial grammars can be unified. Indeed, our learning algorithm makes a crucial use of category-unification, and this kind of technique is quite common in grammatical inference [START_REF] Nicolas | Grammatical inference as unification[END_REF].

As said in paragraph 3, a categorial grammar is defined from a lexicon that maps every word w to a finite set of categories lex G (w). Categories are usually defined from a finite set B of base categories that includes a special base category s. Here we shall consider simultaneously many different categorial grammars since the learning hypothesis varies in the class of categorial grammars. In order to have a common set of base type for all categorial grammars, we shall consider an infinite set of base categories B whose members will be s and infinitely many category variables denoted by x, y, x1, x2, . . ., y1, y2, . . . In other words, B = {s} ∪ V , s ∈ V , V being an infinite set of category variables. The categories arising from B are defined as usual by V ∶∶= s V V V V V V ⊗V. This infinite set of base categories does not really modify categorial grammars: a given categorial grammar only makes use of finitely many base categories. Indeed, there are finitely many words each of them being associated with finitely many categories: there are finitely many symbols in the lexicon hence only a finite number of base categories are used by a given categorial grammar. Choosing an infinite set of base categories is rather important, as we shall substitute a category variable with a complex category using fresh variables, thus turning a categorial grammar into another one, and considering families of grammars over the same base categories.

A substitution σ is a function from categories V to categories V that is generated by a mapping σ V of finitely many variables xi 1 , ⋯, xi p in V to categories of V:

σ(s) = s given x ∈ V, σ(x) = σ V (x) if x = xi k for some k x otherwise σ(A B) = σ(A) σ(B) σ(B A) = σ(B) σ(A)
The substitution σ is said to be a renaming when σ V is a bijective mapping from V to V -otherwise stated σ V is a permutation of the xi 1 , ⋯, xi p ). As usual, substitutions may be extended to sets of categories by stipulating σ(A) = {σ(a) a ∈ A}. Observe that σ(A) can be a singleton while A is not:

{(a (b c)), (a u)}[u ↦ (b c] = {a (b c)}.
A substitution can also be applied to a categorial grammar:

σ(G) = G ′ with lex G ′ (w) = σ(lex G (w))
for any word w. Observe that a substation turns a k-valued (as defined in section 3) categorial grammar into a k ′ -valued categorial grammar with k ′ ≤ k, and possibly into a rigid (or 1-valued) categorial grammar . A substitution σ on Lambek categories (defined by mapping finitely many category variables xi to Lambek categories Li, xi ↦ Li) clearly defines a substitution on linear formulae σ (by xi ↦ L + i ), which preserves the polarities σ (F ) is positive(respectively negative) if and only if F is. Conversely, a substitution ρ on linear formulae defined by mapping variables to positive linear formulae (xi ↦ Fi) defines a substitution on Lambek categories ρ L with the mapping xi ↦ F ○ Lp . One has:

σ(L) = (σ (L+)) ○ Lp and ρ(F ) = (ρ L (F ○ Lp ))+ if F ∈ L ○ and ρ(F ) = (ρ L (F • Lp ))-.
Roughly speaking as far as we use only polarised linear formulae and substitution that preserve polarities, it does not make any difference to perform substitutions on linear formulae or on Lambek categories. Substitution preserving polarities (or Lambek substitutions) can also be applied to proof nets: σ(π) is obtained from π by applying the substitution to any formula in π. A substitution turns an s Lambek proof net into an s Lambek proof net -this is the reason why proof nets in this paper may contain axioms on complex formulae.

Proposition 1. If

σ is a substitution preserving polarities and π a proof net generated by a Lambek grammar G, then σ(π) is generated by σ(G) and π and σ(π) have the same associated s proof frame:

σ(π) f = π f
Two grammars G1 and G2 with their categories in V are said to be equal whenever there exists a renaming ν such that ν(G1) = G2.

A substitution σ is said to unify two categories A, B if one has σ(A) = σ(B). A substitution is said to unify a set of categories T or to be a unifier for T if for all categories A, B in T one has σ(A) = σ(B) -in other words, σ(T ) is a singleton. A substitution σ is said to unify a categorial grammar G or to be a unifier of G whenever, for every word in the lexicon σ unifies lex G (w), i.e. for any word w in the lexicon lex σ(G) (w) has a unique category -in other words σ(G) is rigid. A unifier does not necessarily exists, but when it does, there exists a most general unifier (mgu) that is a unifier σu such for every unifier τ there exists a substitution στ such that τ = στ ○ σu. This most general unifier is unique up to renaming. This result also holds for unifiers that unify a set of categories and even for unifiers that unify a categorial grammar. [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF] An algorithm for unifying two categories C1 and C2 may proceed by managing a finite multi-set E of potential equations on terms, until it fails or reaches a set of equations whose left hand side are variables, each of which appears in a unique such equation -a measure consisting in triple of integers ordered ensures that this algorithm always stops. This set of equations xi = ti defines a substitution by setting ν(xi) = ti.

Initially E = {C1 = C2}. In the procedure below, upper case letters stand for categories, whatever they might be, x for a variable, * and ◇ stand for binary connectives among , , ⊗. Equivalently, unifications could be performed on linear formulae, as said in this article. The most general unifier of n categories can be performed by iterating binary unification, the resulting most general unifier does not depend on the way one proceeds.

E ∪ {C=C} → E E ∪ {A1 * B1=A2 * B2} → E ∪ {A1=A2, B1=B2} E ∪ {C=x} → E ∪ {x=C} if x ∈ V ar(C) E ∪ {x=C} → if x ∈ V ar(C) ∧ x ∈ V ar(E) E ∪ {x=C} → E[x ∶ =C] ∪ {x=C} if ◇ ≠ * E ∪ {A1 * B1=A2 ◇ B2} → E ∪ {s=A2 * B2} → E ∪ {A1 * B1=s} →
Fig. 3. The unification algorithm for unifying two categories Definition 6. Let π be an s proof net whose associated sPF is π f . If all the axioms in π but the s, s ⊥ whose s is π's main output are αi, α ⊥ i with αi ≠ αj when i ≠ j, π is said to be a most general labelling of π f . If π f is the associated sPF of an s proof net π and πv one of the most general labelling of π f , then πv is also said to be a most general labelling of π. The most general labelling of an s proof net is unique up to renaming.

We have the following obvious but important property: Proposition 2. If πv is a most general labelling of an s proof net π, then there exists a substitution σ such that π = σ(πv).

An RG-like algorithm for learning Lambek categorial grammars from proof frames

Assume that we wish to define a consistent learning function φ from positive examples for a class of categorial grammars (see definition 2). Assume that φ already mapped e1, . . . , en to a grammar Gn with e1, . . . , en ⊂ L(Gn) (φ being consistent). If en+1 ∈ L(Gn) it is natural to define φ(e1, . . . , en, en+1) = Gn+1 as being Gn. Otherwise, that is when en+1 ∈ L(Gn), there exists some word w k in the sentence en+1 such that no category of lex Gn (w) is able to account for the behaviour of w k in the sentence en+1. A natural but misleading idea would be to say: if word w k needs category c k n+1 in example en+1, let us add c k to lex Gn (w k ) to define lex G n+1 (w k

). Doing so for every occurrence of a problematic word in the sentence en+1, actually leads to e1, . . . , en, en+1 ⊂ L(Gn+1) and in the limit we should obtain the smallest grammar G∞ such that ∀i e1, . . . , ei ∈ LG∞. Doing so, there is little hope to identify a language in the limit in Gold sense. Indeed, nothing guarantees that the process will stop, and a categorial grammar with infinitely many categories for some word is not even a grammar, that is a finite description of a possibly infinite language. Thus, an important guideline for learning categorial grammars is to bound the number of categories per word. That is the reason why we introduced in section 3 the notion of k-valued categorial grammars, with at most k categories per word. We shall start by learning rigid (1-valued) Lambek categorial grammars with product (LCGp) and this method extends to k-valued LCGp. Our algorithm can be viewed as an extension to Lambek grammars with product of the RG algorithm (learning Rigid Grammars) introduced by Buszkowski and Penn in [START_REF] Buszkowski | Discovery procedures for categorial grammars[END_REF][START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF] initially designed for rigid AB grammars. A difference from their seminal work is that the data ones learns from were functor argument trees while here they are proof frames (or natural deduction frames when the product is not used see section 8). Proof frames may seem less natural than natural deductions, but we have two good reasons for using them:

-Product is of interest for some grammatical constructions as examples 2 and 3 show while there is no fully satisfactory natural deduction for Lambek calculus with product. [4,2] -Proof frames resemble dependency structures, since an axiom between the two conclusions corresponding to two words expresses a dependency between these two words. To illustrate our learning algorithm we shall proceed with the three examples below, whose corresponding s proof frames are given in figure 4. As their sPF structures show, the middle one (9) involves a positive product (the I ℘I in the category of "and ") and the last one [START_REF] Bonato | Uno studio sull'apprendibilità delle grammatiche di Lambek rigide -a study on learnability for rigid Lambek grammars[END_REF] involves an introduction rule (the O ℘ I in the category of "that"). ( 8) Sophie gave a kiss to Christian [START_REF] Berwick | Poverty of the stimulus revisited[END_REF] Christian gave a book to Anne and a kiss to Sophie [START_REF] Bonato | Uno studio sull'apprendibilità delle grammatiche di Lambek rigide -a study on learnability for rigid Lambek grammars[END_REF] Sophie liked a book that Christian liked.

Usually, in order to manipulate right handed sequents with conclusions only, proof nets reverse the order of the hypotheses which correspond to words, as explained in section 4 -in some papers by Glynn Morrill e.g. [START_REF] Morrill | Incremental processing and acceptability[END_REF] the order is not reversed, but then the conclusions of the proof net, that are the linear formulae which are the dual of the Lambek categories are less visible. One solution that will make the supporters of either notation happy is to write the sentences vertically as we do in figure 4.

Example 1

11 I Sophie 11 O ⊗ 00 s ⊥ ⊗ 12 O ⊗ 13 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ gave 13 I ⊗ 14 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ a 14 I kiss 12 I ⊗ 15 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ to 15 I Christian 00 s (sentence) Example 2 21 I Christian 21 O ⊗ 00 s ⊥ ⊗ 22 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ gave 23 I ⊗ 24 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ a 24 I book 25 I ⊗ 26 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ to 26 I Anne 25 O ⊗ 23 O ⊗ 22 I ⊗ 27 O ⊗ 28 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ and 28 I ⊗ 29 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ a 29 I kiss 27 I ⊗ 20 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ to 20 I Sophie 00 s (sentence) Example 3 31 I Sophie 31 O ⊗ 00 s ⊥ ⊗ 32 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ liked 32 I ⊗ 33 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ a 34 I book 34 O ⊗ 33 I ⊗ 35 I ℘ 36 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ that 37 I Christian 37 O ⊗ 36 I ⊗ 35 O ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ liked 00 s (sentence)
Fig. 4. Three S proof frames: three structured sentences for our learning algorithm.

Definition 7 (RG like algorithm for sPFs). Let D = (π k f ) 1≤k≤n be the s proof frames associated with the examples (e k f )1 ≤ k ≤ n, and let (π k ) be most general labellings of the (π k f ) 1≤k≤n . We can assume that they have no common category variables -this is possible because there are infinitely many category variables is infinite and because most general labellings are defined up to renaming. If example e k contains n words w k 1 , . . . , w k n then π k has n conclusions (c k n )-, . . . , (w k 1 )-, s, where all the c k i are Lambek categories.

Let GF (D) be the (non necessarily rigid) grammar defined by the assignments w k i ∶ c k i -observe that a for a given word w there may exist several i and k such that w = w k i .

Let RG(D) be the rigid grammar defined as the most general unifier of the categories lex(w) for each word in the lexicon when such a most general unifier exists.

We define φ(D) as RG(D). When unification fails, the grammar is defined by lex(w) = ∅ for those words whose categories do not unify. 4With the sPF of our examples in 4 yields the following type assignments where the variable xn corresponds to the axiom number n in the examples, they are all different as expected -remember that s is not a category variable but a constant. ...

(x22 ⊗ (x23 ⊗ x25))) that ((x34 x33) (x36 x35)) ((x36 ℘ x ⊥ 35 ) ⊗ (x ⊥ 33 ⊗ x34)) liked (x31 s) x32 x32 ⊗ (s ⊗ x31) (x37 x36) x35 x35 ⊗ (x36 ⊗ x37) gave ((x11 s) (x13 ⊗ x12)) (x13 ⊗ x12) ⊗ (s ⊗ x11) ((x21 s) x22) x22 ⊗ (s ⊗ x21) to x12 x15 x15 ⊗ x ⊥ 12 x25 x26 x26 ⊗ x ⊥ 25 x27 x20 x20 ⊗ x ⊥ 27 a x13 x14 x14 ⊗ x ⊥ 13 x23 x24 x24 ⊗ x ⊥ 23 x28 x29 x29 ⊗ x ⊥ 28 x32 x33 x33 ⊗ x ⊥ 32 Anne x26 x ⊥ 26 Sophie x11 x ⊥ 11 x20 x ⊥ 20 x31 x ⊥ 31 Christian x15 x ⊥ 15 x21 x ⊥ 21 x37 x ⊥ 37 book x24 x ⊥ 24 x34 x ⊥ 34 kiss x14 x ⊥ 14 x29 x ⊥ 29
Unifications either performed on Lambek categories c k i or on the corresponding linear formulae (the (c k i )-that appear in the second column) yield the following equations:

liked x31 = x37 x36 = s x32 = x35 gave x11 = x21 x22 = x13 ⊗ x12 to x12 = x25 = x27 x15 = x26 = x20 a x13 = x23 = x28 = x32 x14 = x24 = x29 = x33 Sophie x11 = x20 = x31 Christian x15 = x21 = x37 kiss x14 = x29 book x24 = x34
These unification equations can be solved by setting:

x36 = s x22 = x13 ⊗ x12 = np ⊗ pp x12 = x25 = x27 = pp prepositional phrase introduced by "to" x13 = x23 = x28 = x32 = x35 = np noun phrase x14 = x24 = x29 = x33 = x34 = cn common noun x11 = x20 = x31 = x15 = x21 = x37 = x15 = x26 = pn proper name
The grammar can be unified into a rigid grammar Gr , namely:

word category(Lambek) category ⊥ (linearlogic) and (((np ⊗ pp) (np ⊗ pp)... ((np ⊗ pp) ⊗ ... ... (np ⊗ pp)) ...((np ⊗ pp) ⊥ ⊗ (np ⊗ pp))) that ((n n) (s np)) ((s ℘ np ⊥ ) ⊗ (n ⊥ ⊗ n)) liked (pp s) np np ⊗ (s ⊗ pn) gave (pp s) (pp ⊗ np)) (np ⊗ pp) ⊗ (s ⊗ pn) to np pn pn ⊗ np ⊥ a np cn cn ⊗ pp ⊥ Anne pn pn ⊥ Sophie pn pn ⊥ Christian pn pn ⊥ book cn cn ⊥ kiss cn cn ⊥
As stated in proposition 1, one easily observes that the sPF are indeed produced by the rigid grammar Gr.

Earlier on, in the definition of an sPF, we allowed non atomic axioms, and we can now precisely see why: the axiom 22 could be instantiated by the single variable x22 but, when performing unification, it got finally instantiated with x13 ⊗ x12. Thus, if we would have forced axioms to always be on propositional variables, the grammar Gr would not have generated the sPF of example 2 but the slightly different sPF with the axioms x13, x ⊥ 13 and x ⊥ 12 , x12 linked by an ⊗ link x ⊥ 13 ⊗ x12 and by a ℘ link x ⊥ 12 ℘ x ⊥ 13 in place of the axiom 22.

Convergence of the learning algorithm

This algorithm converges in the sense defined by Gold [START_REF] Gold | Language identification in the limit[END_REF], see definition 1. The first proof of convergence of a learning algorithm for categorial grammars is the proof by Kanazawa [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF] of the convergence of the algorithm of Buszkowki and Penn [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF] for learning rigid basic categorial grammars from functor argument structures (name free natural deduction with and elimination rules only). Although we learn a different class of grammars from different structures, our proof is quite similar. It follows [START_REF] Bonato | Uno studio sull'apprendibilità delle grammatiche di Lambek rigide -a study on learnability for rigid Lambek grammars[END_REF] that is a simplification of [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF].

The proof of convergence makes use of the following notions and notations:

G ⊂ G ′ This reflexive relation between G and G ′ holds whenever every lexical category assignment a ∶ T in G is in G ′ as well -in particular when G ′ is rigid, so is G, and both grammars are identical. Note that this is just the normal subset relation for each of the words in the lexicon G ′ : lex G (a) ⊂ lex G ′ (a) for every a in the lexicon of G ′ , with lex G (a) non-empty. Throughout the proof, we shall also use the subset relation symbol to signify inclusion of the generated languages; the intended meaning of "⊂" should always be clear from the context. size of a grammar The size of a grammar is simply the sum of the sizes of the occurrences of categories in the lexicon, where the size of a category is its number of occurrences of base categories (category variables or s). G ⊏ G ′ This reflexive relation between G and G ′ holds when there exists a substitution σ such that σ(G) ⊂ G ′ which does not identify different categories of a given word, but this is always the case when the grammar is rigid. sPF(G) As said earlier, sPF(G) is the the set of s proof frames generated by a Lambek categorial grammar G. GF (D) Given a set D of structured examples i.e. a set of s proof frames, the grammar GF (D) is define as in the examples above: it is obtained by collecting the categories of each word in the various examples of D. RG(D) Given a set of sPFs D, RG(D) is the rigid grammar/lexicon obtained by applying the most general unifier, when it exists, to GF (D) -in case the categories of a given word do not unify no category is assigned to this word, see footnote 4.

Proposition 3. Given a grammar G, the number of grammars H such that H ⊏ G is finite.

Proof. There are only finitely many grammars which are included in G, since G is a finite set of assignments. Whenever σ(H) = K for some substitution σ the size of H is smaller or equal to the size of K, and, up to renaming, there are only finitely many grammars smaller than a given grammar. By definition, if H ⊏ G then there exist K ⊂ G and a substitution σ such that σ(H) = K. Because there are only finitely many K such that K ⊂ G, and for every K there are only finitely many H for which there could exist a substitution σ with σ(H) = K (substitutions increase the category sizes) we conclude that, up to renaming, there are only finitely many

H such that H ⊏ G. ⊓ ⊔
From the definition of ⊏ and from proposition 1 one immediately has: Proof. By construction of GF (D), each category variable x labels at most one axiom of at most one sPF of D. According to the hypothesis D ⊂ sPF(G), every sPF ei in D is the sPF associated with an s proof net πi generated by G, and let us chose one such πi in case there are several of them. For every category variable x labelling the positive tip of an axiom ax j i in some of the ei we can define a substitution by σ(x) = T where T is the category that labels the positive tip of the same axiom ax j i in πi: indeed x occurs once, and such a substitution is well defined. When this substitution is applied to GF (D) it yields a grammar which only contains assignments from G -by applying the substitution to the whole sPF, it remains a well-categorised sPF, and in particular the formulae on the conclusions corresponding to the words, that are the dual of the Lambek categories in the lexicon, must coincide. 5 Hence we find a substitution such that GF (D) ⊂ G. This precisely shows that the algorithm proposed in section 6 converges in the sense of Gold's definition [START_REF] Abrusci | Non-commutative logic I: the multiplicative fragment[END_REF].

Proposition 4. If G ⊏ G ′ then sPF(G) ⊂ sPF(G ′ ). Proposition 5. If GF (D) ⊏ G then D ⊂ sPF(G).
8 Learning product free Lambek grammars from natural deduction frames

The reader may well find that the structure of the positive examples that we learn from, sorts of proofnets are too sophisticated structures to learn from. He could think that our learning process is a drastic simplification of the similar algorithms that use functor argument structures, i.e. name free natural deductions.

Let us first see that normal natural deductions are quite a sensible structure to learn Lambek grammars from. Tiede [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] observed that natural deductions in the Lambek calculus (be they normal or not) are plain trees, defined by two unary operators ( and introduction rules) and two binary operators ( and elimination rules), from formulae as leaves (hypotheses, cancelled or free). As opposed to the intuitionistic case, there is no need to specify which hypothesis is cancelled by the introduction rules, as they may be inferred inductively: a (respectively ) introduction rule cancels the left-most (respectively right-most) free hypothesis. He also observed that normal natural deductions should be considered as the proper parse structures, since otherwise any possible syntactic structure (a binary tree) is possible. Therefore is is natural to learn Lambek grammars from normal natural deduction frames -natural deductions from which category names have been erased but the final s. Indeed, s natural deduction frames are to Lambek categorial grammars what the functor-argument (FA) structures are to AB categorial grammars -these FA structures are the standard structures used for learning AB grammars by Buskowski, Penn and Kanazawa [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF][START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF]. The purpose of this section is to exhibit a one to one correspondence between cut-free proof nets of the product free Lambek calculus and normal natural deductions, thus justifying the use of proof frames for learning Lambek grammars. When there is no product, proof frames are the same as natural deduction frames that we initially used in [START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF].

They generalise the standard FA structures, and when the product is used, natural deduction become quite tricky [START_REF] Amblard | Natural deduction and normalisation for partially commutative linear logic and lambek calculus with product[END_REF][START_REF] Amblard | Calculs de représentations sémantiques et syntaxe générative : les grammaires minimalistes catégorielles[END_REF] and there are the only structures one can think about.

The correspondence between on one hand natural deduction or the isomorphic λ-terms and on the other hand, proof nets, can be traced back to [START_REF] Retoré | Le système F en logique linéaire[END_REF] (for second order lambda calculus) but the the closest result is the one for linear λ-calculus [START_REF] De Groote | Semantic readings of proof nets[END_REF].

Proofnets and natural deduction: climbing principal branches

As said in section 3, the formulae of product free Lambek calculus are defined by:

C ∶∶= s B C C C C
Hence their linear counterpart are a strict subset of the polarised linear formulae of subsection 4.1:

L ○ h ∶∶= P (L • h ℘ L ○ h ) (L ○ h ℘ L • h ) L • h ∶∶= P ⊥ (L ○ h ⊗ L • h ) (L • h ⊗ L ○ h )
Let us call these formulae the heterogeneous polarised formulae, which are either positive or negative formulae. In these heterogeneous formulae the connectives ℘ and ⊗ may only apply to a pair formulae with opposite polarity. The translation from Lambek categories to linear formulae and vice versa from subsection 4.1 apply to them as well.

One may think that a proof net corresponds to a sequent calculus proof which itself corresponds to a natural deduction: as shown in our book [START_REF] Moot | The logic of categorial grammars: a deductive account of natural language syntax and semantics[END_REF], this is correct, as far as one does not care about cuts -which are problematic in non commutative calculi, see e.g. [START_REF] Melliès | A topological correctness criterion for multiplicative non commutative logic[END_REF]. As it is well known in the case of intuitionnistic logic, cut-free and normal are different notions [START_REF] Zucker | The correspondence between cut-elimination and normalisation i , ii[END_REF], and proof net are closer to sequent calculus in some respects. If one translate inductively, rule by rule, a natural deduction into a sequent calculus or into a proof net, the elimination rule from A and A B yields a cut on the A B formula, written A ⊥ ℘ B in linear logic. We shall see how this can be avoided.

this rule requires at least two free hyp.

A leftmost free hyp.

.

. . [A] . . . . . . ⋅ ⋅ ⋅ B i binding A A B ∆ ⋅ ⋅ ⋅ A Γ ⋅ ⋅ ⋅ A B e B
this rule requires at least two free hyp.

A rightmost free hyp.

. . . . . . the formula defined as follows:

[A] . . . ⋅ ⋅ ⋅ B i binding A B A Γ ⋅ ⋅ ⋅ B A ∆ ⋅ ⋅ ⋅ A e B Fig
if p = 0 C[] = C if εp = l C[(ε1 ,
G1), . . . , (εp-1, Gp-1), (εp, Gp)] = Gp C[(ε1, G1), . . . , (εp-1, Gp-1)] if εp = r C[(ε1, G1), . . . , (εp-1, Gp-1), (εp, Gp)] = C[(ε1, G1), . . . , (εp-1, Gp-1)] Gp An important property of normal natural deductions is that whenever the last rule is an elimination rule, there is a principal branch leading from the conclusion to a free hypothesis [30, proposition 2.10 page 35] When a rule e (resp. e) is applied between a right premise A X (resp. a left premise X A) and a formula A as its left (resp. right) premise, the premise A X (resp. a left premise X A) is said to be the principal premise. In a proof ending with an elimination rule, a principal branch is a path from the root C = X0 to a leaf C[(ε1, G1), . . . , (εp, Gp)] = Xp such that one has Xi = C[(ε1, G1), . . . , (εi, Gi)] and also Xi+1 = C[(ε1, G1), . . . , (εi+1, Gi+1)] and Xi is the conclusion of an elimination rule, e if εi+1 = l and e if εi+1 = r, with principal premise Xi+1 and Gi+1 as the other premise.

Let d be a normal natural deduction with conclusion C and hypotheses H1, . . . , Hn. The deduction d is inductively turned into a cut-free proof net with conclusions Hn-, . . . , H1-, C+ as follows (we only consider because is symmetrical).

-If d is just an hypothesis A which is at the same time its conclusion the corresponding proof net is the axiom A, A ⊥ . -If d ends with a intro, from A, H1, . . . , Hn ⊢ B to H1, . . . , Hn ⊢ A B, by induction hypothesis we have a proof net with conclusions (Hn)-, . . . , (H1)-, A-, B+. The heterogeneous ℘ rule applies since B+ is heterogeneous positive and A-heterogeneous negative. A ℘ rule yields a proof net with conclusions (Hn)-, . . . , (H1)-, A -℘B+, and A -℘B+ is precisely (A B)+ -The only interesting case is when d ends with an elimination rule, say e. In this case there is a principal branch, say with hypothesis C[(ε1, G1), . . . , (εp, Gp)] which is applied to Gi's. Let us call Γi = H 1 i , . . . , H k i i the hypotheses of Gi, and let di be the proof of Gi from Γi. By induction hypothesis we have a proof net πi with conclusions (Γi)-, (Gi)+. Let us define the proof net π k of conclusion C k -= C[(ε1, G1), . . . , (ε k , G k )]-, Γi for i ≤ k and C+ by:

• if k = 0 then it is an axiom C ⊥ , C (consistent with the translation of an axiom) • otherwise π k+1 is obtained by a times rule between the conclusions C k of π k and G k+1 + of π k+1 When εi = r then the conclusion chose the conclusion of this link to

G k+1 + ⊗C k - that is C k -G k+1 + = C k+1 -and when εi = l the conclusion is C k -⊗G k+1 + that is G k+1 + C k -= C k+1 -.
hence, in any case the conclusions of π k+1 are C k+1 + C+ and the Γi for i ≤ k + 1. The translation of d is simply π p , which has the proper conclusions. As the translation does not introduce any cut-rule, the result is a cut-free proof net.

From cut-free proof nets to normal natural deductions

There is an algorithm that performs the reverse translation, presented for multiplicative linear logic and linear lambda terms in [START_REF] De Groote | Semantic readings of proof nets[END_REF]. It strongly relies on the correctness criterion, which makes sure that everything happens as indicated during the algorithm and that it terminates. This algorithm always points at a formula in the proof net, and draws paths in the proof net. Going up means going to an immediate sub formula, and going down means considering the immediate super formula. The algorithms label the proof net nodes with Lambek lambda terms that are natural deductions written as terms, and the natural deduction that translates the proof net is the Lambek lambda term labelling the output of the proof net.

1. Enter the proof net by its unique output conclusion. 2. Go up until you reach an axiom. Because of the polarities, during this upwards path, you only meet ℘-links, which correspond to the introduction rules λrx T i i or λ l x T i i , the Tis being the input formulae (the hypotheses that are cancelled). Such formulae are labelled with distinct variables xi.

3. Use the axiom link and go down with the input polarity. Hence you only meet ⊗ links (*) until you reach a conclusion or a ℘ link. In both cases, this formula is the type of the head-variable of the normal Lambek λ-term. If it is the premise of a ℘-link, then it is necessarily a ℘ link on the path of step 2 (because of the correctness criterion). In this case, the head variable (the hypothesis of the principal branch) is bound by the corresponding λr or λ l of the previous step 2. Otherwise it the head variable is free. 4. The output formulae that were left unlabelled when going down are the output premises of the ⊗ links (*) that we met at step 3. To label them, one goes up from theses output formulae, applying again step 2. The λ-term that labels the output conclusion is normal: only variables are applied to some arguments during the translation. It is easily read as a normal natural deduction.

Learning product free Lambek grammars from natural deduction

We have defined a bijective correspondence between cut free product free proof nets and normal product free natural deduction. Therefore we also have a correspondence between s proof frames and name free natural deduction whose conclusion is s. Hence, if one wishes to, it is possible to learn product free Lambek grammars from natural deduction without names but the final s, as we did in [START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF]. Such structures are simply the generalisation to Lambek calculus of the FA structures that are commonly used for basic categorial grammars by [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF][START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF].

Conclusion and possible extensions

A criticism that can be addressed to our learning algorithm is that the rigidity condition on Lambek grammars is too restrictive. One can say, as in [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF] that k-valued grammars can be learned by doing all the possible unifications that lead to less than k categories. Every successful unifications yielding a grammar with less than k categories should be kept, because in a later step it is quite possible that one works while the others do not: hence this approach is computationally intractable. An alternative is to use a precise part-of-speech tagger and to consider one word with different categories as several distinct words. This looks more accurate and has been carried out effectively, with the help of some statistical techniques. [START_REF] Sandillon-Rezer | Using tree transducers for grammatical inference[END_REF][START_REF] Moot | Semi-automated extraction of a wide-coverage type-logical grammar for French[END_REF] The principal weakness of identification in the limit is that too much structure is required on the input examples. Ideally, one would like to learn directly from strings, but in the case of Lambek grammars it has been shown to be impossible in [START_REF] Foret | Lambek rigid grammars are not learnable from strings[END_REF]. One may think that it could be possible to try every possible structure on sentences as strings of words as done in [START_REF] Kanazawa | Learnable classes of categorial grammars[END_REF] for basic categorial grammars. Unfortunately, in the case of Lambek grammars, with or without product, this cannot be done. Indeed, there can be infinitely many structures corresponding to a sentence, because a cancelled hypothesis does not have to be anchored in one the finitely many words of the sentence. Hence we ought to learn from structured sentences, as we did. From the point of view of first language acquisition we know that some structure is available, but it is unlikely that the structured sentences are the proof frames of the present article. The real structure available to the learner includes prosodic and semantic informations, and no one knows how to formalise these structures in order to simulate the natural data used during the actual language learning process. From a computational linguistic perspective, our result is not as restrictive as it may seem. Indeed, there exist tools that annotate corpora, and one may implement other tools that turn standard annotations into the annotations we need. These shallow and efficient processes may lead to structures from which one can infer the proper structure for an algorithm like the one we presented in this paper. In the case of proof nets or frames, as observed long ago, axioms express the consumption of the valencies. This is the reason why, apart from the structure of the formulae, the structure of the proof frames is not so different from dependency annotations and such annotations can be used to infer categorial structures as done by Moot and Sandillon-Rezer [START_REF] Sandillon-Rezer | Using tree transducers for grammatical inference[END_REF][START_REF] Moot | Semi-automated extraction of a wide-coverage type-logical grammar for French[END_REF]. However, the automatic acquisition of wide-coverage grammars for natural language processing applications, certainly requires a combination of machine learning techniques and of identification in the limit à la Gold, although up to now there are not so many such works. Grammatical formalisms that can be represented in Lambek grammars can also be learnt like we did in this paper. For instance, a categorial version of Stabler's minimalist grammars [START_REF] Stabler | Derivational minimalism[END_REF] can be learnt that way as the attempts by Fulop or by us show [START_REF] Fulop | On The Logic And Learning Of Language[END_REF][START_REF] Bonato | Learning rigid Lambek grammars and minimalist grammars from structured sentences[END_REF] This should be even better with the so-called Categorial Minimalist grammars of Lecomte, Amblard and us [START_REF] Amblard | Calculs de représentations sémantiques et syntaxe générative : les grammaires minimalistes catégorielles[END_REF][START_REF] Amblard | Categorial minimalist grammars: From generative grammar to logical form[END_REF]

Fig. 1 .

 1 Fig. 1. Human languages and the classes of the Chomsky hierarchy (with parsing complexity).

Fig. 2 .

 2 Fig. 2. Sequent calculus rule for the Lambek calculus

  x23 ⊗ x25) x22)... ((x28 ⊗ x27) ⊗ ... ... (x28 ⊗ x27))

Proof.Proposition 6 .Proposition 7 .

 67 By construction of GF (D), we have D ⊂ sPF(GF (D)). In addition, because of proposition 4, we have sPF(GF (D)) ⊂ sPF(G). ⊓ ⊔ If RG(D) exists then D ⊂ sPF(RG(D)). Proof. By definition RG(D) = σu(GF (D)) where σu is the most general unifier of all the categories of each word. So we have GF (D) ⊏ RG(D), and applying proposition 5 with G = RG(D) we obtain D ⊂ sPF(RG(D)). ⊓ ⊔ If D ⊂ sPF(G) then GF (D) ⊏ G.

⊓ ⊔ Proposition 8 .Proposition 9 .Theorem 4 .

 894 When D ⊂ sPF(G) with G a rigid grammar, the grammar RG(D) exists and RG(D) ⊏ G.Proof. By proposition 7 we have GF (D) ⊏ G, so there exists a substitution σ such that σ(GF (D)) ⊂ G. As G is rigid, σ unifies all the categories of each word. Hence there exists a unifier of all the categories of each word, and RG(D) exists. RG(D) is defined as the application of most general unifier σu to GF (D). By the definition of a most general unifier6 , there exists a substitution τ such that σ = τ ○ σu.Hence τ (RG(D)) = τ (σu(GF (D))) = σ(GF (D)) ⊂ G; thus τ (RG(D)) ⊂ G, hence RG(D) ⊏ G. ⊓ ⊔ If D ⊂ D ′ ⊂ sPF(G) with G a rigid grammar then RG(D) ⊏ RG(D ′ ) ⊏ G.Proof. Because of proposition 8 both RG(D) and RG(D ′ ) exist. We have D ⊂ D ′ and D ′ ⊂ sPF(RG(D ′ )), so D ⊂ sPF(RG(D ′ )); hence, by proposition 8 applied to D and G = RG(D ′ ) (a rigid grammar) we have RG(D) ⊏ RG(D ′ ). ⊓ ⊔ The algorithm RG for learning rigid Lambek grammars converges in the sense of Gold. Proof. Let (Di) i∈N be an increasing sequence of sets of examples in sPF(G) enumerating sPF(G), in other words ∪i∈ωDi = sPF(G): D1 ⊂ D2 ⊂ ⋯Di ⊂ Di+1⋯ ⊂ sPF(G) Because of proposition 8 for every i ∈ ω the rigid grammar RG(Di) exists and because of proposition 9 the rigid grammars RG(Di) define a ⊏-increasing sequence of grammars which by proposition 8 is bounded by G: RG(D1) ⊏ RG(D2) ⊏ ⋯RG(Di) ⊏ RG(Di+1)⋯ ⊏ G As they are only finitely many grammars H ⊏ G (proposition 3) this sequence RG(Di) is stationary after a certain rank: there exists an integer N such that for all n ≥ N RG(Dn) = RG(D N ). Let us show that the langue generated by RG(D N ) is the one to be learnt, i.e. let us prove that sPF(RG(D N )) = sPF(G) by proving the two inclusions: 1. Firstly, let us prove that sPF(RG(D N )) ⊃ sPF(G) Let π f be an sPF in sPF(G). Since ∪i∈ωDi = sPF(G) there exists a p such that π f ∈ sPF(Dp). -If p < N , because Dp ⊂ D N , π f ∈ D N , and by proposition 6 π f ∈ sPF(RG(D N )). -If p ≥ N , we have RG(Dp) = RG(D N ) since the sequence of grammars is stationary after N . By proposition 6 we have Dp ⊂ sPF(RG(Dp)) hence π f ∈ sPF(RG(D N )) = sPF(RG(Dp)). In all cases, π f ∈ sPF(RG(D N )). 2. Let us finally prove that sPF(RG(D N )) ⊂ sPF(G): Since RG(D N ) ⊏ G, by proposition 4 we have sPF(RG(D N )) ⊂ sPF(G) ⊓ ⊔

. 5 .

 5 Fig. 5. Natural deduction rule for product free Lambek calculus

  . Basic categorial grammars BCG also known as AB grammars have their categories in C ∶∶= s B C C C C and the derivable sequents are the ones that are derivable in the Lambek calculus with elimination rules only ∆ ⊢ A and Γ ⊢ B A (respectively Γ ⊢ A B) yields

	Γ, ∆ ⊢ B (respectively ∆, Γ ⊢ B) -in such a setting the empty
	sequence is naturally prohibited even without saying so. [7]
	2. The original Lambek grammars [27] also have their categories in the
	same inductive set C ∶∶= s B C C C C and the derivable sequents
	are the ones that are derivable in the Lambek calculus without empty
	antecedent, i.e. with rules of figure 3 except ⊗i and ⊗ h -a variant
	allows empty antecedents.
	3. Lambek grammars with product (LCGp) have their categories in
	C⊗ ∶∶= s B C⊗ C⊗ C⊗ C⊗ C⊗ ⊗ C⊗ and the derivable sequents

are the ones that are derivable in the Lambek calculus with product without empty antecedents with all the rules of figure

We here say "words" because they are linguistic words, while other say "letters" or "terminals," and we say "sentences" for sequences of words where others say "words" for sequences of "letters" or "terminals"

There is an unimportant choice here: we could either say that φ is undefined in this case. In both cases φ does not seem to be consistent, that is to propose a grammar that actually generates the examples seen so far. However, as we shall see, in the convergence proof, when the algorithm is applied to a language in the class, categories of a given word always unify, and φ is a total and consistent learning function.

One can alternatively proceeds with positive linear formulae F as subsection 4.1 shows.

Unifiers and most general unifiers work as usual even though we unify sets of categories, see section 3.