Computational complexity of higher type functions
Stephen A Cook · Iwanami eBooks · 1990
The customary identification of feasible with polytime is discussed, Next, higher type functions are presented as a way of giving computational meaning to theorems. In particular, if a theorem has a feasibly constructive proof, the associated functions should be polytime. However examples are given to illustrate the difficulty of capturing the notion of polytime for higher type functions. Finally, Konig's Lemma is used to illustrate a theorem whose compu tational meaning is naturally expressed by functions of type level 3.