Bilinear logic in algebra, and linguistics
Jim Lambek · Cambridge University Press eBooks · 1995
The syntactic calculus , a fragment of noncommutative linear logic, was introduced in 1958 because of its hoped for linguistic application. Working with a Gentzen style presentation, one was led to the problem of finding all derivations f : A 1 … A n → B in the free syntactic calculus generated by a context free grammar g (with arrows reversed) and to the problem of determining all equations f = g between two such derivations. The first problem was solved by showing that f is equal to a derivation in normal form , whose construction involves no identity arrows and no cuts (except those in g ) and the second problem is solved by reducing both f and g to normal form. The original motivation for the syntactic calculus came from multilinear algebra and a categorical semantics was given by the calculus of bimodules. Bimodules R F S may be viewed as additive functors R → Mod S , where R and S are rings (of several objects). It is now clear that Lawvere's generalized bimodules will also provide a semantics for what may be called labeled bilinear logic . Introduction. I was asked to talk about one precursor of linear logic that I happened to be involved in, even though it anticipated only a small fraction of what goes on in the linear logic enterprise. I would now call this system “bilinear logic”, meaning “non-commutative linear logic” or “logic without Gentzen's three structural rules”.