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:
“In former times and in less complex societies, children could find their way into the adult world by watching workers and perhaps giving them a hand; by lingering at the general store long enough to chat with, and overhear conversations of, adults...; by sharing and participating in the tasks of family and community that were necessary to survival. They were in, and of, the adult world while yet sensing themselves apart as children.”
—Dorothy H. Cohen (20th century)
“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)