Where are all the Rewrite Rules?
28 comments
·February 19, 2025mikhailfranco
For a historical perspective, look at (in this order):
1. JoGo's OBJ and Maude: algebras on a rewrite engine
https://cseweb.ucsd.edu/~goguen/sys/obj.html
2. SPECWARE: a Category Theory approach from SRI Kestrel Institute
https://www.specware.org/research/specware/
https://github.com/KestrelInstitute/Specware/blob/master/Lib...
practal
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!
philzook
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.
FjordWarden
Rubi integration rules where mentioned, but here is a list of other open-source Mathematica rules: https://github.com/corywalker/expreduce/tree/master/expreduc...
philzook
This looks great! Are there files or sections in particular I might want to focus on?
lutherqueen
I thought this was going to discuss about Apache RewriteRules
philzook
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
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
Can you say more about this? It sounds really interesting!
DamonHD
Yep, and I had a whole bunch ready to show off! I've even given talks about them at conferences! B^>
janderson215
Do you have slides posted anywhere or a video of one of your talks that you could share?
DamonHD
FOSDEM unplanned(!) lightning talk (video and PDF):
https://fosdem.org/2025/schedule/event/fosdem-2025-6839-ligh...
Also see main working page:
https://www.earth.org.uk/RSS-efficiency.html
I can point you to bits of config (it's a bit scattered in my blogs at the moment) like this:
https://www.earth.org.uk/note-on-site-technicals-83.html#202...
null
l0b0
What is the context? Is there tooling to use these to simplify programs? Are they meant only for formal verification? Something else?
codeulike
Yes I also feel some context would help.
o11c
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.
cratermoon
Before clicking, realize this articles not about Apache mod_rewrite
nottorp
Yeah, it could use some info about whose rewrite rules...
fjfaase
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).
nraynaud
Brilliant idea!
tonyhart7
rewrite rules
1: use rust
almostgotcaught
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
> 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
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
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.
Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!