Thursday, 19 July 2001

Just one more X

Listening to:

Brahms, clarinet trio in A minor, op. 114.

There’s a certain class of computer games out there, sometimes characterised as 4X games (“eXplore”, “eXpand”, “eXploit” and “eXterminate” or some such), that are known for their addictive “just one more turn” qualities. The first game in this mold was probably Civilisation, where the player has to control a civilisation from its earliest beginnings all the way to the point where it is ready to send a space-ship to Alpha Centauri. (This PC game has only a very tenuous connection to the classic board-game of the same name.)

I’d just like to briefly claim that interactive theorem-proving is subject to a similar phenomenon, which I (and others) call “just one more lemma”. Say you’re trying to prove big complicated theorem X. You spend a while on this before realising that you can’t prove it, without first proving supporting lemma Y. But then it becomes clear that Y needs a theorem about lists that the developers of the system haven’t included (incredulously you think to yourself, “How on earth could anyone ever prove anything without first knowing that MEM x (FILTER P l) = MEM x l /\ P x ? I mean; come on!”)

These “to prove X, I will first need Y” links build into ever larger stacks. In fact, it can become easy to lose track of the original goal entirely. But now, I have to go and prove sub-lemma Z103.