## Archive for August, 2005

### Plain containers and linear logic…

Tuesday, August 23rd, 2005

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…

### lolly, tensor, no bang

Wednesday, August 17th, 2005

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.)

lollipop

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).

tensor
.
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.

### The universal property of logarithms

Tuesday, August 2nd, 2005

This is Neil’s scribe here.

We have made some progress with taking logarithms of functors, and seem to have a nice categorical analysis. This includes a universal property of the logarithm of a functor, a complete characterisation of those functors which have logarithms, a formula for calculating the logarithm of a functor (when it exists), and a simple derivation of the properties of the logarithm. Don’t get too excited though for reasons which become clear later.

We start by defining a functor by . So Y(A) is a covariant hom functor and Y(A) is exactly what Conor and Hank have been calling Naperian containers’. In general Y doesn’t have a right adjoint, but we call a functor F logarithmic iff there is an object and a bijection between maps in and maps in , or equivalently maps in C.

Thm. Every Naperian container is logarithmic, and the log is calculated by thye McBridean formula .

Prf. If F is Naperian, it is of the form Y(B), so by Yoneda the maps are in bijective correspondence with maps . The result then follows by showing that equals B. []

(We cheat by using Yoneda. Some hygeine is required that we will sort out later.)

Thm. Every logarithmic functor F is a Naperian container.

Prf. By assumption, the maps in are in bijection with the maps in .
By Yoneda, the latter maps are in bijection with elements of F(A). So F(A) equals . So , and hence is Naperian. []

This is a nice result. It shows that the logarithmic functors are precisely the extensions of Naperian containers.

The properties we will derive are these:

• , where 1′ stands for the constant 1-valued functor, and likewise `0′ for the constant 0-valued functor. (These are terminal and initial objects in the functor category.)
• , where K is an object in our category.
• (Conor’s law) .

Prf. For the first property, simply calculate . For the rest, note that F and G must be of the form Y(A) and Y(B). Now just use the first result.

Conclusion. This all looked very nice at one point. But these last results are actually pretty darn trivial. Maybe there is more substance to them if we avoid the use of Yoneda. For example the last three laws can be proved using the universal property.