21–30 of 49 posts
> 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 scop…
Another advantage of de-Bruijn notation is in providing a very simple binary encoding of lambda terms, as demonstrated in my IOCCC submission [1]. [1] https://www.ioccc.org/2012/tromp/
While I have used de bruijn indices successfully in the past, a part of me wonders, why can't this problem be solved at the parser level before we even get a syntax tree? The parser knows when we are introducing a new variable in a lambda abstraction, and it can keep track of a stack of variables to be able to give them new fresh names so that in later passes we won't have to worry about name conflicts. I mean when w…
What happens in the evaluator when you have (\ a . a a) (\ x . \ y . x y) Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope.
While I have used de bruijn indices successfully in the past, a part of me wonders, why can't this problem be solved at the parser level before we even get a syntax tree? The parser knows when we are introducing a new variable in a lambda abstraction, and it can keep track of a stack of variables to be able to give them new fresh names so that in later passes we won't have to worry about name conflicts. I mean when w…
What happens in the evaluator when you have (\ a . a a) (\ x . \ y . x y) Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope.
> 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 scop…
Bad pseudocode:
function stepincrementgenerator(step) -> function (num) -> num + step
addsix = stepincrementgenerator(6)
addsix(5)
11
Whilst a classic lambda expression like `λx.y` has three parts: the argument name `x`, the body/result `y`, and the `λ_._` syntax to distinguish it from a variable or application; if we instead use de Bruijn indices, then we don't need a separate part for the argument: all we need is a body wrapped in some distinguishing syntax (like `λy` in the article).
In Plumb, that distinguishing syntax is square brackets, so the "lambda term" `λy` would be written `[y]`. This wouldn't be possible if we had to write argument names, but ends up having some nice consequences:
- We can write this as-is in many languages, and the result is a data structure (usually a list) which we can easily walk over with an interpreter function.
- Variables are numbers, which can also be written as-is in many languages, and result in data that an interpreter function can handle.
- The final piece of syntax is applications, which necessarily has two parts (the function and the input value). Classic Lambda Calculus uses juxtaposition, whilst Plumb uses an explicit binary operator: the comma `,`. Again, commas can be written as-is in many languages, and they interact nicely with square bracket notation, (host language) function application, and (in the case of Python and Haskell) tuple notation.
The nice thing about using de Bruijn indexen, rather than de Bruijn "levels" or some other approaches to anonymous bindings (like those mentioned at the end of TFA), is that functions defined this way have an "intrinsic meaning"; e.g. `λ0` (or `[0]` in Plumb) is always the identity function; `λλλ(2 0 1)` (or `[[[2 , 0 , 1]]]` in Plumb) is always boolean NOT; etc. This lets us mix and match snippets of Plumb code with snippets of host-language code, embed each inside the other, and sprinkle around calls to an interpreter function willy-nilly, without worrying that the meaning depends on where our code ends up (e.g. at which "level" it reaches an interpreter).
Code: http://t3x.org/clc/code.html
If you know Scheme, you almost don't need the book.
Another advantage of de-Bruijn notation is in providing a very simple binary encoding of lambda terms, as demonstrated in my IOCCC submission [1]. [1] https://www.ioccc.org/2012/tromp/
This has long been my favorite entry! Still on my todo list to go through and fully understand it.
> 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 scop…
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)
> 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 scop…