Language Constructs for Non-Well-Founded Computation

Recursive functions defined on a coalgebraic datatype C may not converge if there are cycles in the input, that is, if the input object is not well-founded. Even so, there is often a useful solution; for example, the free variables of an infinitary λ-term, or the expected running time of a finite-state probabilistic protocol. Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras [2], corecursive algebras [4], and Elgot algebras [1]. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when C is well-founded. If C is not well-founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, namely the least solution in a flat Scott domain, which may not be the one we want. Unfortunately, current programming languages provide no support for specifying alternatives. In this paper we give numerous examples in which it would be useful to do so: free variables, α-conversion, and substitution in infinitary terms; halting probabilities, expected running times, and outcome functions of probabilistic protocols; various functions on streams; semantics of alternating automata and games; and ab- stract interpretation. In each case the function would diverge under the standard semantics of recursion. We propose programming lan- guage constructs that would allow the specification of alternative solutions and methods to compute them. The programmer must es- sentially provide a way to solve equations in the codomain. We show how to implement these new constructs as an extension of OCaml and give implementations of all our examples. In some cases, some of the work can be automated. We also prove some theoretical results characterizing well- founded coalgebras that slightly extend results of Adamek, Luecke, and Milius [2].