refinement relation between `nondetE` trees

[aa755]

Has there been work on defining a refinement relation between trees that have the nondetE effect, saying that t1 refines t2 iff for every choice made for the nondetE actions in t1, there exists a choice for nondetE actions in t2 such that the rest of the two trees line up?

[gmalecha]

We wrote some of this out, didn't we?

[Lysxia]

There is something like that in our DeepWeb experiment but it's unused. In the VST proof we use trace inclusion, which is a coarser relation, but I'm pretty sure the lemmas we actually proved are all compatible with this tree refinement relation, which is a kind of simulation.

[jeehoonkang]

I'd also like to use interaction trees for proving behavior refinement (not equivalence) and wonder if supporting simulation (not bisimulation) is on the roadmap. If not, people in my group are willing to contribute to it.

[Lysxia]

This is in fact likely one of the sooner destinations on the roadmap. I only have very vague ideas at the moment, it would definitely be useful to have more discussion about this. - In our CPP paper we use trace inclusion, where nondeterminism (visible by default) is erased from traces beforehand. That's coarser than simulation of course, but for our purposes of modelling externally visible behavior without liveness concerns it was good enough. But it will take work to generalize. - Since our discussions with Gil about the recent developments in paco, I have a fuzzy idea that there may be a solution using some variant of the concept of respectful closure. - Another place to draw inspiration from is in the literature about the resumption monad (which itree is a variant of). I recently got a sense that they're trying to answer closely related questions, in highly more abstract terms.

…

On Mon, Apr 8, 2019, 14:45 Jeehoon Kang ***@***.***> wrote: I'd also like to use interaction trees for proving behavior refinement (not equivalence) and wonder if supporting simulation (not bisimulation) is on the roadmap. If not, people in my group are willing to contribute to it. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#42 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACZhARub46XoI-ymnuUdOn2HUM9C3pb8ks5veznagaJpZM4Z8SyG> .

[jeehoonkang]

@Lysxia Thank you for your detailed answer. Your second and third bullet explains ideas on solutions, but I don't quite understand the problem. May I ask if why it would be difficult to support interaction tree refinement?

[Lysxia]

Good question. I think the main problem is a problem of generality, so I may be getting carried away. Simulation is one example out of many other relations we may want to support, and we might even want to be able to combine some of them. To fit them all under a common framework is why I'm looking at those solutions.

In this light, a different way to approach this issue is to look at some concrete definition of simulation and decide that it is good enough for most purposes.