If two binary session types $S_1$ and $S_2$ are bisimilar, are all subtypes of $S_1$ also subtypes of $S_2$ and vice versa?
1 Answer
$\begingroup$ $\endgroup$
If two binary session types S1 and S2 are bisimilar, then yes, all subtypes of S1 will also be subtypes of S2, and all subtypes of S2 will also be subtypes of S1. Here's why:
Bisimilarity means that two session types S1 and S2 are behaviorally equivalent. This implies that they allow the same sequences of interactions, such as send and receive actions. More formally, two session types are bisimilar if there is a one-to-one correspondence between their actions, where each action in S1 can be matched by an equivalent action in S2, and vice versa.
