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.