Represent transition firing as composition.

[FabrizioRomanoGenovese]

The firing of a transition in a category FSMC(o,m,source,target) (see #2 for details) can be represented as a function

t : GenMor(FSMC(o,m,source,target)) -> state : Mor(FSMC(o,m,source,target)) -> tokens : Obj(FSMC(o,m,source,target)) -> Mor(FSMC(o,m,source,target))

Morally, you give me the current state of the net (represented by a string diagram), a transition t (which is a generating morphism in the category) and the tokens on which you wanna fire it, tokens (details missing here!) and I give you the next state by postcomposing t with state as specified by tokens. Clearly this thing should be defined only for suitable t, state, tokens.

There is a slight problem here: Suppose I have state:
A x A x C x B x C x D and I want to fire a transition t: A x D -> C using the second A and the only D in the state. To make this work:

• The state must be reshuffled. That is, we have to recursively apply symmetries so that the second A and D come together and we can apply t. We want to do this in a "canonical" way (meaning that we want to find a way to do this that works in the same way for any possible enabled transition in the state).
• My suggestion is: We go from A(1) x A(2) x C(1) x B x C(2) x D to A(2) x D x A(1) x C(1) x B x C(2) (I am using numbers to distinguish copies of the same generating object). This means that the tokens that have to be used are rearranged to become the first in the product.
  1. There should be a precise algorithm to do this. I think I can draft it if you want. This algorithm works like this: You give me t : GenMor(FSMC(o,m,source,target)) -> state : Mor(FSMC(o,m,source,target)) -> tokens : Obj(FSMC(o,m,source,target)) and I give you a list of symmetries tensored with identities that can be sequentially composed with state to reshuffle the object in its target as we want. In our example this effectively maps state, having codomain A(1) x A(2) x C(1) x B x C(2) x D, to state' having codomain A(2) x D x A(1) x C(1) x B x C(2).
  2. At this point we can compose state' with t x id_A x id_C x id_B x id_C and obtain the state representing the firing of t in state state using tokens tokens.
  3. A transaction in the blockchain then can be specified by giving the symmetries produced at point i. and t tensored with identities as in point ii.

Note: If our nets are safe then we don't need to specify tokens in our function. This is because in a product all objects will be different: For instance in our example A(1) x A(2) x C(1) x B x C(2) x D represents having 2 tokens in A and two in C, which is not possible if the net is safe.

You see then that in a safe net a possible state is a product of objects X_1 x X_2 x ... x X_n where all the X_i are generating objects different from each other. In such a situation, if you give me a transition t, two things can happen:

• All objects in the domain of t are present in the codomain of state. In this case there is only one possible way to reshuffle the tokens in the codomain of state as specified above to compose with t.
• Some object in the codomain of t are not present in the codomain of state. In this case t is not enabled in state and so our stuff shouldn't typecheck.

[marcosh]

I may have an alternative idea which could maybe simplify this a bit.

Handle with care, this is a bit sketchy

Consider the state as a partial function state : Tokens -> Places, where Tokens is a set/type of indices. For examples, if we choose Tokens = Int, we could represent the state of the example above as a function f such that f 0 = A, f 1 = A, f 2 = C, f 3 = B, f 4 = C and f 5 = D.

Then, to represent the transition t, we can just say which tokens it wants to consume and where it is mapping them. In our example it could be something like ([1, 5], [C]) where the first element of the pair states which tokens need to be consumed and the second element describes where new tokens should be created.

Notice that this representation is possible only if our set/type of indices for the Tokens allows to auto-generate the next index (in our example it would be 6). This property holds even if we would like to use UUIDs as keys to identify the tokens, which would probably be nice from an implementation point of view. If this property does not hold, we should also specify a new key in the second component of the pair which describes the transition.

[FabrizioRomanoGenovese]

This is interesting, but I have a question: In this representation function domain is implicit. This means that if I specify a transition AxB -> C as, say, ([1,5], [C]) I am implicitly assuming that 1 is in A and 5 is in B. I suppose we need to verify then that state coincides with domain(t) on each token fed to t.

My suggestion is this: On smproc I have seen that James defines a helper function that turns every function f:A \to B into a box of the category. I think it makes sense then to take a look at his smproc in detail and see how he defines composition and if this is suitable for our needs. Since he works with symmetric monoidal category he needs to specify how boxes compose by providing the wiring explicitly, that is, he may have already solved our problem for us.

The helper function above is great because I can specify some functions (i.e. populate transitions with semantic meaning in my Petri net) and then generating the corresponding category just by applying that helper function to all transitions. What do you think?

[marcosh]

I will definitely have a look at smproc.

Regarding you question, I wouldn't say that we are assuming that 1 is in A and 5 is in D. We actually know this because f maps 1 to A and 5 to D. Maybe this is slightly different from a standard net, because here a transition does not map just Places to Places, but actually selects some tokens (some precise one) and moves (creates/deletes) them. In other words we require more data to define a transition