We consider the problem of formalizing general recursive functions in intensional type theory. The proposed solution exploit coinductive types to model infinite computations. Every type A is associated to 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.
展开▼
