Plain containers and linear logic…
As Hank pointed out, the SMCC structure of our “interaction systems” can be backported to plain containers. This is quite interesting because, even if as an object, a plain container is a particular interaction system (with the set of states being ), the notion of morphisms are quite different. (For interaction systems, we identify morphisms “extensionally” and as a result, all the container morphisms are equal when seen as interaction system morphisms.)
Interaction systems form a model for full linear logic with the following proviso:
* we have classical linear logic only when the ambient category is and the meta theory is classical
* there are complications when dealing with the bang of an interaction system since this requires quotienting sets. (I guess we would need a notion of interaction system on a setoid rather than on a simple set…)
There is a small degeneracy in that the product (”with” in the LL terminology) and coproduct (”plus” in the LL terminology) coincide. I don’t care since without that, interpreting the differential -calculus would have been possible!
The question is now to see if we can backport some of those features into plain containers. I first though the answer was no, but I am not sure any more. More precisely, it looks that we can get a model of intuitionistic LL with plain containers, but the additive operations (plus and with) do not correspond to the one on interaction systems!
For example, it is not possible to define my (co)product on containers, but there are products and coproduct for containers. Interestingly enough, those product and coproduct do correspond to operation on interaction systems which I haven’t found applications for.
(Hmmm… That’s not entirely true: the coproduct of containers corresponds to the product of topological spaces, but that is another story.)
Also, product and coproduct are different. (No hope of getting a denotational model for the simply typed differential -calculus there…)
Since we have (indexed) coproducts and finite tensors, it shouldn’t be difficult to construct the container . Using setoids rather than sets, it should then be possible to add some quotient and obtain .
A shape in is given by a finite multiset of shapes in ; and a position from shape is given by a finite multiset of position . (Some care is needed to define this correctly.)
Does it make sense to any of you? I would more or less expect this construction to be the free comonoid generated by , and it wouldn’t be surprising to obtain a model for full intuitionistic LL…
One last thing about the container : since I only pretend to modeling ILL, any container can be used as the interpretation of ; however, the container is particularly well-suited, if only because we have (I think) .
(Recall: is the LL notation for coproduct and is LL notation for product. “” is shorthand for (see Hank’s posting).)
Of course, the miracle of the extensional, set-based version does work any more: this object will not be dualizing…