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