Finding computational content in classical proofs

Summary

Summary

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.