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:
“Every writer is necessarily a critic—that is, each sentence is a skeleton accompanied by enormous activity of rejection; and each selection is governed by general principles concerning truth, force, beauty, and so on.... The critic that is in every fabulist is like the iceberg—nine-tenths of him is under water.”
—Thornton Wilder (1897–1975)
“Jerry: She’s one of those third-year girls that gripe my liver.
Milo: Third-year girls?
Jerry: Yeah, you know, American college kids. They come over here to take their third year and lap up a little culture. They give me a swift pain.
Milo: Why?
Jerry: They’re officious and dull. They’re always making profound observations they’ve overheard.”
—Alan Jay Lerner (1918–1986)