5 ms·

Is there any practical example on this? Whats a common use casE?

opnitro 5y ago
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!
chriswarbo 5y ago
> Whats a common use case? 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 ;)

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!

chriswarbo 5y ago

> Whats a common use case? 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 ;)