| Several recent programming languages, for example Python, C;Capsules, by their coinductive nature, also provide a clean internal representation of coalgebraic datatypes. Recursive functions defined on a such coalgebraic datatypes 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. Unfortunately, current functional programming languages provide no support for specifying alternative solution methods. There are numerous examples in which it would be useful to do so: free variables, alpha-conversion, and substitution in infinitary lambda-terms; halting probabilities and expected running times of probabilistic protocols; abstract interpretation; and constructions involving finite automata. In each case the function would diverge under the standard semantics of recursion. In this dissertation, we first prove some theoretical results characterizing the well-founded case. We then propose programming language constructs that allow the specification of alternative solutions and methods to compute them. Finally, we introduce CoCaml, a functional programming language extending OCaml that implements those constructs and allows the programmer to define functions on coinductive datatypes parameterized by an equation solver. |
