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
1) M is strongly normalizable;
2) M is not typable in the type inference system F_omega, as described
e.g. in .
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  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.
 Giannini, P., Ronchi Della Rocca, S., in: Proc. LiCS'88
Pawel Urzyczyn (after October 1: email@example.com)