proj-oot-ootAlgebraNotes1

an algebraic transform = an optional macro, by which i mean that when you say something like

(a * x) + (b * x) = (a + b) * x

this is sort of like defining a macro that matches on (a * x) + (b * x), and replaces it with (a + b) * x. Except that:

(1) a macro is more constrained; it doesn't just match on a random pattern, it matches on things of the form MACRO_NAME(...). So this is more of a syntax-rule, i guess

(2) this is symmetric, e.g. you can also match on (a + b) * x and replace with the other side. But in general we could have implications rather than only equations, which would yield asymmetric transform rules (syntax rules)

(3) this is optional. The computer is not expected to always substitute (a + b) * x whenever it sees (a * x) + (b * x) , nor to always substitute (a * x) + (b * x) whenever it sees (a + b) * x. Rather, like logical assertions (and, i guess, lazy data structure definitions), this adds to a library of available transform rules which some sort of 'tactics module' then relies upon.