It is well known, that simply-typed λ-terms can be used to represent numbers, as well as some other data types. We prove, however, that in a λ-term of a fixed type we can store only a fixed number of natural numbers, in such a way that they can be extracted using λ-terms. More precisely, while representing k numbers in a closed λ-term of some type we only require that there are k closed λ-terms M 1,...,M k such that Mi takes as argument the λ-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using λ-calculus, one can construct the representation of the k-tuple out of the k numbers in the tuple). Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not). © 2014 Springer International Publishing.
CITATION STYLE
Parys, P. (2014). How many numbers can a lambda-term contain? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8475 LNCS, pp. 302–318). Springer Verlag. https://doi.org/10.1007/978-3-319-07151-0_19
Mendeley helps you to discover research relevant for your work.