Finding computational content in classical proofs
Robert L. Constable, Chet Murthy · Cambridge University Press eBooks · 1991
We illustrate the effectiveness of proof transformations which expose the computational content of classical proofs even in cases where it is not apparent. We state without proof a theorem that these transformations apply to proofs in a fragment of type theory and discuss their implementation in Nuprl. We end with a discussion of the applications to Higman's lemma by the second author using the implemented system. Introduction: Computational content Informal practice Sometimes we express computational ideas directly as when we say 2 + 2 reduces to 4 or when we specify an algorithm for solving a problem: “use Euclid's GCD (greatest common divisor) algorithm to reduce this fraction.” At other times we refer only indirectly to a method of computation, as in the following form of Euclid's proof that there are infinitely many primes: For every natural number n there is a prime p greater than n . To prove this, notice first that every number m has a least prime factor; to find it, just try dividing it by 2, 3, …, m and take the first divisor. In particular n ! + 1 has a least prime factor. Call it p . Clearly p cannot be any number between 2 and n since none of those divide n ! + 1 evenly. Therefore p > n . QED This proof implicitly provides an algorithm to find a prime greater than n .