De Bruijn notation, and why it's useful
blueberrywren.dev
De Bruijn notation, and why it's useful
1–10 of 49 posts
Re: De Bruijn notation, and why it's useful
#2While 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 writing a parser I basically already need to keep a stack of environments to resolve names. I sometimes keep variable names as simply a source code range where it is first introduced: so instead of dealing with the variable "f" I deal with (1,4)-(1,5) meaning the variable introduced in line 1 between columns 4 and 5; here I can still recover the string-based name but I also get to differentiate between identically named variables defined in different locations.
Is this a viable idea?
Re: De Bruijn notation, and why it's useful
#3I used De Bruijn indices when attempting to prove correctness of a toy language of mine. It's an elegant solution, but I found them exceedingly difficult to reason about both intuitively and in proofs. That being said, I've yet to find a better system (that isn't just augmenting De Bruijn indices) for implementing any sort of lambda calculus.
Re: De Bruijn notation, and why it's useful
#4While 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…
Take a look at The Rapier in GHC: https://www.researchgate.net/publication/220676611_Secrets_o...
It employs a similar idea. Track the set of in scope variables and use them to unique variables on collision.
Re: De Bruijn notation, and why it's useful
#5> Now we're cool! Everything works as expected, and it takes much less work
Does it though? It's about the same amount of work as in renaming potentially conflicting variables (and more work than renaming actually conflicting variables). AFAIK, the main argument for them (by B. C. Pierce in his TAPL?) is that if you botch up the implementation of de Bruijn indices/levels, it will blow up in your face almost immediately, while the conventional renaming schemes may have subtle undetected bugs for months.
Re: De Bruijn notation, and why it's useful
#6Another advantage of de-Bruijn notation is in providing a very simple binary encoding of lambda terms, as demonstrated in my IOCCC submission [1].
Re: De Bruijn notation, and why it's useful
#7> Now we're cool! Everything works as expected, and it takes much less work Does it though? It's about the same amount of work as in renaming potentially conflicting variables (and more work than renaming actually conflicting variables). AFAIK, the main argument for them (by B. C. Pierce in his TAPL?) is that if you botch up the implementation of de Bruijn indices/levels, it will blow up in your face almost immediate…
From my perspective, not having to deal with strings is one of the big benefits, but I believe the main argument is actually that it trivializes alpha equivalence.
As for renaming, if you're going to be looking at every binding anyway, changing most of them is no big deal (unless of course that entails doing many deep copies)
Re: De Bruijn notation, and why it's useful
#8While 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.
Re: De Bruijn notation, and why it's useful
#9Another 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/
To you and OP and the others: you're crazy or geniuses, but thanks for posting because that's inspiring whether I understand it or not.
Re: De Bruijn notation, and why it's useful
#10I've implemted this several times before (years ago), but somone tell me, why don't we just consider variables unique. Each instance of a name* should have an absolute (i.e. global) sequence number associated with it. That seems simpler than this relative sequence numbering and the complexity that comes from it.
Scrolling comments, I see somone else nentions this as well. I feel like this is something that got stuck in academia hell but in practice could be solved in more oractical ways. I remember various papers on fresh naming and name calculi from the 00's but why? We have a parser and we have numbers.
The reason I bring this up is because I recall it being easy to introduce bugs into de Bruijn calculi and also adding symbolic debugging to real-world languages was annoying for reasons I have no memory of.
* Note I said name not variable. (\ x . x (\x . x)) Would be (\ x#0 . x#0 (\x#1 . x#1)) similar to de Bruijn indices but could differ in other situations.