How to Build an Algebra Program in Qi
The following was a post to comp.lang.lisp, inspired by reflecting on Kenny Tilton's algebra program which he's writing in Common Lisp. I wondered how I'd do it in Qi. Its not something I'm tempted to do because its a big app but the *architecture* is interesting. So here's my way of how to do it.
1. First begin by defining the syntax of your algebra. Since this is a post lets be simple; I'm supposing that algebraic expressions (exprs) are regimented into fully parenthesised form. Here are the type rules.
X : number;
if (not (element? X [- * / +]))
Op : (number --> number --> number);
A quick test:
(1+) [56 + [x - 7]]
(2+) [[-245 * 67] - [x * y]]
Righto. On to the next step.
2. The next step is to accumulate a series of operations for (e.g.) simplifying exprs. I'm focussing here on algebra as simplification though there's much more to algebra. Again this is a post so keep it simple.
One operation that is useful is to arithmetically simplify by doing arithmetic; so that [9 - 8] becomes 1. Ok here is a piece of code. Its very simple.
(6+) (arith [9 - 8])
3. Lets say that a algebraic operation is (semantically) valid when its meaning preserving; so that mapping [[9 - 8] + x] to [1 + x] is valid because '[[9 - 8] + x]' and '[1 + x]' 'mean' the same. (I'm not going to get too hung in 'mean the same'; we can say that exprs x and y mean the same if x = y is math'lly provable.)
We're going to start by declaring some of our algebraic operations to be valid. arith has to be included if only cos its the only operation that we've coded. OK in it goes.
Now in a real system we'd chuck in a lot more than arith. No matter, we imagine that this is done, so on to the next step.
4. arith and all the other officially registered valid algebraic operations are the bricks of the algebra system, but bricks do not a house make. You also need cement.
Our cement is a series of validity preserving function generators that build bigger and better validity preserving functions. I'm going to pick out of the hat, three pretty useful ones: compose, recurse and fix.
Compose simply takes a list of functions and forms their composition. Here it is in Qi. /. is a geek lambda.
A quick test in Qi:
(compose [sqrt sqrt])
(8+) ((compose [sqrt sqrt]) 16)
Now certainly the composition of valid functions should produce a valid function. We add this as a sequent rule.
Fs : [valid];
Here's another very useful higher-order function.
recurse simply walks through the elements of the expr and the subexpressions etc. applying the function throughout. Its the sort of thing that is often very useful. We're going to appropriate this little function because expr walking is very useful in this app. Recursing on a valid function produces a valid function.
F : valid;
fix is a Qi system
function; it generates a fixpoint for inputs F and
X such that (F X) = X. It works by repeatedly
applying F to Y until (F
5. OK; now what
we want to do is incorporate this stuff about valid
algebraic operations into the type checker so that when
we build our
So syntax AND semantics are secured.
To do this we define a class of ok exprs. An ok expr is an expression that results from the application of a valid algebraic operation to an expr.
F : valid;
Also ok-exprs are exprs themselves.
X : ok-expr;
Then off I go - here's one called kenny that elegantly knocks an expression into submission.
(10+) (kenny arith [x + [12 * [5 - 3]]])
What benefits do you get from doing it this way?
1. Pattern directed programming is easier to read and debug.
2. You get built-in syntactic guarantees; you can never write a program that outputs anything other than syntactically legal algebra.
3. You get semantic guarantees; Qi will also verify that your algebra program performs the transformations correctly.
Ergo your algebra program is clearer and more reliable.
Copyright (c) 2006, Mark