In the context of mathematical logic (specifically proof theory, I suppose), what exactly is the definition of a tensor? For example, in the \pi-calculus, \mid is described as being a tensor, and in linear logic there’s also a tensor connective (\otimes).
Are these two related, in any way? All Google searches on tensor brings up the algebraic variety.
You might want to take a look at this paper and its citations. Googling for “proof theory” tensor turns up promising looking results.
A better explanation of the deep relationship is “Physics, topology, logic and computation: a Rosetta Stone” by John Baez and Mike Stay. Category theory FTW.
Yes, I had a nightmarish vision that this question would have something to do with Category Theory. Thanks for the help.
It’s prejudice against categories like that “nightmarish” comment that keeps me from getting a job, thankyouverymuch…
Really, it’s hard to get a job as a category theorist (harder than getting a job as an academic mathematician, anyway)? It seems like “everything” in computer science, at least, is being reinterpreted with a category-theoretic slant.
The mathematical end of computer science is dominated by algebra. Mathematics departments have a lot of analysts, and analytical techniques in geometry and topology. Even algebraic geometry is of two minds about the subject, and analysts look at category theorists like we’re about to say “where de calculus wimmin at?”
As opposed to the practical end, which seems to be dominated by Java programmers tearing their hair out over massively, massively multithreaded processes with no end in sight. They’ve got bigint problems but a group ain’t one. (If you’re having group problems, I feel bad for you, son.)
Anyway, it could always be worse. You could be writing RPG.
The name “tensor” comes from linear algebra; however, the generalized use with which we are concerned here has to do with monoidal categories (i.e., [weak] 2-categories with a single 0-cell). But, forget the category theory for a moment if you’d like; we’ll boil it down to something simple.:
A tensor is a connective (which I’ll denote “(x)”) with three properties: it (essentially) has an identity, it’s (essentially) associative, and it’s functorial. What this means is that, with every two objects A and B, we associate some tensor product object A (x) B; we also have some designated “identity object” I [from those two, we can of course construct n-ary tensor products in a natural way]. Furthermore, with every map f : A -> A’ and a map g : B -> B’, we associate a corresponding map f (x) g : A (x) A’ -> B (x) B’. Finally, we have canonical isomorphisms which make A, I (x) A, and A (x) I all isomorphic, as well as making A (x) (B (x) C) and (A (x) B) (x) C isomorphic. These all have to satisfy some coherence conditions which are pretty natural [e.g., whenever you have a large tensor product of many things and want to “re-parenthesize” in a certain way, it doesn’t matter what order you carry out associations in], but there’s no need to bother you with the details right now.
As you note, in linear logic, where the objects are propositions and the maps are proofs, the tensor product of most noteworthiness is multiplicative conjunction (actually, many logical connectives in logics more generally are tensors in this sense, but this is the one that actually gets called “tensor” the most, there being few better names for it)…
Bleh, cut out of the edit window without even the full ellipsis. 
Anyway, in the π calculus, as your other example, we would take the objects to be processes, and the maps to be reductions (including structural congruences). Given a reduction from P to P’ and from Q to Q’, there is a corresponding reduction from P | Q to P’ | Q’; furthermore, | is associative up to structural congruence, and 0 is its identity (in the sense that P | 0 and 0 | P are congruent to P). Thus, we see that | is a tensor product (well, technically, we have to check the coherence conditions I haven’t outlined, but they’re all pretty straightforward).
The eponymous example of a tensor product, incidentally, as I hinted above, is in the category whose objects are vector spaces and maps are linear transformations; in this case, the tensor product of V and W is a new space whose dimension is the product of those of V and W. Abstractly, it is characterized by the property that linear maps from V (x) W to Z correspond to bilinear maps from V and W to Z.
But you needn’t worry about that to understand the cases you care about; just remember, “tensor” basically means “associative, with an identity, and functorial”.
Yeah, that’s on like page 2 of the Baez/Stay paper.
Eh, page 12 so far as I can see, but it’s still a good paper to read. 
It occurs to me that perhaps a more familiar word for describing the property I used “functorial” for above, for one comfortable with type systems but not as accustomed to category theory, would be “covariant”. A tensor product is essentially a covariant, associative operator with an identity. [Thus, in typical programming languages, taking types as objects and terms with free variables (equivalently, definable functions) as maps between them, the tuple and tagged union type constructors are tensor products, although there are also better/more specific categorical names for them (“product” and “sum”/“coproduct”, of course). In a “resource-aware” type system, you could imagine a more typical tensor product, which acted like Cartesian product/tuple except in that resources could not be duplicated; this would just, of course, be the Curry-Howardification of affine logic, with a further stipulation that resources could not be dropped, either, moving the correspondence to linear logic. You could even have the “resource-awareness” be “order-aware” as well, with tensor product not being commutative; I believe this has been done to type stack-based languages]
OK, I understood this. Thanks.
By the way, what is the best book to teach yourself category theory? I’ve tried reading “Category Theory for Computer Scientists” by B. J. Pierce, but it skimmed over way too many details to be useful. Is there a better book than Awodey’s (is MacLane’s better)?
I think it really depends on your background and interests (i.e., where you’re coming from and where you’re aiming (at the moment) to go); some books will definitely be much more useful to certain audiences than others, basically. Awodey’s book is a step up from Pierce while still ostensibly aimed at even those who would fall through the cracks of the usual assumed mathematical background, which may be nice; indeed, I recall computer science students who, though they got nothing out of Awodey’s category theory classes in themselves, later returned to the book for self-study and found it very useful. However, if it isn’t working for you, then you might as well borrow a couple others from the library, including MacLane’s (though this is a both more aimed at the traditional mathematician), and skim through them till you find some you mesh better with.
If I understand your background and interests right, you may find it useful to complement such general introductions with something like Lambek and Scott’s “Introduction to Higher-Order Categorical Logic”, which focuses on connections to lambda calculus, type theory, and intuitionistic logic; whatever else the book’s merits and flaws, it will help breed a useful categorical perspective on those topics, and even reveal the latent categorical knowledge anyone familiar with those topics already has, which may whet your appetite for more, or at least soften fear of the alleged inaccessibility of the subject.
“bit more aimed”, not “both more aimed”.
OK, this sounds like a good idea, thanks!
Oops; just correcting the typo here: it should be f (x) g : A (x) B -> A’ (x) B’, of course.
While I’m adding minor things, one thing I could have pointed out when I said n-ary operations can be constructed from binary operators and a distinguished object is that, though the various ways of doing it are not, a priori, equivalent, the stipulation that they become equivalent is just the same thing as associativity (with the identity object’s properties being the 0-ary case of this).
Well, where “various ways of doing it”, were it sharpened, would be understood to mean ways differing in parenthesization but not ordering, as such. But I’m going to quit nitpicking for little gain while I’m ahead.
Sorry for the delay. I’ve been busy apartment hunting.
Anyhow, the standard is MacLane’s Categories for the Working Mathematician, though Herrlich & Strecker is also decent. G.M. Kelly has [Basic Concepts of Enriched Category Theory[/a].
And I’ve had a number of people comment that they’re sending their grad students to read my own notes. The “category theory” category (sorry) starts [url=Category theory « The Unapologetic Mathematician]here](Basic Concepts of Enriched Category Theory), and is arranged in reverse chronological order.
I hope you don’t mind; I’ve fixed your second link up in the quote above. And I agree; your notes are great!