[neel_k]

Vector spaces and linear maps between them form a model of the linearly-typed lambda calculus. That is, each type can be interpreted as a vector space, with each well-typed term representing a linear map between vector spaces.

1. The linear tensor product A ⊗ B gets interpreted as the tensor product of vector spaces.

2. The linear function space A ⊸ B gets interpreted as the vector space of linear functions between A and B.

3. The Cartesian product A × B gets interpreted as the direct product of vector spaces (i.e., the categorical product).

4. The sum type A + B gets interpreted as the direct sum of vector spaces (i.e., the categorical coproduct).

5. The exponential !A gets interpreted by the Fock space construction.

This explains why the choice of name is sensible, but I don't actually know if that was the reason why Jean-Yves Girard named it so. If memory serves, he invented linear logic after thinking about Berry's notion of stable functions, but I don't know for sure when the vector space model was invented. (It's not in his 1987 paper, but it can't have appeared very long after that.)

[joppy]

Are vector spaces really the right category? In particular the product and coproduct of vector spaces are isomorphic (both isomorphic to the direct sum).

[bitdizzy]

It depends on what you mean by right category. It is true that vector spaces identify certain constructs that linear logic distinguishes, but it doesn't identify everything so it still has some interesting content. Finding models that don't make unnecessary identifications is one of main lines of research in the field.

[QuesnayJr]

They're not the right category for computation, but they are a valid interpretation of linear typing. They're one of Girard's original inspirations for linear logic. The resource interpretation came later.

[coldpresent]

Is there an explanation out there about the vector space model? Perhaps one that relates to Gir87's phase semantics?