Feasible Operations and Applicative Theories Based on λη

We study a theory PTO(λη) of polynomial time computability on the type of binary strings (in the style of 6]), as embedded in full lambda calculus with total application and extensionality. We prove that the closed terms of (provable) type W → W are exactly the polynomial time operations. This answers a conjecture of Strahm 13].