[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
- qi (for 1 ≤ i ≤ k), the conditions which determine the different induction steps: one induction step for each qi
- k, the number of induction steps (and thus of conditions)
- σi,j (for 1 ≤ i ≤ k and 1 ≤ j ≤ hi), the substitutions applicable to condition qi; each condition qi may have up to hi hypotheses and corresponding substitutions
- hi, number of induction hypotheses for each induction step qi
- 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, qi ≤ k, k, σi, j, hi, 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.
Sometimes I think Enrique has too much time on his hands.