lolly, tensor, no bang
WARNING: This is the second version of this entry. The first was WRONG!
It’s mentioned in a previous note that bits and pieces of linear logic can be defined on dependent containers. The expert on this is Pierre Hyvernat, who will shortly be shaking the foundations of civilisation with his thesis. It occurred to me to see how much of this linear guff can be `back-ported’ to Plain Old containers. The management summary is (UIAM) you can define lollipop and the tensor, but not bang.
I adopt Conorial notation for Plain Old containers. (Why on earth Dr. Abbot couldn’t see his arrow head was the wrong way round is beyond me.)
This makes a container out of the morphisms, or more exactly to take for shapes the container morphisms , and for positions therein, the pairs where a is a shape of and d is a position in the shape of to which t maps a. So a position is really a shape in the high-level container (that gives you a shape in the low-level one) and a position in that low-level one (that gives you a position in the high-level one).
If one adopts an `imperative’ metaphor (`shapes’:`positions’ :: `instructions’:`responses’), then to issue an instruction in the tensor is to issue two instructions in parallel, but proceed only when the two responses have been returned.
Now one has to show that:
Ok, let’s write it out. First, the left hand side.
Now, the right hand side. (Fiddling around with latex in this wretched system is beyond the limits of human endurance! The following compiles fine on my computer.)
So both sides of the equation boil down to the same thing.
The left-hand end of the lollipop is a contravariant kind of place, so I wouldn’t go taking fixed-points of container expressions when the bound-variable sits anywhere therein.
not bang Now, there’s a bang operation in the dependent case. To use the imperative metaphor, the states of the banged container are multisets of the states of the unbanged one. To have a banged dependent container (/interaction structure) is like having a multiset of unbanged dependent containers, which are lock-step synchronised. (Pierre calls this synchronous multithreading.)
Plain Old containers are dependent containers over a singleton state-space; or, if you prefer signatures that happen to be singly-sorted. If you bang them, they’re no longer singly sorted. Instead, the state-space becomes the free monoid on a single generator, or as old-timers like me prefer to say, the natural numbers. So, AFAICS, you don’t get a bang out of Plain Old containers.