Algebra-mode
So I’ve been wanting to learn math for a while. Really get a handle on calculus, learn some probability theory, and who knows what next? But I’m not terribly great at it. I have problems dealing with the algebra. Managable problems, for sure. But I have an itch. Why not make a program that lets you manipulate algebraic equations without error? I know exactly what form such a program would take.
And it’s not quite this. And it’s nowhere near this or this. Those programs can do a whole bunch, but they don’t do what I want to do. So what is it I want to do?
When you’re solving algebraic equations on paper, you write down the first expression (which can be an equation) and you apply identity-preserving (or truth-preserving, for an equation) transformations on it. Those transformations can be (almost) formally defined in terms of the symbols of the expression combined with the application of a limited number of axioms. For instance, take the axiom that x*y = y*x. This axiom establishes that multiplication is commutative. You can repeatedly apply these axioms, along with some simple arithmetic, to come up with any algebraic manipulation. That includes things like trigonometry. Of course, your axioms aren’t going to be limited to arithmetical things. You’re going to have some axioms defining the behavior of series and sums, for instance, and perhaps some defining the behavior of derivatives. You might be able to squeeze out definitions and relationships for the trigonometric identities based on sums and things, but those are things that aren’t covered in basic math texts.
So anyway, this suggests a computer program in which you start out by entering a mathematical expression, and you repeatedly apply axioms, or series of axioms that are grouped into single commands, on different parts of your expression to transform it into what you’re aiming at. One difficulty in this is efficiently selecting the subexpression and the axiom you want to apply. A great simplification is to use a notation that represents expressions and their subexpressions explicitly. Lisp notation does quite well here. For instance, the multiplicative commutivity axiom could be expressed as ((* x y) (* y x)). Anything that matches the left subexpression gets converted to the right one. Then selecting a subexpression is simply a matter of positioning the cursor on a left parenthesis, or even a single symbol.
The idea is that since each axiom is taken to be valid, and with valid axioms you can only build valid theorems, that any operation you apply to your equation is going to be a good operation. So you never have to worry about getting anything wrong, unless you’re adding axioms. And hopefully you won’t ever have to do that, unless you’re me.
So, you start out this program with a blank document. You add a new theorem, which is simply an arbitrary initial expression with a string of theorems or axioms applied to it. You give it the initial expression to use, and then you go away applying axioms or theorems where you will. When you finish, you can save what you’ve worked on, and use it again later in a single step on other theorems. To choose which theo/axiom to apply on each step, you either press a key that applies it. A key can actually apply a number of different theoaxes that perform analogous transformations, and the correct one is chose depending on the context. For instance, “s” could be the “swap” key, and switch the arguments of a number of different commutative operators. The “+” key could do one thing on an equation (add a number to both sides) and a different thing on any other expression (add and then subtract the same number–presumably the subtraction is to be factored out to simplify something).
If you don’t remember the key to press, or if the theoax you’re looking for doesn’t have a shortcut key, you can look it up in the theoax browser, which shows a hierarchically organized list of theorems and axioms.You can also use this browser to customize shortcut keys, and you can add your own axioms or theorems to this browser if you like.
While you’re editing your theorem, you can see what your equation looks like when typeset all nicely. Press a button, wait half a second, and up pops a nice image of your equation to the right of what you’re editing. When you’ve finished your theorem, you can indent certain lines of the transformation, and then hide everything at that indent level. That way a series of trivial changes can be hidden, and you only see the first and last steps. Finally, you can print a group of theorems out (formatted nicely with two columns) and submit it as your finished homework! Or not.
So, where can you download and start using this program? Well, first, build a time machine… Seriously, I’m working on it, slowly. Picking up some ideas from David Gillespie’s calc-mode. I’ll post any updates here.
