arXiv · 1505.07736
Finitary Corecursion for the Infinitary Lambda Calculus
Abstract
Kurz et al. have recently shown that infinite $\lambda$-trees with finitely many free variables modulo $\alpha$-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational $\lambda$-trees, i.e. those $\lambda$-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational $\lambda$-trees.
Explore related subjects
Keep this discovery
Stefan Milius, Thorsten Wißmann. 2015-05-28. Finitary Corecursion for the Infinitary Lambda Calculus. https://arxiv.org/abs/1505.07736
Cite the original work for its findings. Save a collection to share your selection of sources.