--- title: "The Origin of the Binary-Search Paradigm" authors: - "Zohar Manna" - "Richard J. Waldinger" doi: "" url: "https://ijcai.org/proceedings/1985/41" pdf: "https://ijcai.org/proceedings/1985/0041.pdf" venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence" year: 1985 pages: "222-223" track: "Automatic Programming" keywords: --- # The Origin of the Binary-Search Paradigm Zohar Manna, Richard J. Waldinger *Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 222-223. ## 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. The paper considers how such algorithms might be derived from their specifications by an automatic program-synthesis system. The derivation of the binarysearch concept has been found to be surprisingly straightforward. The ~rograms obtained, though reasonably simple and efficient, are quite different from those that would have been constructed by informal means. ## Full text ## 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 ![Image](https://ijcai.org/proceedings/1985/fulltext/41/image_000004_064a62bb2ad117cf1818234afc472bd69e083c6161e1f65b08abd9d0f8c592f1.png) 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) ![Image](https://ijcai.org/proceedings/1985/fulltext/41/image_000005_622f59efd509e87ceb138444040bc6c763f4ded2191ae1ed3dc3f3c99f27bdb0.png) 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. ## References 1. and Manna 2. N. Dershowitz and Z. Manna, The evolution of pro- grams: Automatic program modification, IEEE Trans- actions on Software Engineering, Vol. SE-3, No. 6, Novem- ber 1977, pp. 377-385. 3. Manna and Waldinger 4. Z. Manna and R. Waldinger, A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems; Vol. 2, No. 1, January 1980, pp. 90-121. 5. Manna and Waldinger [85a 6. Z. Manna and R. Waldinger, The origin of the binary search paradigm, Technical Report, Computer Science Department, Stanford University, Stanford, CA and Ar- tificial Intelligence Center, SRI International, Menlo Park, CA (April 1985). 7. Manna and Waldinger 8. Z. Manna and R. Waldinger, Special relations in auto- mated deduction, Journal of the ACM, 1985, to appear. 9. Manna and Waldinger [85c 10. Z. Manna and R. Waldinger, The Logical Basis for Com- puter Programming, Volume 1: Dedutive Reasoning, Addison-Wesley, Reading, Mass., 1985. 11. N. V. Murray, Completely nonclausal theorem proving, Artificial Intelligence, Vol. 18, No. 1, 1982, pp. 67-85. Robinson 12. J . A. Robinson, Logic: Form and Function, North-Holland, New York, N. Y. , 1979. Russell 13. S. Russell, PSEUDS : A programming system using de- ductive synthesis, unpublished report, Computer Sci- ence Department, Stanford University, Stanford, Calif. , September 1983. Smith 14. D. R. Smith, Top-down synthesis of simple divide-and- conquer algorithms, Artificial Intelligence, 1985, to ap- pear. Wensley 15. J. H. Wensley, A class of nonanalytical iterative pro- cesses, Computer Journal, Vol. 1, January 1959, pp. 163-167.