Abstract
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).
Chapter PDF
References
Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65–116. Addison-Wesley (1990)
Abramsky, S., Luke Ong, C.-H.: Full abstraction in the lazy lambda calculus. Inform. and Comput. 105(2), 159–267 (1993)
Adámek, J.: On final coalgebras of continuous functors. Theor. Comput. Sci. 294(1/2), 3–29 (2003)
Arnold, A., Nivat, M.: The metric space of infinite trees. algebraic and topological properties. Fundamenta Informaticae 4, 445–476 (1980)
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, Revised edition. North-Holland, Amsterdam (1984)
Barr, M.: Terminal coalgebras for endofunctors on sets. Theor. Comp. Sci. 114(2), 299–315 (1999)
Berarducci, A.: Infinite λ-calculus and non-sensible models. In: Logic and Algebra (Pontignano, 1994), pp. 339–377. Dekker, New York (1996)
Cheney, J.: Completeness and Herbrand theorems for nominal logic. J. Symb. Log. 71(1), 299–320 (2006)
Duppen, Y.D.: A coalgebraic approach to lambda calculus. Master’s thesis, Vrije Universiteit Amsterdam (2000)
Fernández, M., Gabbay, M.: Nominal rewriting. Inf. Comput. 205(6), 917–965 (2007)
Gabbay, M., Pitts, A.M.: A new approach to abstract syntax involving binders. In: LICS, pp. 214–224 (1999)
Gabbay, M.J.: A general mathematics of names. Inf. Comput. 205(7), 982–1011 (2007)
Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: Equational logic with names and binding. J. Log. Comput. 19(6), 1455–1508 (2009)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13(3–5), 341–363 (2001)
Kennaway, J.R., de Vries, F.J.: Infinitary rewriting. In: Terese (ed.) Term Rewriting Systems. Cambridge Tracts in Theor. Comp. Sci, vol. 55, pp. 668–711. Cambridge University Press (2003)
Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Infinite Lambda Calculus and Böhm Models. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 257–270. Springer, Heidelberg (1995)
Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Infinitary lambda calculus. Theor. Comp. Sci. 175(1), 93–125 (1997)
Lévy, J.-J.: An algebraic interpretation of the λβK-calculus, and an application of a labelled λ-calculus. Theor. Comp. Sci. 2(1), 97–114 (1976)
Longo, G.: Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Ann. Pure Appl. Logic 24(2), 153–188 (1983)
Matthes, R., Uustalu, T.: Substitution in non-wellfounded syntax with variable binding. Theor. Comput. Sci. 327, 155–174 (2004)
Moss, L.S.: Parametric corecursion. Theor. Comp. Sci. 260, 139–163 (2001)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Pitts, A.M.: Alpha-Structural Recursion and Induction. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 17–34. Springer, Heidelberg (2005)
Salibra, A.: Nonmodularity results for lambda calculus. Fundamenta Informaticae 45, 379–392 (2001)
Severi, P.G., de Vries, F.J.: Weakening the axiom of overlap in the infinitary lambda calculus. In: RTA. LIPIcs, vol. 10, pp. 313–328. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kurz, A., Petrişan, D., Severi, P., de Vries, FJ. (2012). An Alpha-Corecursion Principle for the Infinitary Lambda Calculus. In: Pattinson, D., Schröder, L. (eds) Coalgebraic Methods in Computer Science. CMCS 2012. Lecture Notes in Computer Science, vol 7399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32784-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-32784-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32783-4
Online ISBN: 978-3-642-32784-1
eBook Packages: Computer ScienceComputer Science (R0)