Adding identifiers mechanisms

[aubertc]

The goal is to "tag" every transition with not only a label / action, but also with some unique integer (id). The trick is that we want this id to be unique, but don't want to synchronize between threads, so each thread should have its way of coming up with new identifiers.

The solution we sketched is a bit math-heavy and too abstract, let me try to make it more concrete (and forgetting about reversibility for now):

• A process can only be seen as a collection of threads (e.g. 0 has zero thread, a . P has one thread, a.P + b.Q has one thread, P | Q has two threads, etc.).
• An identifier pattern is a pair of integers (c, s) ("current" and "step") such that s > 0.
• An identified thread (c, s) ○ T is a thread T coupled with an identifier pattern (c,s),
• An identified process is a collection of identified threads.

The idea is that, for the identifier pattern (0, 1), the thread a.b.c.P would reduce as follow:

Origin	(label, id)	Target
(0, 1) ○ a.b.c.P	----(a, 0)---->	(1, 1) ○ b.c.P
(1, 1) ○ b.c.P	----(b, 1)---->	(2, 1) ○ c.P
(2, 1) ○ c.P	----(c, 2)---->	(3, 1) ○ P

etc. The idea is that an identified thread (c, s) ○ T will use c as its next id and then use (c+s, s) as its identifier pattern from now on.

The complication comes when the number of threads change, such as in a . (b.P | c.Q): originally, this process has only 1 thread, but after a transition, it becomes two threads (b.P and c.Q).
For this, we "split" the identifier pattern: we can reason about splitters abstractly, but in our case it's enough to simply split any (c, s) into two identifier patterns: (c+s, s+s) and (c, s+s). It is fairly immediate to see that the stream c+s, c+s+s+s, c+s+s+s+s+s, … and the stream c, c+s+s, c+s+s+s+s, … will never contain the same id (provided, of course, s > 0).

Once this is observed, two things are needed:

• To make sure that the process we begin with has "enough" identifier patterns: it would not be correct to try and execute (0, 1) ○ a.P | b.Q, since we can generate only 1 id for 2 threads.
• To make sure that the number of threads match the number of identifier patterns through the execution.

An example of execution could be:

Origin	(label, id)	Target	Note
(0, 1) ○ a.P | b.Q	=	(0, 2) ○ a.P | (1, 2) ○ b.Q	Otherwise there is a mismatch
(0, 2) ○ a.P | (1, 2) ○ b.Q	---(0, a) --->	(2, 2) ○ P | (1, 2) ○ b.Q
(0, 2) ○ a.P | (1, 2) ○ b.Q	---(1, b) --->	(0, 2) ○ a. P | (3, 2) ○ Q
(2, 2) ○ P | (1, 2) ○ b.Q	---(1, b) --->	(2, 2) ○ P | (3, 2) ○ Q
(0, 2) ○ a. P | (3, 2) ○ Q	---(0, a) --->	(2, 2) ○ P | (3, 2) ○ Q

Note that:

• We can iterate this process. If P is c . Q | d . R, then we can have (2, 2) ○ P = (2, 4) ○ c.Q | (4, 4) ○ d.R
• The identifiers are all unique.
• The "splitting" should take care after each transition ("did the number of threads change? If yes, I need to split") and before the execution ("let me get you an identifier pattern. Oh, you are made of x threads? Let me split it for you").
• A thread will always pick the same identifier (no matter if we reduce on a.P or b.Q's side first, the left-hand side will always get id 0, and the right-hand side will always get id 1).

We don't use this last information, but we could.
When we will be rewinding those threads, some care will be needed to possibly "re-bundle" the identifier patterns, but we can worry about that later.