Improving the Efficiency of Nuprl Proofs

Abstract

In order to use Nuprl system as a programming language with built-in verification one has to improve the efficiency of the programs extracted from the Nuprl proofs. In the current paper we consider proofs from the Nuprl automata library. In some of these proofs (pigeon-hole principle, decidability of the state reachability, decidability of the equivalence relation on words induced by the automata language) sources of exponential-time complexity have been detected and replaced by new complexity cautious proofs. The new proofs now lead to polynomial-time algorithms extracted by the same Nuprl extractor, thus eliminating all known unnecessary exponentials from the Nuprl automata library. General principles of efficient programming on Nuprl are also discussed. Key Words and Phrases: automata, constructivity, Myhill-Nerode theorem, Nuprl, program extraction, program verification, state minimization.