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

41–49 of 49 posts

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

#41

Post by tromp »

jonahx wrote: post #37
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?

I can recommend this book [1] on connect-4 by James Allen, the first person to solve the game. It remains very difficult for humans to play near perfectly, as the harder puzzles in the book demonstrate.

[1] https://www.waterstones.com/book/the-complete-book-of-connec...

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

#42

Post by matheist »

dunham wrote: post #35
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 b…

Thanks! (Just clarifying, it's not my project)

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

#43

Post by SkiFire13 »

guerrilla wrote: post #38
SkiFire13 wrote: post #15

Earlier quoted context omitted.

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?

It's not just space overhead, it requires you to recursively walk the argument of the application and replace all variables with fresh ones, once for every occurrence of the function argument. This means that function application is no longer O(size of the function) but rather O(size of the function + occurrences of the argument * size of the argument). If the size of the argument is big this makes the function application much much slower.

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

#44

Post by [deleted] »

SkiFire13 wrote: post #43
guerrilla wrote: post #38

Earlier quoted context omitted.

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?

It's not just space overhead, it requires you to recursively walk the argument of the application and replace all variables with fresh ones, once for every occurrence of the function argument. This means that function application is no longer O(size of the function) but rather O(size of the function + occurrences of the argument * size of the argument). If the size of the argument is big this makes the function appli…

[deleted]

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

#45

Post by hollerith »

rtpg wrote: post #36
hollerith wrote: post #31

Earlier quoted context omitted.

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

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.

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

#46

Post by jonahx »

tromp wrote: post #41
jonahx wrote: post #37

Earlier quoted context omitted.

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?

I can recommend this book [1] on connect-4 by James Allen, the first person to solve the game. It remains very difficult for humans to play near perfectly, as the harder puzzles in the book demonstrate. [1] https://www.waterstones.com/book/the-complete-book-of-connec...

I have it! But I've always wondered if a more systematic approach based on Victor Allis's paper might be achievable. Can you play perfectly?

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

#47

Post by tromp »

jonahx wrote: post #46
tromp wrote: post #41

Earlier quoted context omitted.

I can recommend this book [1] on connect-4 by James Allen, the first person to solve the game. It remains very difficult for humans to play near perfectly, as the harder puzzles in the book demonstrate. [1] https://www.waterstones.com/book/the-complete-book-of-connec...

I have it! But I've always wondered if a more systematic approach based on Victor Allis's paper might be achievable. Can you play perfectly?

Not only can I not play perfectly (unlike my Fhourstones program), but I really struggle with even the intermediate problems in the book.

A more limited form of perfect play is knowing how to win when playing first. I cannot do that either, but I suspect that I might be able to get close if I were to study hard on it for a year, trying to minimize the size of the opening book I need to keep in my head. The leaves of that book will then resemble the positions where Allis' rules apply so that you can work out further play on the fly.

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

#48

Post by wizzwizz4 »

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.

It's not that expensive: just use De Bruijn notation under the hood. (I've seen a system that does this, and this is how it works.)

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

#49

Post by SkiFire13 »

wizzwizz4 wrote: post #48
SkiFire13 wrote: post #15

Earlier quoted context omitted.

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

It's not that expensive: just use De Bruijn notation under the hood. (I've seen a system that does this, and this is how it works.)

But then the point of giving unique names to avoid using De Brujin indices is moot
Post reply on HN