Synthesis of a Family of Recursive Sorting Procedures

In an earlier paper, we described a method for synthesising recursive logic procedures from their first-order logic specifications. The method is practical because it is strictly top-down and has been implemented as part of a user-guided synthesis system in Prolog. We have used the system to synthesise procedures for a wide variety of algorithms, including a large family of recursive sorting procedures. In this paper we describe the synthesis of this family of procedures. 1 Introduction Although much theoretical work has been done in logic program derivation, most notably by Clark, Hansson, Hogger, and Tarnlund [3, 4, 7, 9], there has been relatively little work in mechanising logic program synthesis. The recent work of Sato and Tamaki [15, 14] is one of the few examples. Independently, we worked on designing and implementing a practical system for mechanised program synthesis. The result is a method for top-down synthesis of recursive logic procedures from their specifications in fir..