4 ms·

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 functio

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 5y ago
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 5y ago
  Yup, was just trying to give an example that utilized primitives to make it easier.
  - tsimionescu 5y ago
    Yes yes, I wanted to add to your example, not to say that you said anything wrong!

tsimionescu 5y ago

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 5y ago
Yup, was just trying to give an example that utilized primitives to make it easier.
- tsimionescu 5y ago
  Yes yes, I wanted to add to your example, not to say that you said anything wrong!