[lambda-calculus] The application of a lambda abstraction to an argument
expression. A copy of the body of the lambda abstraction is made and occurrences
of the bound variable being replaced by the argument. E.g.
(\ x . x+1) 4 --> 4+1
Beta reduction is the only kind of reduction in the pure lambda-calculus.
The opposite of beta reduction is beta abstraction.
These are the two kinds of beta conversion.
See also name capture.
beta abstraction « beta conversion « Betamaxed «
beta reduction » beta testing » beta version »