[17 December 2009]

A mnemonic for ACL2 induction

Lately I’ve been spending time working through a lot of exercises in ACL2. As a way of helping the user internalize the requirements for successful induction, several exercises ask for an explicit reformulation of a problem in terms of the ACL2 induction principle.

Don’t worry: I don’t want to try to explain the ACL2 induction principle here. It suffices for present purposes to observe that a fully explicit application of the ACL2 induction principle requires that you write down a number of things; you, dear reader, don’t need to understand what they are, only that they exist and need to be specified:

**φ**, the formula being proved, the measure to be used when computing the ‘size’ of a particular instance of the formula*m*(for 1 ≤*q*_{i}*i*≤*k*), the conditions which determine the different induction steps: one induction step for each*q*_{i}, the number of induction steps (and thus of conditions)*k***σ**(for 1 ≤_{i,j}*i*≤*k*and 1 ≤*j*≤*h*), the substitutions applicable to condition_{i}*q*; each condition_{i}*q*may have up to_{i}*h*hypotheses and corresponding substitutions_{i}, number of induction hypotheses for each induction step*h*_{i}*q*_{i}- the
**measure conjectures**for the case: (a) that the measure given always produces an ordinal value, and (b) that the measure decreases on each recursive call (i.e. in each induction hypothesis)

After a while, my evil twin Enrique got tired of watching me flip back and forth between the statement of the problem I was trying to solve and the page that showed all the things that needed to be written down; he said “Haven’t you memorized that list yet?” “No,” I said. “It’s not that simple a list, is it?”

“Sure it is,” he said. “Just use a mnemonic to remember it. The full list, with all subscripts, is

φ

m,q,_{i ≤ k}k, σ_{i, j},h,_{i}m c

“So just remember

Philosophersmakequickkeyboardists;strengthinjudgmenthelpsimprovementalcapacity.

“Or if you can remember the subscripts by yourself, and just need (φ, *m*, *q*, σ):

Philosophymultipliesquizzicalsubtleties.

“Easy, see?”

Sometimes I think Enrique has too much time on his hands.