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

[Vasileios Koutavas]

I took a look at barendregt and understood what Felix was saying:

if sigma_0 = sigma_0 -> sigma_0       (where '=' see wavy-equals)
then the type(s) that satisfy this equasion can type arbitrary lambda 
terms.

 The thing here is that this equasion is *special*, and by substituting 
its r.h.s. with something else breaks the above proposition. For instance 
if you do the typings you will see that:

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.

fyi barendregt says that s_0 = s_0 -> s_0 types all terms because it is 
like a recursive domain equation D = [D -> D].

--Vassilis