Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

De Bruijn notation, and why it's useful

blueberrywren.dev

Post reply on HN
Print view View original

11–20 of 49 posts

Re: De Bruijn notation, and why it's useful

#11

Post by hoping1 »

guerrilla wrote: post #10

I'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…

See cvoss's comment in another thread:

" 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 doesn't come up in most mainstream languages, but Zig and Jai are getting people excited about comptime evaluation, and dependent types need comptime evaluation as well. Uniqueness is fine until you're doing higher-order evaluation in your compilation pipeline like this, which will be more and more desirable in the future, at least if the current trends are any indication.

Re: De Bruijn notation, and why it's useful

#12

Post by hoping1 »

Joker_vD wrote: post #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 immediate…

This and the other comment under this seem to be talking about the work the computer is doing at runtime. I believe the point is about the developer's work in implementing this. (For example, renaming potentially conflicting variables is clearly _less_ work than renaming only the actually conflicting variables, in this framing.) This kind of work is important for (1) compilers whose bugs are potentially very financially expensive, and (2) compilers with very intentionally-portable implementations (including but not limited to educational implementations)

Re: De Bruijn notation, and why it's useful

#13

Post by guerrilla »

hoping1 wrote: post #11
guerrilla wrote: post #10

I'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…

See cvoss's comment in another thread: " 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 doesn't come up in most mainstream languages, but Zig and Jai a…

(\ a#0 . a#0 a#0) (\ x#1 . \ y#2 . x#1 y#2)

-->

(\ x#3 . \ y#4 . x#3 y#4)(\ x#5 . \ y#6 . x#5 y#6)

Re: De Bruijn notation, and why it's useful

#15

Post by SkiFire13 »

guerrilla wrote: post #13
hoping1 wrote: post #11

Earlier quoted context omitted.

See cvoss's comment in another thread: " 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 doesn't come up in most mainstream languages, but Zig and Jai a…

(\ a#0 . a#0 a#0) (\ x#1 . \ y#2 . x#1 y#2) --> (\ x#3 . \ y#4 . x#3 y#4)(\ x#5 . \ y#6 . x#5 y#6)

This implies that applying a function is no longer the same as a plain substitution. Moreover this can be pretty expensive computationally.

Re: De Bruijn notation, and why it's useful

#16

Post by marvinborner »

Also, once you get used to it, it makes writing large lambda terms faster, easier and more intuitive. The terms all just kind of magically interconnect in your mind after a while. At least that has been my experience after writing a lot of code in pure de Bruijn-indexed lambda calculus using bruijn [1]. Otherwise, thinking a few reduction steps ahead in complex terms requires alpha conversion, which often ends in confusion.

Similarly, it seems like languages with de Bruijn indices are immune to LLMs, since they require an internal stack/graph of sorts and don't reduce only on a textual basis.

[1]: https://bruijn.marvinborner.de/

Re: De Bruijn notation, and why it's useful

#18

Post by trealira »

> 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.

Re: De Bruijn notation, and why it's useful

#19

Post by maplant »

kccqzy wrote: post #2

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…

Yeah, it's viable. I do this for my scheme implementation. Defining a new lexical variable generates a new globally unique identifier: https://github.com/maplant/scheme-rs/blob/fb89f6481443130399...

Re: De Bruijn notation, and why it's useful

#20

Post by enricozb »

trealira wrote: post #18

> 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…

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.
Post reply on HN