« BackWhere are all the rewrite rules?philipzucker.comSubmitted by todsacerdoti 5 months ago
  • practal 5 months 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!

    [1] http://abstractionlogic.com

    • philzook 5 months 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.

      • practal 5 months ago

        Fair enough. My personal motivation is abstraction logic (AL), and one way of viewing it is as a generalisation of equational reasoning. I am just starting to implement rewriting for AL, but I will definitely drop you a line once you can play around with it. Maybe AL can be your common format, instead of just a 15th engine for it :-) There are two reasons why I think that:

        1. AL is more general than first-order rewriting, because it has general binders, that is general variable binding constructs.

        2. Unlike higher-order logic, which also has general binders, it doesn't have types, so rewrite rules in AL can be taken for face value, and have no hidden type annotations in them, just like in first-order rewriting (that is a consequence of AL having a single mathematical universe).

        I must admit, I am quite excited about implementing rewriting for AL! My PhD father has co-authored a book about (mostly) first-order term rewriting [1]. Higher-order rewriting based on the lambda calculus is mentioned briefly in it (and of course implemented in Isabelle), and I am wondering if rewriting based on AL instead will bring new insights and/or techniques.

        [1] Term Rewriting and All That. https://doi.org/10.1017/CBO9781139172752

    • lutherqueen 5 months ago

      I thought this was going to discuss about Apache RewriteRules

      • chrisweekly 5 months 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 5 months ago

          Can you say more about this? It sounds really interesting!

        • DamonHD 5 months ago

          Yep, and I had a whole bunch ready to show off! I've even given talks about them at conferences! B^>

        • philzook 5 months 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.

          • undefined 5 months ago
            [deleted]
          • mikhailfranco 5 months ago

            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...

            • l0b0 5 months ago

              What is the context? Is there tooling to use these to simplify programs? Are they meant only for formal verification? Something else?

              • philzook 5 months ago

                Wide context.

                But to be a bit more specific, I've been involved in the egraphs community https://github.com/philzook58/awesome-egraphs 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 https://github.com/philzook58/knuckledragger . 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.

                • l0b0 5 months ago

                  Thanks for the explanation, although I now have more questions :

                  - Why the "graph" aspect of "e-graphs", when it seems all of the ones I've seen in your article and on Wikipedia have only a single edge? Why not just "equivalences"?

                  - The Wikipedia page doesn't seem to explain the actual data structure. If it's a data structure, how is the actual data laid out in a series of bits? Or is "data structure" on that page used in a way which is meant to make sense to mathematicians rather than computer scientists?

                  - How does this relate to existing refactoring tools? Is this a new approach? Or is it what IDEs and language servers already use?

                • codeulike 5 months ago

                  Yes I also feel some context would help.

                • FjordWarden 5 months ago

                  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 5 months ago

                    This looks great! Are there files or sections in particular I might want to focus on?

                  • o11c 5 months 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.

                    https://en.wikipedia.org/wiki/Inverse_function

                    https://en.wikipedia.org/wiki/Gray_code

                    • undefined 5 months ago
                      [deleted]
                      • fjfaase 5 months 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).

                        • philzook 5 months ago

                          Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!

                          • cratermoon 5 months ago

                            Before clicking, realize this articles not about Apache mod_rewrite

                            • nottorp 5 months ago

                              Yeah, it could use some info about whose rewrite rules...

                            • nraynaud 5 months ago

                              Brilliant idea!

                              • almostgotcaught 5 months 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 5 months 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 5 months 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 5 months 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.

                                • tonyhart7 5 months ago

                                  rewrite rules

                                  1: use rust

                                  • curtisszmania 5 months ago

                                    [dead]