[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. 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.