東京大学の小林と申します。
以下のように、ワルシャワ大学のPawel Parys氏を招いて講演会を開催しますので、 ふるってご参加ください。 Parysさんは、ここ数年、高階文法、高階プッシュダウンオートマトンなどについて 未解決問題を解いたりしてよい仕事をされている方です
小林直樹 東京大学大学院情報理工学系研究科コンピュータ科学専攻 〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: [email protected]
---------------------------------- Time: 2月18日（水） 15:00〜 Place: 理学部7号館 214号室
Title: A Characterization of Lambda-terms Transforming Numbers
Speaker: Pawel Parys (Warsaw University)
Abstract: 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 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 M1,...,Mk such that Mi 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.