Keywords: Théorie formelle de l'apprentissage, apprentissage automatique, calcul de Lambek, linguistique computationnelle, grammaires formelles

Une étude sur l'apprenabilité des grammaires de Lambek rigides Résumé : On présente les notions élémentaires du paradigme d'apprenabilité à la limite de E. M. Gold, une formalisation du processus cognitif qui permet l'apprentissage des règles de la grammaire d'une langue naturelle à partir d'un échantillon fini d'énoncés bien formés. Ensuite, on présente les grammaires de Lambek, un formalisme issu des grammaires catégorielles qui a des qualités intéréssantes par rapport à l'interface syntaxe-sémantique. Nous détaillons un résultat d'apprenabilité pour les grammaires de Lambek Rigides dans le modèle d'apprentissage de Gold à partir d'exemples structurés.

Introduction

How comes it that human beings, whose contacts with the world are brief and personal and limited, are nevertheless able to know as much as they do know?

Sir Bertrand Russell (quoted by Noam Chomsky in [START_REF] Chomsky | Reflections on Language[END_REF]).

Formal Learning Theory was introduced by E. M. Gold in 1967 (see [START_REF] Gold | Language identification in the limit[END_REF]) as a first effort to provide a rigorous formalization of grammatical inference, that is the process by which a learner, exposed to a finite subset of well-formed sentences of a given language, gets to infer the grammar that generates it. The typical example is first language acquisition in human beings: a child gets to master, in a completely spontaneous way and on the basis of the relatively small amount of information provided by sentences uttered in its cultural environment, the highly complex and subtle rules of her mother tongue, to the point that she can utter correct and original sentences before her third year of life. Another example is scientific inductive reasoning (see [START_REF] Daniel | Formal learning theory[END_REF]). In this case the learner is the scientist who, on the basis of finite amount of empirical evidences provided by natural phenomena, formulates hypotheses about the explanation that account for them.

