Conjoinability and unification in Lambek categorial grammars

Annie Foret Email : foret@irisa.fr IRISA and University of Rennes1, FRANCE

December 18, 2001

Abstract

Recently, learning algorithms in Gold’s model have been proposed for some particular classes of classical categorial grammars [Kan98]. We are interested here in learning Lambek categorial grammars.

In general grammatical inference uses unification and substitution. In the context of Lambek categorial grammars it seems appropriate to incorporate an operation on types based both on deduction (Lambek derivation) and on substitution instead of standard substitution and standard unification.

After an introduction (in connection with learning), this paper will recall conjoinability results [Lam58, Pen93] - using groups - ; we then consider a characterization of conjoinability - using quasi-groups - for the nonassociative version of Lambek calculus. We then relate these characterizations to the modified unification investigated in [For01] for the associative Lambek calculus.

1 Introduction

Categorial grammars have been studied in the domain of natural language processing; these grammars are lexicalized grammars that assign types (or categories) to the lexicon. We focus here on Lambek categorial grammars [Lam58] to which linear logic [Gir95] is closely connected. We also consider the Non-Associative Lambek Calculus introduced in [Lam61] that avoids the associativity of formula concatenation.

Learning (in the sense of Gold [Gol67]) in our context is a symbolic issue that may be described as follows. Let G be a class of grammars, that we wish to learn from examples. The issue is to define an algorithm, that when applied to a finite set of sentences, yields a grammar in the class that generates the examples; the algorithm is also required to converge. Formally, let L(G) denote the language associated with grammar G, and let V be a given alphabet, a learning algorithm is a function ϕ from finite sets of words in V^{∗} to G, such that for G ∈ G with L(G) = (e_{i})_{i∈N} there exists a grammar G′ ∈ G and there exists n_{0} ∈ N such that : ∀n > n_{0} ϕ({e_{1}, …, e_{n}}) = G′ ∈ G with L(G′) = L(G).

One good reason to use categorial grammars in a learning perspective is that they are fully lexicalized : the rules are already known, only types assigned to words have to be derived from examples. Essential known results on this subject may be found in [Kan98]. The learning technique avoids to add a new type each time there is a new use of a word in an example, but applies a unification algorithm instead. One important case is when we limit the number of types per word for example to only one type.

Our aim is to explore learning mechanisms for Lambek calculus. Whereas standard unification is used in existing works such as [BP90, Kan98, Nic99, Bon00], in such a context, it seems appropriate to use not only unification but also deduction to combine grammars in the learning process. This issue is discussed in [For01] for the associative version of the Lambek calculus where we define a preorder ∥= on types and a ∥= -unification that we characterize in terms of groups. This paper is in some sense complementary to it, we show similar results for the non-associative version in terms of quasi-groups. As detailed after, ∥= -unification and conjoinability as introduced in [Lam58] are strongly connected.

The paper is organized as follows. Section 2 addresses background definition and known results. Section 3 gives a characterization of conjoinability in non associative Lambek calculus : we follow the main steps of [Pen93] for the associative case ; we here establish a connection with quasi-groups instead of groups. As pointed by M. Mortgaat, such a characterization of conjoinability in the nonassociative case was observed in [Ver96] but without mentionning quasi-groups. Section 4 applies these conjoinability results to ∥= -unification mixing deduction and substitution ; we establish a characterization of ∥= -unifiability in the nonassociative version, in terms of unification in quasi-groups ; this equational theory has been treated in the context of term rewriting systems by [Hul80], who provides a unification algorithm.

2 Background

2.1 Categorial grammars

In this section, we introduce basic definitions concerning categorial grammars. The interested reader may also consult [Cas88, Ret00, Bus97, Moo97] for an introduction or for further details.

Let Σ be a fixed alphabet.

Types. Types are constructed from P r (set of primitive types) and three binary connectives / , \ and ⊗ for products. In some versions, we drop ⊗.

T p denotes the set of types. P r contains a distinguished type, written S, also called the principal type ; we assume that P r = P r_{c} ∪ V ar, where P r_{c} is a set of constants with S ∈ P r_{c} and V ar is a set of variables (variables are different from constants).

Classical categorial grammar. A classical categorial grammar over Σ is a finite relation G between Σ and T p. If < c, A >∈ G, we say that G assigns A to c, and we write G : c ↦ A.

Derivation ⊢ _{AB} on types without ⊗. The relation ⊢_{AB} is the smallest relation ⊢ between T p^{+} and T p, such that for all Γ, Δ ∈ T p^{+} and for all A, B ∈ T p:

A ⊢ A

if Γ ⊢ A and Δ ⊢ A \ B then Γ, Δ ⊢ B (Backward application) if Γ ⊢ B / A and Δ ⊢ A then Γ, Δ ⊢ B (Forward application)

