[FOM] Checkers is a draw
Timothy Y. Chow
tchow at alum.mit.edu
Thu Jul 26 14:45:56 EDT 2007
Neelakantan Krishnaswami <neelk at gs3106.sp.cs.cmu.edu> sent me a very
informative reply to my remarks/questions about formal verification, which
I am forwarding to FOM with permission.
> Hi Timothy,
>
> I work in formal verification, so maybe I can shed some light on the
> puzzle you posed in this and your earlier message.
>
> The short answer is that proof-checking in most proof assistants (Coq,
> Isabelle, Lego, etc) is not NP-complete -- it is complete for
> higher-order arithmetic. That is, checking a proof can take time
> bounded by the longest-running function you can prove terminates with
> some version of higher-order arithmetic.
>
> So proof checking can take a really stunningly huge amount of time.
>
> The reason for this is that most proof checkers are basically variants
> of typed lambda calculus, whose type theories include a rule of the
> following form:
>
> e : A A <--> B
> ------------------
> e : B
>
> where --> is the reduction relation for the lambda calculus. So if e
> is a proof of A, and A is beta-reducible to B or vice-versa, then e
> is also a proof of B.
>
> So you can write (total) programs as typed lambda terms, and proof
> checking can involve running those programs. We still know that proof
> checking will terminate, because well-typedness plus the consistency
> of the logic guarantees termination, but it can take a really long
> time.
>
> To understand why this sort of rule is necessary, consider the example
> of showing that 170 * 40 = 6800. No one will do this proof by
> appealing to Peano's axioms, because it would be thousands of lines
> long. Instead we will /calculate/ that 170 * 40 gives 6800, and then
> appeal to reflexivity, which is a one-line proof plus some
> computation.
>
> Poincare foresaw the need for this sort of rule a century ago; the
> story goes that upon seeing a formal proof of some trivial arithmetic
> fact he is supposed to have asked, "And how will you prove a real
> theorem?" In his essay, "Science and Hypothesis", he contrasted
> computation (which he called verification) with deduction proper, and
> argued that only deductive steps should be included in a formal proof,
> since the calculations can be re-done by the person checking the
> proof.
>
> So in type theory this sort of conversion rule is sometimes called the
> Poincare principle.
>
> It also means that proofs that are a mix of computation (say, to
> generate and test a huge but finite number of configurations) and
> deduction (to show that these configurations are all the ones you need
> to check) are very natural to represent in type theory. This is
> essential to Gonthier's formal proof of the four-color theorem, and to
> Hales's (ongoing) formal proof of the Kepler conjecture.
>
> --
> Neel R. Krishnaswami
> neelk at cs.cmu.edu
More information about the FOM
mailing list