Semantics of higher-order recursion schemes
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F11%3A00179796" target="_blank" >RIV/68407700:21230/11:00179796 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.2168/LMCS-7(1:15)2011" target="_blank" >http://dx.doi.org/10.2168/LMCS-7(1:15)2011</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.2168/LMCS-7(1:15)2011" target="_blank" >10.2168/LMCS-7(1:15)2011</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Semantics of higher-order recursion schemes
Popis výsledku v původním jazyce
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 terminalsare 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. Fioreet al showed how to capture the type of variable binding in lambda-calculus by an endofunctor H and they explained simultaneous substitution of lambda-terms by proving that the presheaf of lambda-terms is an initial H-monoid. Here we work with the presheaf of rational infinite lambda-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 this monoid.
Název v anglickém jazyce
Semantics of higher-order recursion schemes
Popis výsledku anglicky
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 terminalsare 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. Fioreet al showed how to capture the type of variable binding in lambda-calculus by an endofunctor H and they explained simultaneous substitution of lambda-terms by proving that the presheaf of lambda-terms is an initial H-monoid. Here we work with the presheaf of rational infinite lambda-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 this monoid.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
BA - Obecná matematika
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2011
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Logical Methods in Computer Science
ISSN
1860-5974
e-ISSN
—
Svazek periodika
2011
Číslo periodika v rámci svazku
7
Stát vydavatele periodika
DE - Spolková republika Německo
Počet stran výsledku
43
Strana od-do
1-43
Kód UT WoS článku
000290278900015
EID výsledku v databázi Scopus
—