Re:Types versus sets (and what about categories?)
by mrkeen on Friday September 01, 2023 @05:02AM
(#37348389)
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.
> 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.