Nets as Tensor Theories

This report is intended to describe and motivate a relationship between a class of nets and the fragment of linear logic built from the tensor connective. In this fragment of linear logic a net may be represented as a theory and a computation on a net as a proof. A rigorous translation is described and a soundness and completeness theorem is stated. The translation suggests connecticns between concepts from concurrency such as causal dependency and concepts from proof theory such as cut elimination. The main result of this report is a "cut reduction" theorem which establishes that any proof of a sequent can be transformed into another proof of the same sequent with the property that all cuts are "essential". A net-theoretic reading of this result tells that unnecessary dependencies from a computation can be eliminated resulting in a maximally concurrent computation. We note that it is possible to interpret proofs as arrows in the strictly symmetric strict monoidal category freely generated by a net and establish soundness of our proof reduction rules under this interpretation. Finally, we discuss how other linear connectives may be related to the concepts of internal and external choice.