3 ms·

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 w

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 http://abstractionlogic.com

philzook 2y 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 2y 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 https://doi.org/10.1017/CBO9781139172752

philzook 2y 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 2y 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 https://doi.org/10.1017/CBO9781139172752