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

31–40 of 49 posts

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

#31

Post by hollerith »

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…

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.

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

#32

Post by cvoss »

kccqzy wrote: post #24
cvoss wrote: post #8

Earlier quoted context omitted.

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.

Interesting example! I think at that time I was either working with simply typed lambda calculus or something slightly better (maybe Hindley-Milner based system) where the omega combinator isn't allowed. Do you know what sort of type system restriction would make the above idea sound?

If you'll permit me to tweak the example, I'll now instead choose

(\ a . a a) (\ x . \y . y x) => \ y . y (\ x . \ y' . y' x)

which still exhibits the variable shadowing problem.

In a good language (where "good" means the type system lets you do as much as you want to do while still being sound) you should be able to find some type for omega. The question is whether you can find the right type for omega to let us do what we want for this example.

Try the simple thing first:

w := (\ a : * -> * . a a) : (* -> *) -> * // works because (* -> *) is a subtype of *

Here is a bad thing you shouldn't be able to do with omega:

w w : untypable // thankfully, because (* -> *) -> * is not a subtype of * -> *

And here is a perfectly safe thing to do, which is exactly our example:

f := (\ x : * . \ y : * -> T . y x) : * -> (* -> T) -> T

w f : *

Unhappily such a weak type makes it pretty unusable within larger terms... So alternatively, we can try harder to find a good type for omega

w := (\ a : * -> (* -> T) -> T . a a) : (* -> (* -> T) -> T) -> (* -> T) -> T

w f : (* -> T) -> T // better!

Something similar would happen with the Y combinator. In a good language, there ought to be many valid types you can find for `\ f . (\ x . f x x) (\ x . f x x)` but not any that would permit you to construct a diverging computation with it.

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

#33

Post by shotnothing »

marvinborner wrote: post #16

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

> Similarly, it seems like languages with de Bruijn indices are immune to LLMs

i think large chain of thought LLMs (e.g. o3) might be able to manage

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

#35

Post by dunham »

matheist wrote: post #17

The Faust compiler uses de Bruijn indices internally to reuse computations. Anyone else know any other examples? https://github.com/grame-cncm/faust

Idris[1] and most of the dependent typed languages that I've looked at use de Bruijn numbers. (As does my own[2].)

The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.)

Edit: Oh, I see you mention reusing computations, that may be a bit more subtle. I'll have to look at your repo to see what you mean by that.

[1]: https://github.com/idris-lang/Idris2 [2]: https://github.com/dunhamsteve/newt

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

#36

Post by rtpg »

hollerith wrote: post #31
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…

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.

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

#37

Post by jonahx »

tromp wrote: post #6

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/

Beautiful.

Unrelated, but what would be your advice/study plan for a human to reach near perfect game play in Connect 4, and how difficult would it be?

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

#38

Post by guerrilla »

SkiFire13 wrote: post #15
guerrilla wrote: post #13

Earlier quoted context omitted.

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

The semantics are the same for the user and debugging works, which is what matters. If you're using an object oriented language for implementation then this is already the computational cost. If you're using a functional language then yes there is some space overhead because it breaks sharing but that's the price. Was there something else you were thinking of?

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

#39

Post by practal »

De Bruijn indices are great, I use them to construct what I call the "De Bruijn Abstraction Algebra"; it comes in two forms, one is used to give a characterisation of alpha equivalence for abstraction algebra, the other one is used to prove completeness of abstraction logic. It is described in [1], and I have described and proven correct everything in excruciating detail. That makes it quite a tough read, although in the end, it is elementary and simple.

[1] http://abstractionlogic.com

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

#40

Post by tromp »

icepush wrote: post #34
tromp wrote: post #6

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/

Are you the same Tromp famous for playing the 5 game match against Zen?

Yes, as mentioned at https://senseis.xmp.net/?JohnTromp
Post reply on HN