Search Algorithms in Type Theory

In this paper, we take an abstract view of search by describing search procedures via particular kinds of proofs in type theory. We rely on the proofs-as-programs interpretation to extract programs from our proofs. Using these techniques we explore, in depth, a large family of search problems by parameterizing the specification of the problem. A constructive proof is presented which has as its computational content a correct search procedure for these problems. We show how a classical extension to an otherwise constructive system can be used to describe a typical use of the nonlocal control operator call/cc. Using the classical typing of nonlocal control we extend our purely constructive proof to incorporate a sophisticated backtracking technique known as 'conflict-directed backjumping' (CBJ). A variant of this proof is formalized in Nupr1 yielding a correct-by-construction implementation of CBJ. The extracted program has been translated into Scheme and serves as the basis for an implementation of a new solution to the Hamiltonian circuit problem. This paper demonstrates a nontrivial application of the proofs-as-programs paradigm by applying the technique to the derivation of a sophisticated search algorithm; also, it shows the generality of the resulting implementation by demonstrating its application in a new problem domain for CBJ. (C) 2000 Elsevier Science B.V. All rights reserved.