Semantics of Higher-Order Recursion Schemes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F09%3A00160001" target="_blank" >RIV/68407700:21230/09:00160001 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

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 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 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. Whereas Fiore et al proved that the presheaf F of lambda-terms is an initial H-monoid, we work with the presheaf R 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 R.

Název v anglickém jazyce

Semantics of Higher-Order Recursion Schemes

Popis výsledku anglicky

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 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. Whereas Fiore et al proved that the presheaf F of lambda-terms is an initial H-monoid, we work with the presheaf R 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 R.

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

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ů

Název statě ve sborníku

ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS

ISBN

978-3-642-03740-5

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

Centre International des Sciences Mechaniques

Místo vydání

Udine

Místo konání akce

Udine

Datum konání akce

7. 10. 2009

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000270321400005