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:
“We all have known
Good critics, who have stamped out poet’s hopes;
Good statesmen, who pulled ruin on the state;
Good patriots, who, for a theory, risked a cause;
Good kings, who disembowelled for a tax;
Good Popes, who brought all good to jeopardy;
Good Christians, who sat still in easy-chairs;
And damned the general world for standing up.—
Now, may the good God pardon all good men!”
—Elizabeth Barrett Browning (1806–1861)
“Science is a dynamic undertaking directed to lowering the degree of the empiricism involved in solving problems; or, if you prefer, science is a process of fabricating a web of interconnected concepts and conceptual schemes arising from experiments and observations and fruitful of further experiments and observations.”
—James Conant (1893–1978)