This post springs out of a very long line of thought, which I will only summarise small parts of.

It began with the puzzling realisation that the algorithm which computers use to perform symbolic integration is radically different from the guess-and-check method taught in schools. My first reaction was, why are we not taught the systematic way of doing it? This is true for other areas of mathematics as well. In a few cases, such as solving quadratic equations or systems of linear equations, students are eventually taught the fast way. However, in many cases, the existence of an algorithm is not even mentioned.

My point, however, is not to criticise the educational practice; in fact, I agree with the idea of teaching mathematics as an exploration of ideas rather than an application of formulaic solution methods. Rather, I would like to encourage people to eventually learn the algorithms, and try to apply them. A good algorithm is a study in rational behaviour, and I think we can take home a lesson from each.

I'll just give two examples which I find particularly fascinating: Knuth-Bendix completion and the summary-product algorithm. The first is most relevant to fast mathematical reasoning. The second is relevant to studying the reasonableness of fast-and-messy probabilistic reasoning, the way humans do it.

Knuth-Bendix Completion

Knuth-Bendix completion ("K-B" from now on) is a fascinating formalisation of the mathematical idea of simplification. Everyone should recognise the phrase "simplify your answer" from high school homework assignments. I never suspected that simplification could be a really powerful method for mathematical reasoning.

K-B is a method for reasoning about equality. Equality is one of the simplest relationships we can have between two things, yet the naive way of reasoning about it results in an explosion of possible inferences. If there are N things in our universe, there are N² equality statements which may be true or false. We can substitute equals for equals all day and get nowhere. So why does it seems like such a simple relation? I think the K-B algorithm gives a good answer to that.

We start with the basic axioms for the domain we are reasoning about. The domain consists of a set of expressions, some of which are equal to others. The axioms provide some general equalities; for example, they might be the trigonometric identities, if we a...

arnaw

arnaw

arnaw

arnaw