The Origin of a Binary-Search Paradigm. Revision.

Abstract

In a binary-search algorithm for the computation of a numerical function, the interval in which the desired output is sought is divided in half at each iteration. This paper considers how such algorithms might be derived from their specifications by an automatic system for program synthesis. The derivation of the binary-search concept has been found to be surprisingly straightforward. The programs obtained, though reasonably simple and efficient, are quite different from those that would have been constructed by informal means. Keywords: Program synthesis; Theorem proving; Binary search, Real square root, Lambo function; Deductive tableau system; Computer programming.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1986
Accession Number
ADA193996

Entities

People

  • Richard Waldinger
  • Zohar Manna

Organizations

  • SRI International

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Artificial Intelligence
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Intervals
  • Iterations
  • Language
  • Mathematics
  • Programming Languages
  • Real Numbers
  • Specifications
  • Square Roots
  • Theorems
  • United States

Readers

  • Computational Linguistics
  • Operations Research