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 communist society, where nobody has one exclusive sphere of activity but each can become accomplished in any branch he wishes, society regulates the general production and thus makes it possible for me to do one thing today and another tomorrow, to hunt in the morning, fish in the afternoon, rear cattle in the evening, criticize after dinner, just as I have a mind, without ever becoming hunter, fisherman, shepherd or critic.”
—Karl Marx (1818–1883)
“By sharing the information and observations with the caregiver, you have a chance to see your child through another pair of eyes. Because she has some distance and objectivity, a caregiver often sees things that a parent’s total involvement with her child doesn’t allow.”
—Amy Laura Dombro (20th century)