Argmungers in universal algebra

Some of you might be interested to learn that argmungers are now explicitly included in my thesis: the mathematical concept, that is, not the code. One can recast classical universal algebra (which works syntactically, with words in a recursive language and denumerable sets of variables) in terms of planar trees of operators (abstract syntax trees, effectively) acted on by munging functions (and yes, I use the term "munging function"). Restricting the munging functions allowed is equivalent to imposing syntactic restrictions on the equations defining your theories: I'm writing up a proof of this at the moment. Interestingly, isolating the concept of munging functions makes the whole thing significantly cleaner: up until then, the theorem was frustratingly obvious, but trying to prove it (or even state it!) rigorously was like nailing jelly to the wall.

Maybe I should thank Hitesh in my acknowledgements...

Oh, and current state of play:

Sat Apr 26 00:47:12 BST 2008
4511 lines 22164 words 155551 characters
thesis.log:Output written on thesis.dvi (78 pages, 626444 bytes).
34 fixmes

I was up to 79 pages, but then I deleted some redundant stuff, so now I'm back down to 78.

Right, time to pack for the mountains tomorrow.