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:
“Women born at the turn of the century have been conditioned not to speak openly of their wedding nights. Of other nights in bed with other men they speak not at all. Today a woman having bedded with a great general feels free to tell us that in bed the general could not present arms. Women of my generation would have spared the great general the revelation of this failure.”
—Jessamyn West (1907–1984)
“The truth is, the Science of Nature has been already too long made only a work of the brain and the fancy: It is now high time that it should return to the plainness and soundness of observations on material and obvious things.”
—Robert Hooke (1635–1703)