General Recursion via Coinductive Types

TL;DR

This paper introduces a novel approach to modeling general recursive functions in type theories using coinductive types, enabling the formalization of infinite computations and fixed points.

Contribution

It proposes using coinductive types to represent partial elements and model infinite computations, offering an alternative to traditional methods in recursive function formalization.

Findings

Partial(A) types can model infinite computations.

Fixed points of continuous operators are definable.

The approach defines a strong monad structure.

Abstract

A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.