From: dam@ai.mit.edu (David McAllester)
Date: Sun, 30 Apr 95 14:44:08 EDT
Message-Id: <9504301844.AA21652@spock>
To: pollack@cs.chalmers.se
Cc: qed@mcs.anl.gov
In-Reply-To: Randy Pollack's message of Thu, 27 Apr 1995 20:22:37 +0200 <199504271822.UAA01520@muppet53.cs.chalmers.se>
Subject: Paper on reflection
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


   [The constructed proof of the four color theorem] is clearly big, but not
   clearly infeasible.

I interpret John Harrison as saying, among other things, that one can
always write complex decision procedures in a style in which they
output proofs.  It seems to me that the real issue is one of constant
factors.  A constant factor of 100 can be the difference between
feasible and infeasible.  It seems very likely to me that in the four
color theorem an HOL tactic would run a factor of 100 or more slower
than a C program (probably more like a 1000).  Of course to use a C
program in a foundational verifier one would have to verify C (as John
notes).  Since the four color theorem is by now fairly old, it may be
feasible to solve it with a slow program.  But other "black-box"
theorems may be more challenging, e.g., recent results on the
non-existence of certain quasi-groups.  It seems to me that
cutting-edge black-box theorems will always be challenging for a
foundational prover unless it can verify and run C code or some
imperative equivalent.

I am not saying that these black-box theorems are important to the QED
effort.  Rather, they seem like the primary place where computational
extensions, such as reflection, might pay off.

	David