episciences.org_1177_1652937429
1652937429
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
18605974
04
01
2011
Volume 7, Issue 1
Semantics of HigherOrder Recursion Schemes
Jiri
Adamek
Stefan
Milius
Jiri
Velebil
Higherorder 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
\lambdacalculus in which the terminals are interpreted as continuous
operations. For the uninterpreted semantics based on infinite \lambdaterms 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 \lambdacalculus by an
endofunctor H\lambda and they explained simultaneous substitution of
\lambdaterms by proving that the presheaf of \lambdaterms is an initial
H\lambdamonoid. Here we work with the presheaf of rational infinite
\lambdaterms and prove that this is an initial iterative H\lambdamonoid. We
conclude that every guarded higherorder recursion scheme has a unique
uninterpreted solution in this monoid.
04
01
2011
1177
arXiv:1101.4929
10.48550/arXiv.1101.4929
10.2168/LMCS7(1:15)2011
https://lmcs.episciences.org/1177

https://lmcs.episciences.org/1177/pdf