[logic-ml] 講演会(Pawel Parys氏）

[koba]

東京大学の小林と申します。

以下のように、ワルシャワ大学のPawel Parys氏を招いて講演会を開催しますので、
ふるってご参加ください。
Parysさんは、ここ数年、高階文法、高階プッシュダウンオートマトンなどについて
未解決問題を解いたりしてよい仕事をされている方です

小林直樹
東京大学大学院情報理工学系研究科コンピュータ科学専攻
〒113-0033 東京都文京区本郷7-3-1
Phone: 03-5841-4124
Fax: 03-5841-4124
email: koba at is.s.u-tokyo.ac.jp



----------------------------------
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.