After initial skepticism (largely due to Gold himself, whose first results in his model were proofs of non-learnability for the four classes of grammars of Chomsky's hierarchy), recently there has been a renewal of interest toward this computational model of learning. One of the most remarkable results is Shinohara's (see [START_REF] Shinohara | Inductive inference from positive data is powerful[END_REF]), who proves that if we bound the number of rules in a contextsensitive grammar, it becomes learnable in Gold's paradigm.

Likewise, Lambek grammars have recently known a renewed interest as a mathematical tool for the description of linguistics phenomena, after having being long neglected after their definition in [START_REF] Lambek | The mathematics of sentence structure[END_REF]. Van Benthem was among the first who stressed the singular correspondence between Montague semantics (see [START_REF] Montague | The proper treatment of quantification in ordinary english[END_REF]) and the notion of structure associated to a sentence of a Lambek grammar. Furthermore, a recent work by Hans-Jörg Tiede (see [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF]) has made clearer the notion of structure of a sentence in a Lambek grammar, in contrast with a previous definition by Buszkowski (see [START_REF] Buszkowski | Generative capacity of non-associative lambek calculus[END_REF]). In doing so, he proves that the class of tree languages generated by Lambek grammars strictly contains the class of tree languages generated by context-free grammars. This remarkable result proves that Lambek grammars have more strong generative capacity than contextfree languages, whose structure language is local. This document is organized as follows. Section 2 presents the basic notions of Gold's formal learning theory and summarizes the principal results achieved since its introduction. Section 3 introduces Lambek grammars: special attention is devoted to the features which make them attractive for computational linguistics. Section 4 presents the class of rigid Lambek grammars, which is the object of our learning algorithm. In Section 5 we present a learning algorithm for rigid Lambek grammars from structured sentences. Convergence for the algorithm, and therefore learnability for the class of rigid Lambek grammars is proved.

2 Grammatical Inference 2.1 Child's First Language Acquisition One of the most challenging goals for modern cognitive sciences is providing a sound theory accounting for the process by which any human being masters the highly complex and articulated grammatical structure of her mother tongue in a relatively small amount of time. Between the age of 3 and 5 we witness in children a linguistic explosion, at the end of which the child has learnt all the grammatical rules of her mother tongue, the subsequent learning being but lexical acquisition. Moreover, cognitive psychologists agree (see [START_REF] Daniel | An Invitation to Cognitive Science, volume 1[END_REF]) in stating that the learning process is almost completely based on positive evidence (i.e. correct statements belonging to her mother tongue) provided by the cultural environment wherein the child has grown up. Negative evidence (any information or feedback given to the child to identify wrong sentences) doesn't seem to play any significant role in the process of learning (see [START_REF] Pinker | The Language Instict[END_REF]). Simply stated, the child acquires a language due to the exposition to correct sentences coming from her linguistic environment and not to the negative feedback she gets when she utters a wrong sentence.

The astounding ability to extract highly articulated knowledge (i.e. the grammar of a human language) from a relatively small amount of "raw" data (i.e. the statements of the language the child is exposed to during her early childhood) can be considered as an instance of a grammatical induction problem. Formal learning theory aims at providing a formal framework to account for this process.

Gold's Model

The process of child's first language acquisition can be seen as an instance of the more general problem of grammatical inference. In particular, we will restrict our attention to the process of inference from positive data only. Simply stated, it's the process by which a learner can acquire the whole grammatical structure of a formal language on the basis of well-formed sentences belonging to the target language.

In 1967 E. M. Gold defined (see [START_REF] Gold | Language identification in the limit[END_REF]) the formal model for the process of grammatical inference from positive data that will be adopted in the present work. In Gold's model, grammatical inference is conceived as an infinite process during which a learner is presented with an infinite stream of sentences s 0 , s 1 , . . . , s n . . ., belonging to language which has to be learnt, one sentence at a time. Each time the learner is presented with a new sentence s i , she formulates a new hypothesis G i on the nature of the underlying grammar that could generate the language the sentences she has seen so far belong to: since she is exposed to an infinite number of sentences, she will conjecture an infinite number of (not necessarily different) grammars G 0 , G 1 , . . . , G n . . ..

G

Two basic assumptions are made about the stream of sentences she is presented with: (i) only grammatical sentences (i.e. belonging to the target language) appear in the stream, coherently with our commitment to the process of grammar induction from positive data only; (ii) every possible sentence of the language must appear in the stream (which must be therefore an enumeration of the elements of the language).

The learning process is considered successful when, from a given point onward, the grammar conjectured by the learner doesn't change anymore and it coincides with the grammar that actually generates the target language. It is important to stress that one can never know whether the learning has been successful or not: at each finite stage, there is no way to predict whether next sentence will change or not the current hypothesis. The goal of the theory lies in devising a successful strategy for making guesses, that is, one which can be proved to converge to the correct grammar after a finite (but unknown) amount of time (or positive evidence, which is the same in our model). Gold called this criterion of successful learning identification in the limit.

According to this criterion, a class of grammars is said to be learnable when, for any language generated by a grammar belonging to the class, and for any enumeration of its sentences, there is a learning function that successfully identifies the correct grammar that generates the language. Research on formal learning theory is devoted to identify non-trivial classes of languages which are learnable in Gold's model, or criterions for (un)learnability for a class of languages on the basis of some structural property of the language.

As it will be made clear in the following sections, accepting this criterion for successful learning means that we are not interested in when the learning has taken place. The goal of the theory is to devise effective procedures such that, if applied to the infinite input stream of sentences, are guaranteed to converge after a finite number of steps to the correct grammar.

Basic Notions

We present here a short summary of formal learning theory as described in [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF], whence we take the principal definitions and notation conventions.

Grammar Systems

The fist step to formalize first language acquisition is the definition of the "cultural environment" within which the process takes place and of the "positive evidences" the learner is exposed to. To do this, we introduce the notion of grammar system. Definition 3.1 (Grammar System) A grammar system is a triple Ω, S,L , where

• Ω is a certain recursive set of finitary objects on which mechanical computations can be carried out;

• S is a certain recursive subset of Σ * (the set of finite sequences of elements of Σ), where Σ is a given finite alphabet;

• L is a function that maps elements of Ω to subsets of S, i.e. L : Ω → ℘(S ).

We can think of Ω as the "hypothesis space", whence the learner takes her grammatical conjectures, according to the positive examples she has been exposed to up to a certain finite stage of the learning process. Elements of Ω are called grammars.

Positive examples presented to the learner belong to the set S (often we simply have S = Σ * ); its elements are called sentences, while its subsets are called languages. As it will be made clear in the following sections, the nature of elements in S strongly influences the process of learning: intuitively, we can guess that the more information they bear, the easier the learning process is, if it is possible at all. The function L maps each grammar G belonging to Ω into a subset of S which is designated as the language generated by G. That is why we often refer to L as the naming function. The question of whether s ∈ L(G) holds between any s ∈ S and G ∈ Ω is addressed to as the universal membership problem.

Example 3.2 Let Σ be any finite alphabet and let DFA be the set of deterministic finite automata whose input alphabet is Σ. For every M ∈ DFA, let L(M) be the set of strings over Σ accepted by M. Then DFA, Σ * , L is a grammar system. Example 3.3 Let Σ be any finite alphabet and let RegExpr be the set of regular expressions over Σ. For every r ∈ RegExpr, let L(r) be the regular language represented by r. Then RegExpr, Σ * , L is a grammar system. Example 3.4 [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF] Let Σ any finite alphabet, and let Var be a countably infinite set of variables, disjoint from Σ. A pattern over Σ is any element of (Σ ∪ Var) + : let Pat be the set of patterns over Σ. For every p ∈ Pat, let L(p) be the set of strings that can be obtained from p by uniformly replacing each variable x occurring in p by some string w ∈ Σ + . The triple Pat, Σ + , L is a grammar system.

Learning Functions, Convergence, Learnability

Once formally defined both the set of possible "guesses" the learner can make and the set of the positive examples she is exposed to, we need a formal notion for the mechanism by which the learner formulates hypotheses, on the basis finite sets of well-formed sentences of a given language, about the grammar that generates them. A learning function can be seen as a formalization of the cognitive process by which a learner conjectures that a given finite set of sentences belongs to the language generated by a certain grammar. Since it is a partial function, it is possible that the learner does not infer any grammar from the stream of sentences she has heard so far.

INRIA

φ (l ) φ (l ) φ (l ) Ω S G G L(G) l 1 1 l 2 l n 2 n Figure 1: Grammatical Inference
According to the informal model outlined in section 2.2, in a successful learning process the guesses made by the learner remain the same from a certain point onward in the infinite process of learning. That is to say, there must be a finite (although unknown) stage after which the grammar inferred on the basis of all the positive examples the learner has seen so far does not change. This informal idea can be made precise by introducing the notion of convergence for a learning function: Definition 3.6 (Convergence) Let Ω, S,L be a grammar system, ϕ a learning function, s i i∈N = s 0 , s 1 , . . . an infinite sequence of sentences belonging to S, and let G i = ϕ( s 0 , . . . , s i ) for any i ∈ N such that ϕ is defined on the finite sequence s 0 , . . . , s i . ϕ is said to converge to G on s i i∈N if there exists n ∈ N such that, for each i ≥ n, G i is defined and G i = G (equivalently, if G i = G for all but finitely many i ∈ N).

As we have already pointed out, one can never say exactly if and when convergence of a learning function to a certain grammar has taken place: this is due to the infinite nature of the process through which a learner infers a grammar a given in Gold's model. At any finite stage of the learning process there is no way to know whether the next sentence the learner will see causes the current hypothesis to change or not.

We will say that a class of grammars is learnable when for each language generated by its grammars there exists a learning function which converges to the correct underlying grammar on the basis of any enumeration of the sentences of the language. Formally: Definition 3.7 Let Ω, S,L be a grammar system, and G ⊆ Ω a given set of grammars. The learning function ϕ is said to learn G if the following condition holds:

• for every language L ∈ L(G) = {L(G) | G ∈ G},
• and for every infinite sequence s i i∈N that enumerates L (i.e., {s i | i ∈ N} = L) there exists a G ∈ G such that L(G) = L, such that ϕ converges to G on s i i∈N .

So we will say that a given learning function converges to a single grammar, but that it learns a class of grammars. The learning for a single grammar, indeed, could be trivially implemented by a learning function that, for any given sequence of sentences as input, always returns that grammar. Definition 3.8 (Learnability of a Class of Grammars) A class G of grammars is said to be learnable if and only if there exists a learning function that learns G. It is said to be effectively learnable if the learning function is computable.

Obviously effective learnability implies learnability. Example 3.9 Let Ω, S,L be any grammar system and let G = {G 0 , G 1 , G 2 } ⊆ Ω and suppose there are elements w 1 ,

w 2 ∈ S such that w 1 ∈ L(G 1 ) -L(G 0 ) and w 2 ∈ L(G 2 ) -(L(G 1 ) ∪ L(G 0 )).
Then it's easy to verify that the following learning function learns G:

ϕ( s 0 , . . . , s i ) =    G 2 if w 2 ∈ {s 0 , . . . , s i }, G 1 if w 1 ∈ {s 0 , . . . , s i } and w 2 ∈ {s 0 , . . . , s i }, G 0 otherwise.

INRIA

Example 3.10 Let's consider the grammar system CFG, Σ * , L of context-free grammars over the alphabet Σ. Let G be the subclass of CFG consisting of grammars whose rules are all of the form S → w, where w ∈ Σ * . We can easily see that L(G) is exactly the class of finite languages over Σ. Let's define the learning function ϕ as ϕ( s 0 , . . . , s i ) = Σ, {S}, S, P , where P = {S → s 0 , . . . , S → s i }.

Then ϕ learns G.

Structural Conditions for (Un)Learnability

One of the first important results in learnability theory presented in [START_REF] Gold | Language identification in the limit[END_REF] was a sufficient condition to deduce the unlearnability of a class G of grammars on the basis of some formal properties of the class of languages L = L(G) (see theorem 3.14). We present here some structural conditions sufficient to deduce (un)learnability for a class of grammars.

Existence of a Limit Point

Definition 3.11 (Limit Point) A class L of languages has a limit point if there exists an infinite sequence L n n∈N of languages in L such that1

L 0 ⊂ L 1 ⊂ • • • ⊂ L n ⊂ • • •
and there exists another language L ∈ L such that

L = n∈N L n
The language L is called limit point of L.

Lemma 3.12 (Blum and Blum's locking sequence lemma, 1975) Suppose that a learning function ϕ converges on every infinite sequence that enumerates a language L. Then there is a finite sequence w 0 , . . . , w l (called a locking sequence for ϕ and L) with the following properties:

(i) {w 0 , . . . , w l } ⊆ L, (ii) for every finite sequence v 0 , . . . , v m , if {v 0 , . . . , v m } ⊆ L, then ϕ( w 0 , . . . , w l ) = ϕ( w 0 , . . . , w l , v 0 , . . . , v m ). L 0 L 1 L 2 L n L Figure 2: A limit point for a class of languages.
Intuitively enough, the previous lemma (see [START_REF] Blum | Toward a mathematical theory of inductive inference[END_REF]) states that if a learning function converges, then there must exist a finite subsequence of input sentences that "locks" the guesses made by the learner on the grammar the learning function converges to: that is to say, the learning function always returns the same grammar for any input stream of sentences containing that finite sequence. The locking sequence lemma proves one of the first unlearnability criterions in Gold's framework: Theorem 3.13 If L(G) has a limit point, then G is not learnable.

An easy consequence of the previous theorem is the following Theorem 3.14 [START_REF] Gold | Language identification in the limit[END_REF]) For any grammar system, a class G of grammars is not learnable if L(G) contains all finite languages and at least one infinite language.

Proof sketch. Let L 1 ⊂ L 2 ⊂ . . . be a sequence of finite languages and let L ∞ = ∞ i=1 L i . Suppose there were a learning function ϕ that learns the class {L | L is finite} ∪ {L ∞ }. Then ϕ must identify any finite language in a finite amount of time. But then we can build an infinite sequence of sentences that forces ϕ to make an infinite number of mistakes: we first present ϕ with enough examples from L 1 to make it guess L 1 ; then with enough examples from L 2 to make it guess L 2 , and so on. Note that all our examples belong to L ∞ .

(In)Finite Elasticity

As we have seen in the previous section, the existence of a limit point for a class of languages implies the existence of an "infinite ascending chain" of languages like the one described by the following, weaker condition: Definition 3.15 (Infinite Elasticity) A class L of languages is said to have infinite elasticity if there exists an infinite sequence s n n∈N of sentences and an infinite sequence L n n∈N of languages such that for every n ∈ N,

s n / ∈ L n , INRIA and {s 0 , . . . , s n } ⊆ L n+1 .
The following definition, although trivial, identifies an extremely useful criterion to deduce learnability for a class of grammars: Definition 3.16 (Finite Elasticity) A class L of languages is said to have finite elasticity if it doesn't have infinite elasticity.

Dana Angluin proposed in [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF] a characterization of the notion of learnability in a "restrictive setting" which is of paramount importance in formal learning theory. Such restrictions are about the membership problem and the recursive enumerability for the class of grammars whose learnability is at issue. Let Ω, S,L be a grammar system and G ⊆ Ω a class of grammars, let's define: Condition 3.17 There is an algorithm that, given s ∈ S and G ∈ G, determines whether s ∈ L(G). Condition 3.18 G is a recursively enumerable class of grammars. Condition 3.17 is usually referred to as decidability for the universal membership problem for grammars, and condition 3.18 as the recursive enumerability condition. Such restrictions are not unusual in concrete situations where learnability is at stake, so they do not significantly affect the usefulness of the following characterization of the notion learnability under such restrictive conditions.

Theorem 3.19 [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF] Let Ω, S,L be a grammar system for which the universal membership problem is decidable and let G be a recursively enumerable subset of Ω. Then G is learnable if and only if there exists a computable partial function ψ : Ω × N S such that:

(i) for all n ∈ N, ψ(G, n) is defined if and only if G ∈ G and L(G) = / 0; (ii) for all G ∈ G,T G = {ψ(G, n) | n ∈ N} is a finite subset of L(G); (iii) for all G, G ∈ G, if T G ⊆ L(G ), then L(G ) ⊂ L(G).
Note: From this point onward, unless otherwise stated, we will restrict our attention to classes of grammars that fulfill both condition 3.17 and condition 3.18.

Angluin's theorem introduces the notion of T G as the tell-tale set for a given language. Learnability in the restricted environment is characterized by the existence of a mechanism (the function ψ) to enumerate all the sentences belonging to such a finite subset of the target language. Even more, a tell-tale set for a given grammar G is such that if it is included in the language generated by another grammar G , then

• either L(G) is included in L(G ),
• or L(G ) contains other sentences as well as those belonging to L(G).

Otherwise stated, it is never the case that T G ⊆ L(G ) ⊆ L(G). The point of the tell-tale subset is that once the strings of that subset have appeared among the sample strings, we need not fear overgeneralization in guessing a grammar G. This is because the true answer, even if it is not L(G), cannot be a proper subset of L(G). This means that a learner who has seen only the sentences belonging to the tell-tale set for a given grammar G, is justified in conjecturing G as the underlying grammar, since doing so never results in overshooting or inconsistency.

L( )

G T G L( ) GĹ ( ´´) G Figure 3: A tell-tale set for L(G).
As a consequence of Angluin's theorem, Wright proved in [START_REF] Wright | Identifications of unions of languages drawn from an identifiable class[END_REF] the following Theorem 3.20 [START_REF] Wright | Identifications of unions of languages drawn from an identifiable class[END_REF] Let Ω, S,L and G be as in theorem 3.19. If L(G) has finite elasticity, then G is learnable.

In such a restricted framework, therefore, the task of proving learnability for a certain class of grammars can be reduced to the usually simpler task of proving its finite elasticity. Due to Wright's theorem we can establish the following useful implications

L(G) has finite elasticity † ⇒ G is learnable L(G) has a limit point ⇒ G is unlearnable G is unlearnable † ⇒ L(G) has infinite elasticity
The implications indicated by † ⇒ depend on the decidability of universal membership and recursive enumerability of the class of grammars G at issue, as defined in conditions 3.17 and 3.18.

Kanazawa's Theorem

The following theorem (see [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]), which is a generalization of a previous theorem by Wright, provides a sufficient condition for a class of grammars to have finite elasticity, and therefore to be INRIA learnable. A relation R ⊆ Σ * × ϒ * is said to be finite-valued if and only if for every s ∈ Σ * , the set {u ∈ ϒ * | sRu} is finite. Theorem 3.21 Let M be a class of languages over ϒ that has finite elasticity, and let R ⊆ Σ * × ϒ * be a finite-valued relation. Then

L = {R -1 [M] | M ∈ M } also has finite elasticity.
This theorem is a powerful tool to prove finite elasticity (and therefore learnability) for classes of grammars. Once we prove the finite elasticity for a certain class of grammars in the "straight" way, we can get a proof for finite elasticity of other classes of grammars, due to the relatively loose requirements of the theorem. All we have to do is to devise a "smart" finite-valued relation between the first class and a new class of grammars such that the anti-image of the latter under this relation is the class for which we want to prove finite elasticity.

Σ * Υ * R M M] R [ -1

Constraints on Learning Functions

In the definition of learnability nothing is said about the behaviour of learning functions apart from convergence to a correct grammar. Further constraints can be imposed: one can choose a certain learning strategy. Intuitively, a strategy refers to a policy, or preference, for choosing hypotheses. Formally, a strategy can be analyzed as merely picking a subset of possible learning functions. Strategies can be grouped by numerous properties. We choose to group them by restrictiveness, defined as follows: Definition 3.22 (Restrictiveness) If a strategy reduces the class of learnable languages it is said to be restrictive.

For example, strategies are grouped as computational constraints (computability, time complexity), constraints on potential conjectures (consistency), constraints on the relation between conjectures (conservatism), etc. We provide hereby a list of the most common restrictive strategies that can be adopted by learning functions.

Non-restrictive Constraints

The proof of theorem 3.19 implies that in a grammar system where universal membership is decidable, a recursively enumerable class of grammars is learnable if and only if there is a computable learning function that learns it order-independently, prudently, and is responsive and consistent on this class. Definition 3.23 (Order-independent Learning) A learning function ϕ is said to learn G orderindependently whenever for all L ∈ L(G), there exists G ∈ G such that L(G) = L and for all infinite sequences s i i∈N that enumerate L, ϕ converges on s i i∈N to G.

Intuitively this seems a reasonable strategy. There does not seem to be an a priori reason why either the order of presentation should influence the final choice of hypothesis. On the other hand, it has already been proved (see [START_REF] Jain | Systems that Learn[END_REF]) that in any grammar system, a class of grammars is learnable if and only if there is a computable learning function that learns it order-independently. Definition 3.24 (Exact Learning) A learning function ϕ is said to learn G exactly whenever for all G such that ϕ learns G , L(G ) ⊆ L(G).

In other words, the learning function will not hypothesize grammars that are outside its class. This is not really a constraint on learning functions, but on the relation between a class of languages and a learning function. For every learning function there exists a class that it learns exactly. The reason for this constraint is the idea that children only learn languages that have at least a certain minimal expressiveness. If we want to model language learning, we want learning functions to learn a chosen class exactly. There seems to be empirical support for this idea. Some of it comes from studies of children raised in pidgin dialects, some from studies of sensory deprived children (see [START_REF] Pinker | The Language Instict[END_REF]). Definition 3.25 (Prudent Learning) A learning function ϕ is said to learn G prudently whenever ϕ learns G and range(ϕ) ⊆ G2 .

Note that prudent learning implies exact learning. This reduces to the condition that a learning function should only produce a hypothesis if the learning function can back up its hypotheses, i.e. if the hypothesis is confirmed by the input, the learning function is able to identify the language. Definition 3.26 (Responsive Learning) A learning function ϕ is said to be responsive on G whenever for any L ∈ L(G) and for any finite sequence s 0 , . . . , s i of elements of L ({ s 0 , . . . , s i } ⊆ L), ϕ( s 0 , . . . , s i ) is defined.

This constraint can be regarded as the complement of prudent learning: if all sentences found in the input are in a language in the class of languages learned, the learning function should always produce a hypothesis. Definition 3.27 (Consistent Learning) A learning function ϕ is said to be consistent on G whenever for any L ∈ L(G) and for any finite sequence s 0 , . . . , s i of elements of L, either ϕ( s 0 , . . . , s i ) is undefined or {s 0 , . . . , s i } ⊆ L(ϕ( s 0 , . . . , s i )).

The idea behind this constraint is that all the data given should be explained by the chosen hypothesis. It should be self-evident that this is a desirable property. Indeed, one would almost expect it to be part of the definition of learning. However, learning functions that are not consistent are not necessarily trivial. If, for example, the input is noisy, it would not be unreasonable for a learning function to ignore certain data because it considers them as unreliable. Also, it is a well known fact that children do not learn languages consistently.

Restrictive Constraints

Definition 3.28 (Set-Drivenness) A learning function ϕ which learns G is said to be set-driven whenever ϕ( s 0 , . . . , s i ) is determined by {s 0 , . . . , s i } or, more precisely, if the following holds: whenever {s 0 , . . . , s i } = {u 0 , . . . , u j }, ϕ( s 0 , . . . , s i ) is defined if and only if ϕ( u 0 , . . . , u j ) is defined, and if they are defined, they are equal.

It is easy to see that set-drivenness implies order-independence. Set-driven learning could be very loosely described as order-independent learning with the addition of ignoring "doubles" in the input. It is obvious that this is a nice property for a learning function to have: one would not expect the choice of hypothesis to be influenced by repeated presentation of the same data. The assumption here is that the order of presentation and the number of repetitions are essentially arbitrary, i.e. they carry no information that is of any use to the learning function. One can devise situations where this is not the case. Definition 3.29 (Conservative Learning) A learning function ϕ is conservative if for any finite sequence s 0 , . . . , s i of sentences and for any sentence s i+1 , whenever ϕ( s 0 , . . . , s i ) is defined and s i+1 ∈ L(ϕ( s 0 , . . . , s i )), ϕ( s 0 , . . . , s i , s i+1 ) is also defined and ϕ( s 0 , . . . , s i ) = ϕ( s 0 , . . . , s i , s i+1 ).

At first glance conservatism may seem a desirable property. Why change your hypothesis if there is no direct need for it? One could imagine cases, however, where it would not be unreasonable for a learning function to change its mind, even though the new data fits in the current hypothesis. Such a function could for example make reasonable but "wild" guesses which it could later retract. The function could "note" after a while that the inputs cover only a proper subset of its conjectured language. While such behaviour will sometimes result in temporarily overshooting, such a function could still be guaranteed to converge to the correct hypothesis in the limit.

It is a common assumption in cognitive science that human cognitive processes can be simulated by computer. This would lead one to believe that children's learning functions are computable. The corresponding strategy is the set of all partial and total recursive functions. Since this is only a subset of all possible functions, the computability strategy is a non trivial hypothesis, but not necessarily a restrictive one. The computability constraint interacts with consistency (see [START_REF] Fulk | Saving the phenomenon: Requirements that inductive machines not contradict known data[END_REF]): Proposition 3.30 There is a collection of languages that is identifiable by a computable learning function but by no consistent, computable learning function.

The computability constraint also interacts with conservative learning (see [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF]): Proposition 3.31 [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF] There is a collection of languages that is identifiable by a computable learning function but by no conservative, computable learning function.

Definition 3.32 (Monotonicity)

The learning function ϕ is monotone increasing if for all finite sequences s 0 , . . . , s n and s 0 , . . . , s n+m , whenever ϕ( s 0 , . . . , s n ) and ϕ( s 0 , . . . , s n+m ) are defined,

L(ϕ( s 0 , . . . , s n )) ⊆ L(ϕ( s 0 , . . . , s n+m )).
When a learning function that is monotone increasing changes its hypothesis, the language associated with the previous hypothesis will be (properly) included in the language associated with the new hypothesis. There seems to be little or no empirical support for such a constraint. On the contrary, it seems that hypotheses made by children decrease until they reach the correct hypothesis: in particular, all permutations of constituents are quickly met and then most of them disappear,the remaining ones being the correct hypothesis. Definition 3.33 (Incrementality, Kanazawa 1998) The learning function ϕ is incremental if there exists a computable function ψ such that ϕ( s 0 , . . . , s n+1 ) ψ(ϕ( s 0 , . . . , s n ), s n+1 ).

An incremental learning function does not need to store previous data. All it needs is current input, s n , and its previous hypothesis. A generalized form of this constraint, called memory limitation, limits access for a learning function to only n previous elements of the input sequence. This seems reasonable from an empirical point of view; it seems improbable that children (unconsciously) store all utterances they encounter.

Note that, on an infinite sequence enumerating language L in L(G), a conservative learning function ϕ learning G never outputs any grammar that generates a proper superset of L.

Let G be a class of grammars, and let ϕ be a learning function for G which is:

• conservative,

• computable,

• responsive on G,

• consistent on G,

• and learns G prudently.

Then, whenever {s 0 , . . . ,

s n } ⊆ L for some L ∈ L(G), L(ϕ( s 0 , . . . , s n )) must be a minimal element (w.
ϕ( s 0 ) ψ({s 0 }), ϕ( s 0 , . . . , s i + 1 ) ϕ( s 0 , . . . , s i ) if s i+1 ∈ L(ϕ( s 0 , . . . , s i )), ψ({s 0 , . . . , s i+1 }) otherwise.
Under certain conditions the function just defined is guaranteed to learn G, one such case is where L(G has finite elasticity. 4 Is Learning Theory Powerful Enough?

First Negative Results

One of the main and apparently discouraging consequences of the theorem 3.14 proved by Gold in the original article wherein he laid the foundations of Formal Learning Theory was that none of the four classes of Chomsky's Hierarchy is learnable under the criterion of identification in the limit. Such a first negative result has been taken for a long time as a proof that identifying languages from positive data according to his identification in the limit criterion was too hard a task. Gold himself looks quite pessimistic about the future of the theory he has just defined along its main directions: However, the results presented in the last section show that only the most trivial class of languages considered is learnable... [START_REF] Gold | Language identification in the limit[END_REF]

Angluin's Results

The first example of non-trivial class of learnable grammars was discovered by Dana Angluin (see [START_REF] Angluin | Inductive inference of formal languages from positive data[END_REF]). If Pat is defined like in example 3.4, we can prove that the class of all pattern languages has finite elasticity and, therefore, it is learnable. Furthermore, such a learnable class of grammars was also the first example of an interesting class of grammars that cross-cuts Chomsky Hierarchy, therefore showing that Chomsky's is not but one of many meaningful possible classifications for formal grammars.

Shinohara's Results

Initial pessimism about effective usefulness of Gold's notion of identification in the limit was definitely abandoned after an impressive result by Shinohara who proves (see [START_REF] Shinohara | Inductive inference from positive data is powerful[END_REF]), that k-rigid context sensitive grammars (context-sensitive grammars over a finite alphabet Σ with at most k rules), have finite elasticity for any k. Since the universal membership problem for context-sensitive grammars is decidable, that class of grammars is learnable. This is a particular case of his more general result about finite elasticity for what he calls monotonic formal system.

Kanazawa's Results

Makoto Kanazawa in [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF] makes another decisive step toward bridging the existing gap between Formal Learning Theory and computational linguistics. Indeed, he gets some important results on the learnability for some non-trivial subclasses of Classical Categorial Grammars (also known as AB Grammars). Analogously to what is done in [START_REF] Shinohara | Inductive inference from positive data is powerful[END_REF] he proves that as soon as we bound the maximum number of types a classical categorial grammar assigns to a word, we get subclasses which can be effectively learnable: in particular, he proves effective learnability for the class of k-valued Classical Categorial Grammars, both from structures and from strings.

In the first case, each string of the language the learner is presented to comes with additional information about the underlying structure induced by the grammar formalism that generates the language. The availability of such additional information for each string is somewhat in contrast with Gold's model of learning and gives rise to weaker results. On the other hand, psychological plausibility of the process is preserved by the fact that such an underlying structure can be seen as some kind of semantic information that could be available to the child learning the language from the very early stages of her cognitive development.

Our Results

The present work pushes Kanazawa's results a little further in the direction of proving the effective learnability for more and more powerful and expressive classes of formal languages. In particular, we will be able to prove learnability for the class of Rigid Lambek Grammars (see chapter 9) and to show an effective algorithm to learn them on the basis of a structured input. Much is left to be done: if Lambek grammars are well known, properties of rigid Lambek grammars are still not mastered, in particular with respect to their generative capacity. However, our results confirm once again that initial pessimism toward this paradigm of learning was largely unjustified, and that even quite a complex and linguistically motivated formalism like Lambek Grammars can be learnt according to it.

INRIA

Lambek Grammars

In 1958 Joachim Lambek proposed (see [START_REF] Lambek | The mathematics of sentence structure[END_REF]) to extend the formalism of classical categorial grammars (sometimes referred to also as BCG, or AB grammars, from the names of Ajdukiewicz and Bar-Hillel, who first introduced them) by a deductive system to derive type-change rules. A BCG grammar is basically as a finite relation between the finite set of symbols of the alphabet (usually referred to as words) and a finite set of types. Combinatory properties of each word are completely determined by the shape of its types, which can be combined according to a small set of rules, fixed once and for all BCGs. Lambek's proposal marked the irruption of logics into grammars: Lambek grammars come with a whole deductive system that allows the type of a symbol to be replaced with a weaker type.

It was first realized by van Benthem (see [vB87]) that the proofs of such type-change principles carry important information about their semantic interpretation, following the Curry-Howard isomorphism. Thus, the notion of a proof theoretical grammar was proposed that replaces formal grammars (see [START_REF] Chomsky | Three models for the description of language[END_REF]) with deductive systems and that includes a systematic semantics for natural languages based on the relationship between proof theory and type theory. Thus, rather than considering grammatical categories as unanalyzed primitives, they are taken to be formulas constructed from atoms and connectives, and rather than defining grammars with respect to rewrite rules, grammars are defined by the rules of inference governing the connectives used in the syntactic categories.

Due to the renewed interest in categorial grammars in the field of computational linguistics, Lambek (Categorial) Grammars (LCGs) are currently considered as a promising formalism. They enjoy the relative simplicity of a tightly constrained formalism as that for BCGs, together with the linguistically attractive feature of full lexicalization. Recent developments in this field led to some interesting extensions of categorial grammars, such as Steedman's Combinatory Categorial Grammars (or CCGs, close to rewrite grammars), and Multi-Modal Categorial Grammars (MMCGs, that keep the logical view and are Turing complete with decidable fragments). For an overview of current research in categorial grammars for linguistics, see [START_REF] Retoré | The logic of categorial grammar: lecture notes[END_REF].

Besides, although Pentus proved (in [START_REF] Pentus | Product-free lambek calculus and context-free grammars[END_REF]) that Lambek grammars generate exactly contextfree (string) languages, in [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] it has been shown that their strong generative capacity is greater than that of context-free grammars. These features make them an interesting subject for our inquiry about their properties with respect to Gold's Learnability Theory.

Classical Categorial Grammars

The main idea which lies behind the theory of Categorial Grammars is to conceive a grammar instead as a set of rules which generate any string of the language, as a system which assigns to each symbol of the alphabet a set of types which can be combined according to a small set of rules, fixed for the whole class of Classical Categorial Grammars.

A context-free grammar à la Chomsky is made of a set of rules that generate all the strings of a given language in a "top-down" fashion, starting from an initial symbol which identifies all the well-formed strings. On the contrary, a categorial grammar accepts a sequence of symbols of the alphabet as a well-formed string if and only if a sequence of types assigned to them reduces (in a "bottom-up" fashion) according to a fixed set of rules, to a distinguished type which designates well-formed strings. Definition 5.1 (Classical Categorial Grammar) A Classical Categorial Grammar (henceforth CCG) is a quadruple Σ, Pr, F, s , such that • Σ is a finite set (the terminal symbols or vocabulary),

• Pr is a finite set (the non-terminal symbols or atomic categories),

• F is a function from Σ to finite subsets of Tp, the set of types defined as the smallest set such that:

1. Pr ⊆ T p 2. if A, B ∈ T p, then (A/B), (A\B) ∈ T p If F(a) = {A 1 , . . . , A n } we usually write G : a → A 1 , . . . , A n .
• s ∈ Pr is the distinguished atomic category.

In a CCG, combinatory properties are uniquely determined by their structure. There are only two modes of type combination: so-called (according to the notation introduced in [START_REF] Lambek | The mathematics of sentence structure[END_REF] and almost universally adopted) Backward Application:

A, A\B ⇒ B and Forward Application: B/A, A ⇒ B.
A non-empty sequence of types A 1 , . . . , A n is said to derive a type B, that is

A 1 , . . . , A n ⇒ B,
if repeated applications of the rules of Backward and Forward application to consecutive pairs of types in the sequence A 1 , . . . , A n results in B.

In order to define the language generated by a CCG we have to establish a criterion to identify a string belonging to that language. That's what is done by the following Definition 5.2 The binary relation

⇒⊆ T p * × T p * is defined as follows. Let A, B ∈ T p, let α, β ∈ T p * , α A A\B β ⇒ α B β α B/A A β ⇒ α B β
The language generated by a CCG G is the set

{a 1 • • • a n ∈ Σ * | for 1 ≤ i ≤ n, ∃A i , G : a i → A i , and A 1 . . . A n * ⇒ s}
where * ⇒ is the reflexive, transitive closure of ⇒.

INRIA

Informally, we can say that a string of symbols belongs to the language generated by a CCG if there exists a derivation of the distinguished category s out of at least one sequence of types assigned by the grammar to the symbols of the string.

Example 5. 3 The following grammar generates the language {a n b n | n > 0}:

a : s/B, b : B, s\B
Here is a derivation for a From the proof of Gaifman's theorem, we immediately obtain the following normal form theorem: In the previous example we make use for the first time of a "natural deduction" notation for derivations, that in the present work will substitute the rather obscure notation used in example 5.3.

Extensions of Classical Categorial Grammars

As stated in the previous section, CCG formalism comes with only two reduction rules which yield smaller types out of larger ones. Montague's work on semantics (see [START_REF] Montague | The proper treatment of quantification in ordinary english[END_REF]) led to the definition of two further "type-raising" rules, by which it is possible to construct new syntactic categories out of atomic ones. We can extend the definition of CCGs as presented in the previous section by adding to the former definition two new type change rules:

αBβ ⇒ α(A/B)\Aβ αBβ ⇒ αA/(B\A)β
Other type-change rules that were proposed are the composition:

A/B B/C A/C
C\B B\A C\A and the Geach Rules:

A/B (A/C)/(B/C) B\A (C\B)\(C\A)
We can extend the formalism of CCG by adding to definition 5.2 any type change rule we need to formalize specific phenomena in natural language. Such a rule-based approach was adopted by Steedman (see [START_REF] Steedman | Categorial grammar[END_REF]) who enriches classical categorial grammar formalism with a finite number of type-changes rules. On the other hand, as it will be made clear in the following section, Lambek's approach is a deductive one: he defines a calculus in which type changes rules spring out as a consequence of the operations performed on the types.

One could ask why we should follow the deductive rather than the rule-based approach. To begin with, as proved in [START_REF] Zielonka | A simple and general method for solving the finite axiomatizability problems for Lambek's syntactic calculi[END_REF], Lambek Calculus is not finitely axiomatizable, that is to say that adding a finite number of type-change rules to the formalism of CCG one cannot derive all the type change rules provable in the Lambek Calculus. Moreover, the two approaches are very different under a theoretical viewpoint.

From a linguistic perspective, Steedman pointed out that there is no reason why we should stick to a deductive approach instead of to a rule based one: he underlines the importance of introducing ad hoc rules to formalize specific linguistic phenomena. Why should we subordinate the use of specific type change rules to their derivability in some calculus?

One of the most compelling reasons to do so is given by Moortgat (see [START_REF] Moortgat | Categorial type logics[END_REF]) who stresses the systematicity of the relation between syntax and semantics provided in a deductive framework. Also, Lambek Calculus enjoys an important property: it is sound and complete with respect to free semigroup model, i.e. an interpretation with respect to formal languages . That is to say, rules that are not deducible in Lambek Calculus are not sound, and so they can be considered as linguistically implausible.

(Associative) Lambek Calculus

Categorial grammars can be analyzed from a proof theoretical perspective by observing the close connection between the "slashes" of a categorial grammar and implication in intuitionistic logics.

INRIA

The rule that allows us to infer that if w is of type A/B and v is of type B, then wv is of type A, behaves like the modus ponens rule of inference in logic. On the basis of this similarity Lambek proposed an architecture for categorial grammars based on two levels:

• a syntactic calculus, i.e. a deductive system in which statement of the form A 1 , . . . , A n B, to be read "from the types A 1 , . . . , A n we can infer type B" can be proved;

• a categorial grammar as presented in definition 5.1, wherein the relation ⇒ is changed to allow any type change rule that could be deduced at the previous level.

In doing so, instead of adding a finite number of type change rules to our grammar, every type change rule that can be derived in the Lambek Calculus is added to the categorial grammar.

The following formalizations for Lambek Calculus are presented according, respectively, to the formalism of sequent calculus and to the formalism of natural deduction. Note that in the present work we will use the expression Lambek Calculus to refer to product-free Lambek Calculus: indeed we will never make use of the product '•' (which corresponds to the tensor of linear logic).

[ID] A A Γ, A B [/R] Γ B/A Γ A ∆, B, Π C [/L] ∆, B/A, Γ, Π C A, Γ B [\R] Γ A\B Γ A ∆, B, Π C [\L] ∆, Γ, A\B, Π C ∆ B Γ, B, Π A [Cut] Γ, ∆, Π A Note: in [/R] and [\R]
there is a side condition stipulating that Γ = / 0.

The side condition imposed for [/R] and [\R] rules formalizes the fact that in Lambek Calculus one is not allowed to cancel all the premises from the left-hand side of a derivation. Otherwise stated, in Lambek Calculus there are no deductions of the form A.

Coherently with our interpretation of Lambek Calculus as a deductive system to derive the type of a sequence of symbols of the alphabet out of the types of each symbol, such a derivation makes no sense, since it would mean assigning a type to an empty sequence of words.

Definition 5.8 The natural deduction formalization of the Lambek Calculus is defined as follows:

A [ID] • • • • A/B • • • • B [/E] A • • • • B • • • • B\A [\E] A [B] • • • • A [/I] A/B [B] • • • • A [\I] B\A
Bracketed hypotheses are "discharged" ones, like in traditional first-order logic, but with additional constraints: in [/I] and [\I] rules the cancelled assumption is always, respectively, the rightmost and the leftmost uncancelled assumption, and there must be at least another uncancelled hypothesis.

Both formalisms have advantages and disadvantages. However, due to the close connection between natural deduction proofs and λ-terms and because the tree-like structure of deductions resembles derivations trees of grammars, the natural deduction version will be the primary object of study in the present work.

For later purposes we introduce here the notion of derivation in Lambek calculus that will be useful later for the definition of the structure of a sentence in a Lambek grammar. A derivation of B from A 1 , . . . , A n is a certain kind of unary-binary branching tree that encodes a proof of A 1 , . . . , A n B. Each node of a derivation is labeled with a type, and each internal node has an additional label which, for Lambek grammars, is either /E, \E, /I, or \I and that indicates which Lambek calculus rule is used at each step of a derivation. For each occurrence of an introduction rule there must be a corresponding previously unmarked leaf type A which must be marked as [A] (that corresponds to "discharging" an assumption in natural deduction). INRIA Definition 5.9 Let A, B ∈ Tp and Γ, ∆ ∈ Tp + ,

• A (the tree consisting of a single node labeled by A) is a derivation of A from A.

• "Backslash elimination".

If A G D 1
is a derivation of A from Γ (where A is the leftmost free hypothesis) and

A\B D D 2 is a derivation of A\B from ∆, then A G D 1 A\B D D 2 B \E is a derivation of B from Γ, ∆. RR n • 5964 • "Backslash introduction". If B A, G D 1 is a derivation of B from {A, Γ}, then B [A], G D 1 \I A\B is a derivation of A\B from Γ. The leaf labeled by [A] is called a discharged leaf. INRIA • "Slash elimination". If B/A G D 1 is a derivation of B/A from Γ and A D D 2 is a derivation of A from ∆, then A D D 2 B/A G D 1 B /E
is a derivation of B from Γ, ∆.

• "Slash introduction". If B G, A D 1
is a derivation of B from {Γ, A} (where A is the rightmost free hypothesis) then

/I B/A B G, [A] D 1 is a derivation of B/A from Γ. The leaf labeled by [A] is called a discharged leaf.

Non-associative Lambek Calculus

Lambek Calculus, as defined in the previous section, is implicitly associative. In order to use Lambek calculus to describe some linguistic phenomena we have to forbid associativity and so the hierarchical embedding of hypotheses is respected. Another linguistically attractive feature of non-associative INRIA Lambek calculus is that it provides useful logical to support semantics, but at the same time it prohibits transitivity, that sometimes leads to overgeneration. Definition 5.11 The natural deduction formalization of the non-associative Lambek Calculus (SND) has the following axioms and rules of inference, presented in the sequent format:

[ID] A A Γ A/B ∆ B [/E] (Γ, ∆) A Γ B ∆ B\A [\E] (Γ, ∆) A (Γ, B) A [/I] Γ A/B (B, Γ) A
[\I] Γ B\A Note: in [/I] and [\I] there is a side condition stipulating that Γ = / 0.

Normalization and Normal Forms

As one can easily see, in Lambek Calculus there are infinitely many proofs for any deduction A 1 , . . . , A n B. Since, as it will be extensively explained in section 6, proofs in Lambek Calculus play a decisive role in defining the notion of structure for a sentence generated by a Lambek grammar, such an arbitrary proliferation of proofs for deductions is quite undesirable.

The following definition introduces a useful relation between proofs in Lambek Calculus that formalizes our idea of a "minimal" proof for any deduction. It provides two normalization schemes that can be applied to a derivation to produce a "simpler" derivation of the same result. Definition 5.12 The relation > 1 between proofs in the natural deduction formalization of Lambek Calculus is defined in the following way:

• • • • A [A] • • • • B [\I] A\B [\E] B > 1 • • • • A • • • • B [A] • • • • B [/I] B/A • • • • A [/E] B > 1 • • • • A • • • • B [B] • • • • B\A [\E] A [\I] B\A > 1 • • • • B\A • • • • A/B [B] [/E] A [/I] A/B > 1 • • • • A/B
The symbol ≥ stands for reflexive and transitive closure of > 1 . Relation > 1 is usually defined as β-η-conversion, while ≥ as β-η-reduction.

The relation ≥ satisfies the following properties (see [START_REF] Wansing | The Logic of Information Structures[END_REF], [START_REF] Roorda | Resource Logics: Proof-Theoretical Investigations[END_REF]): Theorem 5.13 [START_REF] Wansing | The Logic of Information Structures[END_REF] The relation ≥ is confluent (in the Church-Rosser meaning), i.e. if δ 1 ≥ δ 2 and δ 1 ≥ δ 3 , then there exists a δ 4 such that δ 2 ≥ δ 4 and δ 3 ≥ δ 4 .

Theorem 5.14 [START_REF] Roorda | Resource Logics: Proof-Theoretical Investigations[END_REF] The relation ≥ is both weakly and strongly normalizing, that is, every proof can be reduced in normal form and every reduction terminates after at most a finite number of steps.

Theorem 5.15 (Church-Rosser, 1937) The relation ≥ is such that if there are two distinct reductions starting from the same term, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts. Definition 5.16 (β-η-normal form) A proof tree for the Lambek Calculus is said to be in β-ηnormal form is none of its subtrees is of the form

[B] • • • • A [/I] A/B B [/E] A B [B] • • • • A [\I] B\A [\E] A A/B [B] [/E] A [/I] A/B [B] B\A [\E] A [\I] B\A

Basic Facts about Lambek Calculus

Let's summarize here some meaningful properties for Lambek calculus, which is:

• intuitionistic: only one formula is allowed on the right-hand side of a deduction. This means there is no involutive negation;

• linear: so-called structural rules of logics are not allowed: two equal hypotheses can't be considered as only one, and on the other hand we are not allowed to "duplicate" hypotheses at will. Lambek calculus is what we call a resource-aware logics, wherein hypotheses must be considered as consumable resources;

• non-commutative: hypotheses don't commute among them, that is, the implicit operator "•" in this calculus is not commutative. This is what makes possible the existence of the two "implications" (/ and \), the first one consuming its right argument, the second one its left argument.

INRIA

Since Lambek proved a cut-elimination theorem for his calculus (see [START_REF] Lambek | The mathematics of sentence structure[END_REF]), among the many consequences of the normalization theorems there are the subformula property, that is: Proposition 5.17 Every formula that occurs in a normal form natural deduction proof of cut-free sequent calculus proof is either a subformula of the (uncancelled) assumptions or of the conclusion; and decidability for Lambek calculus: Proposition 5.18 Derivability in the Lambek Calculus is decidable.

In fact, given a sequent to prove in Lambek calculus, cut-elimination property authorizes us to look for a cut-free proof. But if the sequent comes from the application of a rule other that cut, this can't but be made in a finite number of different ways, and in any case we have to prove one or two smaller (i.e. with less symbols) sequents. This is enough to prove decidability for Lambek calculus. Theorem 5.14 states that any proof has a normal form and theorem 5.13 that this normal form is unique. This doesn't mean that there is a unique normal form proof for any deduction. The following theorem by van Benthem sheds light on this point:

Lambek Grammars

A Lambek grammar modifies the traditional notion of categorial grammars as presented in section 5.1, by extending the derivation mechanism into by a whole deductive system in the following way:

• a lexicon assigns to each word w i a finite set of types

F(w i ) = {t 1 i , . . . ,t k i i } ⊂ ℘(T p);
• the language generated by this fully lexicalized grammar is the set of all the sequences w 1 • • • w n of words of the lexicon such that for each w i there exists a type t i ∈ F(w i ) such that t 1 , . . . ,t n s is provable in Lambek calculus.

Formally:

Definition 5.20 (Lambek grammar) A Lambek grammar is a triple G = Σ, s, F , such that

• Σ is a finite set (the vocabulary),

• s is the distinguished category (a propositional variable),

• F : Σ → ℘(T p) is a function which maps each symbol of the alphabet into the set if its types.

If F(a) = {A 1 , . . . , A n } we write G : a → A 1 , . . . , A n .

For w ∈ Σ * , w = a 1 • • • a n , we say that G accepts w if there is a proof in Lambek calculus of

A 1 , . . . , A n s
with G : a i → A i for each i.

The language generated by a Lambek grammar G is Weak generative capacity for associative Lambek grammars was characterized (see [START_REF] Pentus | Product-free lambek calculus and context-free grammars[END_REF]) by the following celebrated theorem (which proves a 1963 conjecture of Chomsky), one of the finest and most recent achievements in this field:

L(G) = {a 1 • • • a n ∈ Σ * | for 1 ≤ i ≤ n, ∃A i , G : a i → A i and
Theorem 5.22 [START_REF] Pentus | Product-free lambek calculus and context-free grammars[END_REF] The languages generated by associative Lambek grammars are exactly the context-free languages.

Later, for non-associative Lambek grammars Buszkowski proved (see [START_REF] Buszkowski | Generative capacity of non-associative lambek calculus[END_REF]):

Theorem 5.23 [START_REF] Buszkowski | Generative capacity of non-associative lambek calculus[END_REF] The languages generated by non-associative Lambek grammars are exactly the context-free languages.

Proofs as Grammatical Structures

In this section we will introduce the notion of structure for a sentence generated by a Lambek grammar. On the basis of a recent work by Hans-Joerg Tiede (see [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF]) who proved some important theorems about the tree language of proof trees in Lambek calculus, we will adopt as the underlying structure of a sentence in a Lambek grammar a (normal) proof of its well-formedness in Lambek calculus. We will see in section 9 how this choice affects the process of learning a rigid Lambek grammar on the basis of structured positive data. Just as a derivation encodes a proof of A 1 , . . . , A n B, the notion of parse tree introduced by the following definition encodes a proof of

a 1 • • • a n ∈ L(G)
where G is a Lambek grammar and a 1 , . . . , a n are symbols of its alphabet. Definition 6.1 Let G = Σ, s, F be a Lambek grammar, then

• if D is a derivation of B from A 1 , . . . , A n ,

Tree Languages and Automata

In order to fully appreciate the peculiarity of Lambek grammars with respect to their strong generative capacity, we recall here some basic definitions about the notion of tree language as presented in [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF].

Definition 6.3 (Trees and tree languages)

A tree is a term over a finite signature Σ containing function and constant symbols. The set of n-ary function symbols in Σ will be denoted by Σ n . The set of all terms over Σ will be denoted by T Σ ; a subset of T Σ is called a tree language or a forest. Definition 6.4 (Yield of a tree) The yield of a tree t is defined by yield(c) = c, for c ∈ Σ 0 yield( f (t 1 , . . . ,t n )) = yield(t 1 ), . . . , yield(t n ), for f ∈ Σ n , n > 0 Thus, the yield of a tree is the string of symbols occurring as its leaves. Definition 6.5 (Root of a tree) The root of a tree t is defined by

root(c) = c, for c ∈ Σ 0 root( f (t 1 , . . . ,t n )) = f , for f ∈ Σ n , n > 0.
In the following subsections three increasingly more powerful classes of tree languages are presented: local, regular and context-free tree languages. Note that even if the names for these classes of tree languages are the same as those for classes of string languages, their meaning is very different. INRIA

Local Tree Languages

We can think of a local tree language as a tree language whose membership problem can be decided by just looking at some very simple (local) properties of trees. A formalization of such an intuitive notion is given by the following definitions: Definition 6.6 (Fork of a tree) The fork of a tree t is defined by

f ork(c) = / 0, for c ∈ Σ 0 f ork( f (t 1 , . . . ,t n )) = { f , root(t 1 ), . . . , root(t n ) } ∪ n i=1
f ork(t i ) Definition 6.7 (Fork of a tree language) For a tree language L, we define

f ork(L) = t∈L f ork(t)
Note that, since Σ is finite, f ork(T Σ ) is always finite. Definition 6.8 (Local tree language) A tree language L ⊆ T Σ is local if there are sets R ⊆ Σ and E ⊆ f ork(T Σ ), such that, for all t ∈ T Σ , t ∈ L iff root(t) ∈ R and f ork(t) ⊆ E.

Thatcher (see [START_REF] Thatcher | Characterizing derivation trees of context-free grammars through a generalization of finite automata theory[END_REF]) characterized the relation between local tree languages and the derivation trees of context-free string grammars by the following Theorem 6.9 [START_REF] Thatcher | Characterizing derivation trees of context-free grammars through a generalization of finite automata theory[END_REF]) S is the set of derivation trees of some context-free string grammar iff S is local.

Regular Tree Languages

Among many different equivalent definitions for regular tree languages, we follow Tiede's approach in choosing the following one, based on finite tree automata. Definition 6.10 (Finite tree automaton) A finite tree automaton is a quadruple Σ, Q, q 0 , ∆ , such that

• Σ is a finite signature,
• Q is a finite set of unary states,

• q 0 ∈ Q is the start state,
• ∆ is a finite set of transition rules of the following type:

q(c) → c for c ∈ Σ 0 q( f (v 1 , . . . , v n )) → f (q 1 (v 1 ), . . . , q n (v n )) for f ∈ Σ n , q, q 1 , . . . , q n ∈ Q
We can think of a finite tree automaton as a device which scans non-deterministically a tree from root to frontier. It accepts a tree if it succeeds in reading the whole tree, it rejects it otherwise.

In order to define the notion of tree language accepted by a regular tree automaton we need to define the transition relation for finite tree automata. Definition 6.11 A context is a term over Σ ∪ {x} containing the zero-ary term x exactly once. Definition 6.12 Let M = Σ, Q, q 0 , ∆ be a finite tree automaton, the derivation relation

⇒ M ⊆ T Q∪Σ × T Q∪Σ
is defined by t ⇒ M t if for some context s and some t 1 , . . . ,t n ∈ T Σ , there is a rule in ∆

q( f (v 1 , . . . , v n )) → f (q 1 (v 1 ), . . . , q n (v n )) and t = s[x → q( f (t 1 , . . . ,t n ))] t = s[x → f (q 1 (t 1 ), . . . , q n (t n ))].

If we use ⇒ *

M to denote the reflexive, transitive closure of ⇒ M , we say that a finite automaton M accepts a term t ∈ T Σ if q 0 (t) ⇒ * M t. The tree language accepted by a finite tree automaton M is {t ∈ T Σ | q 0 (t) ⇒ * M t}. Definition 6.13 (Regular tree language) A tree language is regular if it is accepted by a finite tree automaton.

The following theorem (see [START_REF] Kozen | Automata and Computability[END_REF]) defines the relation between local and regular tree languages: Theorem 6.14 Every local tree language is regular.

while the following (see [START_REF] Gécseg | Tree Automata[END_REF]) establishes a relation between regular tree languages and contextfree string languages: Theorem 6.15 The yield of any regular tree language is a context-free string language.

Context-free Tree Languages

The final step in the definition of more and more powerful tree language classes is made possible by introducing the notion of pushdown tree automaton. Again, we stick to Tiede's approach in choosing Guesserian's useful definition (see [START_REF] Guesserian | Pushdown tree automata[END_REF]): Definition 6.16 (Pushdown tree automaton) A pushdown tree automaton is a system Σ, Γ, Q, q 0 , Z 0 , ∆ , such that

• Σ is a finite signature (the input signature),

INRIA

• Γ is a finite signature (the pushdown signature; we assume Σ ∩ Γ = / 0),

• Q is a finite set of binary states,

• q 0 ∈ Q is the start state,

• Z 0 ∈ Γ is the initial stack symbol,

• ∆ is a finite set of rules of the form

q( f (v 1 , . . . , v n ), E(x 1 , . . . , x m )) → f (q 1 (v 1 , γ 1 ), . . . , q n (v n , γ n )), q(v, E(x 1 , . . . , x m )) → q (v, γ ), q(c) → c with -q, q , q 1 , . . . , q n ∈ Q, -c ∈ Σ 0 , -f ∈ Σ n , n > 0, -E ∈ Γ m , -γ , γ 1 , . . . , γ n ∈ T Γ∪{x 1 ,...,x m } .
The transition relation for pushdown tree automata ⇒ can be defined straightforwardly as a generalization of definition 6.12. A term t is accepted by a pushdown automaton if q 0 (t, Z 0 ) ⇒ * t, where ⇒ * is the reflexive, transitive closure of ⇒. Definition 6.17 (Context-free tree language) The language accepted by a pushdown tree automaton is called a context-free tree language.

The relationship between regular and context-free tree languages is exemplified by the following proposition:

Proposition 6.18 The intersection of a regular and a context-free tree language is context-free.

We know that the yield of a regular tree language is a context-free string language: there is a similar connection between the class of context-free tree languages and the class of indexed languages, as stated by the following Proposition 6.19 The yield of any context-free tree language is an indexed string language.

Linear indexed languages have been proposed as an upper bound of the complexity of natural languages, after it was shown that certain phenomena in natural languages cannot be described with context-free grammars (see [START_REF] Gazdar | Applicability of indexed grammars to natural languages[END_REF]).

Proof Trees as Structures for Lambek Grammars

In [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] Hans-Joerg Tiede proposes, in contrast with a previous approach by Buszkowski, to take as the structure underlying a sentence generated by a Lambek grammar, one of the infinite proof trees of the deduction A 1 , . . . , A n s, where A 1 , . . . , A n is a sequence of types assigned by the grammar to each symbol, and s is the distinguished atomic category. Following Tiede's approach, we give the following The terms over this signature represent proof trees that neither have information about the formulas for which they are a proof, nor about the strings that are generated by a grammar using this proof. These terms represent proofs unambiguously, since the assumption discharged by an introduction rule is univocally determined by the position of the corresponding [/I] or [\I] function symbol in the proof tree.

Example 6.21 The term t = [\I]([/E]([ID], [ID])

) is an example of well-formed term over this signature. There's no need for additional information about the discharged assumption since, as we can see from the tree-like representation of the term, the discharged assumption is unambiguously identified.

[ID] ID /E

\I

The following terms are examples of not well-formed proof trees for the tree language generated by any Lambek grammar:

• [\E](x, [/I](y)).
Since the major premise of the \E function symbol is something with a (. . .)\(. . .) shape, there's no way to reduct that term by a \E rule;

INRIA • [/E[([\I](x), y).
Analogous to the previous situation;

• [\I]([\E](x, [ID]
)) if the term x does not contain at least two uncancelled assumptions;

• [/I]([/E]([ID],
x)), if the term x does not contain at least two uncancelled assumptions.

By taking a proof tree as the structure of a sentences generated by Lambek grammars, Tiede proved some important results about their strong generative capacity, that is, the set of the structures assigned by a grammar to the sentences it generates. Since strong generative capacity can provide a formal notion of the linguistic concept of structure of a sentence, this result justifies the current interest toward Lambek Grammars as a promising mathematical tool for linguistic purposes. Theorem 6.22 [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] The set of well-formed proof trees of the Lambek Calculus is not regular.

This amounts to stating that there exist Lambek grammars whose trees do not form a regular tree language. Theorem 6.23 [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] The set of proof trees of the Lambek Calculus is a context-free tree language.

These two theorems show that the language of proof trees is properly a context-free tree language.

In particular, these theorems show that Lambek grammars are more powerful, with respect to strong generative capacity, than context-free grammars, whose structure language is a local tree language as shown in theorem 6.9.

We can easily introduce the notion of normal form proof tree by simply extending the notion of normal form proof as presented in definition 5.16. We can say that for normal form trees, in addition to the rules that prohibit terms of the form

[\E](x, [/I](y)), [/E]([\I](x), y),

we have rules that prohibit terms of the form

[\E](x, [\I](y)) [/E]([/I](x), y)
and terms of the form

[/I]([/E](x, [ID])) [\I]([\E]([ID], y))
which correspond to β-redexes and η-redexes, respectively, as one can easily see from definition 5.16.

We can easily extend to the formalism of proof trees the "reduction rules" we've seen in section 5.5 to get a normal form proof tree out of a non-normal one.

t 1 t 1 t 2 t 2 \E ® \I [ ] [ ] t 2 t 2 t 1 t 1 /E /I ® [ ] [ ] , t t /E /I ® [ ] t t \E \I ® [ ] ,
As a corollary of theorem 6.22, Tiede proves that Theorem 6.24 [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF] The set of normal form proof trees of a Lambek grammar is not regular, which, together with Theorem 6.25 The set of normal form proofs of a Lambek grammar is a context-free tree language

shows that the tree language of normal form proof trees of Lambek Calculus is properly a contextfree tree language.

Proof-tree Structures

Given a Lambek grammar G, a proof-tree structure over its alphabet Σ is a unary-binary branching tree whose leaf nodes are labeled by either [ID] (these are called "discharged leaf nodes") or symbols of Σ and whose internal nodes are labeled by either \E, /E, \I, or /I. The set of proof-tree structures over Σ is denoted Σ P . Often we will simply say 'structure' to mean proof-tree structure. A set of proof-tree structures over Σ is called a structure language over Σ.

Example 6.26 The following is an example of a proof-tree structure for the sentence he likes him seen in example 6.2:

INRIA /E /E [ID] likes /E he /I him
Let G be a Lambek grammar, and let P be a partial parse tree of G. The result of stripping P of its type labels is a proof-tree structure, that is called the proof-tree structure of P . If T is the structure of a parse tree P , we say that P is a parse of T .

We say that a Lambek grammar G generates a structure T if and only if for some parse tree P of G, T is the structure of P . The set of structures generated by G is called the (proof-tree) structure language of G and is denoted PL(G). In order to distinguish L(G), the language of G, from PL(G), its structure language, we often call the former the string language of G.

The yield of a proof-tree structure T is the string of symbols a 1 , . . . , a n labeling the undischarged leaf nodes of T , from left to right in this order. The yield of T is denoted yield(T ). Note that L(G) = {yield(T ) | T ∈ PL(G)}.

Decidable and Undecidable Problems about Lambek Grammars

Since, as stated in by theorem 5.18, Lambek calculus is decidable, the universal membership problem "s ∈ L(G)" is decidable for any sentence s and any Lambek grammar G.

On the other hand, the questions "L(G 1 ) = L(G 2 )" and "L(G 1 ) ⊆ L(G 2 )" for arbitrary Lambek grammars G 1 and G 2 are undecidable, because the same questions are undecidable for context-free grammars and there exists an effective procedure for converting a context-free grammar G to a Lambek grammar G such that L(G ) = L(G).

Given a proof-tree structure t the question "t ∈ PL(G)" is decidable. In fact, as shown by Tiede in 6.23, every proof tree language of a Lambek Grammar is a context-free tree language; and that problem is decidable for context-free tree languages (you just have to run the pushdown tree automata on t).

Unfortunately, the question "PL(G 1 ) ⊆ PL(G 2 )" has been proved decidable only for G 1 , G 2 nonassociative Lambek grammars. Whether it is decidable or not for (associative) Lambek grammars is still an open question and the subject of active research in this field.

Substitutions

In this section we introduce the notion of a Lambek grammar being a substitution instance of another. Besides, we define a notion of size of a Lambek grammar that will be decisive in our proof of learnability for Rigid Lambek Grammars presented in section 9. 4

σ(t) = t σ(A/B) = σ(A)/σ(B) σ(A\B) = σ(A)\σ(B)
for all A, B ∈ T p.

We use the notation {x

1 → A 1 , . . . , x n → A n } to denote the substitution σ such that σ(x 1 ) = A 1 , . . . , σ(x n ) = A n

INRIA

The following definition introduce the notion of a Lambek grammar being a substitution instance of another: Definition 6.31 Let G = Σ, s, F be a Lambek grammar, and σ a substitution. Then σ[G] denotes the grammar obtained by applying σ in the type assignment of G, that is:

σ[G] = Σ, s, σ • F σ[G] is called a substitution instance of G.
It easy to prove also for Lambek grammars this straightforward but important fact that was first proved for CCGs in [START_REF] Buszkowski | Categorial grammars determined from linguistic data by unification[END_REF] Proposition 6.32 If σ[G 1 ] ⊆ G 2 , then the set of proof-tree structures generated by G 1 is a subset of the set of proof-tree structures generated by G 2 , that is PL(G 1 ) ⊆ PL(G 2 ).

Proof. Suppose σ[G 1 ] ⊆ G 2 . Let T ∈ PL(G 1
) and let P be a parse of T in G 1 . Let σ[P ] the result of replacing each type label A of P by σ(A). Then it is easy to see that σ

[P ] is a parse of T in G 2 . Therefore, T ∈ PL(G 2 ). Corollary 6.33 If σ[G 1 ] ⊆ G 2 , then L(G 1 ) ⊆ L(G 2 ).
Proof. Immediate from the previous proposition and the remark at the end of section 6.4.

A substitution that is a one-to-one function from Var to Var is called a variable renaming. If σ is a variable renaming, then G and σ[G] are called alphabetic variants. Obviously grammars that are alphabetic variants have exactly the same shape and are identical for all purposes. Therefore, grammars that are alphabetic variants are treated as identical.

Proposition 6.34 Suppose σ 1 [G 1 ] = G 2 and σ 2 [G 2 ] = G 1 .
Then G 1 and G 2 are alphabetic variants and thus are equal.

Proof. For each symbol c ∈ Σ, σ 1 and σ 2 provide a one-to-one correspondence between {A | G 1 : c → A} and {A | G 2 : c → A}. Indeed, if it didn't and, say,

{σ 1 (A) | G 1 : c → A} ⊂ {A | G 2 : c → A}, then σ 2 [G 2 ] = σ 2 [σ 1 [G 1 ]
] couldn't be equal to G 1 , and likewise for σ 2 . Then, it is easy to see that σ 1 ↑ Var(G 1 ) is a one-to-one function from Var(G 1 ) onto Var(G 2 ), and Let

σ 2 ↑ Var(G 2 ) = (σ 1 ↑ Var(G 1 )) -1 . One can extend σ 1 ↑ Var(G 1 ) to a variable renaming σ. Then σ[G 1 ] = σ 1 [G 1 ] = G 2 .

Grammars in Reduced Form

σ 1 = {y → x}, σ 2 = {y → x\s}.
Then σ 1 is faithful to G, while σ 2 is not. Definition 6.37 Let be a binary relation on grammars such that G 1 G 2 if and only if there exists a substitution σ with the following properties:

• σ is faithful to G 1 ; • σ[G 1 ] ⊆ G 2 .
From the definition above and proposition 6.34 it's immediate to prove the following: Proposition 6.38 is reflexive, transitive and antisymmetric. As explicitly stated in the original paper wherein Lambek laid the foundations of the Lambek Calculus, his aim was [...] to obtain an effective rule (or algorithm) for distinguishing sentences from nonsentences, which works not only for the formal languages of interest to the mathematical logician, but also for natural languages such as English, or at least for fragments of such languages. ([Lam58]) That's why, even if Lambek grammars can be simply considered as interesting mathematical objects, it will be useful to underline here some properties that make them also an interesting tool to formalize some phenomena in natural languages.

The importance of Lambek's approach to grammatical reasoning lies in the development of a uniform deductive account of the composition of form and meaning in natural language: formal grammar is presented as a logic, that is a system to reason about structured linguistic structures.

The basic idea underlying the notion of Categorial Grammar on which Lambek based his approach is that a grammar is a formal device to assign to each word (a symbol of the alphabet of the grammar) or expression (an ordered sequence of words) one or more syntactic types that describe their function. Types can be considered as a formalization of the linguistic notion of parts of speech.

CCGs assign to each symbol a fixed set of types, and provide two composition rules to derive the type of a sequence of words out of the types of its components. Such a "fixed types" approach leads to some difficulties: to formalize some linguistic phenomena we should add further rules to the two elimination rules defined for CCGs as described in section 5.2. In the following subsections we present some examples where the deductive approach of Lambek grammars leads to more an elegant and consistent formalization of such linguistic phenomena.

In the following subsections we take s as the primitive type of well-formed sentences in our language and np as the primitive type for noun phrases (such as John, Mary, he).

Transitive verbs

Transitive verbs require a name both on their left and right hand sides, as it is apparent from the well-formedness of the following sentences.

Mary

Both parenthesizations lead to a derivation of s as type of the whole expression. This would mean that in an CCG we should assign to any transitive verb at least two distinct types: (np\s)/np and np\(s/np). On the contrary, in a Lambek grammar, since we can prove both (np\s)/np np\(s/np) and np\(s/np) (np\s)/np we can simply assign to a transitive verb the type np\s/np without any further parenthesizations.

Pronouns

If we try to assign a proper type to the personal pronoun he we notice that its type is such that the following sentences are well-formed:

Jane

We have two choices: either we give he the same type as a name (that is, np) or we give it the type s/(np\s). In the first case there is a problem: expressions like Jane likes he are considered as well-formed sentences. So, we assign to he the type s/(np\s).

Analogously, since the personal pronoun him makes the following sentences well-formed: for him, we assign to him the type (s/np)\s (and not type np, since expressions like him likes John would be well-formed). Since a pronoun is, according to its own definition, something that "stands for a noun", we wish that in our grammar each occurrence of a pronoun could be replaced by a name (while the converse is not always true): but this means that any name (say, John, of type np) should also be assigned the type of he and him, that is, respectively, type s/(np\s) and type (s/np)\s. In other words, we need something that accounts for a type-raising. But since in Lambek Calculus we can prove np s/(np\s) np (s/np)\s for any np and s, a Lambek grammar provides a very natural formalization of the relationship between names and pronouns: while a name can always be substituted to a pronoun in a sentence (and the type-raising derivation guarantees that a name can always "behave like" a pronoun if we need it to), the converse is not true (the converse of the type-raising proof doesn't hold in Lambek Calculus). The proof of the first deduction is reported in example 5.10 as a derivation in a Lambek grammar.

Adverbs

If we look for the proper type for adverbs like here we can consider the well-formed sentence John works here. We can choose between two possible parenthesizations here, that is: The first one suggests for here the type s\s, while the second one the type (np\s)\(np\s). The good news is that, while in a CCG we should assign each adverb at least two different types, in a Lambek grammar we can prove that s\s (np\s)\(np\s) that is to say, in Lambek grammars any adverbial expression of type s\s has also type (np\s)\(np\s). More generally, we can show that in Lambek Calculus x\y (z\x)\(y\x) x/y (x/z)/(y/z).

Hypothetical reasoning

In the following example, sentences s, noun phrases np, common nouns n, and propositions phrases pp are taken to be "complete expressions", whereas the verb dances, the determiner the and the preposition with are categorized as incomplete with respect to these complete phrases. Since the relative pronoun whom (of type (n\n)/(s/np)) wants to enter into composition on its right with the relative clause body, we'd like to assign type s/np to the latter. In order to show that Francesca dances with is indeed of type s/np, we make a hypothetical assumption and suppose to have a "ghost word" of type np on its right. It's easy to derive the category s for the sentence Francesca dances with np. By withdrawing the hypothetical np assumption, we conclude that Francesca dances with has type s/np.

We can say that the cancelled hypothesis is the analogous of a "trace" à la Chomsky moving whom before Francesca.

Transitivity

In the framework of CCGs a difficulty arises when we try to show the well-formedness of s/(np\s) he np\s/np likes (s/np)\s him so some authors proposed to introduce two new rules, which are often referred to as 'transitivity rules':

(x/y)(y/z) → x/z, (x\y)(y\z) → x\z
It's easy to show that such rules are derivable in Lambek Calculus, as we can easily see from the following proof tree:

/E y/z [z] y x/y /E x I/
x/z

Lambek Grammars and Montague Semantics

From a linguistic point of view, one of the main reasons of interest in Lambek grammars lies in the natural interface that proof-tree structures provide for Montague-like semantics. Just like Curry-Howard isomorphism shows that simply typed λ-terms can be seen as proofs in intuitionistic logics, and vice-versa, syntactical analysis of a sentence in a Lambek grammar is a proof in Lambek calculus, which is naturally embedded into intuitionistic logics. Indeed, if we read B/A and A\B like the intuitionistic implication A → B, every rule in Lambek calculus is a rule of intuitionistic logics.

In order to fully appreciate this relation between syntax and semantics which is particularly strong for Lambek grammars, we define a morphism between syntactic types and semantic types: the latter are formulas of a minimal logics (where the only allowed connector is →, that is, intuitionistic implication) built on the two types e (entity) and t (truth values).

(Syntactic type)* = Semantic type s * = t (a sentence is a proposition) sn * = e (a nominal sintagma denotes an entity) n * = e → t (a noun is a subset of entities)

(A\B) * = (B/A) * = A * → B * extends ( ) * to every type.
The lexicon associates also to every word w a λ-term τ k for every syntactic type t k ∈ L(w), such that the type of τ k is precisely t * k , the semantic type corresponding to that syntactic type. We introduce some constants for representing logical operations of quantification, conjunction etc:

INRIA Constant Type ∃ (e → t) → t ∀ (e → t) → t ∧ t → (t → t) ∨ t → (t → t) ⊃ t → (t → t)
Let the following be given:

• a syntactical analysis of w 1 . . . w n in Lambek calculus, that is to say, a derivation D of t 1 , . . . ,t n s and

• the semantics for every word w 1 , . . . , w n , that is to say, λ-terms τ i : t * i , then we get the semantics of the sentence by simply applying the following algorithm:

• Substitute in D every syntactic type with its corresponding semantic image; since intuitionistic logics is an extension of Lambek calculus, we get a derivation D * into intuitionistic logic of t * 1 , . . . ,t * n t = s * ;

• this derivation in intuitionistic logic due to Curry-Howard isomorphism can be seen as a simply typed λ-term D * λ , containing a free variable x i of type t * i for every word w i ;

• in D * λ replace each variable x i with λ-term τ i , equally typed with t * i ;

• reduce the λ-term resulting at the end of the previous step, and we get the semantic representation of the analyzed sentence.

Let's consider the following example (taken from [START_REF] Retoré | Proof-nets for the lambek calculus -an overview[END_REF]): First of all, we'll prove that Some sentences talk about themselves is a well formed-sentence, that is, it belongs to the language generated by the lexicon at issue. This means building a natural deduction of:

word
(s/(sn\s))/n, n, sn\(s/sn), ((sn\s)/sn)\(sn\s) s.

If we indicate with S, N, T, M the left-hand side of syntactic types we get S (s/(sn\s))/n N n [/E] S, N s/(sn\s) T (sn\s)/sn M ((sn\s)/sn)\(sn\s)

[\E] T, M sn\s

[\E] S, N, T, M s By applying the isomorphism between syntactic and semantic types, we get the following intuitionistic proof, where S * , N * , T * , M * are the abbreviations for semantic types associated to S, N, T, M:

S * (e → t) → (e → t) → t N * e → t [→ E] S * , N * (e → t) → t T * e → e → t M * (e → e → t) → e → t [→ E] T * , M * e → t [→ E] S * , N * , T * , M * t
The λ-term coding this proof is simply ((sn)(tm)) of type t, where s, n,t, m are variables of types respectively S * , N * , T * , M * .

By replacing these variables with λ-terms of the same types associated by the lexicon to the words, we get the following λ-term of type t: If we recall that the x in this last term is of type e, the latter reduced term represents the following formula in predicate calculus:

∃x : e(sentence (x) ∧ talk about(x, x)) which is the semantic representation of the previously analyzed sentence.

INRIA 8 Rigid Lambek Grammars

In the present section we introduce the notion of rigid Lambek grammar (often referred to as RLG), whose learnability properties will be the subject of our inquiry in section 9. Basic notions and results presented here are almost trivial extensions of what has already been done for rigid CCGs (see [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]), since a specific a specific theory for rigid Lambek grammars is still missing.

Rigid and k-Valued Lambek Grammars

A rigid Lambek grammar is a triple G = Σ, s, F , where Σ and s are defined like in definition 5.20, while F : Σ T p is a partial function that assigns to each symbol of the alphabet at most one type. We can easily generalize the notion of rigid Lambek grammar to the notion of k-valued Lambek grammar by a function F that assigns to each symbol of the alphabet at most k types. Formally,

F : Σ k i=1 T p k .
Let an alphabet Σ be given. We call G rigid the class of rigid Lambek grammars over Σ, and G k-valued the class of k-valued Lambek grammars over Σ.

Let's define two classes of proof-tree structures:

P L rigid = {PL(G) | G ∈ G rigid }, P L k-valued = {PL(G) | G ∈ G k-valued }.
Members of P L rigid are called rigid (proof-tree) structure languages, and members of P L k-valued are called k-valued (proof-tree) structure languages.

Let's define two classes of strings: Then G 2 is a rigid grammar, while G 1 is not. G 1 is a 2-valued grammar. The following propositions are almost trivial extensions to rigid Lambek grammars of analogous results proved by Kanazawa for CCGs in [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]. However, they deserve some attention since they can provide a first superficial insight about properties of RLGs.

L rigid = {L(G) | G ∈ G rigid }, L k-valued = {L(G) | G ∈ G k-valued }.
First of all we prove a hierarchy theorem about strong generative capacity of k-valued Lambek grammars.

i times

Then for each k ≥ 1, {T 1 , . . . , T k } ∈ P L k+1-valued -P L k-valued .

Thus, for each k ∈ N, P L k-valued ⊂ P L k+1-valued .

Proof. (See [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]) Let G k be the following k+1-valued grammar: 3. T is the following proof-tree structure:

G k : a → x, s/x, (
T 1

\I

Then any partial parse tree of G whose structure is T has the form where P 1 is a partial parse

B [A], G P 1 \I A\B
tree of G whose structure is T 1 . By induction hypothesis, P 1 is unique. This means the the type label A\B is uniquely determined, so P is also unique. Note that last corollary doesn't state that if G is rigid, then each string s ∈ L(G) has a unique parse: in general for each sentence there are infinitely many proof trees, as extensively shown in section 6. Lemma 8.7 Let G be a rigid Lambek grammar. Then for each incomplete proof-tree T, there is at most one incomplete parse tree P of G such that T is the structure of P . Proof. See [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF] which trivially extends to Lambek grammars.

Most General Unifiers and Operator

Unification plays a crucial role in automated theorem proving in classical first-order logic and its extensions (see, for example, [START_REF] Fitting | First-Order Logic and Automatic Theorem Proving[END_REF] for an exposition of its use in first-order logic). Since types are just a special kind of terms, the notion of unification applies straightforwardly to types.

INRIA 9 Learning Rigid Lambek Grammars from Structures

In the present chapter we will explore a model of learning for Rigid Lambek Grammars based on positive structured data. In addition to the standard model where sentences are presented to the learner as flat sequences of words, in this somewhat enriched model, strings come with additional information about their "deep structure". Following the approach sketched in section 6, largely indebted with Tiede's study on proof trees in Lambek calculus as grammatical structures for Lambek grammars (see [START_REF] Tiede | Deductive Systems and Grammars: Proofs as Grammatical Structures[END_REF]), in our model each sentence comes to the learner with a structure in the form of a proof tree structure as extensively described in section 6.

Formally, given a finite alphabet Σ, we will present a learning algorithm for the grammar system G rigid , Σ P , PL : that is to say, samples to which the learner is exposed to are proof-tree structures over the alphabet Σ, and guesses are made about the set of rigid Lambek grammars that can generate such a set of structures. We follow the advice of Kanazawa (see [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]) who underlines how such an approach, which turns out to be quite logically independent from an approach based on flat strings of words, seems to make the task of learning easier but doesn't trivialize it. If, on one hand, in the process of learning from structures the learner is provided with more information, on the other hand the criterion for successful learning is stricter. It is not sufficient that the string language of G contains exactly the yields of the structures in the input sequence, the learning function is required to converge to a grammar G that generates all the grammatical structures which appear in the input sequence. We could say that the learning function must converge to a grammar that is both weakly and strongly equivalent to the grammar that generated the input samples.

Clearly, from a psycholinguistic point of view, both learning from flat strings and from proof tree structures are quite unrealistic models of first language acquisition by human beings. In the first case, experimental evidences (see [START_REF] Pinker | The Language Instict[END_REF]) show that children can't acquire a language simply by passively listening to flat strings of words. First of all, we can think that prosody (or punctuation, in written text) can provide "structural" information to the children on the syntactic bracketing of the sentences she is exposed to (although they do not always coincide) and it is known that prosody is needed to learn a language for a child. Furthermore, another interesting evidence of the fact that a child needs something more to learn her mother tongue is given by the fact that no children can improve their grammatical skills during the early stages of their language acquisition process by watching TV: it seems very likely they need "richer data" than simple sentences uttered by an adult. Some researchers (see [START_REF] Tellier | Rôle de la compositionnalité dan l'acquisition d'une langue[END_REF]) hypothesize this additional information comes to the children as the semantic content of the first sentences she is exposed to, whose she could have a first, primitive grasp through first sensory-motor experiences.

On the other hand, it is also highly unlikely that a child can have access to something like a proof tree structure of the sentence she is exposed to. Our belief is that a good formal model for the process of learning should rely on something "halfway" between flat strings of words and highly structured and complete information coming from the proof tree structure of the sentence. However, since, as we've already seen in section 7.2, proof tree structures provide a very natural support for a Montague-like semantics, we think that our model for learning a rigid Lambek grammar from structured data represents a first, simple but meaningful approximation of a more plausible model of learning.

In any case, even though in most of real-world applications only unstructured data are available, we are often interested not only in the sentences that a grammar derives, but also in derivation strings that grammar assigns to sentences. That is, we generally want a grammar that makes structural sense.

Grammatical Inference as Unification

We set our inquiry over the learnability for rigid Lambek grammars in the more general logical framework of the Theory of Unification. We will stick to the approach described in [START_REF] Nicolas | Grammatical inference as unification[END_REF] based on the attempt to reduce the process of inferring a categorial grammar to the problem of unifying a set of terms. This approach establishes a fruitful connection between Inductive Logic Programming techniques and the field of Grammatical Inference, a connection that has already been proved successful in devising efficient algorithms to infer k-valued CCGs from positive structured data (see [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]). Our aim is to exploit as much as possible what has already been done in this direction by exploring the possibility of adapting existing algorithms for CCGs to rigid Lambek grammars.

Argument Nodes and Typing Algorithm

Our learning algorithm is based on a process of labeling for the nodes of a set of proof tree structures. We introduce here the notion of argument node for a normal form proof tree. We will be a bit sloppy in defining such a notion, and sometimes we will use the same notation to indicate a node and the type it's labeled by, when this doesn't engender confusion, and much will be left to the graphical" interpretation of trees and their nodes. However, we can always think of a node as a De Bruijn-like object (a notation for lambda terms in which variable names are replaced by "paths" within the tree in which they occur, see [dB72]) without substantially affecting the meaning of what will be proved. Definition 9.1 Let P be a normal form partial parse tree. Let's define inductively the set Arg(P ) of argument nodes of P . There are three cases to consider:

• P is a single node labeled by a type x, which is the only member of Arg(P ).

• P looks like one of the following

G G P 1 P 1 D D P 2 P 2 \E /E B B , A A\B B/A A INRIA \E \E /E /E x 2 x 2 x 2 x 2 x 1 x 1 x 1 x 1 x \x 2 1 ® ® x /x 1
x 1 t 1 t 1 x \x 1 2 t 2 t 2 x 2 x 2 \E \E ® x 1
and t 2 has all of its argument nodes (uniquely) labeled. So, by induction hypothesis, its fully and uniquely labeled, and so is t.

2. t ≡ /E(t 1 ,t 2 ). Analogous to case 1.

3. t ≡ \I(t 1 ) or t ≡ /I(t 1 ). By definition, Arg(t) = Arg(t 1 ), then by hypothesis, any argument node in t 1 is labeled. Then, by induction hypothesis, t 1 is fully (and uniquely) labeled, and since t is well-formed, there must be at least two undischarged leaves in t 1 . So t can be fully labeled according, respectively, to the following rules:

INRIA \I \I x \x 2 1 x 1 x 1 t 1 t 1 x 2 [x ] 2 ® ... ... ... ... /I /I x /x 1 2 x 1 x 1 t 1 t 1 x 2 [x ] 2 ® ,
where x 2 labels, respectively, the leftmost and the rightmost undischarged leaf.

The proof of the previous proposition has implicitly defined an algorithm for labeling in the most general way the nodes of a normal form proof tree structure. Definition 9.3 A principal parse of a proof tree structure t is a partial parse tree T of t, such that for any other partial parse tree T of t, there exists a substitution σ such that, if a node of t is labeled by type A in T , it's labeled by σ(A) in T .

From the proof of proposition 9.2 it's easy to devise an algorithm to get a principal parse for any well formed normal form proof tree structure.

PRINCIPAL PARSE ALGORITHM

• Input: a well formed normal form proof tree structure t;

• Output: a principal parse T of t in a Lambek grammar G.

Step 1. Label with distinct variables each argument node in t;

Step 2. Compute the types for the remaining nodes according to the rules described in the proof of proposition 9.2.

Obviously, this algorithm always terminates. If T is the resulting parse, we can easily prove it's principal. If T is another parse for t, let's define a substitution σ in the following way: for each variable x ∈ Var(G), find the (unique, for construction) node in T labeled by x, and let σ(x) be the type labeling the same node in T . By induction on A ∈ T p(G) (where T p(G) is the set of all subtypes appearing in a Lambek Grammar G), we prove that if A labels a node of T , σ(A) labels the corresponding node of T . Induction Basis. If A ∈ Var, this holds by definition.

Induction

Step. Let A = B\C labels a node of T . Then the relevant part of T must look like one of the following cases:

• First case: • Second case:

INRIA

The case A = C/B is entirely similar, thus completing the induction.

It follows that if a node of T is labeled by A, then the corresponding node of T is labeled by σ(A). That is to say, with a small abuse of notation, T = σ(T ).

RLG Algorithm

Our algorithm (called RLG from Rigid Lambek Grammar) takes as its input a finite set D of proof tree structures over a finite alphabet Σ and returns a rigid Lambek grammar G over the same alphabet whose structure language contains (properly) D, if it exists; a correct statement that there's no such a rigid Lambek grammar otherwise.

Our algorithm is based on the type algorithm described in section 9.2 and on the unification algorithm described in section 8.2.

RLG ALGORITHM.

• input: a finite set D of proof tree structures.

• output: a rigid Lambek grammar G such that D ⊂ PL(G), if there is one.

We illustrate the algorithm using the following example: Step 1. Normalize all the proof tree structures in D, if they are not normal, according to the rules described in section 6.3.

Step 2. Assign a type to each node of the structure in D as follows:

1. Assign s to each root node. x /x 2 5

(x /x )\x Our algorithm is based on the "principal parse algorithm" described in the previous section, which has been proved to be correct and terminate, and the unification algorithm described in section 8.2. The result is, intuitively, the most general rigid Lambek Grammar which can generate all the proof tree structures appearing in the input sequence.

Properties of RLG

In the present section we prove some properties of the RLG algorithm that will be helpful to study its behaviour in the limit.

The following lemma is almost trivial but it will play an important role in the convergence proof for the RLG algorithm. It simply states that the tree language of the grammar inferred just after the labeling of the structures properly contains the sample structures. This work aims at making a further step in the direction of bridging the gap which still separates any formal/computational theory of learning from a meaningful formal linguistic theory.

We have introduced the basic notions of Formal Learnability Theory as first formulated by E.M. Gold in 1967, and of Lambek Grammars, which appeared for the first time in an article of 1958.

The former, which is one of the first completely formal descriptions of the process of grammatical inference, after an initial skepticism about its effective applicability, is at present to object of a renewed interest due to some meaningful and promising learnabiluty results.

Even the latter, long neglected by the linguistic community, is experiencing a strong renewed interest as a consequence of recent linguistics achievements which point at formal grammars completely lexicalized, as Lambek grammars are. Even if they're still far from being the ultimate formal device for the formalization of human linguistics competence, they're universally looked at as a promising tool for further developments of computational linguistics.

In the present work we've drawn the attention to a particular class of Lambek grammars called rigid Lambek grammars, and we've proved that they are learnable in Gold's framework from a structured input. We've used most recent results by Hans-Joerg Tiede for formally define our notion of structure for a sentence: he has recently proved that the proof tree language generated by a Lambek grammar strictly contains the tree language generated by context-free grammars. His notion of a proof as the grammatical structure of a sentence in a categorial grammar is also useful in providing a natural support to a Montagovian semantics for that sentence. Therefore, our choice for a structured input for our learning algorithm in the form of proof tree structures is not gratuitous, but it's coherent with the mainstream of (psycho-)linguistics theories about first language learning which stress the importance of providing the learner with informatioannly and semantically rich input in the process of her language acquisition.

We believe it to be a partial but meaningful result, which once more shows how versatile and powerful can be this learning theory, once neglected because it was widely held that it couldn't but account for the learnability of most trivial classes of grammars.

Much is left to be done along many directions. First of all, there's still no real theory of rigid, or k-valued, Lambek grammars: we still know very few formal properties of such grammars which seem to have an undisputable linguistic interest. We still lack, for example, a hierarchy theorem for languages generated by k-valued Lambek grammars.

Another important point which is still unanswered lies in the decidability for PL(G 1 ) ⊆ PL(G 2 ) for G 1 , G 2 Lambek grammars, that is deciding whether the tree language generated by a grammar is contained in the tree language generated by another one, for any two grammars. Such a question is decidable for the non-associative variant of Lambek grammars. Proving this question decidable would allow as to very easily devise a learning algorithm for k-valued Lambek grammars.

Our learnability result is in our opinion a first step toward a more convincing and linguistically plausible model of learning for k-valued Lambek grammars from less and less structurally rich input. Needless to say, learning from such an informationally rich input like proof-tree structures hardly has any linguistic plausibility. On the other hand the deep connections between proof tree structures for a sentence in Lambek grammars and its "Montague-like" semantics seems to address to a more convincing model for learning based both on syntactic and semantic information.

INRIA

Definition 3 . 5 (

 35 Learning Function) Let Ω, S,L be a grammar system. A learning function is a partial function that maps finite sets of sentences to grammars,ϕ : k≥1 S k Ωwhere S k denotes the set of k-ary sequences of sentences.

Figure 4 :

 4 Figure 4: Kanazawa's theorem.

  r.t. to inclusion) of the set {L ∈ L(G) | {s 0 , . . . , s n } ⊆ L}. This implies the following condition: Condition 3.34 There is a computable partial function ψ that takes any finite set D of sentences and maps it to a grammar ψ(D) ∈ G such that L(ψ(D)) is a minimal element of {L ∈ L(G) | D ⊆ L} whenever the latter set is non-empty. INRIA Definition 3.35 Let ψ a computable function satisfying condition 3.34. Define a learning function ϕ as follows

Proposition 3 .

 3 36 Let G be a class of grammars such that L(G) has finite elasticity, and a computable function ψ satisfying condition 3.34 exists. Then the learning function ϕ defined in definition 3.35 learns G.

Theorem 5 . 5 (

 55 Gaifman normal form) Every categorial grammar is equivalent to a categorial grammar which assigns only categories of the form A, A/B, (A/B)/C. Example 5.6 A CCG equivalent to that in example 5.3 in Gaifman normal form is the following a : s/B, (s/B)/s b : B and here is a derivation for a 3 b 3 :

Definition 5 . 7

 57 The sequent calculus formalization of the Lambek calculus contains the axiom [ID] and the rules of inference [/R], [/L], [\R], [\L], and [Cut]:

Example 5 . 10

 510 The following example is a derivation of x from y/(x\y) (which proves one of the two type-raising rules in Lambek Calculus):

Theorem 5 .

 5 19 (van Benthem) For any sequent A 1 , . . . , A n B there are only finitely many different normal form proofs in the Lambek Calculus.

INRIA 6 .

 6 1 (Partial) Parse Trees for Lambek Grammars

Definition 6 .

 6 20 (Proof tree) A proof tree for a Lambek grammar is a term over the signature Σ = {[/E], [\E], [/I], [\I], [ID]} where • [ID] is the 0-ary function symbol, • [/E] and [\E] are the binary function symbols, • [/I] and [\I] are the unary function symbols.

  and σ(y) = y for all other variables y. Example 6.30 Let σ = {x → x\y, y → s, z → s/(s/x)}. Then σ((s/x)\y) = (s/(x\y))\t and σ(((s/x)\y)/(x/z)) = ((s/(x\y))\s)/((x\y)/(s/(s/x))).

Definition 6 .

 6 35 A substitution σ is said to be faithful to a grammar G if the following condition holds: for all c ∈ dom(G), if G 1 : c → A, G 1 : c → B, and A = B, then σ(A) = σ(B). Example 6.36 Let G be the following grammar G : Francesca → x, dances → x\s, y well → y\(x\s).

Definition 6 .

 6 39 For any grammar G, define the size of G, size(G), as follows: size(G) = ∑ c∈Σ ∑ G:c →A |A|, where, for each type A, |A| is the number of symbol occurrences in A. Lemma 6.40 If G 1 G 2 , then size(G 1 ) ≤ size(G 2 ), Proof. For any type A and any substitution σ, |A| ≤ |σ(A)|. Then the lemma is immediate from the definition of . Corollary 6.41 For any grammar G, the set {G | G G} is finite. Proof. By lemma 6.40, {G | G G} ⊆ {G | size(G ) ≤ size(G)}. The latter set must be finite, because for any n ∈ N, there are only finitely many grammars G such that size(G) = n.If we write G 1 G 2 to mean G 1 G 2 and G 1 = G 2 ,we have Corollary 6.42 is well-founded. Definition 6.43 A grammar G is said to be in reduced form if there is no G such that G G and PL(G) = PL(G ). INRIA 7 Lambek Grammars as a Linguistic Tool 7.1 Lambek Grammars and Syntax

Example 7 . 1 s

 71 Here is the derivation for the sentence Francesca dances with the boy. This is an example of grammatical reasoning where, on the basis of the types we assigned to each word, we infer the well-formedness of a sequence of words. On the other hand we can assume a different perspective: knowing that a sentence is well-formed, what can be said about the type of its components? In the words of Lambek: "Given the information about the categorization of a composite structure, what conclusions could be draw about the categorization of its parts?" ([START_REF] Lambek | The mathematics of sentence structure[END_REF]). That's where the following inference patterns come into play: from Γ, B A, infer Γ A/B, from B, Γ A, infer Γ B\A which gives a linguistic interpretation of the role of the "introduction" rules. That's what is done in the following derivation which allows us to infer that the expression the boy Francesca dances with is of type np:

(

  (λP λQ (∃ (λx(∧(P x)(Q x)))))(λx (sentence x))) ((λP λx ((P x)x))(λx λy ((talk about x)y))) ↓ β (λQ (∃(λx(∧(sentence x)(Q x)))))(λx((talk about x)x)) ↓ β (∃(λx(∧(sentence x)((talk about x)x))))

G 2 :

 2 Members of L rigid are called rigid (string) languages, and members of L k-valued are called k-valued (string) languages. Example 8.1 Let {well, Francesca, dances} ⊆ Σ and let G 1 , G 2 be the following Lambek grammars: G 1 : Francesca → x, dances → x\s, y, well → y\(x\s), Francesca → x, dances → x\s, well → (x\s)\(x\s).

Proposition 8 . 3

 83 Let a ∈ Σ. For each i ≥ 1, let T i be the following proof-tree structure:

4 .Corollary 8 . 6

 486 Exactly like Case 3, with /I in place of \I. If G is a rigid Lambek grammar, each proof-tree structure T ∈ PL(G) has a unique parse.

  , the corresponding part of T looks like:s(B) s(C) \E AT hen A = σ(B)\σ(C) = σ(B\C) = σ(A).

  hypothesis, the corresponding part of T looks like: σ(B)\σ(C) = σ(B\C) = σ(A).

2 . 2 \E 3 .

 223 Assign distinct variables to the argument nodes. Compute types for the remaining nodes according to the rules described in proposition 9.2.

7 INRIAStep 3 . 7 John → x 6 Step 4 .

 73764 Collect the types assigned to the leaf nodes into a grammar GF(D) called the general form induced by D. In general, GF(D) : c → A if and only if the previous step assigns A to a leaf node labeled by symbol c. GF(D) : passionately → x 1 \s him → (x 2 /x 5 )\x 1 a → x 3 /x 4 , x 7 /x 8 girl → x 4 , x 8 loves → (x 3 \x 2 )/x 5 , (x 6 \s)/x Unify the types assigned to the same symbol. Let A = {{A | GF(D) : c → A} | c ∈ dom(GF(D))}, and compute σ = mgu(A). The algorithm fails if unification fails.σ = {x 7 → x 3 , x 8 → x 4 , x 6 → x 3 , x 2 → s, x 5 → x 3 } Step 5. Let RLG(D) = σ[GF(D)].RLG(D) : passionately → x 1 \s him → (s/x 3 )\x 1 a → x 3 /x 4 girl → x 4 loves → (x 3 \s)/x 3 John → x 3

Lemma 9 . 4 t

 94 Let D be the input set of proof tree structures for the RLG algorithm. Then the set of the proof tree structures generated by the 'general form' grammar contains properly D. That is, D ⊂ PL(GF(D)).By induction hypothesis, the corresponding part of Q i looks like: σ(B)\σ(C) = σ(B\C) = σ(A).

  A 1 , . . . , A n s}.

Example 5.21 Let Σ = {Mary, cooked, the, beans} be our alphabet and s our distinguished category. Let's take F such that Mary : np cooked : (np\s)/np the : np/n beans : n Then Mary cooked the beans belongs to the language generated by this grammar, because in Lambek calculus we can prove: np, (np\s)/np, np/n, n s

  and a 1 , . . . , a n are symbols of alphabet Σ such that G : a i → A i for 1 ≤ i ≤ n, the result of attaching a 1 , . . . , a n , from left to right in this order, to the undischarged leaf nodes of D is a partial parse tree of G.

	(np\s)/np likes			[np]
	he		/E
	s/(np\s)		np\s
	/E
	s
	A 1 s/np a 1 /I	...	A n a n	(s/np)\s him
		D	\E
			s
		B
	Then the following is a parse for he likes him:

• A parse tree of G is a partial parse tree of G whose root node is labeled by the distinguished category s.

If a 1 • • • a n is the string of symbols attached to the leaf nodes of a partial parse tree P , a 1 • • • a n is said to be the yield of P . If a parse tree P of G yields

a 1 • • • a n , then P is called a parse of a 1 • • • a n in G.

Example 6.2 Let Σ = {he, him, likes} be our alphabet and let G a Lambek grammar such that G : likes → (np\s)/np, he → s/(np\s), him → (s/np)\s.

  . First of all, let's define what we mean when we say that a Lambek grammar is subset of another one: Definition 6.27 Let G 1 , G 2 be Lambek grammars; we say that G 1 ⊆ G 2 if and only if for any a ∈ Σ such that G 1 : a → A we have also G 2 : a → A. Example 6.28 Let {Francesca, loves, Paolo} ⊆ Σ and let G

1 : Francesca → np loves → np\s G 2 : Francesca → np loves → np\s, np\(s/np) Paolo → np Obviously, G 1 ⊆ G 2

Definition 6.29 A substitution is a function σ : Var → T p that maps variables to types. We can extend it to a function from types to types by setting

  Definition 8.2 Any type A can be written uniquely in the following form: (. . . ((p|A 1 )|A 2 )| . . .)|A n where B|C stands for either B/C or C\B and p ∈ Pr. For 0 ≤ i ≤ n, we call the subtype (. . . (p|A 1 )| . . .)|A i of A a head subtype of A. p is the head of A and is denoted head(A). A i 's are called argument subtypes of A. The number n is called the arity of A.

  Then one can easily verify that {T 1 , . . . ,T k } ⊂ PL(G k ).Let G be a grammar such that {T 1 , . . . , T k } ⊂ PL(G): we will show that G is at least k+1-valued.

	s/x)/x,
	. . .
	(. . . ((s/ x)/x)/ . . .)/x	.
	k times

INRIA

2. Exactly like Case 1, with /E in place of \E.

2 ,

 2 InductionStep. Let t be a normal form proof tree structure of height h > 1. There are 3 cases to consider:1. t ≡ \E(t 1 ,t 2 ). Since, by hypothesis, each node in Arg(t) = {Root(t)} ∪ Arg(t 1 ) ∪ Arg(t 2 ) -{Root(t 2 )}, is labeled, then also Root(t) is labeled with, say, x 2 .For the same reason, any node of Arg(t 1 ) is labeled, too, and so, by induction hypothesis, t 1 is fully (and uniquely) labeled.In particular its root is labeled with, say, x 1 . Since t is well formed, t 2 cannot be the result of the application of a [/I] rule, and since t is normal, t 2 cannot be the result of the application of a [\I] rule, so its root node is one of its argument nodes, too. By hypothesis, each node in Arg(t 2 ) -{Root(t 2 )} has a type, so we can apply the following rule:

RR n • 5964

Symbol ⊂ is used for "is strictly contained in".RR n • 5964

We define the range of a function f : A → B as {x ∈ B : x = f (a) for some a ∈ A} INRIA

Recall that the symbol means that either both sides are defined and are equal, or else both sides are undefined RR n • 5964

Let P i be a parse of T i in G for 1 ≤ i ≤ k. Then the leftmost leaf of P i is the ultimate functor of P i , and if we call A i the type labeling it, we can easily verify that the its arity must be exactly i.

Thus, i = j implies A i = A j .

We show that there is at least one type B such that G : a → B and B ∈ {A 1 , . . . , A k }. Since the relation "is an argument subtype of" is well-founded, there is at least one i such that the argument subtypes of A i are not in {A 1 , . . . , A k }. But in order to produce P i , any argument subtype of A i must be a type assigned to a by G. Therefore G must be at least k+1-valued.

The proof of proposition 8.3 shows Corollary 8.4 There is no Lambek grammar G such that PL(G) = Σ P . Lemma 8.5 Let G be a rigid Lambek grammar. Then for each proof-tree structure T, there is at most one partial parse tree P such that T is the structure of P .

Proof. By induction on the construction of T .

Induction basis. T = c ∈ Σ. Any partial parse tree P whose structure is T is a height 0 tree whose only node is labeled by the symbol c and a type A such that G : c → A. Since G is rigid, there is at most one such type A. Then P , if it exists, is unique. Induction step. There are 4 cases to consider: 1. T is the following proof-tree structure:

\E

Then any partial parse tree of G whose structure is T has the form where P 1 and P 2 are partial

parse trees of G whose structures are T 1 and T 2 , respectively. By induction hypothesis, P 1 and P 2 are unique. This means that the type label B is also uniquely determined, so P is also unique. A substitution σ is said to unify a set A of types if for all A 1 , A 2 ∈ A, σ(A 1 ) = σ(A 2 ). We say that σ unifies a family of sets of types, if σ unifies each set in the family.

A most general unifier is unique up to 'renaming of variables'.

Example 8.9 Let A consist of the following sets:

Then the most general unifier of A is:

There are many different efficient algorithms for unification, which decide whether a finite set of types has a unifier and, if it does, compute a most general unifier for it. For illustration purposes, we present here a non-deterministic version of an unification algorithm.

Our algorithm uses the notion of disagreement pair. The easiest way to define disagreement pair is to consider the types to be tree-like: Definition 8.10 Let A and B be two types. A disagreement pair for A and B is a pair of subterms of A and B, A , B , such that A = B and the path from the root of A to the root of A is equal to the path from the root of B to the root of B .

The following, non-deterministic version of the unification algorithm is taken from [START_REF] Fitting | First-Order Logic and Automatic Theorem Proving[END_REF]: UNIFICATION ALGORITHM.

• input: two types A and B;

• output: a most general unifier σ of A, B, if it exists, or a correct statement that A and B are not unifiable.

Let

The previous algorithm present one of many efficient algorithms for unification, so we the following is a well-defined notion: Definition 8.11 We define a computable partial function mgu that maps a finite family A of finite sets of types to a most general unifier mgu(A), if A is unifiable.

The set G rigid of all rigid Lambek grammars is partially ordered by . Definition 8.12 Let G ⊆ G rigid , and let

We introduce here a new operator among rigid grammars that will be used to prove an interesting property for our learning algorithm at the end of the fifth chapter. Definition 8.13 Let G 1 and G 2 be rigid Lambek grammars. We can assume that G 1 and G 2 have no common variables (if they do, we can always choose a suitable alphabetic variant of one of them such that Var(G 1 ) ∩Var(G 2 ) = / 0). Let

Example 8.14 Let G 1 and G 2 be the following rigid Lambek grammars:

Obviously, from definition 8.13, we have

Proposition 8.16 [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]

Proof. (See [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]).

INRIA then in the first case Arg(P ) = {Root(P )} ∪ Arg(P 1 ) ∪ Arg(P 2 ) -{Root(P 2 )}, and in the second case Arg(P ) = {Root(P )} ∪ Arg(P 1 ) ∪ Arg(P 2 ) -{Root(P 1 )}.

• P looks like one of the following G, [A]

, then Arg(P ) = Arg(P 1 ).

The following proposition justifies our interest for argument nodes for a normal form proof tree structure: Proposition 9.2 Let t be a well formed normal form proof tree structure. If each argument node is labeled, then any other node in t can be labeled with one and only one type.

Proof. We prove that, once argument nodes are labeled, any other node can be labeled, by providing a typing algorithm; uniqueness of typing follows from the rules applied.

By induction on the height h of t:

Induction Basis. There are two cases to consider:

1. h = 0. Trivially, by definition 9.1, t is a single argument node, the result of the application of a single axiom rule [ID] and by definition it's already typed.

2. h = 1. Then t must be the result of a single application of a [/E] or [\E] rule. By hypothesis and definition 9.1, its two argument nodes are labeled with, say, x 1 and x 2 , and the remaining node must be labeled according to one of the following rules:

Proof. Let D = {T 1 , . . . , T n }. The labeling of the nodes of the structures in D that precedes the construction of GF(D) in fact forms a parse tree P i of GF(D) for each structure T i in D. This shows D ⊆ PL(GF(D)). The proper inclusion follows trivially from the fact that D is by hypothesis a finite set, while PL(G), the set of proof tree structures generated by a Lambek grammar G, is always infinite.

Lemma 9.5 Each variable x ∈ Var(GF(D)) labels a unique node in a unique parse tree of D.

Proof. Obviously, by construction, if x ∈ Var(GF(D)), then there must be an i ∈ N such that x labels one of the nodes of a parse tree P i . Since, by construction, for each i = j the sets of variables that label P i are disjoint, x appears in one and only one P i . Besides, since variables are assigned only during the first phase of the type-assignment process of our algorithm, again by construction each variable labels only one node in the deduction tree.

The following lemma makes explicit the relation between the grammar inferred just after the labeling of the structures in the algorithm RLG, and the structure language of the rigid grammar we are trying to infer. Lemma 9.6 Let D be a finite set of proof tree structures. Then, for any Lambek grammar G, the following are equivalent:

Proof. (ii)⇒(i). Suppose there is a substitution σ such that σ[GF(D)] ⊆ G. Then, from proposition 6.32, we have that PL(GF(D)) ⊆ PL(G). This, together with lemma 9.4 proves (i).

(i) ⇒(ii). Let D = {T 1 , . . . , T n } and let P i be GF(D)'s parse of T i for 1 ≤ i ≤ n. Assume D ⊆ PL(G). Then G has a parse Q i of each T i . Define a substitution σ as follows: for each variable x ∈ Var(GF(D)), find a (unique, due to lemma 9.5) P i that contains a (unique, again due to lemma 9.5) node labeled by x, and let σ(x) be the type labeling the corresponding node of Q i . We show that if A labels a node of some P i , then σ(A) labels the corresponding node of Q i .

Proof. By induction on

Induction basis. If A ∈ Var, this holds by definition. If A = t, then any node labeled by A in {P 1 , . . . , P n } is the root node of some P i . Since Q i is a parse tree of G, the root node of Q i must be labeled by t. Induction step. Let A = B\C labels a node of P i . Then the relevant part of P i must look like one of the two following cases: INRIA By induction hypothesis, the corresponding part of Q i looks like: t

The case A = C/B is entirely similar, thus completing the induction. It follows that if

The following proposition establishes an "if and only if" relation between the inclusion of our set of positive samples D in a tree language generated by a rigid grammar G and the successful termination of the RLG algorithm when it has D as its input set. Even more, we have that the rigid grammar inferred by the algorithm is not "larger" than the rigid grammar G.

Definition 9.9 Let ϕ RLG be the learning function for the grammar system G rigid , Σ P , PL defined as follows: 3 ϕ RLG ( T 0 , . . . , T n ) RLG({T 0 , . . . , T n }).

Thanks to previous propositions and lemmas we are able to prove the convergence for the RLG algorithm: Theorem 9.10 ϕ RLG learns G rigid from structures.

Proof. We prove that ϕ RLG learns the class of rigid Lambek grammars from proof tree structures.

Let G be any rigid Lambek grammar and let T i i∈N be an infinite sequence enumerating PL(G). For each i ∈ N, {T 0 , . . . , T i } ⊆ PL(G), so by proposition 9.7 ϕ RLG ( T 0 , . . . , T i ) = RLG({T 0 , . . . , T i }) is defined and ϕ RLG ( T 0 , . . . , T i ) ϕ RLG ( T 0 , . . . , T i+1 ), by corollary 9.8, and ϕ RLG ( T 0 , . . . , T i ) G.

Since, by corollary 6.41, there are only finitely many Lambek grammars G G, ϕ RLG must converge on T i i∈N to some G . Then PL(G) = {T i | i ∈ N} ⊆ PL(G ). Since G G, by proposition 6.32, PL(G ) ⊆ PL(G). Therefore, PL(G ) = PL(G).

When RLG is applied successively to a sequence of increasing set of proof tree structures D 0 ⊂ D 1 ⊂ D 2 ⊂ • • • , it is more efficient to make use of the previous value RLG(D i-1 ) to compute the current value RLG(D i ). Definition 9.11 If G is a rigid Lambek grammar and D is a finite set of proof tree structures, then let RLG (2) (G, D) G RLG(D).

Lemma 9.12 If D 1 and D 2 are two finite sets of proof tree structures, RLG (2) (RLG(D 1 ), D 2 ) RLG(D 1 ∪ D 2 ).

Proof. (See [START_REF] Kanazawa | Learnable Classes of Categorial Grammars[END_REF]). Suppose that RLG (2) (RLG(D 1 ), D 2 ) is defined. By lemma 8.15, RLG(D 1 ) RLG (2) (RLG(D 1 ), D 2 ) and RLG(D 2 ) = RLG (2) (RLG(D 1 ), D 2 ). This implies that D 1 ∪D 2 ⊆ PL(RLG (2) (RLG(D 1 ), D 2 )), so by proposition 9.7, RLG(D 1 ∪ D 2 ) exists and RLG(D 1 ∪ D 2 ) RLG (2) (RLG(D 1 ), D 2 ).