We give a formulation of Lambek calculus, written L, including products consisting in introduction rules on the left and on the right of a sequent. For Lambek calculus without products, one simply drops the rules for ⊗.

Lambek Derivation ⊢ _{L}. The relation ⊢_{L} is the smallest relation ⊢ between T p^{+} and T p, such that for all Γ, Γ′ ∈ T p^{+}, Δ, Δ′ ∈ T p^{∗} and for all A, B ∈ T p :

A ⊢ A

if A, Γ ⊢ B then Γ ⊢ A \ B ( \right ) if Γ, A ⊢ B then Γ ⊢ B / A ( /right ) if Γ ⊢ A and Δ, B, Δ′ ⊢ C then Δ, Γ, A \ B, Δ′ ⊢ C ( \left ) if Γ ⊢ A and Δ, B, Δ′ ⊢ C then Δ, B / A, Γ, Δ′ ⊢ C ( /left ) if Δ, A, B, Δ′ ⊢ C then Δ, (A ⊗ B), Δ′ ⊢ C (⊗-left) if Γ ⊢ A and Γ′ ⊢ B then Γ, Γ′ ⊢ (A ⊗ B) (⊗-right)

When we replace T p^{+} by T p^{∗} in Γ ∈ T p^{+} in the definition above, we get another version of Lambek calculus, without the non-empty left hand-side requirement, which we refer to as L_{∅} with derivation relation ⊢_{L_{∅}}.

We now give a formulation of Non associative Lambek calculus, written NL, including products. In the Gentzen presentation, the derivability relation holds between a term in S and a formula in T p, where the term language is S ::= T p|(S, S). Terms in S are also called G-terms. A sequent is a pair (Γ, A) ∈ S × T p. The notation Γ[Δ] represents a G-term with a distinguished occurrence of Δ (with the same position in premise and conclusion of a rule).

Non associative Lambek Derivation ⊢ _{NL}. The relation ⊢_{NL} is the smallest relation ⊢ between S and T p, such that for all Γ, Δ ∈ S and for all A, B, C ∈ T p:

A ⊢ A
if (A, Γ) ⊢ B then Γ ⊢ A \ B ( \right )
if (Γ, A) ⊢ B then Γ ⊢ B / A ( /right )
if Γ ⊢ A and Δ[B] ⊢ C then Δ[(Γ, A \ B)] ⊢ C ( \left )
if Γ ⊢ A and Δ[B] ⊢ C then Δ[(B / A, Γ)] ⊢ C ( /left )
if Δ[(A, B)] ⊢ C then Δ[A ⊗ B] ⊢ C (⊗-left)
if Γ ⊢ A and Δ ⊢ B then (Γ, Δ) ⊢ (A ⊗ B) (⊗-right)

Gentzen terms translation. For Δ ∈ S, we define its formula translation Δ^{∘} as : (Δ_{1}, Δ_{2})^{∘} = Δ_{1}^{∘} ⊗ Δ_{2}^{∘} and A^{∘} = A for A ∈ T p.

Note. We recall that the cut rule is satisfied by ⊢_{AB}, ⊢_{L} and ⊢_{NL}.

Notation. In some sections, we may write simply ⊢ instead of ⊢_{AB}, ⊢_{L} or ⊢_{NL}.

Language. Let G be a classical categorial grammar over Σ. G generates a string c_{1} … c_{n} ∈ Σ^{+} iff there are types A_{1}, …, A_{n} ∈ T p such that :

G : c_{i} ↦ A_{i} (1 ≤ i ≤ n) and A_{1}, …, A_{n} ⊢ _{AB} t

The language of G, written L(G), is the set of strings generated by G. We define similarly L_{L}(G) replacing ⊢ _{AB} with ⊢ _{L} in the definition of L(G). We also define similarly L_{NL}(G) replacing ⊢ _{AB} by ⊢ _{NL} in the sequent where the types are parenthesized in some way.

Rigid and k-valued grammars. Categorial grammars that assign at most k types to each symbol in the alphabet are called k-valued grammars; 1-valued grammars are also called rigid grammars.

Example 1 Let Σ_{1} = {John, Mary, likes} and let P r = {S, N} for sentences and nouns respectively.

Let G_{1} = {John ↦ N, Mary ↦ N, likes ↦ N \ (S / N)}

We get (John likes Mary) ∈ L(G_{1}) since (N, N \ (S / N), N ⊢_{AB} S) G_{1} is a rigid (or 1-valued) grammar.

2.2 Unification and grammatical inference

Substitution and unification play an important role in grammatical inference. In this section we recall some related definitions.

Substitutions. A substitution σ is a function from variables in V ar to types in T p which is extended from types to types by :

σ(p) = p for p ∈ P r_{c} (with σ(S) = S)

σ(A \ B) = σ(A) \ σ(B) σ(B / A) = σ(B) / σ(A)

