https://en.m.wikipedia.org/wiki/Value_numbering Is this what you're looking for? You're reminding me of something, but it's way back in my mind.

https://en.m.wikipedia.org/wiki/De_Bruijn_index

YES, thank you both 🙂

For some reason I don't understand the complete use of this. In particular the "De Bruijn Index". For me it simply looks like a stack-based language code of some kind of expressions where you expect that the "stack" would contain this number of arguments. Is this correct?

can someone ELI5 this?

Canonical representation of code without name collisions

You don't really need this if you just want to read Lisp code, the evaluate it. But it could enable compiler optimizations that would be harder to implement otherwise.

I found that De Brujin graph is an Euler graph and can be used to shrink the source code. But I'm not familiar with the notation they use in wikipedia. It could be De Bruijn notation but even then it's not clear what goes where. So is this also meant to shrink the code some way? i.e. to match for code chunks that are the same?

In this vid the guy used the De Bruijn graph for DNA matching. It's basically a regex state machine that encodes a graph. And not any graph, Euler graph: https://www.youtube.com/watch?v=TNYZZKrjCSk

Yeah, De Bruijn is used a lot in bioinformatics :thumbsup:

https://www.youtube.com/watch?v=eGzDhIE5jI4

It's the only way to "properly" show function/expression equality

Re: de bruijin indices being a weird stack language, there are optimized transformations of lambda terms to ski terms (avoids the term size explosion that the naive transform results in) that requires knowing the de bruijin index of each variable

https://git.sr.ht/~hiredman/lions/tree/master/item/src/com/manigfeald/comb.clj is an version of that in clojure

http://okmij.org/ftp/tagless-final/ski.pdf is the paper about it

I’m looking at this before coffee, and it took me a moment, but I just realized… De Bruijin indexing is analogous to skolemizing a logic expression.

(Yes, I know I’m 2 days late here)

Make that “roughly analogous” since variable indices change depending on their relative position

There's probably a logic which shows they're related

@U051N6TTC can I get this on a T shirt “De Bruijin indexing is analogous to skolemizing a logic expression”

Get it in remorse

Is this the right chat? What is the topic?

I recall it being here in #off-topic since java compiler messages don't come up in clojure dev

https://clojurians.slack.com/archives/C03RZGPG3/p1639854358051200?thread_ts=1639716316.475700&cid=C03RZGPG3 Original thread @U028ART884X