Where are all the Rewrite Rules?
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...
What is the context? Is there tooling to use these to simplify programs? Are they meant only for formal verification? Something else?
Rubi integration rules where mentioned, but here is a list of other open-source Mathematica rules: https://github.com/corywalker/expreduce/tree/master/expreduc...
I thought this was going to discuss about Apache RewriteRules
Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!
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.
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).
Before clicking, realize this articles not about Apache mod_rewrite
Brilliant idea!
rewrite rules
1: use rust
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.
[dead]
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!
[1] http://abstractionlogic.com