资料来源 : Free On-Line Dictionary of Computing

beta reduction
     
        [{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}.