> This is "the capture problem", and it is quite annoying. Generally to avoid this, we need to rename everything1 in our "substituted" term to names that are free (do not occur) in the "subsitutee" so nothing is accidentally captured. What if we could introduce a notation that avoids this?
I've heard of this problem, but I've never really gotten why the solution in lambda calculus is to rename variables in lower scopes with overlapping names so that everything has a globally unique name. The way that programming languages usually solve this is by keeping a stack of symbol tables for scopes, right? Why is that never presented as a possible solution?
Of course, De Bruijn notation seems to sidestep that completely, which is convenient. I guess I'm just commenting on lambda calculus implementations in general.
Lambda variables are also scoped, in the sense that a bound variable shadows one with the same name if it is in scope at bind-time. When looking at lambda calculus as purely a term rewriting system, the rule for substitution is just a bit nuanced, that's all. With DeBruijn notation, substitution is a much simpler operation.
> I've heard of this problem, but I've never really gotten why the solution in lambda calculus is to rename variables in lower scopes with overlapping names so that everything has a globally unique name. The way that programming languages usually solve this is by keeping a stack of symbol tables for scopes, right? Why is that never presented as a possible solution?
That's a perfectly fine way to implement this-or-that language (and is hence why many/most programming languages do it). However, it's not a valid solution in lambda calculus, since lambda calculus only has variables, lambdas or applications; there's literally no way to write down "a stack of symbol tables", or whathaveyou (note that you can implement such a thing using lambda calculus, but that would be more like an interpreter for some other language; "running" that implementation would still require a way to beta-reduce the "host" language in a capture-avoiding way)
The idea is that you want functions that can return functions, those inner functions being defined in part by the arguments to the outer function. This can't happen without intentionally leaky namespaces.
Bad pseudocode:
function stepincrementgenerator(step) -> function (num) -> num + step
addsix = stepincrementgenerator(6)
addsix(5)
11
Stack of symbol tables is more elegant, but is only understandable by programmers whereas maybe lambda calc gets taught to a lot of non-programmers?
Note that lambda calc was invented ("defined") before the invention of the digital computer.
A stack of symbol tables is more machinery. It might also be hard to prove that the stack of symbol tables strategy is actually correct!
A big part of the value in the lambda calculus is in its aggressive simplicity meaning that you can do a bunch of theoretical work with relatively few concepts.
The less concepts and moving parts, the less proving necessary. And then you can layer on things and prove that they can also fit into your calculus.
I think most LC work _isn't_ about implementing something based on LC so much as providing theoretical foundations for your work being sound. And in that model you are likely going to focus on theoretical ease.
Yeah. It is coming back to me now: in lambda calc, there is no universe of values to which the universe of lambda expressions might be mapped. Instead, there is a process called lambda reduction that maps the set of all lambda expressions to the set of lambda expressions in normal form.
The expression λf.λx.f(f(fx)) for example is in normal form. The number 3 and the string "3" do not exist in the formalism, but at least some of the time, λf.λx.x is used to represent 0, λf.λx.fx to represent 1, λf.λx.f(fx) to represent 2, λf.λx.f(f(fx)) to represent 3, etc.
Again, lambda calc precedes the digital computer.