Semantics of Higher-Order Recursion Schemes

Higher-order recursion schemes are equations defining recursively 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 λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-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. Whereas Fiore et al proved that the presheaf Fλ of λterms is an initial Hλ-monoid, we work with the presheaf Rλ of rational infinite λ-terms and prove that this is an initial iterative Hλ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in Rλ. Key Words: Higher-order recursion schemes, infinite λ-terms, sets in context, rational tree

• Type: Conference
• Year: 2009
• Where: CALCO
• Authors: Jirí Adámek, Stefan Milius, Jiri Velebil
• Keywords: CALCO 2009, Interpreted Semantics, Infinite λ-terms, Mathematics, Recursion Schemes