How Many Numbers Can a Lambda-term Contain?

It is well known that simply-typed lambda-terms can be used to represent natural numbers, as well as some other data types. Of course there exist higher-order functions containing arbitrarily many numbers, like g ( f ) = n 1 + f ( n 2 + f ( n 3 + f (⋯ + f ( n k )⋯))). If we want to know precisely the result of our function g for each f, we need to remember each n 1, …, n k separately. If, however, we allow approximation of the result up to some error, the situation changes dramatically. In this paper we consider the domination-equivalence relation, widely used e. g. in the context of regular cost functions: two functions are domination-equivalent if for each set of arguments X, one function is bounded if and only if the second function is bounded. We prove that, modulo this equivalence relation, for each type there exist only finitely many shapes of functions, and for each of them we need to specify only a fixed number of constants appearing in the function. For example, our function g, assuming that all n 1, …, n k are positive, is equivalent to g '( f ) = n 1 + f ( m ), where m = n 2 +⋯+ n k. As a consequence, we obtain a result concerning representation of tuples in lambda-terms. We know that pairs or tuples of natural numbers can be represented in lambda-terms. Notice, however, that, in the standard implementation, the type of terms representing k -tuples of numbers depends on k. From our result it follows that, indeed, in a lambda-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 lambda-terms. 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). Our results hold as well when we consider the lambda-Y-calculus, that is when we add the Y combinator to our syntax, introducing infinite recursion.

Authors

• Pawel Parys

Keywords

No keywords are indexed for this paper.