I asked this question in another location, but perhaps this is a better palce. It&#39;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<br>
<br><div style="margin-left: 40px;">T a = T a [T a]<br>N a = N (T [N a])<br><br></div>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?<br>
<div style="margin-left: 40px;"><br></div>