[Prev][Next][Index][Thread]
Typability in F_omega
Date: Thu, 26 Sep 91 17:42:30 -0400
The following is an example of a pure lambda term M of the following
properties:
1) M is strongly normalizable;
2) M is not typable in the type inference system F_omega, as described
e.g. in [1].
To my best knowledge this is the first example known to have these properties.
Terms known to be SN but not typable in F, like that of [1] or the term 22K
(2 is the Church numeral 2) are typable in the lowest nontrivial level of
F_omega, i.e., with constructors of rank 1 (functions from types to types).
I do not know any examples separating the levels of F_omega. Does anybody?
The term M is \z.((\x.z(x1)(xJ))(\y.yyy)), where "\" is lambda and:
1 is \fu.fu (the Church numeral 1);
J is \uf.fu.
[1] Giannini, P., Ronchi Della Rocca, S., in: Proc. LiCS'88
Pawel Urzyczyn (after October 1: urzy@plearn.bitnet)