Typing the Y-combinator - Polymorphism and Functions on Void

Here we discuss these variations, and consequences.

Our sample typing will be Y  (k:. (kT)(k+1)T)T, which could be used to type functions defined by primitive recursion over as we shall exemplify here.
See Polymorphism, Recursive Functions and Void.

Consider this definition of factorial and the use of the Y combinator underlying it.

Def x! == if x=0 1 else x(x-1)! fi  (recursive)

z! * Y((f,x. if x=0 1 else xf(x-1) fi),z)

So factorial is a fixed point of

Thm* (f,x. if x=0 1 else xf(x-1) fi)  (k:. (k)(k+1))

This typing theorem says that this function takes a function with finite domain, and generates a function over a certain one-element extension to that domain. From the above typing for Y,

Thm* Y(f,x. if x=0 1 else xf(x-1) fi)  

would follow trivially from the two typings of Y and the given function.

Now, as indicated by the theorem above, we can still prove this application of Y has type , but examination of the proof actually given would reveal it to be a complex proof involving induction and rewriting, rather than the simple type inference we desire, exploiting the type of Y itself.

How might we prove Y  (k:. (kT)(k+1)T)T? Most of a proof is given HERE; there is only one unproved subgoal:

1. T : Type
2. F : k:. (kT)(k+1)T
  Y(F)  0T

The type 0T is the one-element type of functions over the empty domain (see Void). Our current (standard) primitive definition of a type AB requires that each term of that type must reduce to a "[var].<*>" form. Indeed, if one plugs in an expression of form "f,x. b(f;x)" in place of F, one can simply rewrite

Y(f,x. b(f;x)) * x.b(Y(f,x. b(f;x));x)

then easily type this in 0T. But we do not have this syntactic form in "Y(F)" and so cannot proceed this way.

A direct solution would be to modify the Function Extensionality rule.

CONTINUE

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html