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  $ (s : S \lhd P(s) )$ for Plain Old containers. (Why on earth Dr. Abbot couldn’t see his arrow head was the wrong way round is beyond me.)

lollipop

\[
\begin{array}[t]{l}
(A \lhd\, B) \mathbin{\relbar\mskip-8mu\circ} (C \lhd\, D) \\
= ( \begin{array}[t]{l}
         \langle t, \_ \rangle : (\Sigma t : A \to C)(\Pi a : A)D(t(a)) \to B(a)  \\
         \lhd \, (\Sigma a : A)D(t(a)))
       \end{array}
\end{array}
\]
This makes a container out of the morphisms, or more exactly to take for shapes the container morphisms   $\langle t,f \rangle $ , and for positions therein, the pairs  $\langle a, d \rangle$ where a is a shape of  $(A \lhd B)$ and d is a position in the shape of  $ (C \lhd D) $ 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
 $(A \lhd \, B) \otimes (C \lhd \, D) = (\langle a,c \rangle : A \times C \lhd \, B(a) \times D(c))$ .
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:

\[
\begin{array}[t]{l}
Cont[(A \lhd B) \otimes (C \lhd D), (E \lhd F) ] \\
\simeq Cont[(A \lhd B),(C \lhd D) \mathbin{\relbar\mskip-8mu\circ} (E \lhd F)]
\end{array}
\]

Ok, let’s write it out. First, the left hand side.

\[
\begin{array}[t]{cl}
&Cont[(A \lhd B) \otimes (C \lhd D), (E \lhd F) ] \\
=&
Cont[(\langle a,c\rangle : A \times C \lhd B(a) \times D(c)),(E \lhd F)]\\
=&
(\Sigma g :
\begin{array}[t]{@{}l}
A \times C \to E) \\
(\Pi \langle a, c \rangle : A \times C)F(g \langle a,c \rangle) \to B(a) \times D(c)
\end{array}
\end{array}
\]

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

\[
\begin{array}[t]{cl}
&
Cont[(A \lhd B), (C \lhd D)  \mathbin{\relbar\mskip-8mu\circ} (E \lhd F) ]
\\
=&
Cont[
\begin{array}[t]{@{}l}
  (A \lhd B),\\
  (\begin{array}[t]{@{}l}
     \langle t, f \rangle :
         \begin{array}[t]{@{}l}
             (\Sigma t : C \to E)
             \\
             (\Pi c : C) F(t(c))\to D(c)
         \end{array}
     \\
     \lhd (\Sigma c : C)F(t(c)) ) ]
   \end{array}
\end{array}
\\
=&
\begin{array}[t]{@{}l}
  (\Sigma h:A \to
         \begin{array}[t]{@{}l}
              (\Sigma t : C \to E)
              \\
              (\Pi c : C)
                   F(t(c))\to D(c))
         \end{array}
  \\
  (\Pi a : A)(\begin{array}[t]{@{}l}
                  (\Sigma c : C)F((h(a))_0(c))) \\
                  \to B(a) \end{array}
\end{array}
\\
=&
\begin{array}[t]{@{}l}
  (\Sigma h:A \to C \to E) \\
  (\Sigma k:(\Pi a : A, c : C)F(h(a,c)) \to D(c)) \\
  (\Pi a : A, c : C)F(h(a,c)) \to B(a)
\end{array}
\\
=&
\begin{array}[t]{@{}l}
(\Sigma h : A \times C \to E) \\
(\Pi \langle a, c \rangle)F(h\langle a, c \rangle) \to B(a) \times D(c)
\end{array}
\end{array}
\]
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.

One Response to “lolly, tensor, no bang”

  1. PierreH Says:

    OK, it is probably the perfect time for me to step in and say a few things…

    As Peter pointed out, there is a notion of container of morphisms (linear arrow). I had actually never realized that the “dependent container” linear arrow could be backported to “plain” containers.

    From the South of France point of view, morphisms for dependent containers are “proof irrelevant”: a morphism is a relation with a proof that it is a simulation. (It is an obvious generalization of the container morphisms or of usual simulation relations.)
    However, equality of morphisms is defined as extensional equality of the relations…

    This was necessary for the work I was doing with “dependent containers”:
    simulations become some kind of continuous function (extensionality is thus important); and it latter became a necessary condition to obtain a model for _full_ linear logic.
    (Without it, I wouldn’t be able to get _classical_ linear logic…)

    Plain containers are dependent containers with a singleton set of states; it is thus stupid to identify simulations extensionally.

    So:
    * plain containers form a symmetric monoidal closed category (modeling intuitionistic multiplicative linear logic)

    * there is no dualizing object (in the dependent case, it is given by the trivial dependent container SKIP; but the proof that it is dualizing requires classical logic.)

    * I don’t think there is a BANG operator: the set of states wouldn’t be a singleton. (For dependent containers, the BANG is given by the free tensor comonoid…)

    * Are plain containers closed under product and coproduct? I don’t expect them to be. (In my case, the product of two plain containers is not a plain container: its set of states would contain two elements. Moreover, product and coproduct coincide.)

    Hmm… That’s about it for now…