# Does bisimulation or the approximation lemma work for monadic streams?

For ordinary streams $S_A := \nu X. A \times X$, there is a bisimulation lemma. It says that two streams are equal if there exists a bisimulation between them. A bisimulation is a relation $\sim$ on streams defined like this: $s_1 \sim s_2 \iff \operatorname{head} s_1 = \operatorname{head} s_2 \wedge \operatorname{tail} s_1 \sim \operatorname{tail} s_2$.

Now, let $M$ be a monad. We'll define the type of "monadic streams" $S^M_A := \nu X. M (A \times X)$. Intuitively, if $M$ corresponds to a side effect, every time I retrieve the head from the stream I have to perform the side effect. I can define $\operatorname{head}^M: S^M_A \to M A$ and $\operatorname{tail}^M: S^M_A \to M S^M_A$ (using functoriality of $M$).

My question is now: Is there anything similar to bisimulation for monadic streams? Can I prove equality of monadic streams in the same way, using $\operatorname{head}^M$ and $\operatorname{tail}^M$? If not, what are proof methods that work on this coinductive type? Maybe the approximation lemma?

Edit: Maybe there has to be a restriction on the monad, like being completely positive?

• I believe this would benefit from a bisimulation and a coinduction tag, but these don't exist. Mar 31, 2016 at 9:13
• I think Monads in general are Trees not just Lists. Could you modify Reed's recursion for tree canonization? Read, Ronald C. (1972), "The coding of various kinds of unlabeled trees", Graph Theory and Computing, Academic Press, New York, pp. 153–182 Apr 2, 2016 at 13:42

• I know that S in my example is a monad. But that's not the question. I'm asking about monadic streams, which are a generalisation of streams. Apr 1, 2016 at 8:32
• (Friendlier version of my original comment.) Thanks, I agree that we're talking past one another. For the purposes of the question, it's irrelevant whether S is a monad or not. Do resumption monad transformers give you any tools for proving equality of two monadic streams? Apr 1, 2016 at 20:53