[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
• m, the measure to be used when computing the ‘size’ of a particular instance of the formula
• q_i (for 1 ≤ i ≤ k), the conditions which determine the different induction steps: one induction step for each q_i
• k, the number of induction steps (and thus of conditions)
• σ_i,j (for 1 ≤ i ≤ k and 1 ≤ j ≤ h_i), the substitutions applicable to condition q_i; each condition q_i may have up to h_i hypotheses and corresponding substitutions
• h_i, number of induction hypotheses for each induction step 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

Philosophers make quick keyboardists; strength in judgment helps improve mental capacity.

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

Philosophy multiplies quizzical subtleties.

“Easy, see?”

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