β-reduction

A beta reduction (also written β-reduction) is the process of calculating a result from the application of a function to an expression. For example, suppose we apply the function 
     ( λx . 2 * x * x + y )
to the value 7. To calculate the result, we substitute 7 for every free occurrence of x, and so the application of the function 
     ( λx . 2 * x * x + y )  ( 7 )
is reduced to the result 2*7*7+y. This is β-reduction, which is defined as follows: 
     ( λx . E ) f  ⇒β E[ f/x ]
The actual parameter f is substituted for the formal parameter x throughout the function body, E[f/x]. An example of β-reduction is as follows: 
    ( λ n . n * 2 + 3 ) 7
 ⇒β 7 * 2 + 3 = 17
The actual parameter 7 is substituted for n. The modified body is then evaluated. Recall 
    define  Twice = λf . λx . f ( f x )
Another example of β-reduction is 
    Twice ( λn . ( add n 1 ) )  5 
 ⇒ ( λf . λx . ( f ( f x ) ) )  (λn.(add n 1))  5
 ⇒β ( λx . ( (λn.(add n 1)) ( (λn.(add n 1))  x) ) )  5
 ⇒β ( λn.(add n 1) )  ( (λn.(add n 1)) 5 )
 ⇒β ( add ( (λn.(add n 1)) 5 ) 1 )
 ⇒β ( add ( add 5 1 ) 1 )
 =  7