[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)