[Haskell-beginners] Nested data types and bisimilarity
Brent Yorgey
byorgey at seas.upenn.edu
Sat Mar 5 05:40:44 CET 2011
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
More information about the Beginners
mailing list