Writing Constructive Proofs Yielding Efficient Extracted Programs

Abstract The NuPRL system [3] was designed for interactive writing of machine-checked constructive proofs and for extracting algorithms from the proofs. The extracted algorithms are guaranteed to be correct which makes it possible to use NuPRL as a programming language with built-in verification[1,5,7,8,9,10]. However it turned out that proofs written without algorithmic efficiency in mind often produce very inefficient algorithms-- exponential and double-exponential ones for problems that can be solved in polynomial time. In this paper we present some general principles of efficient programming in constructive type theory as well as describe a case study that shows how these principles apply to particular problems. We consider the proof of the Myhill-Nerode automata minimization theorem from the NuPRL automata library [4] which leaded to a double-exponential (in time) extracted program. Systematic use of the presented principles allowed us to build a new complexity cautious proof leading to polynomial-time algorithm extracted by the same NuPRL extractor. We believe that the principles presented in this paper in combination with other methods may lead to an efficient technique of programming-by-proofs