4 ms·

It was all fun and games until The most basic rule of the λ-calculus is β-reduction, which replaces (λx.M)N by M[N/x], which denotes a copy of M in which every

It was all fun and games until The most basic rule of the λ-calculus is β-reduction, which replaces (λx.M)N by M[N/x], which denotes a copy of M in which every free occurrence of x has been replaced by N. Obviously, [...]. You know, obviously.

bmacho 3y ago
The author linked an introductory article about Lambda Calculus before this.
mrkeen 3y ago
I wouldn't call β-reduction "The most basic rule", but I'd call it the most important. > denotes a copy of M in which every free occurrence of x has been replaced by N ...breaking it down... > a copy of Weird wording, but if you're used to mutability everywhere, and you want to do an immutable operation, then it makes sense to make a copy. But it's kind of like saying 4+3 'makes a copy of four which is three bigger'. > every free occurrence Paraphrasing, this says 'pay attention to variable scope'. If you start replacing every x within a scope, and you come across a new declaration of x inside that scope, you should ignore occurrences of that inner x, because it's a different variable (despite having the same name.) > (λx.M)N ... M[N/x] This one adds no clarity for me, despite being throughout the literature. Explaining that (λx.M)N is M[N/x] doesn't help a beginner, because you then immediately have to explain what M[N/x] is. N.replace(x, M) would probably suit a modern audience. Why bother with all this nonsense? The power-to-weight ratio. λ-calculus (including β-reduction) gives you all of computing. Compared to its contemporary Turing Machine (which was super important theoretically at the time), you can just bootstrap a new language off the lambda calculus.
yoneda 3y ago
The "obvious" observation from the article is: > Obviously, λx.M should be seen as a sort of function The fact that lambdas can be seen as a syntax for describing functions (or function-like things) is kind of obvious to anyone who knows basic programming language theory (and many software engineers who use lambdas when they map over a list, for example). The sentence before it about β-reduction is describing the rule for how to call a function, which we learned in high school as "plug-and-chug". I think the confusion here might just be that the syntax is unfamiliar. You have probably seen these concepts before.

bmacho 3y ago

The author linked an introductory article about Lambda Calculus before this.

mrkeen 3y ago

I wouldn't call β-reduction "The most basic rule", but I'd call it the most important. > denotes a copy of M in which every free occurrence of x has been replaced by N ...breaking it down... > a copy of Weird wording, but if you're used to mutability everywhere, and you want to do an immutable operation, then it makes sense to make a copy. But it's kind of like saying 4+3 'makes a copy of four which is three bigger'. > every free occurrence Paraphrasing, this says 'pay attention to variable scope'. If you start replacing every x within a scope, and you come across a new declaration of x inside that scope, you should ignore occurrences of that inner x, because it's a different variable (despite having the same name.) > (λx.M)N ... M[N/x] This one adds no clarity for me, despite being throughout the literature. Explaining that (λx.M)N is M[N/x] doesn't help a beginner, because you then immediately have to explain what M[N/x] is. N.replace(x, M) would probably suit a modern audience. Why bother with all this nonsense? The power-to-weight ratio. λ-calculus (including β-reduction) gives you all of computing. Compared to its contemporary Turing Machine (which was super important theoretically at the time), you can just bootstrap a new language off the lambda calculus.

yoneda 3y ago

The "obvious" observation from the article is: > Obviously, λx.M should be seen as a sort of function The fact that lambdas can be seen as a syntax for describing functions (or function-like things) is kind of obvious to anyone who knows basic programming language theory (and many software engineers who use lambdas when they map over a list, for example). The sentence before it about β-reduction is describing the rule for how to call a function, which we learned in high school as "plug-and-chug". I think the confusion here might just be that the syntax is unfamiliar. You have probably seen these concepts before.