Isabela Dramnesc, Tudor Jebelean,
"Synthesis of list algorithms by mechanical proving"
, in Journal of Symbolic Computation, Vol. 69, Seite(n) 61--92, 2015, ISSN: 1095-855X
Synthesis of list algorithms by mechanical proving
Sprache des Titels:
We address the automation of the processes of algorithm synthesis and systematic exploration of the theory of lists. Our focus is on methods, techniques, inference rules and strategies for computer based synthesis of list algorithms based on proving. Starting from the specification of the problem (input and output conditions), a synthesis statement is built: ?for any list satisfying the input condition, there exists a list satisfying the output condition?. The main difficulty is to find a constructive proof of this statement, from which the corresponding algorithm is easily extracted as a set of conditional equalities. In more detail, we aim at computer automation of the proof of the existence of the sorted version of the input list. By using different proof methods we automatically synthesize five sorting algorithms: Selection-Sort, Insertion-Sort, Quick-Sort, Merge-Sort, and a novel algorithm, which we call Unbalanced-Merge-Sort, as well as the auxiliary functions used in the sorting algorithms. The theory we use is first order, and mostly contains formulae which are equivalent to Horn clauses. Therefore, except for induction, SLD resolution style inferences are in principle sufficient for performing the proofs. However, for most of the proofs this leads to a very large search space. Therefore we introduce several novel inference rules and specific strategies, which are based on the properties of lists, and which we developed in the course of this case study on sorting. Moreover, during the process of algorithm synthesis we explore the theory of lists by introducing (automatically prove, and then use) the necessary properties. When the knowledge base does not contain the auxiliary functions needed for the respective version of the algorithm, then the proof fails and from this failure a new proof goal is created, which is the synthesis statement for the missing auxiliary functions (?cascading?).