« lolly, tensor, no bang
Fixpoints of Indexed Containers »

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 \mathbf{Set} 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 \lambda-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 \lambda-calculus there…)

Since we have (indexed) coproducts and finite tensors, it shouldn’t be difficult to construct the container \bigoplus_{0\leq n} w^{\otimes n} . Using setoids rather than sets, it should then be possible to add some quotient and obtain \mathbf{!}w := \bigoplus_{0\leq n} \frac{w^{\otimes n}}{\mathfrak{S}^n} .

A shape in \mathbf{!}(A\triangleright D) is given by a finite multiset of shapes in A\triangleright D; and a position from shape [a_1,. . .,a_n] is given by a finite multiset of position [d_1,. . .,d_n]. (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 \otimes comonoid generated by w, and it wouldn’t be surprising to obtain a model for full intuitionistic LL…

One last thing about the container \bot: since I only pretend to modeling ILL, any container can be used as the interpretation of \bot; however, the container (\{*\}\triangleright \lambda \_.\{*\}) is particularly well-suited, if only because we have (I think) (\_\oplus\_)^\bot \equiv (\_^\bot \mathbin{\&} \_^\bot) .
(Recall: \oplus is the LL notation for coproduct and \& is LL notation for product. “w^\bot” is shorthand for w \multimap \bot (see Hank’s posting).)

Of course, the miracle of the extensional, set-based version does work any more: this object will not be dualizing… :(

This entry was posted on Tuesday, August 23rd, 2005 at 4:12 pm and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

4 Responses to “Plain containers and linear logic…”

  1. Hank Says:
    September 1st, 2005 at 11:56 am

    About representing multisets in type theory, one option
    seems to be as a quotient of $(\Sigma\,n : N) n \rightarrow S$
    (here the second “n” is being used for the set “Fin(b)” or
    $ \{ i : N \,|\, i S$ .

    About Pierre’s suggestion for a bang on plain containers, I take
    it the idea is that

    (1)

    an angel’s move (shape) in the bang of a contrainer is a multiset of angel’s moves (shapes) in the unbagged container $(C!).A = (C.A)!$. We now have to arrange that the set of positions for a shape does not depend on the particular order in which a shape is given.

    (2)

    a demon’s response (position) to an angel’s move $a = [a_0,...,a_{n-1}]$ is (represented by) a permutation p of dom(a), and a function $d : (\Pi i : dom(a)) \rightarrow (C.D)(a(p(i)))$ . Equality of representations is modulo permutations.

    It is as iff the angel has an inexhaustible supply of slave devices
    to which she can issue as many commands in parallel as she likes
    (possibly none). But she has to wait for all the responses.

    What does one have to show about this? That C! is the free $\otimes$ comonoid generated by C? What is this in layman’s
    terms?

  2. Hank Says:
    September 2nd, 2005 at 6:08 am

    I don’t completely understand “all the container morphisms are equal when seen as interaction system morphisms”. The relation between these two
    kinds of morphisms seems very subtle. It seems to me that a dependent
    container morphism (one with a *function* mapping high-level sorts to
    low-level sorts) is the same as an interaction system morphism which happens to be (the graph of) a total function.

    I can see, I think, that several different container morphisms can “satisfy” extensionally the same simulation relation, but not that all container morphisms are extensionally equal.

  3. PierreH Says:
    September 5th, 2005 at 10:49 am

    About multisets in type theory:

    the easiest is probably to use setoids and define \mathcal{M}(S,\equiv) := (\mathbf{List}(S),\approx), where \approx is just the “quotient” of \equiv modulo permutations of lists.

    (Of course, we must require that the family of shapes is a family of setoids, indexed by a setoid: it must respect equality… This gets very messy…)

    Then, an action/shape is just given by a tuple [s_1,\ldots,s_n], and a reaction/position is just a tuple of [p_1,\ldots,p_n], where each p_i is a position in shape s_i.

    Note that this is not the same as the bang defined on interaction systems, since the number of actions/shapes is not determined by the state. In particular, while iterating the container, the number of shapes can change.

    That !C is the free \otimes comonoid just means that it is the “smallest” such comonoid:
    (1) there is an arrow e : !C \to \mathbf{Skip}
    (2) there is an arrow !C \to !C \otimes !C
    Those arrows satisfy some commutativity and associativity diagrams, and are universal in some sense (”free”).

    A more abstract way to look at it is by saying that the functor !\_ from the category of containers to the category of \otimes-comonoids is adjoint to the obvious forgetful functor from \otimes-comonoids to the containers…

    All of this seems very important to LL people, but I have to admit I don’t have strong intuitions about them…

    About the link between container morphisms and simulations between interaction systems: the relation seems very subtle. When I wrote that container morphisms are all “equal” I had the “classical” notion of simulation: usual relations. In the case of containers, the set of states are trivial: \{*\}. There is only one non-empty relation between two such sets: \{(*,*)\}.

    In a constructive setting, this is far more complex than that!

  4. Hank Says:
    September 13th, 2005 at 12:40 am

    Concerning setoids, the “Container Gang” before the Coming of Hancock, have a paper Constructing Polymorphic Programs with Quotient Types from 2004 explaining the East Midlands take on quotienting the positions. (You probably have had a look.)

    Conor has some further ideas that must be somehow related about putting well-orders on positions, that are somewhere in this blog. They both seem
    to involve putting some structure on positions.

    I am very curious about the relations between containers with quotients and “species of structures” a la Fiore/Joyal/.. . Species seem very oriented towards data-structures with a finite number of distinguishable positions.

Leave a Reply

You must be logged in to post a comment.