Venanzio Capretta - General Recursion via Coinductive Types

lmcs:2265 - Logical Methods in Computer Science, July 13, 2005, Volume 1, Issue 2 - https://doi.org/10.2168/LMCS-1(2:1)2005
General Recursion via Coinductive Types

Authors: Venanzio Capretta ORCID-iD

    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.


    Volume: Volume 1, Issue 2
    Published on: July 13, 2005
    Submitted on: December 22, 2004
    Keywords: Computer Science - Logic in Computer Science,F.3.1

    Linked data

    Source : ScholeXplorer References DOI 10.1007/3-540-44755-5_10
    • 10.1007/3-540-44755-5_10
    Nested General Recursion and Partiality in Type Theory
    Venanzio Capretta ; Ana Bove ;

    67 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 612 times.
    This article's PDF has been downloaded 464 times.