Normal Forms and Confluence
For the untyped lambda calculus, β-reduction as a rewriting rule is neither strongly normalising nor weakly normalising.
However, it can be shown that β-reduction is confluent. (Of course, we are working up to α-conversion, i.e. we consider two normal forms to be equal, if it is possible to α-convert one into the other.)
Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.
Read more about this topic: Lambda Calculus
Famous quotes containing the words normal and/or forms:
“The normal present connects the past and the future through limitation. Contiguity results, crystallization by means of solidification. There also exists, however, a spiritual present that identifies past and future through dissolution, and this mixture is the element, the atmosphere of the poet.”
—Novalis [Friedrich Von Hardenberg] (1772–1801)
“The analogy between the mind and a computer fails for many reasons. The brain is constructed by principles that assure diversity and degeneracy. Unlike a computer, it has no replicative memory. It is historical and value driven. It forms categories by internal criteria and by constraints acting at many scales, not by means of a syntactically constructed program. The world with which the brain interacts is not unequivocally made up of classical categories.”
—Gerald M. Edelman (b. 1928)