[Haskell-beginners] Nested data types and bisimilarity

[Felipe Almeida Lessa]

On Sat, Mar 5, 2011 at 2:32 AM, dan portin <danportin at gmail.com> wrote:
> 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.