A Type of Partial Recursive Functions

11 years 3 months ago
A Type of Partial Recursive Functions
We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises the traces of the computation of the function. The structure of a prophecy is a possibly infinite tree, which is coerced by linearisation to a type of partial results defined by applying the delay monad to the co-domain of the function. Using induction on a weight relation defined on the prophecies, we can reason about them and prove that the formal type-theoretic version of the recursive function, resulting from the present method, satisfies the recursive equations of the original function. The advantages of this technique over the method previously developed by the authors via a special-purpose accessibility (domain) predicate are: there is no need of extra logical arguments in the definition of the recursive function; the function can be applied to any element in its domain, regardless of termination...
Ana Bove, Venanzio Capretta
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Authors Ana Bove, Venanzio Capretta
Comments (0)