[Haskell-beginners] Nested data types and bisimilarity

[Brent Yorgey]

On Sat, Mar 05, 2011 at 02:51:46AM +0000, Felipe Almeida Lessa wrote:
> 
> 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!

Actually, you are missing the point. ;)  The point of bisimulations is
that they are defined *coinductively*, so they let you work with
potentially infinite data structures.  In your example, proving that
xs and ys are in the relation R really is that simple -- 1 = 1, and
then to complete the proof we are allowed to use the coinduction
hypothesis that xs and ys are in the relation R, since they are
guarded by a constructor (:).  

Dan, does this help answer your original question?  If not I can try
to give a more detailed answer in the morning.

-Brent