Nottingham FP Lab Blog

Peano, episode 3

by Conor on August 7, 2007.
Tagged as: Lunches.

I 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.

> double : Nat -> Nat > double one = suc one > double (suc n) = suc (suc (double n)) > > measure : Bin -> Nat > measure 1 = one > measure (b ; 0) = double (measure b) > measure (b ; 1) = suc (double (measure b))
Show that stripping bsuc decreases the measure.
J doesn’t have to define doubling, of course, and ACL2 knocks off

$%format == = \equiv > measure (bsuc i) = suc (measure i)$
%format == = \equiv > measure (bsuc i) = suc (measure i)

without 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.