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:

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.

comments powered by Disqus