Editing Lambda calculus (section)

==== β-reduction ====
The β-reduction rule{{efn|name=beta}} states that an application of the form <math>( \lambda x . t) s</math> reduces to the term <math> t [ x := s]</math>. The notation <math>( \lambda x . t ) s \to t [ x := s ] </math> is used to indicate that <math>( \lambda x .t ) s </math> β-reduces to <math> t [ x := s ] </math>.
For example, for every <math>s</math>, <math>( \lambda x . x ) s \to x[ x := s ] = s </math>. This demonstrates that <math> \lambda x . x </math> really is the identity.
Similarly, <math>( \lambda x . y ) s \to y [ x := s ] = y </math>, which demonstrates that <math> \lambda x . y </math> is a constant function.

The lambda calculus may be seen as an idealized version of a functional programming language, like [[Haskell]] or [[Standard ML]]. Under this view,{{anchor|betaReducIsAcomput}} β-reduction corresponds to a computational step. This step can be repeated by additional β-reductions until there are no more applications left to reduce. In the untyped lambda calculus, as presented here, this reduction process may not terminate. For instance, consider the term <math>\Omega = (\lambda x . xx)( \lambda x . xx )</math>.
Here <math>( \lambda x . xx)( \lambda x . xx) \to ( xx )[ x := \lambda x . xx ] = ( x [ x := \lambda x . xx ] )( x [ x := \lambda x . xx ] ) = ( \lambda x . xx)( \lambda x . xx )</math>.
That is, the term reduces to itself in a single β-reduction, and therefore the reduction process will never terminate.

{{anchor|untypedData}}Another aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to [[truth value]]s, strings, or other non-number objects.