The following post was 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 is
How to build an Algebra Program in Qi
_________________________________
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 (hiya 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.
OK, breakfast calls. 12.38 - definitely turning into a hacker.
Mark