I don't remember enough of the proof for system F to say whether halting problem reduces to it, although usually the proofs are made in such a fashion that it would, and then, in the third sense, we would have an equivalence..
BTW, if we know that type inference for a program in system F nonterminates, does this tell us anything about the program?
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2007-01-07 04:31 pm (UTC)BTW, if we know that type inference for a program in system F nonterminates, does this tell us anything about the program?