σ(B ⊗ A) = σ(B) ⊗ σ(A)^{1} We extend this definition to G-terms and sequences by : σ(Γ, Δ) = (σ(Γ), σ(Δ)) and respectively by : σ(A_{1}, …, A_{n}) = σ(A_{1}), …, σ(A_{n})

Note. The following principle (hereafter called the replacement principle) holds for ⊢_{AB}, ⊢_{L} and ⊢_{NL} : if Γ ⊢ B then σ(Γ) ⊢ σ(B).

Substitutions extended to grammars. Given a substitution σ, and a grammar G, σ(G) denotes the grammar obtained by applying σ in the type assignments, that is : σ(G) = {< c, σ(A) >; < c, A >∈ G}.

Preorders based on substitutions. Substitution allows to define several preorders as follows :

⪯ on types defined by A ⪯ B iff ∃σ : σ(A) = B (B is said an instance of A, or also A is said more general than B) ;

⪯ on substitutions defined by σ ⪯ θ iff ∀A ∈ T p : σ(A) ⪯ θ(A) ; this yields σ ⪯ θ iff ∃ρ : ρσ = θ (where we write ρσ the composition of substitutions σ with ρ as : ∀x : ρσ(x) = ρ(σ(x))) ; σ is said to be more general than θ;

⊑ on grammars as follows : G_{1} ⊑ G_{2} iff ∃σ : σ(G_{1}) ⊆ G_{2} ^{2} where we write G_{1} ⊆ G_{2} whenever G_{2} contains all type assignments of G_{1}.

Note. It is easy to see (using the replacement principle) that if G_{1} ⊑ G_{2} then L(G_{1}) ⊆ L(G_{2}) (also for L and NL). This fact is useful in the learning approach.

Unification. A set of types A is said unifiable whenever there exists a substitution σ such that σ(A) = σ(B) for all A, B ∈ A ; σ is then said a unifier of the types A. Let U(A)) denote the set of unifiers of A. A principal unifier of A is a unifier σ, such that ∀θ ∈ U(A) : σ ⪯ θ.

1for a calculus including ⊗

2this is a simplified version : Kanazawa adds a faithfullness condition such that if two types assigned to the same symbol in G_{1} are distinct they are kept distinct by σ which has no impact in the rigid case.

The usual unification problem is as follows : given two types to indicate whether these types are unifiable and if so to give a principal unifier. One important property is that when two types are unifiable, they admit a principal unifier that is unique modulo variable renaming.

Unification extended to rigid categorial AB-grammars and least upper bounds . A substitution σ is said to unify a family F of sets of types, if σ unifies each set in the family. A principal unifier σ of F is a unifier of F such that forall unifier θ of F : σ ⪯ θ.

Let us fix mgu a function that computes a principal unifier (undefined if there is none) for each set of types (or family of sets of types). Let G_{1} and G_{2} be rigid grammars with no common variables. We consider the family F of the sets A_{c} for each c in the alphabet of G_{1} or G_{2} : A_{c} = {A; < c, A >∈ G_{1} or < c, A >∈ G_{2}}. We let G_{1} ⊔ G_{2} = mgu(F)(G_{1} ∪ G_{2}). This operation computes the least upper bound of rigid grammars (with respect to ⊑ ); it has properties of particular interest for the convergence of the learning algorithm.

2.3 Conjoinability

We now define the conjoinability relation introduced in [Lam58]. We also view this equivalence as the special case of ∥= -unifiability without variables.

Equivalence on types.

1. The join-equivalence, written ∼, is defined by :

t ∼ t′ iff ∃t_{1}, ..., t_{n} : ∀i < n (t_{i} ⊢ t_{i+1} or t_{i+1} ⊢ t_{i}) with t = t_{1}, t′ = t_{n} 2. We also define ∼^{1} by : t ∼^{1} t′ iff t ⊢ t′ or t′ ⊢ t The equivalence ∼ is thus the transitive closure of ∼^{1}.

3. Types t_{1}, t_{2}, ...t_{n} are said conjoinable whenever there exists t such that t_{i} ⊢ t (for all i ≤ n). In this case t is called a join for t_{1}, t_{2}, ...t_{n} .

2.4 Conjoinability and group models in Lambek Calculus

We now recall some properties of conjoinability in the ⊢_{L} case. The following result is due to Lambek.

Proposition 1 (Diamond property in L) Let t_{1} and t_{2} be two types. The following assertions are equivalent in L :

(i) t_{1} and t_{2} are conjoinable (∃t : t_{1} ⊢ t and t_{2} ⊢ t) (ii) (∃t′ : t′ ⊢ t_{1} and t′ ⊢ t_{2})

Proof. We follow the version of [Pen93]

- if t_{i} ⊢ t, for i=1,2, we verify that t′ ⊢ t_{i}, for i=1,2, where :

t′ = (t_{1} / t).t.(t \ t_{2})

- if t′ ⊢ t_{i}, for i=1,2, we verify that t_{i} ⊢ t, for i=1,2, where :

