General Observations
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term . Recursion can be added to the language by either having a special operator of type or adding general recursive types, though both eliminate strong normalization.
Since it is strongly normalizing, it is decidable whether or not a simply typed lambda calculus program halts: it does! We can therefore conclude that the language is not Turing complete.
Read more about this topic: Simply Typed Lambda Calculus
Famous quotes containing the words general and/or observations:
“Everyone confesses in the abstract that exertion which brings out all the powers of body and mind is the best thing for us all; but practically most people do all they can to get rid of it, and as a general rule nobody does much more than circumstances drive them to do.”
—Harriet Beecher Stowe (1811–1896)
“I have never yet seen any plan which has not been mended by the observations of those who were much inferior in understanding to the person who took the lead in the business.”
—Edmund Burke (1729–1797)