Synthesis of list algorithms by mechanical proving. (July 2015)

• Record Type: Journal Article
• Authors: Drămnesc, Isabela; Jebelean, Tudor
• Is Part Of: Journal of symbolic computation. Volume 69(2015)
• Page Start: 61
• Page End: 92
• Publication Date: 2015-07
• Subjects: List -- Algorithm synthesis -- Theorema; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2014.09.030
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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 callUnbalanced-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").