Semantics of Higher-Order Recursion Schemes
The result's identifiers
Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Semantics of Higher-Order Recursion Schemes
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
BA - General mathematics
OECD FORD branch
—
Result continuities
Project
—
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2009
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS
ISBN
978-3-642-03740-5
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
—
Publisher name
Centre International des Sciences Mechaniques
Place of publication
Udine
Event location
Udine
Event date
Oct 7, 2009
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000270321400005