Lambda the Ultimate

I am actually kind of perplexed by this. My understanding is that if P != NP there should exist problems in NP that are not in P that aren't NP-complete but is the reverse also true? i.e. should there be a problem whose solution is in NP but not in P but not NP-complete would this imply that P != NP?

For example, it would seem to me at first blush that certain problems do fall in this class if one allows for imperfect knowledge of subroutine code (which occurs in practice). For example password cracking would be one assuming the verification subroutine runs in polynomial time.

1. It is in NP since one can nondeterministically guess all strings and verify each in P time.
2. It is rather straight forward to prove that it takes exp time to get the correct string in the worse case since given any alphabet A of size k there are k^N possible strings to examine with the subroutine verifier. Since from a sort of information theoretical point of view testing one string yields no information about the correct string except that the current string is not the correct string when answered in the negative(i.e. it yields no information whatsoever about whether another even similar string is the correct string or not). One needs k^N unique string tests in the worse case each executing sequentially in polynomial time which isn't in P.

My understanding about this subject is limited however but it would seem that this problem is guaranteed to execute in O(P*exp) on a TM and P time on a NTM and there is no room for improvement on a TM- why doesn't this show that P != NP? It seems like something that must have been considered by many people.

Thanks in advance,

P.S. I asked a CS professor already and he wasn't sure about it since it isn't his specialty. So I thought it might be worth asking on a general forum.

I was wondering if anyone could recommend some good books on the more theoretical aspects of type theory as it pertains to computer science and guarantees w.r.t to certain properties as related to language theory. The only books I know of are the two by Pierce but they seem more on the applied side focusing on very specific applications of various theories that in many cases have a long history which aren't really covered by either book. Are there better books covering some of the theory more in depth?

Thanks.