Finitary Corecursion for the Infinitary Lambda Calculus
2015
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.
Keywords:
- Correction
- Cite
- Save
- Machine Reading By IdeaReader
1
References
0
Citations
NaN
KQI