Bisimulations Generated from Corecursive Equations

We consider the problem of determining the unicity of solutions for corecursive equations. This can be done by transforming the equations into a guarded form, that is, representing them as a coalgebra. However, in some examples this transformation is very hard to achieve. On the other hand, mere unicity of solutions can be determined independently by constructing a bisimulation relation. The relation is defined inductively by successive steps of reduction of the body of the equation and abstraction of the recursive calls. The algorithm is not complete: it may terminate successfully, in which case unicity is proved; it may terminate with a negative answer, in which case no bisimulation could be constructed; or it may run forever. If it diverges, the inductively defined relation is in fact a bisimulation and unicity obtains. However, we cannot decide whether the algorithm will run forever or not.