[Prev][Next][Index][Thread]
braids in linear logic
Date: Thu, 7 May 92 12:10:40 EDT
To: linear@cs.stanford.edu
BRAIDS IN LINEAR LOGIC- Rick Blute
----------------------
The purpose of this note is to suggest a possible method of
introducing braided structures into linear logic. This is done by
extending the usual linear inference rules with a set of
``twisted'' inference rules, which can be thought of as a weakening of
the exchange rule. Also discussed are the appropriate categorical
structures, braided monoidal categories. Finally, recent work on
crossed G-sets and representations of hopf algebras and quantum groups
are discussed in terms of possible semantics.
There has been a great deal of work recently on monoidal categories
where morphisms are classified by braids. In other words, morphisms in
the theory are assigned braids, and then two morphisms will be equal
if and only if they have the same braid, see [JS1], [FY1], and [FY2]. The
monoidal structure of braids has also been studied in [Y1].
These results are examples of coherence theorems, and results of
this sort originated with the work of Lambek, and Kelly-Mac Lane, see
[L] and [KM]. In [KM], the notion of Kelly-Mac Lane graph, is
introduced. These are pairings of the variables which classify
morphisms in symmetric monoidal closed categories in the same way as above.
In my thesis, [B], a connection between Kelly-Mac Lane graphs
and proof nets was established. In [B], morphisms were represented
by nets, the cut free net giving each morphism a unique normal form.
Then, the traditional Kelly-Mac Lane graph can be read off as the
axiom links of the cut-free net.
By defining a notion of braided linear logic, it seems that a
similar approach to braided monoidal categories could be established.
Braided Linear Logic, (bLL), can be thought of as an intermediate logic
between the usual commutative logic, and the fully noncommutative
logic. (Vaughan Pratt referred to it as weakly commutative in a recent note
on the network.) There will be no exchange rule, but the inference
rules will be extended with certain ``twisted'' inference rules. For
example, the rules for the tensor fragment are:
\Gamma,A,B, \Delta \vdash C \Gamma \vdash A \Delta \vdash B
--------------------------- ------------------------------------
\Gamma, A\otimesB, \Delta \vdash C \Gamma, \Delta \vdash A\otimesB
\Gamma,A,B, \Delta \vdash C \Gamma \vdash A \Delta \vdash B
--------------------------- ------------------------------------
\Gamma, B\otimesA, \Delta \vdash C \Gamma, \Delta \vdash B\otimesA
NOTE- \otimes is tensor. \vdash is entailment.
These last two rules are the left and right twisted tensor rules.
Analogous rules can be formulated for full multiplicative LL. There
are also other possible choices for inference rules which yield
analogous structure.
It should be noted that one can prove all of the same sequents as
in the commutative case, but that the equivalence relation on sequents
has changed. One only requires that the left twisted rule is inverse
to the right twisted rule. This is weaker than having a full exchange rule.
A proof net for the tensor fragment above will just be a braid
on the variables appearing in the derived sequent. (Assume that
there is exactly one formula on the left hand side of the sequent.)
Model the left tensor rule by crossing the A-strand over the B-strand,
and conversely for the right tensor rule. Cut formulas will appear
as nodes lying on the strands of the braids. Cut elimination
then corresponds to erasing such nodes and then reducing
by the Reidemeister moves, see [K] for these.
It is an interesting consequence of this approach that the
Reidemeister moves correspond to cut-elimination. This seems to work
because the moves satisfy the same sort of local reduction properties
as the usual cut-elimination procedure in nets.
Proof nets for full multiplicative LL can be obtained by adding two
new twisted links to the usual Danos-Regnier nets. One should have a
left overcrossing. The other should have a left undercrossing. The
correctness criterion is as usual. The cut-elimination procedure is
also the usual one, except that eliminating one of the twisted links
will leave a twisting in the remaining structure. One way to do
this is to push all of the twisting up into the axiom links.
This leads to an interesting property of braided logic. It will not
satisfy cut-elimination in the categorical sense. Not every deduction
is equivalent to a cut-free deduction, under the equations of the
theory. This is because of the different nature of the structural
rules.
Categorically, one can iterate the symmetry any number of times, and one
will always have either the symmetry or the identity. However, if
one iterates the braiding, then the result is a morphism which clearly
cannot be constructed in a cut-free way. In terms of nets, this
corresponds to the fact that there is a residual twisting remaining
after the cut links are eliminated.
The appropriate categorical structures are the braided monoidal
categories of Joyal and Street, see [JS1]. These are monoidal
categories equipped with a canonical isomorphism,
s: A\otimesB ---> B\otimesA
which satisfies the usual bilinearity conditions of a symmetry, but not
the equation ss=identity. Joyal and Street prove that the free braided
monoidal category is the category of braids. Objects are natural
numbers, morphisms are braids on natural numbers. The tensor product
is given by adjoining braids in the evident way.
So braids are the appropriate notion of Kelly-Mac Lane graph for
this theory. Similar results have been obtained by Freyd and Yetter
for braided closed categories, see [FY1], [FY2].
Thus, examples of braided monoidal categories give semantics for our
theories mentioned above. The Freyd-Yetter example of crossed G-Sets
gives a sound and complete semantics of the tensor fragment outlined
above.
Let G be a group. A crossed G-Set is a set, X, together with a left
G-action, and a map | |:X ---> G, satisfying:
|gx|=g|x|g^{-1}
for all g in G, x in X. g^{-1} denotes the inverse of g.
Tensor is given by set-theoretic product. (Note this is not a product
in this category.)
The braiding is given by:
s(x,y)=(|x|y,x)
Theorem: Let (Z,+) denote the integers. Crossed Z-sets provide a sound
and complete semantics for braided tensor logic. This is complete in
the sense that if A does not entail B in the logic, there is a model
such that HOM(A,B) is empty. Also, if F and G are two unequal
deductions that C entails D, then there is a model in which they are unequal.
So this is completeness on proofs, not just provability.
Crossed G-sets are not in general closed. A possible semantics for
full bLL is given by looking at the representation theory of hopf algebras
and quantum groups. It has been observed in several places that, given
a bialgebra in the category of vector spaces, then its category of
modules or comodules forms a monoidal category. To induce a braiding,
one looks for a solution to the quasitriangular equations. Variants can
be found in [JS2], [M2], and [Ma2]. These are closely related to the
Yang-Baxter equations of quantum physics. [JS2] and [Ma1] provide an
excellent overview of the subject. Such a solution induces
a braiding in a natural way. A noncommutative Hopf-algebra with such
a solution is what may be called a quantum group. (Although the
definition of quantum group does vary.) A partial semantic result is
that of Joyal and Street:
Theorem(Joyal-Street): Given a quantum group, with a bijective
antipode, the category of finite dimensional comodules is braided monoidal
closed, and has negation given by the usual duality for vector spaces.
Freyd and Yetter refer to this as a pivotal category. Joyal and
Street call them autonomous. (But this conflicts with other uses of
the term.)
NOTE-The bijective antipode is a natural restriction for linear logic,
since it can be thought of as a negation. To study the intuitionistic
case, one might wish to drop this.
So, these are models, but they will always have tensor isomorphic to
par. Possible solutions to this are being explored. One possibility
would be to allow infinite dimensional modules, and recover duality by
inducing a topology on the underlying spaces, and then restricting to
linear continuous maps. This idea has been studied by Barr in [Ba]. It
is also mentioned in [M1].
The representations of quantum groups are being explored extensively,
see for example [Y2], [M1], [M2], [JS2], [Ma1], [Ma2]. For example, S. Majid
gives a construction on finite dimensional Hopf algebras, the quantum
dual, which yields a quantum group. It would be interesting to have a
logical viewpoint of these constructions.
I hope to have more to report on the semantics of bLL via quantum
groups in the future. Also, I will try to have a TeX file exhibiting
some of the constructions described above.
Rick Blute
REFERENCES:
[Ba] M. Barr, Duality for Vector Spaces, Cahiers de Top. et Geom.
Diff., Vol 17, 1976
[B] R. Blute, Linear Logic, Coherence and Dinaturality, to appear in
Theoretical Computer Science, 1992
[FY1] P. Freyd, D. Yetter, Braided Compact Closed Categories with
Applications to Low-Dimensional Topology, Advances in Mathematics 77,
p156-182 (1989)
[FY2] P. Freyd, D. Yetter, Coherence Theorems via Knot Theory, to
appear in Journal of Pure and Applied Algebra (1992)
[JS1] A. Joyal, R. Street, Braided Tensor Categories, to appear in
Advances in Mathematics, (1992)
[JS2] A. Joyal, R. Street, An Introduction to Tannaka Duality and
Quantum Groups, Springer Lecture Notes in Mathematics 1488 (1991)
[KM] G.M. Kelly, S. Mac Lane, Coherence in Closed Categories, 1,
p. 97-146, (1971)
[K] L. Kaufmann, On Knots, Princeton University Press, 1987
[L] J. Lambek, Deductive Systems and Categories II, Springer Lecture
Notes in Mathematics 87, 1969
[Ma1] S. Majid, Physics for Algebraists: Noncommutative and
Noncocommutative Hopf Algebras by a bicrossproduct construction, J. of
Alg. 130, p. 17-64 (1990)
[Ma2] S. Majid, Braided Groups and Duals of Monoidal Categories, to
appear in Category Theory '91
[M1] Y. Manin, Quantum Groups and Noncommutative Geometry, CRM,
Universite' de Montreal 1988
[M2] Y. Manin, Topics in Noncommutative Geometry, Princeton University
Press, 1991
[Y1] D. Yetter, Markov Algebras, in Braids, Contemporary Mathematics
Volume 78
[Y2] D. Yetter, Quantum Groups and Representations of Monoidal
Categories, Math. Proc. Camb. Phil. Soc. 108, p. 261-290 1990