%0 Conference Proceedings
%T An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
%+ Department of Computer Science
%A Kurz, Alexander
%A Petrişan, Daniela
%A Severi, Paula
%A Vries, Fer-Jan, De
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS)
%C Tallinn, Estonia
%Y Dirk Pattinson
%Y Lutz Schröder
%I Springer
%3 Coalgebraic Methods in Computer Science
%V LNCS-7399
%P 130-149
%8 2012-03-31
%D 2012
%R 10.1007/978-3-642-32784-1_8
%Z Computer Science [cs]Conference papers
%X Gabbay and Pitts proved that lambda-terms up to alpha-equivalence constitute an initial algebra for a certain endofunctor on the category of nominal sets. We show that the terms of the infinitary lambda-calculus form the final coalgebra for the same functor. This allows us to give a corecursion principle for alpha-equivalence classes of finite and infinite terms. As an application, we give corecursive definitions of substitution and of infinite normal forms (Böhm, Lévy-Longo and Berarducci trees).
%G English
%2 https://inria.hal.science/hal-01539877/document
%2 https://inria.hal.science/hal-01539877/file/978-3-642-32784-1_8_Chapter.pdf
%L hal-01539877
%U https://inria.hal.science/hal-01539877
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-CMCS
%~ IFIP-LNCS-7399
%~ IFIP-ETAPS