Basically, beta-reduction is the single primitive that performs all computation in the lambda calculus. When you apply the function mapping x to M, to argument N, the result is M with all occurences of x replaced by N.
Any evaluation of a functional-based language is going to use this. Here's a simple example:
Let's say I have a function `add1`
`add1 = \x -> x + 1` (A function that takes a value `x` and then computes `x + 1`
And then I write the program:
`add1 2`
If we want to evaluate this program, first we substitute the variable to get
`add1 2` -> `(\x -> x + 1) 2`
Then we perform "beta reduction" to get:
`(\x -> x + 1) 2` -> `2 + 1`
Then it's simple arithmetic:
`2 + 1` -> `3`
"The point" here is to have formal rules for defining what a computation means. This helps with writing proofs about what programs do, or what is possible for programs to do.
For example, say I have a simple program with static types. I might want to prove that if the programs type checks, type errors will never occur when you run the program. In order to do this proof, I have to have some formal notion of what it means to "run the program". For a functional language, beta reduction is one of those formal rules.
I will note though that in the actual lambda calculus there is no "+", "2" or "1" - it's functions all the way.
1 is typically defined in the Church encoding as \f -> \x -> f x. Addition is \m -> \n -> \f -> \x -> m f (n f x). Finding the Church encoding of 2 is left as an exceecise.
We can then use beta reduction to compute 1 + 1 by replacing m and n with 1:
1 = \f -> \x -> f x
(\m -> \n -> \f -> \x -> m f (n f x)) 1 1 =>beta
\f -> \x -> 1 f (1 f x)
\f -> \x -> 1 f x = (\f -> \x -> f x) f x =>beta
1 f x = f x
\f -> \x -> 1 f (1 f x) <=> \f -> \x -> 1 f (f x)
(\f -> \x -> f x) f (f x) =>beta
\f -> \x -> f f x - the Church encoding of 2.
This is how computation using beta reduction only looks like.
If we expand the discussion from "lambda calculus" to "pretty much every programming language", then "beta reduction" becomes "calling a function with an argument"
> Is there any practical example on this?
Given the above, you'll be able to find beta-reduction in practically all software ever written ;)
"Compilation" usually describes translation from one language to another (e.g. C to machine code).
In contrast, beta-reduction rewrites expressions in the same language. It's a "reduction" since it brings expressions closer and closer to their "normal form" (i.e. a halted program); although some expressions have no normal form (they run forever, i.e. the Halting Problem).
In Javascript syntax, the following expression is not in "normal form":
(function(x) { return x + 5; })(42)
If we apply beta-reduction to it, we get back the function body, with occurrences of 'x' substituted by '42':
42 + 5
That expression can no longer be beta-reduced; it is "beta-normal". Lambda calculus only uses beta-reduction (although there are "alpha" and "eta" replacements, which are more like refactorings).
However, Javascript has more reduction rules than just beta-reduction; in this case we can use its numerical operations, to reduce the expression further:
47
That is in normal form for Javascript; i.e. the program has halted.
Note that it's not "compilation", since we stayed in the same language at all times, just replacing one expression with an equivalent expression.
