10.2168/LMCS-7(1:15)2011
https://lmcs.episciences.org/1177
Adamek, Jiri
Jiri
Adamek
Milius, Stefan
Stefan
Milius
Velebil, Jiri
Jiri
Velebil
Semantics of Higher-Order Recursion Schemes
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.
episciences.org
Computer Science - Logic in Computer Science
Mathematics - Category Theory
math.CT
2015-06-25
2011-04-01
2011-04-01
eng
journal article
arXiv:1101.4929
10.48550/arXiv.1101.4929
1860-5974
https://lmcs.episciences.org/1177/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 7, Issue 1
Researchers
Students