TODO.md

Concrete todos

• Merge master into companion and then back and kill companion

• Transitivity of bisim

• Non-trivial law up-to bisim (interp or iter)

• Add: fork 0 ~ spin, and similar

• Define weak bisimulation

• Define strong bisimulation

• Pushing forward CCS

  • Some done, need to discuss what is relevant to prove
  • To check: is weak bisimulation inherited into ctrees too weak, a.k.a. in particular would be a congruence for +

• Sketch the yield experiment

  • Modify schedule so it works over a thread pool and take the starting thread as an argument

• Should the target monad for interpretation somehow be aware of the visibility flag?

Observable states, non-observable states

Consider the following trees, where "a" is some kind of trigger:

-t1 = Choice 2 (Choice 1 a) b -t2 = Choice 2 a b

From the perspective of [bisim], both trees are equivalent: they each can challenge over either a or b, and move to the empty process by doing so. However, they are also a very natural representation of respectively the CCS processes (P = τa + b) and (Q = a + b), processes that are not equated by weak bisimulation. Indeed, from the perspective of this equivalence, P can use the τ to internally take the left branch, without consuming "a" yet: it reduces by doing so to the process "a". In contrast, Q cannot take any branch as it would require from it to draw either "a" or "b". It can match the step by refusing to move, but the resulting processes are then not weakly bisimilar since the right one can now challenge the left one over a "b".

Of course one possible conclusion of this observation is that "t1" and "t2" should not be the encoding of P and Q. Operationally, stepping on either side of a "+" requires to exhibit the proof that this side can step, so that this step is taken: maybe the encoding should work harder and simulate this behavior.

However, another take could be that this highlight that there are really two primitive "scheduling nodes": invisible ones, that the scheduler cannot stop on, and visible ones, that can be stopped on. With the current definitions of [bisim], all choice nodes are invisible: the scheduler can only stop when it reaches a [vis] or a [ret]. There are therefore "less" challenges than with a traditional weak bisimulation, we equate more processes. Conjecture to check: it corresponds to the strong game over the [=> -a>] relation where [a] is a non-τ event.

If we were to change [bisim] so that we can stop at any node on the way to the first [vis] or [ret] reachable, we would make all nodes visible. This would this time leads to more challenges than with traditional weak bisimulation in the sense that the tree contains more states than the usual transition systems. In particular, (P = (a + b) + c) and (Q = a + (b + c)) mapped into trees (t1 = Choice 2 (Choice 2 a b) c) and (t2 = Choice 2 a (Choice 2 b c)) would not be equivalent under this new equivalence since the state (Choice 2 a b) would be reachable from t1, and t2 would have no way to answer it.

I hence think that it makes sense to fundamentally distinguish in the structure visible from invisible choice nodes, by adding a boolean flag to the constructor. Our bisimulation would hence allow the scheduler to stop additionally on the visible states. A process algebra that treats "+" such as CCS does could therefore simply model it as:

• model (P + Q) = choice false 2 (model P) (model Q) In contrast, if the language always allows choice to pick a side, i.e. [P+Q → P] is always valid, then it could be simply modelled as:

• model (P + Q) = choice true 2 (model P) (model Q) And in the case of ccs, we would therefore have ccs's tau steps interpreted into [choice true 1] in contrast with "itree-style taus" used as guards that would be [choice false 1].

Another note: to get to weak bisimulation, we need somehow to also call [schedule] after matching. Otherwise, the following example is problematic: ca + c (a + b) / c (a + τa + b) This is basically whether the bisim is built upon =>-> or =>->=>

• TODO: write this cleanly, in particular what is [matching] for a [choice true] challenge?

A few notes on trailing things to consider

Shared code with itrees, level of abstraction

- Some generic code could be reused from the itree library.
  + Do we want to depend on the itree library?
  + Do we want to pull the generic code from the itree library to an external one?
	+ Do we want to recode it. If so:
		* Do we want to keep it categorical?
		* Do we want to specialize it?

Symmetry argument

The companion support arguments by symmetry to avoid the duplication of proof scripts for bisimulation. Can we use it in our setup?

Interpretation and scheduling

What do we want to do w.r.t. implementation of the internal choice?

From the perspective of reasoning, we don't need anything particular since the bisimulation should be precise enough to capture all equivalences w.r.t. this effect. We could hence simply delegate the implementation on the OCaml side.

It could however also be interesting to study what it means to interpret it inside of Coq.

Bisimulation and "Cosimulation"

The [BisimSched] rule amounts to the traditional bisimulation: locally, both computations challenge one another.

We could alternatively mimick the usual simulation, breaking the symmetry in the relation, and ask for both computations to simulation one another -- let's call this to be in cosimulation.

It is well known that traditionally cosimulation is strictly weaker than bisimulation. Is it also the case in this setup?

Weak bisimulation, barbed bisimulations and the whole zoo

From the perspective of a calculus like ccs of the pi-calculus, we expect to define an equivalence as ctree's notion of bisimulation applied to the representation function as ctrees of the terms.

However it is well known that there exists many bisimulations defined on top of the operational semantics of these calculi. Hence the question: which one do we get naturally, if any? And how would we get the others: by defining a different equivalence over ctrees, or by changing the representation function?