t = (t′ / t_{1}) \ t′ / (t_{2} \ t′)

Proposition 2 Let t_{1} and t_{2} be two types. The assertion t_{1} ∼ t_{2} in L is also equivalent to (i) and (ii) of the diamond property above.

Free group interpretation.

Let F G denote the free group with generators P r, operation . and with neutral element Λ.

We associate with each formula A an element in F G written [[A]] as follows : [[p]] = p for p atomic [[A_{1} \ A_{2}]] = [[A_{1}]]^{−1}.[[A_{2}]] [[A_{1} / A_{2}]] = [[A_{1}]].[[A_{2}]]^{−1} [[A_{1} ⊗ A_{2}]] = [[A_{1}]].[[A_{2}]] We extend the notation to non-empty sequents by : [[A_{1}, A_{2}, …, A_{n}]] = [[A_{1}]].[[A_{2}]]. . . . .[[A_{n}]]

The following known property states that such groups are models :

if Γ ⊢_{L} A then [[Γ]] =_{F G} [[A]]

Proposition 2 together with the following completeness result of Pentus is of particular interest for the investigations of ∥= -unification.

Theorem 1 (characterization of ∼ in L by groups) For any types t and t′ : t ∼ t′ in L iff [[t]] =_{F G} [[t′]]

3 Conjoinability and quasi-groups in NL

3.1 Conjoinability in NL

We first get the following useful congruence property. Recall that a pre-congruence is a binary relation that is compatible with the operations here with respect to / , \ , ⊗ ; a pre-congruence is a congruence if it is an equivalence.

Proposition 3 In NL : ∼^{1} and ∼ are pre-congruences and ∼ is a congruence.

Proof. We get easily that ∼^{1} is a pre-congruence :

- if A ⊢ B then (A, C) ⊢ B ⊗ C then A ⊗ C ⊢ B ⊗ C ;

- if A ⊢ B then (A / C, C) ⊢ B then A / C ⊢ B / C ;

- if A ⊢ B then (C / B, A) ⊢ C then C / B ⊢ C / A; the other cases are similar. We then get that ∼ is a congruence as a corollary

Next property is a central one. It has analogues in the associative case, in [Lam58] or in [Pen93] where the constructed types are different. In the following property we take the construction in [Lam58] and show that it can be extended in the non-associative case ( the simplified one in [Pen93] is not suitable^{3}, this is also observed in [Ver96]).

Proposition 4 (Diamond property in NL) Let t_{1} and t_{2} be two types. The following assertions are equivalent in NL :

(i) t_{1} and t_{2} are conjoinable (∃t : t_{1} ⊢ t and t_{2} ⊢ t) (ii) (∃t′ : t′ ⊢ t_{1} and t′ ⊢ t_{2})

Proof. We extend the version of Lambek to NL

- if t_{i} ⊢ t, for i=1,2, we verify ^{4} that t′ ⊢ t_{i}, for i=1,2, where :

t′ = (t_{1} / ((t / t) \ t)) ⊗ ((t / t) \ t_{2})

- if t′ ⊢ t_{i}, for i=1,2, we verify ^{5} that t_{i} ⊢ t, for i=1,2, where :

t = (t_{1} ⊗ (t′ \ t′)) / (t_{2} \ (t′ ⊗ (t′ \ t′)))

Corollaries.

1. As a corollary in NL, we get that two types t_{1} and t_{2} are join-equivalent (t_{1} ∼ t_{2}) iff they have a join, that is (i) (∃t : t_{1} ⊢ t and t_{2} ⊢ t) or equivalently iff (ii) (∃t′ : t′ ⊢ t_{1} and t′ ⊢ t_{2}) . ^{6}

3it involves different parenthesizing

4from t_{2} ⊢ t :

((t / t), (t / t) \ t_{2}) ⊢ t (by \ -left)

(t / t) \ t_{2} ⊢ (t / t) \ t (by \ -right)

(t_{1} / ((t / t) \ t)) ⊗ ((t / t) \ t_{2}) ⊢ t_{1} (by / -left, ⊗-left)

hence t′ ⊢ t_{1} and secondly t′ ⊢ t_{2} from t_{1} ⊢ t and t ⊢ (t / t) \ t:

(t_{1} / ((t / t) \ t), t) ⊢ t (by / -left)

(t_{1} / ((t / t) \ t)) ⊢ (t / t) (by / -right)

(t_{1} / ((t / t) \ t)) ⊗ ((t / t) \ t_{2}) ⊢ t_{2} (by \ -left, ⊗-left)

5from t′ ⊢ t_{2} and t′ ⊗ (t′ \ t′) ⊢ t′ :

(t′, t_{2} \ (t′ ⊗ (t′ \ t′))) ⊢ t′ (by \ -left)

t_{2} \ (t′ ⊗ (t′ \ t′)) ⊢ (t′ \ t′) (by \ -right)

