Typing the Y-combinator - continued from Typing Y

"(k:. (kT)(k+1)T)T"

"Y(F)  0T"

The difficulty of doing so is indicated in Typing Y, where it was also suggested that we might modify the Function Extensionality rule to achieve this typing.

The current Function Extensionality rule permits inferences of the form:

  f = g  AB

from
1. x : A
  f(x) = g(x)  B,

  A  Type,   f  CD, and   g  EF

The last two subgoals serve merely to require that f and g reduce to "[var].<*>" forms.

Suppose we were to use a different primitive definition of AB, stipulating for type AB, t1 = t2  AB just when

for any expressions r1 and r2, if r1 = r2  A then t1(r1) = t2(r2)  B.

This definition was taken from Function Types and simplified. Then in the case that A is empty, every closed term has type AB. (See Void.)

The only obstacle to adopting this definition would appear to be the a priori desire that every value of every type should evaluate to some canonical form. It should be noted that users of standard Nuprl have already implicitly abandoned this presumption by adopting the Intersection Types. All the current standard rules would remain valid under this new primitive definition of function types (how to generalize it to dependent types is obvious). In addition a new, more liberal Function Extensionality rule should then be adopted, allowing inference to

  f = g  AB

simply from from

1. x : A
  f(x) = g(x)  B, and

  A  Type.

The proof of Y  (k:. (kT)(k+1)T) would then be quite simple to complete by proving the sole remaining subgoal

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

using the new rule, since

1. T : Type 2. F : k:. (kT)(k+1)T 3. x : 0 Y(F,x) T by Auto

and

1. T : Type 2. k:. (kT)(k+1)T 0 Type by Auto

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