Jiri Adamek ; Stefan Milius ; Jiri Velebil - Semantics of Higher-Order Recursion Schemes

lmcs:1177 - Logical Methods in Computer Science, April 1, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:15)2011
Semantics of Higher-Order Recursion SchemesArticle

Authors: Jiri Adamek ; Stefan Milius ; Jiri Velebil

    Higher-order recursion schemes are recursive equations defining new operations from given ones called "terminals". Every such recursion scheme is proved to have a least interpreted semantics in every Scott's model of \lambda-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite \lambda-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in \lambda-calculus by an endofunctor H\lambda and they explained simultaneous substitution of \lambda-terms by proving that the presheaf of \lambda-terms is an initial H\lambda-monoid. Here we work with the presheaf of rational infinite \lambda-terms and prove that this is an initial iterative H\lambda-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.


    Volume: Volume 7, Issue 1
    Published on: April 1, 2011
    Imported on: January 11, 2010
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory,math.CT

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1529 times.
    This article's PDF has been downloaded 330 times.