Search Algorithms in Type Theory

JL Caldwell, Ian Philip Gent, J Underwood

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)55-90
Number of pages36
JournalTheoretical Computer Science
Volume232
Issue number1-2
DOIs
Publication statusPublished - 6 Feb 2000

Keywords

  • search algorithms
  • proofs-as-programs
  • conflict-directed backjump search
  • nonlocal control (call/cc)
  • Nupr1
  • Hamiltonian circuit

Fingerprint

Dive into the research topics of 'Search Algorithms in Type Theory'. Together they form a unique fingerprint.

Cite this