Corecursion is the ability of defining a function that produces some infinite data in terms of the function and the data itself, as supported by lazy evaluation. However, in languages such as Haskell strict operations fail to terminate even on infinite regular data, that is, cyclic data. Regular corecursion is naturally supported by coinductive Prolog, an extension where predicates can be interpreted either inductively or coinductively, that has proved to be useful for formal verification, static analysis and symbolic evaluation of programs. In this paper we use the meta-programming facilities offered by Prolog to propose extensions to coinductive Prolog aiming to make regular corecursion more expressive and easier to program with. First, we propose an interpreter where the search tree is pruned to guarantee termination for certain kinds of predicate definition; then we introduce finally clauses, to provide a default value for all those cases where unification with a coinductive hypothesis is not correct. Finally, we propose a finer grain semantics where the user can specify only a subset of the arguments that have to be considered when coinductive hypotheses are unified. The semantics defined by these vanilla meta-interpreters are an interesting starting point for a more mature design and implementation of coinductive Prolog.

Co-recursion is the ability of defining a function that produces some infinite data in terms of the function and the data itself, and is typically supported by languages with lazy evaluation. However, in languages as Haskell strict operations fail to terminate even on infinite regular data. Regular co-recursion is naturally supported by co-inductive Prolog, an extension where predicates can be interpreted either inductively or co-inductively, that has proved to be useful for formal verification, static analysis and symbolic evaluation of programs. In this paper we propose two main alternative vanilla meta-interpreters to support regular co-recursion in Prolog as an interesting programming style in its own right, able to elegantly solve problems that would require more complex code if conventional recursion were used. In particular, the second meta-interpreters avoids non termination in several cases, by restricting the set of possible answers. The semantics defined by these vanilla meta-interpreters are an interesting starting point to study new semantics able to support regular co-recursion for non logical languages.

Corecursive FeatherWeight Java (coFJ) is a recently proposed extension of the calculus FeatherWeight Java (FJ), supporting cyclic objects and regular recursion, and explicitly designed to promote a novel programming paradigm inspired by coinductive Logic Programming (coLP), based on coinductive, rather than inductive, interpretation of recursive function definitions. We present a slightly modified version of coFJ where the application of a coinductive hypothesis can trigger the evaluation of a specific expression at declaration, rather than at use site. Following an approach inspired by abstract compilation, we then show how coFJ can be directly translated into coLP, when coinductive SLD is extended with a similar feature for explicitly solving a goal when a coinductive hypothesis is applied. Such a translation is quite compact and, besides showing the direct relation between coFJ and coinductive Prolog, provides a first prototypical but simple and effective implementation of coFJ.

Despite cyclic data structures occur often in many application domains, object-oriented programming languages provide poor abstraction mechanisms for dealing with cyclic objects. Such a deficiency is reflected also in the research on theoretical foundation of object-oriented languages; for instance, Featherweigh Java (FJ), which is one of the most widespread object-oriented calculi, does not allow creation and manipulation of cyclic objects. We propose an extension to Featherweight Java, called coFJ, where it is possible to define cyclic objects, {abstractly corresponding to regular terms}, and where an abstraction mechanism, called regular corecursion, is provided for supporting implementation of coinductive operations on cyclic objects. We formally define the operational semantics of coFJ, and provide a handful of examples showing the expressive power of regular corecursion; such a mechanism promotes a novel programming style particularly well-suited for implementing cyclic data structures, and for supporting coinductive reasoning.