D IAGRAMMES

J. L AMBEK
On a connection between algebra, logic and linguistics
Diagrammes, tome 22 (1989), p. 59-75
<http://www.numdam.org/item?id=DIA_1989__22__59_0>

© Université Paris 7, UER math., 1989, tous droits réservés.
L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright.

Article numérisé dans le cadre du programme
Numérisation de documents anciens mathématiques
http://www.numdam.org/

DIAGRAMMES

VOLUME 22

,

1989

ACTES DES JOURNEES E . L . I . T .
( U N I V . P A R I S 7 , 2"7 JUIIM-2 J U I L L E T 1 9 8 8 )

ON A C O N N E C T I O N B E T W E E N ALGEBRA, LOGIC AND LINGUISTICS

J.

LAMBEK, MCGILL

UNIVERSITY

Une grammaire indépendante du contexte (avec flèches renversées) consiste en dérivations Ai . . . An —» A n + i ; on appelle les Ai types. O n peut considérer u n e telle grammaire comme u n calcul de séquences à la Gentzen, mais
sans ses trois règles structurelles: permutation, contraction et atténuation.
(Les trois règles sont permises dans la logique intuitioniste, les deux premières
dans la "logique pertinente", et la première dans la "logique linéaire" de Girard.)
L'idée d'une multicatégorie trouve son origine dans la méthode des applications bi-linéaires de Bourbaki. Formellement, une multicatégorie est
une grammaire indépendante du contexte avec une relation d'équivalence
appropriée entre dérivations (séquences). Elle peut être caractérisée pax son
langage interne. Si on postule des équations appropriées correspondantes aux
trois règles structurelles, on obtient une théorie algébrique (multisortale).
Une grammaire catégorielle est une grammaire indépendante d u contexte avec une opération binaire / ( = sur) entre types; la notation logique
est <= ( = si). Dans une multicatégorie, A/B est le Hom(B,A)
interne; dans
B
le cas spécial, A 4= B est l'exponentiation A .
Le langage interne d'une
multicatégorie avec / est une version unilatérale du À-calcul; avec les règles
structurelles de Gentzen, elle devient le ÀJFf-calcul usuel de Church. Pour
une grammaire catégorielle (de l'anglais, par exemple) le passage du premier
au second est essentiellement ce que fait la sémantique de Montague.

It is claimed that logic is to linguistics as universal algebra is t o multilinear algebra, the common thread being Gentzen's notion of "sequent",
which goes under différent names in the four fields: déduction, dérivation,
opération and multilinear form.
1.

Contextfree grammars as multicategories.

A contextfree dérivation has the form / : A\ . . . An —> A, where Ai and
A are syntactic types (also called "grammatical catégories"). T h e arrow hère

reçu

1«

11/09/1969

follows the convention in categorial grammar, in generative grammar t h e
arrow is reversed.
Among the dérivations there is the reflexive law

a n d a rule for constructing new dérivations from old:
/:A-»A
g<f>:

g:TAA->B
TAA -> B
'

called the eut rule, which represents substitution of / into g. Hère capital
Greek letters dénote strings of types, e.g. A = Ai . . . A n , n > 0. T h e notation
g < f > for the new dérivation is somewhat ambiguous, inasmuch as it does
not show where / has been substituted; but we shall use it just the same, as
the place of substitution will usually be clear from the context and because
a more précise notation would appear to be rather cumbersome.
Among the syntactic types will be s for "statement" and others to be
discussed in Section 6 below. It is sometimes convenient to include English
words among the types, think of them as one-element types. An analysis
would yield two distinct dérivations
expérience

teaches

spiders that time /lies

—* s,

interpreting the sentence to the left of the arrow in two différent ways. To
see this compare the passive sentences spiders that time flies are taught by
expérience and spiders are taught by expérience that time flies. On the other
hand, there seems to be no need for distinguishing the dérivations
John ( likes Jane)

—> s

(John

—> s,

and
likes) Jane

assuming t h a t b o t h dérivations are possible.
Anyway, equality of dérivations is something that should be considered.
If this is done, a contextfree grammar becomes what has been called a multicategory [L1969]. However, the rules of equality are a bit awkwaxd to s t a t e
directly, so I now [L1989] prefer to do this with the help of the internai language: we adjoin countably many variables of each type, say xt- is one such
variable of type A,-, then fxx . . . xn is to be regarded as a term of type A

60

whenever / : Ai . . . A n —• A is a dérivation. If also g : Ai . . . A n —> A, we
shall say that / = g provided we can prove fx\ . . . xn = gx\... x n from the
usual rules of equality, including the rule of substitution of tenus of a certain
type for variables of that type.
While we are hère mainly interested in applications to linguistics, it
should be pointed out that dérivations / : A —> A hâve appeared in multilinear algebra under a différent name: multilinear forms.
2.

The rôle of Gentzen's structural rules.

The reader will hâve noticed the similarity between dérivations in linguistics and déductions in logic, called "sequents" by Gentzen, who imposed
three structural rules on déductions in intuitionistic logic, which axe absent
in linguistics:
/ : TAABA -> C
f{ : TBAAA -+ C
f : TAAA -> C
/ c : TAA - C

interchange,
contraction,

/ : TA -> C

thinning.

P : TAA -> C

Again our notation f%,fc,ff
ignores the place where the interchange, contraction and thinning occurs. The capital letters now dénote "formulas";
recall the popular slogan: "formulas as types".
While logicians axe not usually interested in the question when two
déductions are equal, this is sometimes important. For example, one ought
to distinguish between the two déductions A A A —> A obtained by putting
J3 = A i n A A i ? — • A and A A B —> B respectively.
Going over to the internai language of a "Gentzen multicategory" [see
Szabo 1978], one may think of the variable x,- of type A,- as an assumption
that A, holds. If / : Ai . . . A n —> A is a déduction à la Gentzen, one may
think of / x i . . . x n as a proof of A from the assumptions x,(i = 1 , . . . , n) à la
Prawitz. Note that the saine formula may be assumed several times in one
proof.
Gentzen's structural rules may now be viewed as définitions of new déductions, when we write x, y, z,... for variables of types A, B, C , . . . respectively, and u = Ui . . . u m , v, w,... for strings of vaxiables of types T, A, A , . . .

61

respectively:
f*uywxv = fuxwyv,
fcuxv = fuxxv,
fluxv = fuv.
Actually, a Gentzen multicategory may be considered to be a manysorted algebraic theory, in which the formulas axe usually called sorts and
the déductions are called opérations.
To adopt a neutral terminology, let us use Gentzen's word sequent for
/ : Ai . . . A„ —• A. We may then summarize our observations by saying
that sequents appear in linguistics as dérivations, in linear algebra as forms,
in logic as déductions and in uni versai algebra as opérations. Curiously, in
linguistics, logic and algebra, people hâve considered variants in which some
of Gentzen's structural rules axe permitted while others axe forbidden.
In linguistics, the three structural rules should be absent from syntax,
at least the way I see it, but présent in semantics, as conceived by Curry
[1958] and Montague [1974]. However some linguists, notably van Benthem
[1983, 1988], hâve advocated that the interchange rule should be admitted
when one discusses languages with free word order. Steedman [1988] and
Szabolcsi [1989] seem to forbid thinning and to allow contraction.
In intuitionistic logic, ail three rules axe permitted, in "relevance logic"
only interchange and contraction and, in Girard's linear logic as originally
formulated [1987], only interchange. However, one can conceive of a nonsymmetric lineax logic in which ail structural rules axe forbidden [see Girard
1989].
In algebra, I am only aware of multilineax algebra, in which ail three
rules are forbidden, and universal algebra, in which ail three axe allowed.
I haven't corne across any other variants, unless one wishes to consider as
an algebraic theory Church's A-calculus [1941], which forbids thinning, as
opposed to his Àif-calculus, which allows it.
3.

Type forming opérations.

Let us now look at opération on types, formulas or sorts as studied in
linguistics, logic and algebra respectively.
We are primarily concerned with binaxy and nullary opérations, presented in their most common notation in algebra and linguistics, as opposed
to logic, where they axe called connectives and occur in a rival notation. In

62

this connection, one may also consider "quantifiers" with respect to variable
types.
algebra:
logic:

®

/
\
<= =»

x +
A V

/

1
T

0
±

Ux
Vx

\lx
3x

We shall henceforth refer to thèse type forming opérations as "connectives".
They axe usually introduced in terms of the set [V, A] of ail sequents / : T —»
A. To do full justice to the quantifiers, one must declaxe the free variables
and should write / : T-> A or / G [I\ A\x, where A' is a set of variables which
includes ail the variables occurring freely in Y and A. Such free variables are
of course subject to the usual law of substitution, to which I plan to return
on another occasion. In principle, ail connectives are introduced by means
of certain biunique correspondences, namely as follows:
[T(A®B)A,C]^[TABA,C],
[T,A/B]^[TB,A],
[T,B\A]^[BT,A],
[T,AxB]^[T,A]x[T,B],
[r(A + B)A, C] S [rAA, C] x [VBA, C],
[TIA,C)^[TA,C],

[r,i]-w,
[roA,c]^{*},
[T,l[A(X))^[T,A(X))x,
x
[r\jA(X)A,C]^[rA(X)A,C}x.
X

On the right side, x dénotes the caxtesian product of sets and {*} is a typical
one-element set.
If the reader is puzzled by the absence of / , ® and <= in the usual logical
Systems, linear logic excepted, this cornes from the fact that, in the présence
of Gentzen's three structural rules, 1 = 1, A®B = AxB and B\A = A/B.
[See L1989].
More precisely, the connectives axe introduced by specifying a particulax
sequent and providing additional information to ensure that it induces a
biunique correspondent as required:

63

(1) mAB:AB
-+A®B;
if / : TABA - • C then 3!/§ : T(A ® B)A - • C such that
/Sumxyu = fuxyv.
(2) e A B : (A/B)B -> A;
if / : TB -> A then 3!/* : T -» A/JB such that
/*euy = / « y .
(2') e'AB : B ( B \ A ) - A;
if f :BT -> A then 3 ! / + : T -> £ \ A such that
e'yf+u = fyu.
(3) PAB : A x B -+ A, qAB
:AxB-*B;
if / : T -> A and g : T -*• 5 then 3! < / , y >: T -* A x B such that
P(< / , £ > « ) = / « , q(< />0 > «) = 0U(4) kAB : A -> A + B, lAB : B -» A + B;
if / : TAA -H- C and s : TBA - • C then 3![/,y] : T(A + B)A -* C such
that
[/,y]ukxu = /uxu, [f,g]u £yv = ytxyu.
(5)i:
-I;
if / : TA -> C then 3 ! / # : VIA - • C such that
/*uiu = /uv.
(6) o r : r -+ 1,
3!flf : T - 1.
(7) DFA : TOA - C;
3!^ : TOA -> C.
(8) * x : I l x A ( X ) ^ A ( X ) ;
if V ( X ) : T$A(X) then 3!y>A : T - • Ux A(X) such that
*x<PAu =x <f{X)u.
(9) /ex : il(X) * U x A(X);
if y>(X) : rA(X)A * C then 3!v?v : T ]\x
¥? V U(KXZ)V = X <p(X)uzv.

64

A{X)A - • B such that

Note that, in principle, VCÏAB^AB etc should carry subscripts; but, in
practice, we hâve usually omitted them. We hâve also been négligent in failing to declaxe free variables other than variable types in the above équation.
This becomes more important when Gentzen's structural rules axe admitted.
It should be pointed out that, in ail cases considered, the existence and
uniqueness of the sequent with a certain property can be expressed by means
of équations which do not contain free variables, except variable types:
1) / § < m > = / , (g < m >)§ = g.

[2) e<r>=f,(e<g

>)* = g.

; 2 ') e' < / t > = / , (c' < g >)t = g.
[3) P < / , $ » = / , q < / , $ > = 0 , < p < ^ > , q < A > = h.
;4) [/,y] < k > = / , [f,g] < i>= g,[h<k>,h<
£>} = h.
;5)/#<i>=/,
(g<i>)*=g.
6) o r = g.
8) 7TX < ¥>A > = x <p{X\ (TTX < g >) A = g.
;9) c^v < /c x > = x <p(X), (g < KX > ) v = g.
As regards (2), the notation for e^jsty in [LS 1986] was t'y (read t of y)
and the usual notation for f*u is Xy^sfuy. The two équations in (2) then
t a i e the more familiar form:
^yeBfuy

c

y = u , y fuy, \yeB(gu

c

y) = u grz,

where, for once, we hâve declaxed the variables. Moreover, in the first of
thèse équations, we may substitute any term b of type B for y. In paxticulax,
if b contains no free variables other than such as appeax in the string u, we
obtain:
KtBfuy 'b=u fub.
A similax, but distinct, notation could be adopted for (2'). But is it worth
the trouble to introduce an analogous notation for (1)?
As regards (6) and (7), I am not entirely happy with the way they hâve
been stated.
4.

Freelv gênerated categorial grammars.

Let us concentrate on the applications to linguistics and multilineax algebra, so we can forget about Gentzen's structural rules. The question now

65

arises: given a contextfree grammar Q ( t h a t is, a multicategory), w h a t h a p pens when we freely adjoin some or ail of the connectives ®, / , \ , x , . . . ? More
precisely, we wish to construct the left adjoint F to the forgetful functor U
from contextfree grammaxs with connectives to contextfree grammaxs witho u t . Thus F{Ç) is the contextfree g r a m m a r with (g),/, etc. freely generated
by Q. We hope t h a t the multifunctor G -» UF(Ç) will t u r n out to be full
a n d faithful.
T h e main problem we face is to calculate the set [T, A] of ail sequents
r —> A in UF(G). T h e problem splits into two parts:
(I) Find ail sequents / : T -> A.
(II) Given sequents / , g : T -> A, décide when / = g.
T h e solution to Problem I will show that Q -> UF(Q) is full, while the
solution to P r o b l e m II, sometimes called the "cohérence problem", should
imply t h a t it is faithful.
I hâve looked at Problem I repeatedly, using Gentzen's m e t h o d of eut
élimination, first ignoring équations between sequents [L1958] a n d later
bringing t h e m in [L1969]. I intend to look at it once more, exploiting the
internai language to get a better insight into what is going on. W h a t this
means, essentially, is that one replaces Gentzen style déductions by Prawitz
style proofs.
My attacks on Problem II [L1968, 1969] contained what I still believe
were some good ideas, but also contained some mistakes. More successful
attacks, sometimes for related Systems, were carried out by m a n y people; in
particulax Mine [1977] and Szabo [1978] made use of normalization and the
Church-Rosser property, which I believe to be the n a t u r a l method. To this
also I hope to r e t u r n on another occasion.
Hère we shall merely illustrate how Problem I is to be solved, by confining attention to one connective only, and also give a hint for attacking
Problem IL Suppose we hâve a sequent 0 —> C in UF(G) containing at most
t h e connective / , it must be of one of the following forms:
(i) it is already a sequent in G]
(ii) it is of the form 1^ : A —> A;
(iii) it is obtained by a eut:
/:A->A
g< f>:

££

g:TAA->C
TAA -> C

(iv) it is of the form (2a):
eAB : (A/B)B

- A;

(v) it is of the form (2b):
/ : eB -» A
/*:0^A/B'
Given 0 and C, it is easy to find ail sequents 0 —• C (if any) of the
form (i), (ii) and (iv). If C = A / B , we may reduce the problem of finding
ail sequents 0 —• C of the form (v) to that of finding ail sequents QB —• A.
The difficulty is with the eut (iii): suppose we hâve decomposed 0 as TAA,
how do we know which A to try? The way out, following an idea of Gentzen,
is to replace (iv) (that is (2b)) by the following more powerful rule:
(iv')

/ : A -> B
g: TAA
g[f] : T(A/B)AA -> C

'

where g[f] = g < e < / > > is given by
g[f]utwv =

guetfwv,

t being a variable of type A/B. While (iv') was constructed with the help of
a eut, it is a haxmless rule, inasmuch as the premises contain nothing which
does not already occur in the conclusion.
One byproduct of replacing (iv) by (iv') is that we may dispense with
(ii). For, unless (ii) is already an arrow in Ç/, hence a spécial case of (i), it is
of the form IA/B : A/B —» A/B, in which case it may easily be proved, with
the help of the internai language, that
IA/B=(U[1B]Y-

Thus IA/B c a n be constructed without using (ii), provided 1,4 and 1# can
be so constructed, which we may assume by an appropriate inductional assumption.
More importantly, if we use (iv') in place of (iv), any sequent constructed
with eut is equal to one without eut. This is Gentzen's eut élimination
theorem in the absence of structural rules, although Gentzen himself did not
bother about "equality".

67

Limitations of space do not permit me to include the proof of the eut
élimination theorem hère. On the face of it, the démonstration that a sequent
constructed with eut equals one constructed without makes use of both équations e < / * > = / and (e < g >)* = g. When translated into A-notation
however, it appeaxs that, while Axç^(/?(x) cx = (f(x) is used, the équation
A X G A ( / C Z) = / is not used in full generality, but only a conséquence of it,
namely the implication:
if tp(x) = x ip(x) then AxGA(p(x) =

\XGAHX)'

Anyway, both the proof of eut élimination and the proof that IA/B =
make use of the following technique, which seems to be useful
for attacking Problem II: to compaxe two axrows f,g : T —> A/B, compare
the expressions efuy and eguy in the internai language. Détails of thèse
arguments will be found in the proceedings of the fortheoming conférence
"Kleene '90" in Bulgaria.
( 1 A [1B])*

5.

Some linguistic applications.

Although I now believe that production grammaxs axe better suited to
natural languages then categorial ones, I am willing to ask the question: of
what possible significance axe the connectives ® , / , \ , x etc. in linguistics?
While we only discussed one of the connectives in some détail hère, it appeaxs
that they may be freely added to a contextfree grammar without loss in
generality. More precisely, when we look at the contextfree grammar G and
the enhanced grammar UF{G) as multicategories, the multifunctor G —*
UF(G) is a full embedding. In particulax, it is a conservative extension.
For the purpose of illustration, let G be the contextfree component of the
small fragment of English grammar discussed in "Grammar as mathematics"
[L1989b]. In this contextfree grammar one may, for example, generate the
pseudo-sentence
(t)

John may hâve Perf be Paxt corne often.

Hère Perf ( = perfect paxticiple of) and Paxt ( = présent participle of) axe
certain grammatical terms, which I hâve called "inflectors". Of course Perf
be should be converted to been and Paxt co7ne to coming, but the rules
permitting this are not contextfree.

68

One can of course handle strings like (f) in a categorial grammar. Let us
introduce the following types, except for subscripts the same as in [L1959]:
Si = statement in présent tense,
n 3 = name ( = third person noun phrase),
i =

infinitive,

p = présent paxticiple,
q = past participle.
If the différent words in (j) axe assigned types as follows, (f) is easily calculated to be of type Sj :
John
n3

may
(n3\si)/i

hâve
i/q

Perf
q/i

be
i/p

Part
p/i

corne
i

often
i\i

To convert (f) into an actual sentence, the production grammar of
[L1989b] requires two non-contextfree rules. As it is customaxy to reverse
axrows in categorial grammaxs, thèse two rules will take the forbidden form:
coming

—* Paxt corne,

been —• Perf be.

But ail is not lost. Let us incorporate the tensor product ® to mimic juxtaposition, then thèse rules take the permitted form:
coming

—» P a r t ® corne,

been —> P e r f ® 6e.

We may infer t h a t coming has type ( p / i ) ® i —» p and 6een has type ( q / i ) ®
( i / p ) —> q / p . We need the more complex types to the left of the axrows, for
example, to check t h a t
coming
often
(p/i) ® i
i\i
has type p , as is shown in the following Gentzen-style argument:

(P/J)i

(p/i)i(i\i) -» p
((p/i)®i)(i\i)-p-

fi«ï

In a similax manner we find that has and is hâve types
( ( n 3 \ s i ) / i ) 0 (i/q) -> ( n 3 \ s i ) / q
and
( ( n 3 \ S l ) / i ) ® (i/p) -

(n3\Sl)/p

respectively, but being does not hâve type
(p/i) ® (i/p) -

p/p,

plausible as this might be, since the following is not an English sentence:
* John is being coming.
The connectives ®, / and \ hâve been used before; in fact, the above
account closely follows [L1959], With a bit of imagination, it is not difficult
to find linguistic applications for some of the other connectives. For example,
if
ni = first person noun phrase,
112 = plural noun phrase,
then hâve in they hâve corne will hâve the following type:
((nAsO/i) ® (i/q) -+ ( n i \ s ) / q
and the same with ni replaced by 112. Ignoring the more elaborate type on
the left of the arrow, for the purpose of illustration only, we may infer that
hâve has type
(i/q) x ( ( n i \ s i ) / q ) x ((n 2 \si)/q),
which is isomorphic to

(i/q) x (((m + n2)\s)/q).
Similaxly, a modal verb such as may has type n\(s 1 /i), where n = ni + n 2 +
n 3 . However, we must distinguish between hâve of type ((ni + n 2 ) \ s i ) / q
and has of type ( n 3 \ s i ) / q .
A case can also be made for assigning to the word only the polymorphic
type f][ x (X/X), where X is a variable type, although some provision has to

70

be m a d e to ensure that only modifies only expressions which axe stressecL We
may also try to ascribe to the word and the polymorphic type n A -(-X"\JC)/JÏ";
b u t there is a difficulty with this: when and is placed between any two noun
phrases, whether of type n i , n 2 or n 3 , the resulting expression always has
type n 2 .
There seems to be no doubt that contextfree g r a m m a r s can be meaningfully enhanced by introducing opérations on types such as / , \ , ®, x
and + , and perhaps also Ylx a n < ^ others. More controversial is the claim
implicit in many articles on categorial grammar, including eaxly papers of
the présent author, t h a t the entire grammar of English can be squeezed into
the dictionary by assigning appropriate types to the words of the language.
In view of the décision procédure provided by eut élimination, this would
imply that the set of English sentences is not only recursively enumerable,
which almost no one dénies, b u t even recursive.
6.

Postscript.

At a récent workshop and conférence on categorial g r a m m a r , the author
was surprised by the number of people seriously engaged in research in this
axea. In a paxallel course of lectures by Moortgat and Oehrle, the above
décision procédure was discussed in great détail. Following van Benthem
[1983, 1988], they associated A-expressions to dérivations, particularly in
connection with eut élimination, although appaxently their A-calculus was
t h e usual one and neither the lineax variant discussed hère nor the variant
permitting interchange by van Benthem.
Not ail the speakers at the conférence, however, were aware of the existence of a décision procédure. Thus, one speaker proposed the rule

(X/(Y/Z))

(Y/W)

->

X/(W/Z)

on empirical grounds, although it is in fact provable. Another speaker proposed the rule

((Z/Y)/X)

(Y/X)

->

Z/X,

which is not provable, in fact, not valid syntactically, although it holds of
course in the semantic calculus one obtains when Gentzen's structural rules
are admitted.
Several people suggested applications for some of the not so traditional
connectives. Thus Oehrle had an interesting use for x , allowing one to account for a phonological component in addition to the syntactic one. Morrill

71

[1989] also proposed uses for + and even Girard's [1987] "why not". Actually,
Giraxd's linear logic also allows a négation and consequently the De Morgan
duals of ® and "why not", b u t thèse seem to hâve no obvious applications
in linguistics.
T h e r e is however another kind of duality, in view of the fact t h a t the
dual of a production grammar is also a production g r a m m a r . Thus one might
consider the connectives corresponding to "over" a n d "under" in t h e dual
g r a m m a r . They could be viewed as two kinds of subtraction, say "less" and
"from", even though the connective corresponding to ® is still ®. As fax as I
know, no one has explored applications of thèse last mentioned connectives.

Corrections added in proof.
To Section 1, penultimate paxagraph, add:
More generally, if ai is any terni of type A,-, / a i . . . an is a term of type A,-.
We stipulate t h a t l ^ x = x and that g < f > u i . . . umwx ... wnvi ... Vk =
gui . . . umfw1 . . . wnv1
...vk.
In Section 3, (2), replace / * e by e / * .
To Section 4, add: Alternatively, we could hâve constructed
1.4/B =

e

AB-

To Section 5, last paragraph, add:
T h e above claim amounts to saying t h a t the g r a m m a r of English has the
form F{G), where G has only sequents of the form 1^.

REFERENCES
Bourbaki, N.: Algèbre multilinéaire, Hermann, Paris, 1948.
Buszkowski, W., W. Marciszewski and J. van Benthem (eds.): Categorial Grammar, John Benjamins Publ. Co., Amsterdam, 1988.
Church, A.: The calculi of lambda-conversion, Annals of Mathematics
Studies 6, Princeton University Press, Princeton, N.J., 1941.
Curry, H.B. and R. Feys: Combinatory Logic I, North Holland, Amsterdam, 1958.
Curry, H.B.: Some logical aspects of grammatical structure, Proc. Symposia Appl. Math. 12 (1961), 56-68.
Girard, J.Y.: Linear logic, Theoretical Computer Science 50 (1987),
1-102.
Girard, J.Y.: Towaxds a geometry of interaction, Contemporary Math.
92 (1989), 69-108.
Kleene, S.C.: Introduction to metamathematics, Van Nostrand, New
York and
Toronto, 1952.
Laxnbek, J.: The mathematics of sentence structure, Amer.
Monthly 65 (1958), 154-69.

Math.

Lambek, J.: Contributions to a mathematical analysis of the English
verb-phrase, J. Can. Linguistic Assoc. 5 (1959), 83- 89.
Lambek, J.: On the calculus of syntactic types, Amer. Math. Soc.
Proc. Symposia Appl. Math. 12 (1961), 166-78.
Lambek, J.: Deductive Systems and catégories I, J. Math.
Theory 2 (1968), 278-318.

Systems

Lambek, J.: Deductive Systems and catégories II, Springer LNM 86
(1969), 76-122.

73

Lambek, J.: Categorial and categorical grammaxs, in: Oehrle et al.
1988, 297-317.
Lambek, J.: Multicategories revisited, Contemporaxy Math. 92 (1989),
217-239.
Lambek, J.: Grammar as mathematics, Canad. Math. Bull. 31 (1989),
1-17.
Lambek, J. and P.J. Scott: Introduction to higher order categorical
logic, Cambridge studies in advanced mathematics 7 (1986).
Mine, G.E.: Closed catégories and the theory of proofs, translated from
Zapiski Nauchnych Seminarov Leningradskogo Otdeleniya Mat. Instit u a im. V.A. Stuklova AN SSSR 68 (1977), 83-144.
Montague, R.: Formai philosophy, selected papers of Richard Montague,
edited by R.H. Thomason, Yale University Press, New Haven, 1974.
Moortgat, M.: Categorial investigations, Foris Publications, Dordrecht,
1988.
Morrill, G.: Grammar as logic, Research Paper EU CCS/RP- 34 (1989),
Centre for Cognitive Science, University of Edinburgh.
Oehrle, R.T., E. Bach and D. Wheeler (editors): Categorial grammaxs
and natural language structures, Reidel, Dordrecht, 1988.
Steedman, M.: Combinators and grammaxs, in: Oehrle et al. 1988,
417-442.
Szabo, M.E. (éd.): The collected papers of Gerhard Gentzen, Studies in
Logic and the Foundations of Mathematics, North Holland, Amsterdam,
1969.
Szabo, M.E.: A categorical équivalence of proofs, Notre Dame J. Formai
Logic 15 (1974), 177-91.
Szabo, M.E.: Algebra of Proofs, Studies in Logic and the Foundations
of Mathematics 88, North Holland, Amsterdam, 1978.

74

Szabolcsi, A.: Combinatory grammar and projection from the lexicon,
Preprint 1989.
van Benthem, J.: The semantics of vaxiety in categorial grammar, Simon
Fraser University, Report 83-26 (1983), reprinted in: Buszkowski et al.
1988, 37-55.
van Benthem, J.: The Lambek calculus, in: Oehrle et al. 1988, 35-88.

Mathematics Department
McGill University
Montréal, Québec H3A 2K6.