Exponentials

[np]

Why exponentials?

I'd like to gather here examples of the use of exponentials in the context of Ling, my conclusion so far is that they do not address the need for client/server behavior. If you disagree let's be constructive and have some examples.

Exponentials Now

First since Ling can views processes as terms and send/recv terms it does support a form of exponention [citation needed about Contextual Modal Linear Logic]:

• ? S becomes ? < S > which means receiving a process following session S.
• ! S becomes ! < S > which means sending a process following session S.

Upon receiving a process you can decide to use as many times as you want which is the expected behavior.
Sending a process require this process to be replicable, this is the case since you first need to wrap it as a term with proc(c : S). Thus, while you can still use the processes received as terms, your (linear) context only contains c.

I don't see how this form of exponential adrresses the client/server behavior, in a way you get to first download the code and then run it. Moreover it does not gives you access to more resources than you had before.

One might however consider a more direct support for exponentials.

A deeper integration of exponentials

In order to best integrate exponentials, I propose to mark the channels with exponentials. In this proposal the mark is a leading * in the channel name to express the repetition effect. The focus is first on the why not connective (noted ? in linear logic but this would conflict with our use of ? for sessions to receive data). The why not connective is essentially a flexible/repeatble version of par (⅋).

Let's assume S a Session used as the basis, we then have *c : S (in Linear Logic we would have something like c : ?S).

I'm proposing a syntax which enrich the current par splitting, for instance:

*c{c0,c1,*c2,*c3}

means that *c is splitted in four parts, with the following session assignment:

c0 : S
c1 : S
*c2 : S
*c3 : S

Therefore c0 and c1 can be used right away and *c2 and *c3 can be split further.

Getting rid of an unneccessary * channel can be done with empty splitting *c2{} for instance.

This design is (seems) compatible with the inference done on the processes.

The standard treatment of exponentials would be the following: Upon splits check that all the sessions are equivalente and propagate upward such session. One caveat is that when the split is empty we have no information to start with. The workaround could be to ignore the sessions which are *ended.

What about *c[ ... ] or *c[: ... :], they could be accepted as well with their corresponding rules. This would be consistent since we have mix ([Γ] ⊸ {Γ}) and ([:Γ:] ⊸ {Γ}). Intuitively if you have the choice of the processing order ({Γ}) you can decide to restrict yourself to proccessing in parallel ([Γ]) or in-order ([:Γ:]).

However the dual side will not be able to take advantage of these additional restrictions and will have to process all the request independently.