(t_{1}, (t_{2} \ (t′ ⊗ (t′ \ t′)))) ⊢ (t_{1} ⊗ (t′ \ t′)) (by ⊗-right)

hence t_{1} ⊢ t and secondly t_{2} ⊢ t from t′ ⊢ t_{1} :

(t′ ⊗ (t′ \ t′)) ⊢ (t_{1} ⊗ (t′ \ t′)) (by ⊗-right, ⊗-left)

(t_{2}, (t_{2} \ (t′ ⊗ (t′ \ t′)))) ⊢ (t_{1} ⊗ (t′ \ t′)) (by \ -left)

2. Note also that a finite set of types has a join iff the types are pairwise conjoinable.

3.2 Quasi-groups

Quasi-groups are sets equiped with three binary operations ., / , \ that satisfy the following equations :

x.(x \ y) = y

(x / y).y = x

x \ (x.y) = y

(x.y) / y = x

The equational theory, here written QG, of quasi-groups admits a canonical rewriting system as found by Knuth and Bendix (70) and further studied in [Hul80].

The above four equations oriented from left to right are completed with two new rules to produce such a canonical rewrite system :

(x / y) \ x → y

x / (y \ x) → y

Variants. The case of quasi-groups with a neutral element e is similar, see [Hul80] for details. ^{7}

QG-Unification. Solving equations in quasi-groups, or QG-unification admits a complete finite algorithm as shown by [Hul80], whose procedure is based on rewriting. A similar result holds for quasi-groups with identity [Hul80].

6if (i) then t_{1} ∼ t_{2} is obvious. If t_{1} ∼ t_{2} we proceed by induction on n such that for 1 ≤ i < n:

s_{i} ⊢ s_{i+1} or s_{i+1} ⊢ s_{i} : if s_{n} ⊢ s_{n+1} = t_{2} then by induction ∃s_{0} such that s_{0} ⊢ s_{i}(i < n+1) from which by cut s_{0} ⊢ s_{i}(i ≤ n + 1) ; if s_{n+1} ⊢ s_{n} then by induction ∃s′ such that s_{i} ⊢ s′(i < n + 1)

from which by cut s_{i} ⊢ s′(i ≤ n + 1)

7one adds the equations :

e.x = x

x.e = x

that are also oriented from left to right and a canonical rewrite system is obtained by adding the following rules :

e \ x → x

x / e → x

x / x → e

x \ x → e

3.3 Quasi-groups as models

We show that quasi-groups are models for ⊢_{NL}. Our interest is to use them as (complete) models for conjoinability.

Free quasi-group. Let F QG denote the free quasi-group with generators P r, operations ., / \ .

From types to F QG. We associate with each type formula A an element in F QG written [[A]] as follows :

[[p]] = p for p atomic

[[A_{1} \ A_{2}]] = [[A_{1}]] \ [[A_{2}]]

[[A_{1} / A_{2}]] = [[A_{1}]] / [[A_{2}]]

[[A_{1} ⊗ A_{2}]] = [[A_{1}]].[[A_{2}]]

We extend the notation to G-terms by :

[[(A_{1}, A_{2})]] = [[A_{1}]].[[A_{2}]]

Proposition 5 (Models) If Γ ⊢_{NL} A then [[Γ]] =_{F QG} [[A]]

Proof. We may proceed by induction on derivations (see Annex).

Residuated groupoids. We may also consider quasi-groups as a particular case of residuated groupoids that are known as (complete) algebraic models [Bus97] for NL. A residuated groupoid is a structure (M, ∘, ⇒, ⇐, ≤) such that (M, ∘) is a groupoid, ≤ is a partial ordering on M, and ⇒, ⇐ are binary operations on M which fullfill the equivalences (for a, b, c ∈ M) : a ≤ c ⇐ b iff a ∘ b ≤ c iff b ≤ a ⇒ c . In the case of quasi-groups, we may take (. , \ , / , =) as (∘, ⇒, ⇐, ≤) for which the above equivalences are easy to verify. ^{8}

From F QG to types. We define Φ from F QG to Tp as the morphism from (F QG, ., \ , / ) to (T p, ⊗ , \ , / ) defined by Φ (p) = p for p atomic; (by this we mean ^{9} : Φ (p) = p for p atomic , Φ (a.b) = Φ (a) ⊗ Φ (b) , Φ (a \ b) = Φ (a) \ Φ (b) , Φ (a / b) = Φ (a) / Φ (b) ).

Remarks. The following facts are straightforward :

1. Φ ([[A]]) = A

2. [[ Φ (a)]] =_{F QG} a

3. If a =_{F QG} b then [[ Φ (a)]] =_{F QG} [[ Φ (b)]]^{10}

8if a = c / b then a. b = (c / b). c = c ; if a. b = c then c / b = (a. b) / b = a ; the other verification are dual to these ones.

