[sharkbot]

Far from it; rather, that the simply typed lambda calculus is not Turing complete. One cannot represent a Turing machine in the simply typed lambda calculus, exactly because non terminating programs cannot be expressed.

One can add a fix point to the calculus (such as the titular Y combinator), but that introduces inconsistency to the type system.