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:
“What journeyings on foot and on horseback through the wilderness, to preach the gospel to these minks and muskrats! who first, no doubt, listened with their red ears out of a natural hospitality and courtesy, and afterward from curiosity or even interest, till at length there “were praying Indians,” and, as the General Court wrote to Cromwell, the “work is brought to this perfection that some of the Indians themselves can pray and prophesy in a comfortable manner.””
—Henry David Thoreau (1817–1862)
“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)