9For the variant with neutral element, we add : Φ (e) = S \ S

10Note however that we may have a =_{F QG} b with Φ (a) ≠ Φ (b)

3.4 Characterizing NL-conjoinability by quasi-groups

We show how NL-conjoinability and quasi-groups are related, in a way similar to [Pen93] for L-conjoinability and groups.

We recall that QG also denotes the set of four equations defining its equational theory as in section 3.2.

Proposition 6 (quasi-group equality and ∼ in NL)

1. If a = b is an instance of an equation in QG then Φ (a) ∼^{1} Φ (b)

2. If a =_{F QG} b then Φ (a) ∼ Φ (b)

Proof. See Annex.

Theorem 2 (characterization of ∼ in NL by quasi-groups)

For any types t and t′ : t ∼ t′ in NL iff [[t]] =_{F QG} [[t′]]

Proof. This property is a corollary of previous results as follows :

- if t ∼ t′ then we can find t_{0} such that both t_{0} ⊢ t and t_{0} ⊢ t′ therefore since quasi-groups are models : [[t_{0}]] =_{F QG} [[t]] =_{F QG} [[t′]] ;

- if [[t]] =_{F QG} [[t′]] then we get Φ ([[t]]) ∼ Φ ([[t′]]) by prop 6 ; but we also have by remark 1 Φ ([[t]]) = t and Φ ([[t′]]) = t′, hence the result An alternate proof is to consider a quasi-group on classes for ∼ .

4 An application to unification for learning in NL

∥= -unification has been investigated in [For01] in the associative Lambek calculus. It strongly relies on the characterization of ∼ by free groups in [Pen93].

In this section, we proceed similarly for NL using the characterization of ∼ by free quasi-groups.

In Lambek calculus, from a learning point of view, we are interested in the following relation on types :

Definition 1 The relation ∥= on types is defined by

t_{1} ∥= t_{2} iff ∃σ : t_{1} ⊢ σ(t_{2})

where t_{1}, t_{2} are types and σ is a substitution.

We recall standard definitions on unification modulo a set of equations.

Unification in (modulo) an equational theory. For any set E of equations, let =_{E} denote the equivalence generated by E. We say that a set of terms A is unifiable modulo E (or E-unifiable) whenever there exists a substitution σ (then called E-unifier), such that for all terms t, t′ ∈ A : σ(t) =_{E} σ(t′). Unification has been studied for many equational theories, in particular in connection with rewriting. We recall that free groups (in the abelian case, and also in the non abelian case) admit a finite presentation by equations, that produces a canonical rewriting system; let G denote such a set of equations for non abelian groups.

We now adapt the standard definitions of unification to deal with deduction.

Definition 2 Two types A, B are said ∥= -unifiable whenever (i) there exists a type t and a substitution σ such that t ⊢ σ(A) and t ⊢ σ(B) ; σ is then said a ∥= -unifier of A and B and t is a ∥= -unificand of A and B. These definitions are extended to sets of types in the usual way.

Two remarks :

1. If σ is a (standard) unifier of types A and B (ie σ(A) = σ(B)) then σ also is a ∥= -unifier of A and B (taking σ(A) as left-hand side).

2. When A and B have no common variables, this definition (i) is equivalent to (ii) the existence of a type t such that both t ∥= A and t ∥= B.

The case without shared variable is precisely the interesting one for the unification step in a learning process such as the RG-algorithm in [Kan98].

The following property relates ∥= -unification in L to G-unification ( [For01]):

Proposition 7 (Characterizing ∥= -unifiablity and ∥= -unifiers in L) Let A and B be two types in Tp, L is such that :

1. A and B are ∥= -unifiable iff their images [[A]] and [[B]] are G-unifiable.

2. σ is a ∥= -unifier of types A and B iff its translation σ_{G} is a G-unifier of [[A]] and [[B]], (where σ_{G} is defined by : σ_{G} (p) = [[ σ (p)]] for p atomic) ; conversely any G-unifier of [[A]] and [[B]] is the translation of a ∥= -unifier of types A and B.

Note. A similar result holds for L_{∅}. We now formulate a similar result for NL, relying on quasi-groups instead of groups.

Proposition 8 (Characterizing ∥= -unifiablity and ∥= -unifiers in NL) Let A and B be two types in Tp, NL is such that :

1. A and B are ∥= -unifiable iff their images [[A]] and [[B]] are QG-unifiable.

2. σ is a ∥= -unifier of types A and B iff its translation σ_{QG} is a QG-unifier of [[A]] and [[B]], (where σ_{QG} is defined by : σ_{QG} (p) = [[ σ (p)]] for p atomic) ; conversely any QG-unifier of [[A]] and [[B]] is the translation of a ∥= -unifier of types A and B.

Proof. See Annex.

We may thus benefit from existing results for quasi-groups such as the existence of term rewriting systems and unification algorithms. Let us conclude with examples.

