Cited By
View all- Tarau Pde Paiva V(2020)Deriving Theorems in Implicational Linear Logic, DeclarativelyElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.325.18325(110-123)Online publication date: 19-Sep-2020
Quantitative Aspects of Linear and Affine Closed Lambda Terms
Article No.: 9, Pages 1 - 18
Abstract
Affine λ-terms are λ-terms in which each bound variable occurs at most once, and linear λ-terms are λ-terms in which each bound variable occurs once and only once. In this article, we count the number of affine closed λ-terms of size n, linear closed λ-terms of size n, affine closed β-normal forms of size n, and linear closed β-normal forms of size n, for several measures of the size of λ-terms. From these formulas, we show how we can derive programs for generating all the terms of size n for each class. The foundation of all of this is a specific data structure, made of contexts in which one counts all the holes at each level of abstractions by λ’s.
References
[1]
Henk P. Barendregt. 1984. The Lambda-Calculus, Its Syntax and Semantics (2nd ed.). Elsevier Science Publishers B. V. (North-Holland), Amsterdam.
[2]
Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. 2016. Combinatorics of λ-terms: A natural approach. CoRR abs/1609.07593 (2016). http://arxiv.org/abs/1609.07593
[3]
Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. 2016. A natural counting of lambda terms. In SOFSEM 2016: Theory and Practice of Computer Science—42nd International Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 23-28, 2016, Proceedings (Lecture Notes in Computer Science), Vol. 9587, eds. Rusins Martins Freivalds, Gregor Engels, and Barbara Catania. Springer, 183--194.
[4]
Maciej Bendkowski, Katarzyna Grygiel, and Paul Tarau. 2017. Boltzmann samplers for closed simply-typed lambda terms. In Practical Aspects of Declarative Languages—19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings (Lecture Notes in Computer Science), Vol. 10137, eds.Yuliya Lierler and Walid Taha. Springer, 120--135.
[5]
Olivier Bodini, Danièle Gardy, and Bernhard Gittenberger. 2011. Lambda terms of bounded unary height. In Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics. 23--32. http://www.siam.org/proceedings/analco/2011/anl11_03_bodinio.pdf.
[6]
Olivier Bodini, Danièle Gardy, Bernhard Gittenberger, and Alice Jacquot. 2013. Enumeration of generalized BCI lambda-terms. Electr. J. Comb. 20, 4 (2013), P30. http://www.combinatorics.org/ojs/index.php/eljc/article/view/v20i4p30.
[7]
Olivier Bodini, Danièle Gardy, and Alice Jacquot. 2013. Asymptotics and random sampling for BCI and BCK lambda terms. Theor. Comput. Sci. 502 (2013), 227--238.
[8]
Olivier Bodini, Bernhard Gittenberger, and Zbigniew Gołȩbiewski. 2017. Enumerating lambda terms by weighted length of their de Bruijn representation. CoRR (2017).
[9]
Alonzo Church. 1940. A formulation of the simple theory of types. J. Symb. Log. 5 (1940), 56--68.
[10]
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). The MIT Press.
[11]
René David, Christophe Raffalli, Guillaume Theyssier, Katarzyna Grygiel, Jakub Kozik, and Marek Zaionc. 2009. Some properties of random lambda terms. Log. Methods Comput. Sci. 9, 1 (2009).
[12]
Nicolaas G. de Bruijn. 1972. Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. Koninkl. Nederl. Akademie van Wetenschappen 75, 5 (1972), 381--392.
[13]
Philippe Flajolet and Robert Sedgewick. 2008. Analytic Combinatorics. Cambridge University Press.
[14]
Bernhard Gittenberger and Zbigniew Gołȩbiewski. 2016. On the number of lambda terms with prescribed size of their de Bruijn representation. In 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France (LIPIcs), Vol. 47, eds. Nicolas Ollinger and Heribert Vollmer. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, 40:1--40:13.
[15]
Katarzyna Grygiel, Pawel M. Idziak, and Marek Zaionc. 2013. How big is BCI fragment of BCK logic. J. Log. Comput. 23, 3 (2013), 673--691.
[16]
Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and generating lambda terms. J. Funct. Program. 23, 5 (2013), 594--628.
[17]
Katarzyna Grygiel and Pierre Lescanne. 2015. Counting and generating terms in the binary lambda calculus. J. Funct. Program. 25 (2015).
[18]
J. Roger Hindley. 1989. BCK-Combinators and linear lambda-terms have types. Theor. Comput. Sci. 64, 1 (1989), 97--105.
[19]
J. Roger Hindley. 1997. Basic Simple Type Theory, Vol. 42: Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
[20]
Zofia Kostrzycka and Marek Zaionc. 2004. Statistics of intuitionistic versus classical logics. Stud. Log. 76, 3 (2004), 307--328.
[21]
Pierre Lescanne. 2013. On counting untyped lambda terms. Theor. Comput. Sci. 474 (2013), 80--97.
[22]
Pierre Lescanne. 2014. Boltzmann samplers for random generation of lambda terms. CoRR abs/1404.3875 (2014). http://arxiv.org/abs/1404.3875
[23]
John Tromp. 2006. Binary lambda calculus and combinatory logic. In Kolmogorov Complexity and Applications (Dagstuhl Seminar Proceedings), Vol. 06051, eds. Marcus Hutter, Wolfgang Merkle, and Paul M. B. Vitányi. Internationales Begegnungs—und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.
[24]
Marek Zaionc. 2005. On the asymptotic density of tautologies in logic of implication and negation. Rep. Math. Log. 39 (2005), 67--87. http://www.iphils.uj.edu.pl/rml/rml-39/a-zai-39.htm.
[25]
Marek Zaionc. 2006. Probability distribution for simple tautologies. Theor. Comput. Sci. 355, 2 (2006), 243--260.
[26]
Noam Zeilberger. 2015. Counting isomorphism classes of β-normal linear lambda terms. ArXiv abs/1509.07596 (2015). http://arxiv.org/abs/1509.07596.
[27]
Noam Zeilberger. 2016. Linear lambda terms as invariants of rooted trivalent maps. J. Funct. Program. 26 (2016), e21.
[28]
Noam Zeilberger and Alain Giorgetti. 2015. A correspondence between rooted planar maps and normal planar lambda terms. Log. Methods Comput. Sci. 11, 3 (2015).
Index Terms
- Quantitative Aspects of Linear and Affine Closed Lambda Terms
Recommendations
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer ApplicationsThe Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...
On counting untyped lambda terms
Despite @l-calculus is now three quarters of a century old, no formula counting @l-terms has been proposed yet, and the combinatorics of @l-calculus is considered a hard problem. The difficulty lies in the fact that the recursive expression of the ...
Infinitary Lambda Calculi from a Linear Perspective
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceWe introduce a linear infinitary λ-calculus, called ℓΛ∞, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the ...
Comments
Information & Contributors
Information
Published In
April 2018
275 pages
Copyright © 2018 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 28 June 2018
Accepted: 01 December 2017
Revised: 01 September 2017
Received: 01 April 2017
Published in TOCL Volume 19, Issue 2
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 74Total Downloads
- Downloads (Last 12 months)3
- Downloads (Last 6 weeks)1
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
Cited By
View all- Tarau Pde Paiva V(2020)Deriving Theorems in Implicational Linear Logic, DeclarativelyElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.325.18325(110-123)Online publication date: 19-Sep-2020
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in