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.

The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.

We describe an inductive abstract semantics for coFJ, a Java-like calculus where, when the same method call is encountered twice, non-termination is avoided, and the programmer can decide the behaviour in this case, by writing a codefinition. The proposed semantics is abstract in the sense that evaluation is non-deterministic, and objects are possibly infinite. However, differently from typical coinductive handling of infinite values, the semantics is inductive, since it relies on detection of cyclic calls. Whereas soundness with respect to the reference coinductive semantics has already been proved, we conjecture that completeness with respect to the regular subset of such semantics holds as well. This relies on the fact that in the proposed semantics detection of cycles is non-deterministic, that is, does not necessarily happens the first time a cycle is found.