Example 2 Consider the lifting rule that holds in the non-associative NL. Suppose that after some type computation, we get the following grammars (where N denotes a constant, and x_{1}, … are variables) :

G_{1} = {c_{1} ↦ x_{1}, c_{2} ↦ x_{2}, c_{3} ↦ (x_{1} / N) \ x_{2}}

G_{2} = {c_{1} ↦ x_{3}, c_{2} ↦ x_{4}, c_{3} ↦ N}

G_{3} = {c_{1} ↦ x_{5}, c_{2} ↦ x_{6}, c_{3} ↦ x_{5} / (N \ x_{6})}

Standard unification fails to produce a rigid grammar since the types for c_{3} are not unifiable. However ∥= -unification succeeds in L and in NL since the types for c_{3} are ∥= -unifiable :

[[(x_{1} / N) \ x_{1}]] =_{F QG} [[N]] =_{F QG} [[x_{1} / (N \ x_{1})]]

Example 3 Consider the Geach rule that holds in the associative calculus but not in the non-associative NL :

[[A / B]] =_{F QG} [[A]] / [[B]]
[[(A / C) / (B / C)]] =_{F QG} ([[A]] / [[C]]) / ([[B]] / [[C]])

do not simplify in quasi-groups for atomic A, B, C. Whereas in a group interpretation they get reduced to the same formula [[A]].[[B]]^{−1}.

References

[Bon00] Roberto Bonato. A Study On Learnability for Rigid Lambek Grammars. Italian laurea degree master thesis and irisa research report, to appear, 2000.

[BP90] Wojciech Buszkowski and Gerald Penn. Categorial grammars determined from linguistic data by unification. Studia Logica, 49:431–454, [Bus97] W. Buszkowski. Mathematical linguistics and proof theory. In van

Benthem and ter Meulen [vBtM97], chapter 12, pages 683–736.

[Cas88] Claudia Casadio. Semantic categories and the development of categorial grammars. In R. Oehrle, E. Bach, and D. Wheeler, editors, Categorial Grammars and Natural Language Structures, pages 95–124. Reidel, Dordrecht, 1988.

[For01] Annie Foret. On mixing deduction and substitution in Lambek categorial grammars. LACL’01, Le Croisic, 2001.

[Gir95] Jean-Yves Girard. Linear logic: its syntax and semantics. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Notes, pages 1–42. Cambridge University Press, 1995.

[Gol67] E.M. Gold. Language identification in the limit. Information and control, 10:447–474, 1967.

[Hul80] J. M. Hullot. Compilation de formes canoniques dans des théories équationelles. PhD thesis, University de Paris–Sud, 1980.

[Kan98] Makoto Kanazawa. Learnable classes of categorial grammars. Studies in Logic, Language and Information. FoLLI & CSLI, 1998. distributed by Cambridge University Press.

[Lam58] Joachim Lambek. The mathematics of sentence structure. American mathematical monthly, 65:154–169, 1958.

[Lam61] Joachim Lambek. On the calculus of syntactic types. In Roman Jakobson, editor, Structure of language and its mathematical aspects, pages 166–178. American Mathematical Society, 1961.

[Moo97] Michael Moortgat. Categorial type logic. In van Benthem and ter Meulen [vBtM97], chapter 2, pages 93–177.

[Nic99] Jacques Nicolas. Grammatical inference as unification. Rapport de Recherche RR-3632, INRIA, 1999. http://www.inria.fr/RRRT/publications-eng.html.

[Pen93] M. Pentus. The conjoinability relation in Lambek calculus and linear logic. ILLC Prepublication Series ML–93–03, Institute for Logic, Language and Computation, University of Amsterdam, 1993.

[Ret00] Christian Retoré. Systèmes déductifs et traitement des langues:un panorama des grammaires catégorielles. Technical Report RR-3917 2000, INRIA, Rennes, France, 2000. A revised version to appear in Traitement automatique du langage naturel, TSI.

[vBtM97] J. van Benthem and A. ter Meulen, editors. Handbook of Logic and Language. North-Holland Elsevier, Amsterdam, 1997.

[Ver96] Koen Versmissen. Grammatical Composition: Modes, Models, Modalities. PhD thesis, Utrecht University, 1996.

ANNEX

Proof of proposition 5 by induction on derivations case (axiom) is obvious. case ( \right ) if (A, Γ) ⊢ B then Γ ⊢ A \ B

By induction [[A]].[[Γ]] =_{F QG} [[B]], using [[Γ]] =_{F QG} [[A]] \ ([[A]].[[Γ]]) this entails : [[Γ]] =_{F QG} [[A]] \ [[B]] = [[A \ B]] ;

case ( /right ) is treated similarly. case ( \left ) if Γ ⊢ A and Δ[B] ⊢ C then Δ[(Γ, A \ B)] ⊢ C

