linguistic:translation, information:extraction
β-reduction

The β-reduction rule states that an application of the form (λ x. t) s {\displaystyle (\lambda x.t)s} reduces to the term t {\displaystyle t}. The notation (λ x. t) s → t {\displaystyle (\lambda x.t)s\to t} is used to indicate that (λ x. t) s {\displaystyle (\lambda x.t)s} β-reduces to t {\displaystyle t}.For example, for every s {\displaystyle s}, (λ x. x) s → x = s {\displaystyle (\lambda x.x)s\to x=s}. This demonstrates that λ x. x {\displaystyle \lambda x.x} really is the identity.Similarly, (λ x. y) s → y = y {\displaystyle (\lambda x.y)s\to y=y}, which demonstrates that λ x. y {\displaystyle \lambda x.y} 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, β-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 Ω = (λ x. x x) (λ x. x x) {\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}.Here (λ x. x x) (λ x. x x) → (x x) = (x) (x) = (λ x. x x) (λ x. x x) {\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)=(x)(x)=(\lambda x.xx)(\lambda x.xx)}.That is, the term reduces to itself in a single β-reduction, and therefore the reduction process will never terminate.

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 values, strings, or other non-number objects.