科研之友
微信
新浪微博
Facebook
分享链接
摘要
It is well known that simply typed lambda-terms can be used to represent numbers, as well as some other data types. We show that lambda-terms of each fixed (but possibly very complicated) type can be described by a finite piece of information (a set of appropriately defined intersection types) and by a vector of natural numbers. On the one hand, the description is compositional: having only the finite piece of information for two closed lambda-terms M and N, we can determine its counterpart for MN, and a linear transformation that applied to the vectors of numbers for M and N gives us the vector for MN. On the other hand, when a lambda-term represents a natural number, then this number is approximated by a number in the vector corresponding to this lambda-term. As a consequence, we prove that 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. More precisely, while representing k numbers in a closed lambda-term of some type, we only require that there are k closed lambda-terms M-1,..., M-k such that M-i takes as argument the lambda-term representing the k-tuple, and returns the i-th number in the tuple (we do not require that, using lambda-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). All the results remain true when we allow the Y combinator (recursion) in our lambda-terms, as well as uninterpreted constants.
- 出版日期2016
