To me, saying the initial events have no parent is more expressive than saying they’ve got a parent that is “the null entity”. This one is mostly a matter of taste, though so your opinion may be fixed on this but I don’t think there is a strong argument for changing our definition.
Sure it works either way. My intention is to condense your paper into a small algorithm in “standard presentation”… So its not that important. On the level of implementation you handled it in the “cause” enum. My personal taste would be different though, but that too is not important.
I’m not sure if it’s clear to you but there are exactly
Nevents that have no ancestors. These are the initial events by each node. Nothing more, nothing less.
I’m not talking about the gossip graph, as such. I’m talking about the subgraph H_{X,B}. Since it is only a subgraph, we have situations, where a vertex in H_{X,B} has no ancestors IN H_{X,B} without being an initial event. It might in fact be trivial to show, that each of these vertices is an observer. But IMHO that needs to be said for the various functions on H_{X,B} to be well defined.
The point is, that IF there is a vertex e in H_{X,B} that has no self parent INSIDE H_{X,B} and is not an observer, then functions like aux, are not well defined. The value aux(e) is computed as aux(self_parent(e)) but self_parent(e) is not in H_{X,B}. However, note that this can easily be changed. In your implementation you used Some() (if I remember correctly), but that is specific to a certain programming style.
The statement
decide()used at line08 allows the invoking process p_i to decide but does not stop its execution. A process executes round forever. This facilitates the description and the understanding of the algorithm.
We could define the decide() value in such a way, that it is only computed from aux, bv, est and so on, if self parent decide is still empty. Therefore once a decide() is not empty anymore, it doesn’t change forever. This way, once a node decides, changes in aux, bv and est have no influence on it and it is static from that point on, no matter how aux, est and bv behave in the future.
Doing it like that, takes meta_election out of a lot of other functions and makes their involved, recursive definition a lot less complicated. And opens them to a pure recursive/inductive definition on the linear ordered set of self ancestors in H_{X,B}
I would love to see your suggestion in more details. I feel like we’ve hit or are close to the simplest necessary wording to describe the algorithm. If you can see a way to express it in a purer, more succinct fashion, I would be genuinely interested.
Might be true… But still I give it a go. After all its part of me trying to understand every bit of the algorithm. Mostly to validate the proofs.
As I mentioned above, I think that having the paper be clear enough that you can see a way of implementing it is more a feature than a bug: it means that every detail is clear enough that you can fully understand it.
Not much arguing here. I think it is a matter of taste, as you said. Depends although on what you want to achieve. If for example you want to verify the proof of PARSEC with CoQ or Isabell a different style might be preferred. After all, having additional papers like “PARSEC from a mathematicians p.o.v.”, can’t be a bad thing and reflects the open nature of your project.