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:
“Anti-Nebraska, Know-Nothings, and general disgust with the powers that be, have carried this county [Hamilton County, Ohio] by between seven and eight thousand majority! How people do hate Catholics, and what a happiness it was to show it in what seemed a lawful and patriotic manner.”
—Rutherford Birchard Hayes (1822–1893)
“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)