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
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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)