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:
“It has been an unchallengeable American doctrine that cranberry sauce, a pink goo with overtones of sugared tomatoes, is a delectable necessity of the Thanksgiving board and that turkey is uneatable without it.... There are some things in every country that you must be born to endure; and another hundred years of general satisfaction with Americans and America could not reconcile this expatriate to cranberry sauce, peanut butter, and drum majorettes.”
—Alistair Cooke (b. 1908)
“The natural historian is not a fisherman who prays for cloudy days and good luck merely; but as fishing has been styled “a contemplative man’s recreation,” introducing him profitably to woods and water, so the fruit of the naturalist’s observations is not in new genera or species, but in new contemplations still, and science is only a more contemplative man’s recreation.”
—Henry David Thoreau (1817–1862)