5 ms·

Can someone point me to a reference explaining what beta reduction is?

tromp 5y ago
https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reducti... 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.
- agounaris 5y ago
  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 ;)
- melony 5y ago
  Isn't that the process of compilation?
  - chriswarbo 5y ago
    "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.

https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reducti... 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.

agounaris 5y ago
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 ;)
melony 5y ago
Isn't that the process of compilation?
- chriswarbo 5y ago
  "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.