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.

(datatype expr

__________________________
(number? X) : verified >> X : number;

X : number;
_________
X : expr;

if (not (element? X [- * / +]))
X : symbol;
_________
X : expr;

Op : (number --> number --> number);
X : expr;
Y : expr;
=======
[X Op Y] : expr;)

A quick test:

(1+) [56 + [x - 7]]
[56 + [x - 7]] : expr

(2+) [[-245 * 67] - [x * y]]
[[-245 * 67] - [x * y]] : expr

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.

(define arith
{expr --> expr}
[X Op Y] -> (Op X Y) where (and (number? X) (number? Y))
X -> X)

Test:

(6+) (arith [9 - 8])
1 : expr

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.

__________
arith : valid;

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.

(define compose
{[(A --> A)] --> (A --> A)}
[F] -> F
[F | Fs] -> (/. X ((compose Fs) (F X))))

A quick test in Qi:

(7+) (compose [sqrt sqrt])
#<COMPILED-FUNCTION compose-1> : (number --> number)

(8+) ((compose [sqrt sqrt]) 16)
2 : number

Now certainly the composition of valid functions should produce a valid function. We add this as a sequent rule.

Fs : [valid];
_________________
(compose Fs) : valid;

Here's another very useful higher-order function.

(define recurse
{(expr --> expr) --> expr --> expr}
F [X Op Y] -> (F [(recurse F X) Op (recurse F Y)])
F X -> (F X))

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;
________________
(recurse 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
X) = X is true. Certainly the operation of applying a valid operation until you cannot reduce the input further is itself perfectly valid. So lets add fix.

F : valid;
__________
(fix F) : valid;

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
algebra system, the typechecker can not only tell us "Yes, that function outputs syntactically legal algebra" but also it can tell us "And also the heuristics you are using are valid".

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;
X : expr;
_______
(F X) : ok-expr;

Also ok-exprs are exprs themselves.

X : ok-expr;
_________
X : expr;

Then off I go - here's one called kenny that elegantly knocks an expression into submission.

(define kenny
{valid --> expr --> ok-expr}
F E -> (fix (recurse F) E))

Test:

(10+) (kenny arith [x + [12 * [5 - 3]]])
[x + 24] : ok-expr

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.

Mark