_______ __ _______
| | |.---.-..----.| |--..-----..----. | | |.-----..--.--.--..-----.
| || _ || __|| < | -__|| _| | || -__|| | | ||__ --|
|___|___||___._||____||__|__||_____||__| |__|____||_____||________||_____|
on Gopher (inofficial)
URI Visit Hacker News on the Web
COMMENT PAGE FOR:
URI Where are all the Rewrite Rules?
philzook wrote 1 hour 32 min ago:
Surely Hacker News has awareness of many, many rewrite rule files. Keep
em coming!
cratermoon wrote 1 hour 46 min ago:
Before clicking, realize this articles not about Apache mod_rewrite
nottorp wrote 1 hour 42 min ago:
Yeah, it could use some info about whose rewrite rules...
l0b0 wrote 3 hours 37 min ago:
What is the context? Is there tooling to use these to simplify
programs? Are they meant only for formal verification? Something else?
philzook wrote 1 hour 5 min ago:
Wide context.
But to be a bit more specific, I've been involved in the egraphs
community [1] and we don't currently have a shared database of
rewrite rules for benchmarking, nor do we collect the rules from
different projects. Seeing the actual files is helpful.
On a slightly different front, I'm also trying to collect rules or
interesting theories up in my python interactive theorem prover
Knuckledragger [2] . Rewrite rule or equational theory looking things
are easier to work with than things with deeply nested notions of
quantifiers or tons of typeclass / mathematical abstraction like you
find when you try to translate out of Coq, Lean, Isabelle.
There are also different approaches to declarative rewrite rules in
major compilers. GCC, LLVM, and cranelift have their own declarative
rewrite rule systems for describing instruction selection and
peephole optimizations but also of course lots of code that
programatically does this. I also want to collate these sorts of
things. Working on fun clean systems while not confronting the ugly
realities of the real and useful world is ultimately empty feeling.
Science is about observing and systematizing. Computer science ought
to include occasionally observing what people actually do or need.
URI [1]: https://github.com/philzook58/awesome-egraphs
URI [2]: https://github.com/philzook58/knuckledragger
codeulike wrote 1 hour 33 min ago:
Yes I also feel some context would help.
mikhailfranco wrote 3 hours 37 min ago:
For a historical perspective, look at (in this order):
1. JoGo's OBJ and Maude: algebras on a rewrite engine [1] 2. SPECWARE:
a Category Theory approach from SRI Kestrel Institute [2]
URI [1]: https://cseweb.ucsd.edu/~goguen/sys/obj.html
URI [2]: https://www.specware.org/research/specware/
URI [3]: https://github.com/KestrelInstitute/Specware/blob/master/Libra...
FjordWarden wrote 3 hours 48 min ago:
Rubi integration rules where mentioned, but here is a list of other
open-source Mathematica rules:
URI [1]: https://github.com/corywalker/expreduce/tree/master/expreduce/...
philzook wrote 1 hour 28 min ago:
This looks great! Are there files or sections in particular I might
want to focus on?
nraynaud wrote 3 hours 55 min ago:
Brilliant idea!
tonyhart7 wrote 5 hours 7 min ago:
rewrite rules
1: use rust
almostgotcaught wrote 7 hours 48 min ago:
x = x
x = x + x - x
x = x + x - x + x - x
...
you get the point
this isn't deep - there's a reason why ZFC stands out amongst all
possible sets of "foundations" - it's because in lieu of an analytic
cost function (which isn't possible) we have consensus.
maweki wrote 4 hours 47 min ago:
> we have consensus
It's decidable whether a TRS is confluent, i.e. if a fixpoint exists,
exactly one fixpoint exists. Or what do you mean?
almostgotcaught wrote 4 hours 29 min ago:
i don't know what you're trying to say. i'm saying that "all" the
rewrite rules don't matter, only the "interesting" ones matter but
interesting is related to opinion/taste/cost.
maweki wrote 4 hours 21 min ago:
rewriting rules are more like function/predicate definitions in
FP or LP and not like axioms. Term rewriting does have its own
axioms, like ZFC does.
What you're saying is akin to "not all functions are
interesting". Well, yes...
But that's true for any model of computation.
fjfaase wrote 8 hours 7 min ago:
I have been thinking about implementation oriented rewrite rules that
for example express that you can add two numbers smaller than 2^2n with
three addition operations (and some other operations) on numbers
smaller than 2^n or with two addition operations that take an
additional integer smaller than 2 (usually called a carry in hardware
implementations).
practal wrote 8 hours 44 min ago:
Such a database of rewrite rules only doesn't make much sense because
the semantic part is missing (what does a rule mean, and why is it
correct?), and so you will run into inconsistencies quickly as the
database grows.
But if you take the idea of a universal system for rewrite rules
seriously, and add just enough semantics to make it work as a logic,
you might arrive at abstraction logic [1]. That is actually a great way
of explaining abstraction logic to computer scientists, come to think
of it!
URI [1]: http://abstractionlogic.com
philzook wrote 1 hour 33 min ago:
I don't always care about consistency between rule sets. Depends what
I'm trying to do.
The question at hand is motivating and getting benchmarks for
different approaches or engines to equational reasoning / rewriting.
I sometimes lose sight of motivations and get discouraged. Doing
associativity and commutativity and constant fusion for the nth time
I start to become worried it's all useless.
o11c wrote 9 hours 4 min ago:
In general, for any invertible function (or partially invertible
function if we can know the input is in the right subset) we need to
recognize a rule fâ»Â¹(f(x)) === x; note that this usually does not
apply when floats are involved.
One interesting case for `f` is the gray code conversion, whose inverse
requires a (finite) loop. This can be generalized to shifts other than
1; this is common in components of RNGs. [1]
URI [1]: https://en.wikipedia.org/wiki/Inverse_function
URI [2]: https://en.wikipedia.org/wiki/Gray_code
lutherqueen wrote 9 hours 17 min ago:
I thought this was going to discuss about Apache RewriteRules
philzook wrote 1 hour 38 min ago:
I'm curious if there is a useful connection between Apache's rule and
other term rewriting. Some sort of static analysis? If there is a
interesting database of them, I'd add it.
chrisweekly wrote 2 hours 47 min ago:
Me too. I went DEEP into mod_rewrite, mod_proxy and friends in the
early 2000's. It's a dangerous place to put too much logic, but also
incredibly powerful. On multiple occasions, I used it to solve
problems in a couple hours that would've taken the engineering team
weeks or months to address.
pavel_lishin wrote 1 hour 38 min ago:
Can you say more about this? It sounds really interesting!
DamonHD wrote 5 hours 13 min ago:
Yep, and I had a whole bunch ready to show off! I've even given
talks about them at conferences! B^>
janderson215 wrote 4 hours 54 min ago:
Do you have slides posted anywhere or a video of one of your talks
that you could share?
DamonHD wrote 4 hours 46 min ago:
FOSDEM unplanned(!) lightning talk (video and PDF): [1] Also see
main working page: [2] I can point you to bits of config (it's a
bit scattered in my blogs at the moment) like this:
URI [1]: https://fosdem.org/2025/schedule/event/fosdem-2025-6839-...
URI [2]: https://www.earth.org.uk/RSS-efficiency.html
URI [3]: https://www.earth.org.uk/note-on-site-technicals-83.html...
janderson215 wrote 4 hours 7 min ago:
Thank you!
DIR <- back to front page