The origin of a binary-search paradigm (Q1098328)

The authors study a problem which is very important both from the theoretical and the practical point of view. The problem consists in determining programs from their specifications by an automatic system for program synthesis. Various researchers have shown that the automatic program synthesis can be obtained as general program schemata, which can be then specialized to particular applications. The authors of this paper prove that the binary search is one of these schemata which can be applied to derive simple and efficient programs for the computation of a numerical function. In this paper, only applicative or functional programs has been considered. The specifications for these programs have the form f(a)\(\Leftarrow find\) z such that R[a,z] where P[a]. Here f is the program, a is the input, P[a] is the input condition and R[a,z] is the output condition. The derived programs are obtained by transforms applied on deductive tableaux using the resolution rule and the induction rule. The paper contains examples which illustrate the application of the deductive tableaux system for a square-root program. Finally, several analogous binary-search derivations for different problems and for different specifications of the same problem have been considered.