In this paper certain proof-theoretic techniques of [BCST] are applied to non-symmetric linearly distributive categories, corresponding to non-commutative negation-free multiplicative linear logic (mLL). First, the correctness criterion for the two-sided proof nets developed in [BCST] is adjusted to work in the non-commutative setting. Second, these proof nets are used to represent morphisms in a (non-symmetric) linearly distributive category; a notion of proof-net equivalence is developed which permits a considerable sharpening of the previous coherence results concerning these categories, including a decision procedure for the equality of maps when there is a certain restriction on the units. In particular a decision procedure is obtained for the equivalence of proofs in non-commutative negation-free mLL without non-logical axioms.
Theory and Applications of Categories, Vol. 6, 1999, No. 9, pp 105-146 http://www.tac.mta.ca/tac/volumes/6/n9/n9.dvi http://www.tac.mta.ca/tac/volumes/6/n9/n9.ps ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.dvi ftp://ftp.tac.mta.ca/pub/tac/html/volumes/6/n9/n9.psTAC Home