## Peano, episode 3

August 7th, 2007 by ConorI did the Peano gig for the Edinburgh DReaMers. It was great to meet J Moore there, and he got interested enough to bang out a proof of binPeano with ACL2, in double quick time. His proof goes in three easy stages:

- Define a
*measure*from Bin to the ordinals.

Actually, we don’t go above ω, so the naturals will do. The obvious measure is

just the translation from binary to unary representation. For today only, start Nat at one. - Show that stripping bsuc
*decreases*the measure.

J doesn’t have to define doubling, of course, and ACL2 knocks offwithout the slightest trouble. It’s a slam dunk for ‘recursion analysis’ as

brought to us by…Bob Boyer and J Moore. Structural induction on i, symbolic evaluation, inductive hypothesis. - Ordinal induction.

I claim that James McKinna’s proof is just what happens when you do J Moore’s proof ‘by smugness’. The Peano family is exactly Nat marked up with the bsuc semantics. Then double becomes double and measure becomes peano. So we’re singing the same old happy song, after all.

August 7th, 2007 at 8:07 pm

> double (suc n) = suc (suc n)

Shouldn’t that be

> double (suc n) = suc (suc (double n))

?

September 22nd, 2007 at 9:43 am

Yes. Fixed. I wish I had a typechecked blog.