[Haskell-beginners] Nested data types and bisimilarity

[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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20110304/344c4f16/attachment-0001.htm>