The Origin of the Binary-Search Paradigm

Introduction of the Recursive Calls

Let us continue the derivation one more step. By the well­ founded induction rule, we may introduce the induction hypoth­ esis

In other words, we assume inductively that the output Bqrt(x, v) of the program will satisfy the input-output condition for any inputs x and v such that (x, v) -<w (r, £). The boxed subsentences of goal 3 and the induction hypothesis are unifiable; a most­ general unifier is

We obtain (after true-falBe transformation)

Note that at this point three recursive calls Bqrt(r, 2£) have been introduced into the output entry. The condition (0 ~ r and 0 < 2£) ensures that the arguments r and 2£ of these recursive calls will satisfy the input condition for the program, that r is nonnegative and 2£ is positive. The condition (r, 2£) -<w (r, £) ensures that the newly introduced recursive calls cannot lead to a nonterminating computation. The well-founded relation -<w that serves as the basis for the induction is as yet unspecified.

We omit those portions of the derivation that account for the introduction of the base case and the choice of the well-founded relation. The final program we obtain is

A few words on this program are in order.

Discussion of the Program

The program first checks whether the error tolerance £ is reasonably small. If £ is very big, that is, if max( r, 1) < £ , then the output can safely be taken to be 0. For, because 0 ::; r, we have

And because max(r, 1) <£,we haver< f and 1 < f, and hence r < £ 2 - that is,

Thus, 0 satisfies both conjuncts of the output condition in this case.

Iff is small, that is, f ::; max(r, 1), the program finds a rougher estimate sqrt(r, 2£), which is within 2£ less than ,Jr. The program asks whether increasing this estimate by f will leave it less than ,Jr. If so, the rough estimate is increased by £; if not, the rough estimate is already close enough.

The termination of the program is a bit problematic, because the argument f is doubled with each recursive call. However, the argument r is unchanged and recursive calls are evaluated only in the case in which f ::; max(r, 1), so there is a uniform upper bound on these increasing arguments. More precisely, the well­ founded relation -<w selected in the proof is one such that

provided that 0 < y::; max(r, 1).

If the multiple occurrences of the recursive call sqrt( r, 2£) are combined by eliminating common subexpressions, the program we obtain is reasonably efficient; it requires rlog2(max(r, 1)/£)1 recursive calls.

Our final program is somewhat different from the iterative program we considered in the beginning. The iterative program divides an interval in half at each iteration; the recursive program doubles an interval with each recursive call. Division of the in­ terval in half occurs implicitly as the recursive program unwinds, i.e., when the recursive calls yield output values.

It is possible to obtain a version of the iterative program by formal derivation within the deductive-tableau system. Although the derivation and the resulting program are more complex (it requires two additional inputs), it was this derivation we discov­ ered first, because we were already familiar with the iterative program.

We first found the recursive program in examining the con­ sequences of purely formal derivation steps, not because we ex­ pected them to lead to a program but because we were looking for strategic considerations that would rule them out. When we examined the program initially, we suspected an error in the derivation. We had not seen programs of this form before, and we certainly would not have constructed this one by informal means.

DISCUSSION

The derivations were first discovered manually; the real­ number square-root derivation was subsequently reproduced by Yellin in an interactive program-synthesis system. The only au­ tomatic implementation of the system (Russell [83]) is unable to construct the derivation for a simple reason: it never attempts to apply the resolution rule to a goal and itself.

The results of this investigation run counter to our usual ex­ perience. It is common for a bit of reasoning that seems simple and intuitively straightforward to turn out to be difficult to for­ malize and more difficult still to duplicate automatically. Here the opposite is true: an idea that requires a substantial leap of human ingenuity to discover is captured in .a few easy formal steps. We may hope that truly original ideas will arise from the fortunate application of simple mechanisms.

Acknowledgments

We would like to thank Martin Abadi, Yoni Malachi , Eric Muller, Mark Stickel, Jonathan Traugott, and Frank Yellin for discussions and helpful suggestions on the subject of this paper.