
4 Mar
2011
4 Mar
'11
9:04 p.m.
I asked this question in another location, but perhaps this is a better palce. It's unclear to me how conditions for a relation to be a bisimulation on nested data types can be generated. I understand, by analogy with streams and binary trees, how to define such conditions for regular types. However, consider the types T a = T a [T a] N a = N (T [N a]) and a relation R over then. What conditions must be fulfilled for R to a bisimulation? In particular, how is the nesting of a list (or tree) dealt with?