Bug: formalization error in lifted variant of reflexive and transative closure over silent steps

[betawave]

We have an error in the definition of $P \mathrel{{\twoheadrightarrow}{S}} Q$.

We have defined it as such: $P \mathrel{{\twoheadrightarrow}{S}} Q \equiv \forall p \in P. \forall q \in Q. p \twoheadrightarrow q$.

This contradicts what is written in the paper, where the lifting procedure for single steps is described: $P \overset{\alpha}{\rightarrow} Q \equiv Q = \{ q \in \mathcal{P} | \exists p \in P . p \overset{\alpha}{\rightarrow} q \}$

We could redefine $P \mathrel{{\twoheadrightarrow}{S}} Q$ as such:

1. $P \mathrel{{\twoheadrightarrow}{S}} Q \equiv (Q = \{ q \in \mathcal{P} | \exists p \in P . p \twoheadrightarrow q \})$, or
2. $P \mathrel{{\twoheadrightarrow}{S}} Q \equiv ((\forall q \in Q. \exists p \in P. p \twoheadrightarrow q) \land (\forall p \in P. \forall q. p \twoheadrightarrow q \rightarrow q \in Q ))$, or
3. WRONG (see belows comment) $P \mathrel{{\twoheadrightarrow}{S}} Q \equiv (\forall p \in P. \forall q. p \twoheadrightarrow q \leftrightarrow q \in Q)$

I' not sure if all these variants are equivalent and/or correct.

[betawave]

After some investigation, I learned that above formalization options 1 & 2 are equivalent, while both diverge from option 3. While not equivalent to our current definition, option 3 seems to be related to it an presents similar issues with empty sets and the cartesian product of processes in P and Q.

[crmrtz]

Woudn't we also need to change step_set (↦S)?

[crmrtz]

1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q}), or
2. P↠SQ≡((∀q∈Q.∃p∈P.p↠q)∧(∀p∈P.∀q.p↠q→q∈Q)),

For 1 and 2 to be equivalent, one would also need that Q is a subset of P, right?

So something like:

2. P↠SQ≡((∀q∈Q. q∈P ∧(∃p∈P.p↠q))∧(∀p∈P.∀q∈P.p↠q→q∈Q))

[betawave]

1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q}), or
2. P↠SQ≡((∀q∈Q.∃p∈P.p↠q)∧(∀p∈P.∀q.p↠q→q∈Q)),

For 1 and 2 to be equivalent, one would also need that Q is a subset of P, right?

No. I was able to show equivalence without that premiss.

[betawave]

Woudn't we also need to change step_set (↦S)?

Yeah, looks like it.... I was unaware of its existence.

[betawave]

I'm also very confused by the abbreviation called non_tau_step_set, which afaik just exactly the same as step_set. To me, it looks like there is a condition missing given the name of the abbreviation.

[crmrtz]

Woudn't we also need to change step_set (↦S)?

Yeah, looks like it.... I was unaware of its existence.

Then we also need to fix non_tau_step_set (↦aS). Sorry for not saying anything earlier

[betawave]

Could you elaborate on what non_tau_step_set (↦aS) is supposed to mean and how that is realized in the current definition: "P ↦aS α Q ≡ ∀p ∈ P. ∀q ∈ Q. p ↦a α q" ?

[crmrtz]

I'm also very confused by the abbreviation called non_tau_step_set, which afaik just exactly the same as step_set. To me, it looks like there is a condition missing given the name of the abbreviation.

Apperently we defined it the same. In the case of the spectroscopy game the difference might not have any relevance though - looking at the conditions of (branching) observations.

[crmrtz]

Could you elaborate on what non_tau_step_set (↦aS) is supposed to mean and how that is realized in the current definition: "P ↦aS α Q ≡ ∀p ∈ P. ∀q ∈ Q. p ↦a α q" ?

Check out Definition 2 in the paper one is supposed to be p ↦α q and one is p ↦(α) q

But I'm confused by our naming and usage in the definition of spectroscopy_moves. To me that seems inconsistent.

[crmrtz]

1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q}), or
2. P↠SQ≡((∀q∈Q.∃p∈P.p↠q)∧(∀p∈P.∀q.p↠q→q∈Q)),

For 1 and 2 to be equivalent, one would also need that Q is a subset of P, right?

No. I was able to show equivalence without that premiss.

I think you were only able to because you changed 1 as well. You ignored the bold part: 1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q})

[betawave]

1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q}), or
2. P↠SQ≡((∀q∈Q.∃p∈P.p↠q)∧(∀p∈P.∀q.p↠q→q∈Q)),

For 1 and 2 to be equivalent, one would also need that Q is a subset of P, right?

No. I was able to show equivalence without that premiss.

I think you were only able to because you changed 1 as well. You ignored the bold part: 1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q})

Okay, I see your point. But I do very much disagree that Q ought to be a subset of P! To my understanding $P \mathrel{{\twoheadrightarrow}{S}} Q$ means that Q contains all processes that are reachable via tau steps from P. Requiring that Q be a subset of P breaks this interpretation.

[benkeks]

You ignored the bold part: 1. P↠SQ≡(Q={q∈P|∃p∈P.p↠q})

Oh, sorry, the naming in the paper is sub-optimal: $P$ (the starting set of processes for the transition) and $\mathcal P$ (the global supply of states / processes) are different sets!

[Vervada]

Could you elaborate on what non_tau_step_set (↦aS) is supposed to mean and how that is realized in the current definition: "P ↦aS α Q ≡ ∀p ∈ P. ∀q ∈ Q. p ↦a α q" ? Check out Definition 2 in the paper one is supposed to be p ↦α q and one is p ↦(α) q

I think you are right. I remember that non_tau_step_set (↦aS) should be p ↦(α) q.

[betawave]

We've now implemented non_tau_step_set by appealing to $\mathrel{{\mapsto}{a}}$, which - according to @TheHllm - formalizes the notion of p ↦(α) q.