notes on term rewriting

1 files changed, 54 insertions, 0 deletions

diff --git a/notes/term_rewriting.md b/notes/term_rewriting.md
new file mode 100644
index 0000000..9d0255a
--- /dev/null
+++ b/notes/term_rewriting.md
@@ -0,0 +1,54 @@
+
+Syntax for term re-writing:
+
+    (rule <pattern>
+          <substitute>)
+
+Pattern examples:
+
+    (? a)
+    (? a number?)
+    (? a not-number?)
+    (? a number? odd?)
+    (? a (free? x))
+    (? a (neq? 0))
+
+    ; match zero or more into a list; expand list in-line, same order
+    (?* l)
+
+Full examples:
+
+    (rule (/ 1 (/ (? a) (? b)))
+          (/ (? b) (? a)))
+
+Simplifications:
+
+- variable names must be single Latin letter
+- predicates are fixed to a set of type checks
+
+## Implementation
+
+Separate rule lists, one for each "head" type (Sum, Product, Power, etc).
+
+    struct RuleSet {
+        sum_rules: Vec<Rule>,
+        product_rules: Vec<Rule>,
+        [...]
+    }
+
+    struct Rule {
+        variables: HashMap<type, char, Vec<predicates>>,
+        pattern: MatchExpr,
+        substitute: MatchExpr,
+    }
+
+    enum MatchExpr {
+        variable: char,
+        atom: CExpr,
+        list: { head: expr_type, tail: Vec<MatchExpr> },
+    }
+
+----------------
+
+Backburner:
+- are additional pattern-wide predicates necessary or helpful?