Checking equivalence of corecursive streams: An inductive procedure

In recent work, non-periodic streams have been defined corecursively, by representing them with finitary equational systems built on top of various operators, besides the standard constructor. When only the stream constructor is allowed in equations, only periodic streams can be represented, and the structures of periodic streams and infinite regular trees are isomorphic. Therefore, one can use the theory of regular trees to get a sound and complete procedure to decide whether two equational systems are equivalent, that is, define the same streams. However, such an isomorphism no longer exists if one allows other operators in equations; in particular, there exist systems of equations which have the same unique solution as streams, but not as regular trees. Hence, equality of regular trees becomes stronger then equality of streams, with a negative impact on termination of functions whose definition is based on the equivalence of the representation of streams as finitary equational systems. To overcome this problem, we provide a weaker definition of equivalence, and prove its soundness and relative completeness. This definition is coinductive, hence non-algorithmic. However, we show that it can be turned into an equivalent inductive procedure.