On Sat, Mar 5, 2011 at 2:32 AM, dan portin
Actually, let me rephrase the question. I know that a relation R over streams is a bisimulation if, for all lists l1 and l2, (a) their heads are equal and their tails are in the relation R, or (b) both l1 and l2 are empty. Similarly, I know that a relation R over in binary trees is a bisimulation if, for all trees t1 and t2, the values at the root node of t1 and t2 are equal, and the left and right subtrees of t1 and t2 are in the relation R. From the definition of a bisimulation, the conditions for a relation R over types constructed from arrow, cross, and so on, is easy to derive.
However, suppose I have a data type
data N a = N a [N a]
By analogy, I might suppose that a relation R over trees t1 and t2 of type N a is a bisimulation if (a) the values at their root node are equal, and (b) their forests are equal. However, proving equality using this definition can lead to a circular proof. For instance, it might be the case that the values at the roots of t1 and t2 are equal, but that the head of the forests of t1 and t2 are, again, t1 and t2! (that is, assume T(t1,t2), and if their root values are equal, show that their forests are equal; if each is an infinite list, show that their heads are equal, but perhaps their heads are t1 and t2!). So I am slightly confused as to how equality of such types can be proved by the bisimulation method. In fact, I'm confused as to what the appropriate conditions are!
I don't really know much about bisimulations, so I may be missing the point or going into the wrong direction. So read this e-mail with a grain of salt =). Your N data type isn't the only one that may have some weird infinite recursion. Consider let xs = 1 : ys ys = 1 : xs To prove that xs and ys are on a relation R, you have to proove that ys and xs are on a relation R. Oops! As I said, I don't know much about bisimulations. However, you don't seem to think that there is a problem with xs/ys defined as above. So I am tempted to read your definition of a bisimulation on lists as some form of induction. Being explicit, let's define R_0 = { ([], []) } as the relation with only the empty list and R_{n+1} = R_n ∪ { (x:s, x:t) | s, t ∈ R_n, x ∈ ℕ } Now, (xs, ys) ∉ R_n for all n ∈ ℕ, as R_n contains lists of at most length n, and xs/ys have infinite length. However, (xs, ys) ∈ R_ω, where ω = |ℕ| is the first ordinal. In a real machine we only have finite time, so we can't (in general) know for sure that (xs, ys) ∈ R. Well, the same thing happens when you consider your N data type. If you have let t1 = N 1 [t1, t2] t2 = N 1 [t2, t1] then you can't know for sure in finite time in a machine in general that (t1, t2) ∈ R, however you can given infinite countable time ω. I hope that helps you to answer at least a little bit of your question =). -- Felipe.