[opnitro]

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.

[tsimionescu]

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.

[opnitro]

Yup, was just trying to give an example that utilized primitives to make it easier.

[tsimionescu]

Yes yes, I wanted to add to your example, not to say that you said anything wrong!