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:
“Some people are under the impression that all that is required to make a good fisherman is the ability to tell lies easily and without blushing; but this is a mistake. Mere bald fabrication is useless; the veriest tyro can manage that. It is in the circumstantial detail, the embellishing touches of probability, the general air of scrupulous—almost of pedantic—veracity, that the experienced angler is seen.”
—Jerome K. Jerome (1859–1927)
“All observations point to the fact that the intellectual woman is masculinized; in her, warm, intuitive knowledge has yielded to cold unproductive thinking.”
—Helene Deutsch (1884–1982)