[PL-sem-jr] Followup on today's talk

[Felix S Klock]

On Oct 19, 2004, at 7:08 AM, Vasileios Koutavas wrote:
> 1) non-recursive equations don't work: s_0 = s_1 -> s_2
> 2) even recursive equations don't work: s_0 = s_1 -> s_0
> 3) but there are other recursive equations that work (at least for 
> typing
> Omega):
>      s_0 = s_0 -> (s_0 -> s_0)
> and more generally:
>     forall s_1.  s_0 = s_0 -> s_1
>
> I don't know if #3 can type arbitrary terms because it can type Omega, 
> and
> barendregt's one-line justification of why s_0 = s_0 -> s_0 does, 
> makes me
> think that #3 probably doesn't have this power.

If I'm understanding your notation, your #3 is something like the 
following:

sigma_#3 = mu alpha . (alpha -> (alpha -> alpha))

And yes, I believe that this does have a derivation for Omega : sigma_#3

1. My intuition here is this:
sigma_0 = (mu alpha . (alpha -> alpha))  is able to type everything 
because you can expand AND retract it to fit whatever you are trying to 
type.
sigma_0
approx (sigma_0 -> sigma_0)
approx ((sigma_0 -> sigma_0) -> sigma_0)
approx (sigma_0 -> (sigma_0 -> sigma_0))
approx ...

So for whatever closed term you hand me, I'll just expand sigma_0 to 
fit it.  [[ Not a formal proof, just my intuition here ]]

2. sigma_#3 = (mu alpha . (alpha -> (alpha -> alpha)))
should also be able to type arbitrary terms; its infinite tree is the 
same as the infinite tree for sigma_0, which satisfies the definition 
of approx.

I admit that this was not my initial intuition about sigma_#3 though.  
At first I agreed with you that it would not be able to type all terms. 
  But now I think it can.

I am now curious about whether there are versions of lambda-mu which 
distinquish between sigma_#3 and sigma_0, perhaps by putting the 
individual folds and unfolds into the type derivation itself, rather 
than shoving them all into a coinductively-defined helper function.  
Maybe I'll ask Mitch about that.

3. There's still the important lesson that these recursive types that 
we're showing can type any term are not necessarily the *principal* 
types for the terms they are typing.  Boy, now I really wish I had a 
chance to give the formal definition for principal types.

A principal type for M is a type sigma where
1. |- M : sigma
2. (  |- M : tau  )     implies     Exists a substitution S where 
S(sigma) = tau
where a substitution replaces type variables with types (which are 
possibly just type variables themselves).  See Barendregt's chapter for 
the gory details.

Now take K = \xy.x for example.  A principal type for K : alpha -> beta 
-> alpha.

But you could easily prove that K : sigma_0 -> (sigma_0 -> sigma_0)   
[[ this comes as no surprise; just substitute sigma_0 for alpha and 
beta in the above principal type for K) and thus by retracting twice we 
get K : sigma_0.

But K : sigma_0 is *not* a principal type for K; there are lots of 
other types for K that are valid that we cannot find simply by 
substituting types into free variables in sigma_0, because there are 
*no* free variables in sigma_0.  Any substitution on sigma_0 is going 
to just yield. . . sigma_0.

-Felix