Math editor
Well, I’ve finally made some progress on my algebra editor. (Really, it’s more of an environment for the construction of formal systems at this point, but I plan to make it extremely algebra-friendly, such that using it will be much faster and less error prone than pen and paper for most students.) I did this by giving up the idea of implementing it in Lisp, and instead using a language that I use professionally, C#, to really get something done with it. And it really works. I have it to where you can add, edit, delete, and organize axioms, and create theorems and proofs and apply axioms to parts of them. And it’s all saved to disk, too. For instance, if you have
(+ (+ a b) (+ c d))
and you want to change it to
(+ (+ a c) (+ b d))
you need to use two axioms. The first is additive commutativity. It says that any (+ x y) can be transformed into (+ y x), where x and y match any expression. The second is additive associativity, which says that (+ x (+ y z)) can be transformed into (+ (+ x y) z) (and vice versa). So let’s see how this pans out with our problem, shall we?
(+ (+ a b) (+ c d))
(+ a (+ b (+ c d)))
(+ a (+ (+ c d) b))
(+ a (+ c (+ d b)))
(+ (+ a c) (+ d b))
(+ (+ a c) (+ b d))
Using this two axioms, and over a dozen others, I’ve been able to do a lot of algebra, including proving the quadratic formula.
Of course, seeing all these axioms lying around can be a bit disconcerting. I mean, doesn’t it seem like you’d be able to prove a lot of these things? I feel kind of weird putting things like (* (^ x n) (^ y n)) -> (^ (* x y) n) as axioms instead of being able to prove them. But how would I go about proving these things with my current system? I think it’s actually impossible, and I think the reason is that my simple symbol substitution system doesn’t allow for the use of inductive proofs. But I’m not sure how to add this capability cleanly. Surely there’s a way?
Here’s the rules. You start with an expression, which is a nested list of symbols. You apply a transformation (either an axiom or theorem) to it, which is two lists of symbols with named wildcards. If the first list matches your expression (list structure + symbol contents, except for wildcards), you replace the wildcards in the second list with their values from the match in the first list. You repeat as necessary.
Can this process be used to prove things using mathematical induction? Axioms specifically for the support of induction are allowed. But I can’t see a way.
Another issue that I’ve come across is that it’s possible to do some bad things with this system, like, say, proving 2 = 1. Here’s how (using ascii format instead of prefix lisp format for clarity).
1. 1 = 1
2. x = 1, letting x = 1
3. x*x = x, multiplying by x
4. x*x - 1 = x - 1
5. (x + 1)(x - 1) = x - 1, factoring
6. x + 1 = 1, dividing
Of course, this proof is invalid, since dividing by x - 1 is division by zero. But how should this be handled in my program? The axiom used in step 5 looks like this: (= x y) -> (= (* x z) (* y z)). Is there anything wrong with that? Perhaps it’s not the axiom that’s at fault, but the value substituted for z, namely, (/ (+ x (- 1))), or 1/(x - 1). Perhaps anytime a new value is introduced into the equation containing a dividend, a constraint should be added such that the dividend cannot equal zero. (Not a terribly clean solution, and may sometimes be more than what’s necessary.)
Another thing that I’ve come across is the handling of +/- values from square roots. I’m not sure how to do this cleanly either. Again, the suspect axiom is an equation operation: (= x y) -> (= (^ x n) (^ y n)). It’s perfectly valid for all natural n, but if n becomes fractional, as in (/ 2) for square root, then all of a sudden it looks more like (= (+- (^ x n)) (+- (^ y n))). I think. I’m not too sure, actually. All I know is that (= x y) -> (= (^ x n) (^ y n)) just doesn’t work.
In other words, things are just a bit of a mess with it mathematically at the moment. I think that if I could figure out the induction thing, the proofs I come up with could lead to the natural falling out of some solutions for my problems with division by zero and the taking of square roots. I suppose maybe possibly. In any case, the induction issue is probably more interesting for me.
If you’re interested in working with the program any, just drop me a line and I can send you a copy. The software requires Windows and the .NET 2.0 framework.
