Strictly for insiders only? I wouldn't even know where to find out what language that is. It has something to do with e-graphs, which seems to be a veritable rabbit hole.
Yes, perhaps. This is not written as a general introduction to e-graphs. They are a data structure that compactly holds many equivalent versions of terms / syntax trees. Egraphs are a solution to phase ordering issues for greedy rewrites. They are also just a useful fabric for optimization tasks. They are being used in many compiler projects https://github.com/philzook58/awesome-egraphs . Mostly research compilers, but cranelift and luminal are not for example.
Many applications are naturally expressed using bound variables (lambdas, summation expressions, einstein indices, integrals, loops) but the basic e-graph doesn't really support the concept. One can instead model using combinators (SKI combinators, relation algebra, categorical combinators, other) but this tends to be not entirely natural and tends to explodes in the search space of different ways to encode the same concept using combinators.
Lifting e-graphs are a variant of sorts of slotted e-graphs, which are techniques to supports binders in egraphs. It's more subtle to do so than one might think. Lambda microegg also adds a surface syntax to play around more easily.
Thank you. I remember reading “Gödel, Escher, Bach” and getting into the rabbit hole of term-rewriting. Then figured out it would be a fantastic way to build a compiler, simply by iteratively rewriting expressions into what is basically assembly code. Would also be a great framework for a modular bring-your-own-parser compiler construction kit. Going from theory to practice on how to achieve that, i.e. the best way to declaratively encode such transformations in Lisp-like language, how to deal with conflicts, ambiguity and the exponentially exploding search space eventually led me to e-graphs and some of the stuff you mention in this comment…
At which point it felt like having jumped into the deep sea, at night, and sharks are all around. I have no formal education in CS, and a lot of this stuff is way above my pay grade. Though it made me wonder why none of this stuff has hit mainstream; modern compilers are still very crude, it seems like such an obvious idea to model compilation as transformation of one graph into another. Is this just fringe academic research that hasn’t yet trickled down to the masses of us code monkeys?
I still have a soft-spot for this niche of computer science, but I need to find 5 years and 20 IQ points to understand how it all fits together.
I personally have a great respect and love of the intuitive and consider formalism or abstract mathematics only interesting in the service of elaboration or exploration of the intuitive.
Basically all optimizing compilers have a simplifier or rewriter in them. I don't see it as a requirement or even necessarily a priori desirable to frame their discussion or formulation in terms of high barrier mathematical language. Do so if it is fun or useful. Sometimes it is. It is to my subjective taste to do so. Compiler writers are a pretty clever group by and large and are aware of a decent amount of useful math.
There is also a tendency to underestimate where 10 years of study and effort applied to a subject can bring you and attribute it totally to some intrinsic intelligence.
Term rewriting _is_ really neat. Realizing and remembering what you find neat and exciting is important. I like equations.
I'd like to think I know a thing or two about math/cs... but I don't really understand what the author is trying to present. And it's not presented to be accessible...
Strictly for insiders only? I wouldn't even know where to find out what language that is. It has something to do with e-graphs, which seems to be a veritable rabbit hole.
Yes, perhaps. This is not written as a general introduction to e-graphs. They are a data structure that compactly holds many equivalent versions of terms / syntax trees. Egraphs are a solution to phase ordering issues for greedy rewrites. They are also just a useful fabric for optimization tasks. They are being used in many compiler projects https://github.com/philzook58/awesome-egraphs . Mostly research compilers, but cranelift and luminal are not for example.
Many applications are naturally expressed using bound variables (lambdas, summation expressions, einstein indices, integrals, loops) but the basic e-graph doesn't really support the concept. One can instead model using combinators (SKI combinators, relation algebra, categorical combinators, other) but this tends to be not entirely natural and tends to explodes in the search space of different ways to encode the same concept using combinators.
Lifting e-graphs are a variant of sorts of slotted e-graphs, which are techniques to supports binders in egraphs. It's more subtle to do so than one might think. Lambda microegg also adds a surface syntax to play around more easily.
Thank you. I remember reading “Gödel, Escher, Bach” and getting into the rabbit hole of term-rewriting. Then figured out it would be a fantastic way to build a compiler, simply by iteratively rewriting expressions into what is basically assembly code. Would also be a great framework for a modular bring-your-own-parser compiler construction kit. Going from theory to practice on how to achieve that, i.e. the best way to declaratively encode such transformations in Lisp-like language, how to deal with conflicts, ambiguity and the exponentially exploding search space eventually led me to e-graphs and some of the stuff you mention in this comment…
At which point it felt like having jumped into the deep sea, at night, and sharks are all around. I have no formal education in CS, and a lot of this stuff is way above my pay grade. Though it made me wonder why none of this stuff has hit mainstream; modern compilers are still very crude, it seems like such an obvious idea to model compilation as transformation of one graph into another. Is this just fringe academic research that hasn’t yet trickled down to the masses of us code monkeys?
I still have a soft-spot for this niche of computer science, but I need to find 5 years and 20 IQ points to understand how it all fits together.
I personally have a great respect and love of the intuitive and consider formalism or abstract mathematics only interesting in the service of elaboration or exploration of the intuitive.
Basically all optimizing compilers have a simplifier or rewriter in them. I don't see it as a requirement or even necessarily a priori desirable to frame their discussion or formulation in terms of high barrier mathematical language. Do so if it is fun or useful. Sometimes it is. It is to my subjective taste to do so. Compiler writers are a pretty clever group by and large and are aware of a decent amount of useful math.
There is also a tendency to underestimate where 10 years of study and effort applied to a subject can bring you and attribute it totally to some intrinsic intelligence.
Term rewriting _is_ really neat. Realizing and remembering what you find neat and exciting is important. I like equations.
I'd like to think I know a thing or two about math/cs... but I don't really understand what the author is trying to present. And it's not presented to be accessible...