Behavioural differential equations and coinduction for binary trees

A binary tree T can be encoded as a function from the set of words over the alphabet {0,1} to a set K (corresponding to the information stored in the nodes). If this set K has a semiring structure then T is a formal power series. Following previous work by Rutten, we show how functions with the set of binary trees as codomain can be defined by behavioural differential equations and how we can define a closed formula (only involving constants) to represent (specific) trees. Finally, we discuss how this framework on trees could be used to represent bi-infinite streams.  

hosted by