By induction Γ =_{F QG} A and [[Δ[B]]] =_{F QG} [[C]] which entails using [[A]].([[A]] \ [[B]]) =_{F QG} B : [[(Γ, A \ B)]] =_{F QG} [[A]].([[A]] \ [[B]]) =_{F QG} B then [[Δ[(Γ, A \ B)]]] =_{F QG} [[Δ[B]]] =_{F QG} [[C]]

case ( /left ) is similar. case (⊗-left) is obvious case (⊗-right) if Γ ⊢ A and Δ ⊢ B then (Γ, Δ) ⊢ (A ⊗ B)

By induction [[Γ]] =_{F QG} [[A]] and [[Δ]] =_{F QG} [[B]] which entails [[(Γ, Δ)]] =_{F QG} [[A]].[[B]] = [[A ⊗ B]]

Proof of proposition 6. Part 1 :

Φ (x.(x \ y)) ∼^{1} Φ (y)  from x ⊗ (x \ y) ⊢ y
Φ ((x / y).y) ∼^{1} Φ (x) similarly from (x / y) ⊗ y ⊢ x
Φ (x \ (x.y)) ∼^{1} Φ (y)  from y ⊢ x \ (x ⊗ y)
Φ ((x.y) / y) ∼^{1} Φ (x) similarly from x ⊢ (x ⊗ y) / y

Part 2. We proceed by induction on an equational deduction for a =_{F QG} b. Such a deduction either is an instance of an equation, an instance of the reflexivity rule or follows from the symmetry rule, from the transitivity rule, or from the compatibility rules. The case of an equation is dealt by part 1 of this proposition. The cases of reflexivity, symmetry and transitivity are obvious. The case of compatibility is obtained by the congruence property for ∼

Proof of proposition 8. We proceed in several steps.

• The assertion “A and B are ∥= -unifiable” is equivalent to “there exists C and σ such that both C ⊢ σ(A) and C ⊢ σ(B)”; from the conjoinability results, this is still equivalent to σ(A) ∼ σ(B) and also to [[σ(A)]] =_{F QG} [[σ(B)]] from the characterization of ∼ by quasi-groups.

• Let σ_{QG} denote the QG-substitution defined by σ_{QG} (p) = [[ σ (p)]] (for p atomic). We can easily show that σ_{QG} ([[t]]) =_{F QG} [[σ(t)]] for any type t. ^{11}

• Suppose that [[σ(A)]] =_{F QG} [[σ(B)]] , we also have σ_{QG} ([[A]]) =_{F QG} [[σ(A)]] and σ_{QG} ([[B]]) =_{F QG} [[σ(B)]], therefore σ_{QG} is a QG-unifier of [[A]] and [[B]]. Conversely, suppose that σ_{QG} is a QG-unifier, using the same arguments, we get [[σ(A)]] =_{F QG} [[σ(B)]]. Which provides the first assertion in part 2 of the proposition.

• Suppose that θ is any is QG-unifier of [[A]] and [[B]] we consider the substitution θ_{NL} defined by θ_{NL}(p) = Φ (θ(p)) (for p atomic) and show that it is a ∥= -unifier of A and B. We first get [[θ_{NL}(p)]] =_{def} [[ Φ (θ(p))]] =_{F QG} θ(p) (for p atomic), from previous remark 2 on Φ . We then get [[θ_{NL}(t)]] =_{F QG} θ([[t]]) for any t, by easy induction on t^{12}. This provides the second assertion in part 2 of the proposition, since θ([[A]]) =_{F QG} θ([[B]]) implies [[θ_{NL}(A)]] =_{F QG} [[θ_{NL}(B)]]

• Finally we get part 1 from the whole construction above

11case t atomic is clear from the definition of σ_{QG} since [[p]] = p ; case t = t_{1} \ t_{2} is σ_{QG} ([[t_{1} \ t_{2}]]) = σ_{QG} ([[t_{1}]] \ [[t_{2}]]) = σ_{QG} ([[t_{1}]]) \ σ_{QG} ([[t_{2}]]) =_{ind} [[ σ (t_{1})]] \ [[ σ (t_{2})]] = [[ σ (t_{1}) \ σ (t_{2})]] = [[σ(t)]] ; the other cases are similar.

This may also be viewed as two compositions of morphisms : σ_{QG} ∘ [[]] and [[]] ∘ σ , that are equal on atomic formulas.

12case t atomic is clear from the definition of θ_{NL} since [[p]] = p ; case t = t_{1} \ t_{2} is θ([[t_{1} \ t_{2}]]) = θ([[t_{1}]] \ [[t_{2}]]) = θ([[t_{1}]]) \ θ([[t_{2}]]) =_{ind} [[θ_{NL}(t_{1})]] \ [[θ_{NL}(t_{2})]] = [[θ_{NL}(t_{1}) \ θ_{NL}(t_{2})]] = [[θ_{NL}(t)]] ; the other cases are similar.