Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246

Summary: We develop logic and combinatorial methods for automating the generation of sorting algorithms for binary trees, starting from input-output specifications and producing conditional rewrite rules. The main approach consists in proving (constructively) the existence of an appropriate output from every input. The proof may fail if some necessary sub-algorithms are lacking. Then, their specifications are suggested and their synthesis is performed by the same principles. Our main goal is to avoid the possibly prohibitive cost of pure resolution proofs by using a natural-style proving in which domain-specific strategies and inference steps lead to a significant increase of efficiency. In addition to classical techniques for natural-style proving, we introduce novel ones (priority of certain types of assumptions, transformation of elementary goals into conditions, special criteria for decomposition of the goal and of the assumptions), as well as methods based on the properties of domain-specific relations and functions. In particular, we use combinatorial techniques in order to generate possible witnesses, which in certain cases lead to the discovery of new induction principles. From the proof, the algorithm is extracted by transforming inductive proof steps into recursions, and case-based proof steps into conditionals. The approach is demonstrated in parallel using the Theorema system, by developing the theory, implementing the prover, and performing the proofs of the necessary properties and synthesis conjectures. It is also validated in the Coq system, which allows to compare the facilities of the two systems from the point of view of our application.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P10 Searching and sorting
Full Text: DOI HAL


[1] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press
[2] Back, R.-J.; von Wright, J., Refinement calculus, (1998), Springer Verlag
[3] Balaa, A.; Bertot, Y., Fix-point equations for well-founded recursion in type theory, (Aagaard, M.; Harrison, J., Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 1869, (2000), Springer Berlin/Heidelberg), 1-16 · Zbl 0974.68183
[4] Barthe, G.; Courtieu, P., Efficient reasoning about executable specifications in coq, (Theorem Proving in Higher Order Logics, LNCS, vol. 2410, (2002), Springer Berlin), 31-46 · Zbl 1013.68539
[5] Barthe, G.; Forest, J.; Pichardie, D.; Rusu, V., Defining and reasoning about recursive functions: a practical tool for the coq proof assistant, (Hagiya, M.; Wadler, P., Functional and Logic Programming, Lecture Notes in Computer Science, vol. 3945, (2006), Springer Berlin/Heidelberg), 114-129 · Zbl 1185.68616
[6] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Nilsson, J. F., Synthesis of programs in computational logic, (Program Development in Computational Logic, (2004), Springer), 30-65 · Zbl 1080.68562
[7] Bertot, Y.; Casteran, P., Interactive theorem proving and program development coq’art: the calculus of inductive constructions, Texts in Theoretical Computer Science, vol. XXV, (2004), Springer · Zbl 1069.68095
[8] Buchberger, B., Theory exploration with theorema, (Analele Universitatii Din Timisoara, Ser. Matematica-Informatica, vol. XXXVIII, (2000)), 9-32 · Zbl 1004.68589
[9] Buchberger, B., Algorithm invention and verification by lazy thinking, (Analele Universitatii de Vest Timisoara, Ser. Matematica-Informatica, vol. XLI, (2003)), 41-70 · Zbl 1073.68814
[10] Buchberger, B., Algorithm supported mathematical theory exploration: a personal view and strategy, (Proceedings of AISC 2004, LNCS, vol. 3249, (2004), Springer), 236-250 · Zbl 1109.68664
[11] Buchberger, B.; Craciun, A., Algorithm synthesis by lazy thinking: examples and implementation in theorema, Electron. Notes Theor. Comput. Sci., 93, 24-59, (2004) · Zbl 1271.68208
[12] Buchberger, B.; Jebelean, T.; Kutsia, T.; Maletzky, A.; Windsteiger, W., Theorema 2.0: computer-assisted natural-style mathematics, J. Formaliz. Reason., 9, 1, 149-185, (2016)
[13] Bundy, A.; Dixon, L.; Gow, J.; Fleuriot, J., Constructing induction rules for deductive synthesis proofs, Electron. Notes Theor. Comput. Sci., 153, 3-21, (March 2006)
[14] Claessen, K.; Johansson, M.; Rosén, D.; Smallbone, N., Automating inductive proofs using theory exploration, (CADE-24: Proceedings of the 24th International Conference on Automated Deduction, (2013), Springer Berlin, Heidelberg), 392-406 · Zbl 1381.68263
[15] Cohen, C.; Dénès, M.; Mörtberg, A., Refinements for free!, (Gonthier, G.; Norrish, M., Certified Programs and Proofs, Lecture Notes in Computer Science, vol. 8307, (2013), Springer International Publishing), 147-162 · Zbl 1426.68165
[16] Colton, S., Automated theory formation in pure mathematics, (2012), Springer Science & Business Media
[17] Craciun, A.; Hodorog, M., Decompositions of natural numbers: from a case study in mathematical theory exploration, (SYNASC 2007: Proceedings of the 8th International Symposium on Numeric and Symbolic Algorithms for Scientific Computing, (2007), IEEE), 41-47
[18] Delaware, B.; Claudel, C. P.; Gross, J.; Chlipala, A., Fiat: deductive synthesis of abstract data types in a proof assistant, (Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, (2015), ACM New York, NY, USA), 689-700 · Zbl 1346.68175
[19] Deville, Y.; Lau, K. K., Logic program synthesis, J. Log. Program., 19/20, 321-350, (1994) · Zbl 0942.68525
[20] Dixon, L.; Fleuriot, J. D., Isaplanner: a prototype proof planner in isabelle, (Proceedings of CADE’03, LNCS, vol. 2741, (2003)), 279-283
[21] Dixon, L.; Johansson, M., Isaplanner 2: A proof planner in isabelle, (2007), DReaM Technical Report (System description)
[22] Dramnesc, I.; Jebelean, T., Proof techniques for synthesis of sorting algorithms, (SYNASC 2011: Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, (2011), IEEE Computer Society), 101-109
[23] Dramnesc, I.; Jebelean, T., Automated synthesis of some algorithms on finite sets, (SYNASC 2012: Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, (2012), IEEE Computer Society), 143-151
[24] Dramnesc, I.; Jebelean, T., Discovery of inductive algorithms through automated reasoning: a case study on sorting, (SISY 2012: Proceedings of IEEE 10th Jubilee International Symposium on Intelligent Systems and Informatics. IEEE Xplore, (2012)), 293-298
[25] Dramnesc, I.; Jebelean, T., Theory exploration in theorema: case study on lists, (SACI 2012: Proceedings of IEEE 7th International Symposium on Applied Computational Intelligence and Informatics, (2012), IEEE Xplore), 421-426
[26] Dramnesc, I.; Jebelean, T., A case study in proof based synthesis of algorithms on monotone lists, (SACI 2015: Proceedings of the 10th IEEE International Symposium on Applied Computational Intelligence and Informatics, (2015), IEEE), 483-488
[27] Dramnesc, I.; Jebelean, T., Synthesis of List algorithms by mechanical proving, J. Symb. Comput., 68, 61-92, (2015) · Zbl 1315.68263
[28] Dramnesc, I.; Jebelean, T.; Stratulat, S., Combinatorial techniques for proof-based synthesis of sorting algorithms, (SYNASC 2015: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, (2015)), 137-144
[29] Dramnesc, I.; Jebelean, T.; Stratulat, S., Synthesis of some algorithms for trees: experiments in theorema, (2015), Johannes Kepler University Linz, Austria, Tech. Rep. 15-04, RISC Report Series
[30] Dramnesc, I.; Jebelean, T.; Stratulat, S., Theory exploration of binary trees, (SISY 2015: Proceedings of the 13th IEEE International Symposium on Intelligent Systems and Informatics, (2015), IEEE), 139-144
[31] Dramnesc, I.; Jebelean, T.; Stratulat, S., A case study on algorithm discovery from proofs: the insert function on binary trees, (SACI 2016: Proceedings of the 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, (2016), IEEE), 231-236
[32] Dramnesc, I.; Jebelean, T.; Stratulat, S., Proof-based synthesis of sorting algorithms for trees, (LATA 2016: Proceedings of the 10th International Conference on Language and Automata Theory and Applications, (2016), Springer), 562-575 · Zbl 1443.68045
[33] Flener, P., Achievements and prospects of program synthesis, (Computational Logic: Logic Programming and Beyond, (2002)), 310-346 · Zbl 1012.68500
[34] Gulwani, S., Dimensions in program synthesis, (Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP ’10, (2010), ACM New York, NY, USA), 13-24
[35] Johansson, M.; Dixon, L.; Bundy, A., Conjecture synthesis for inductive theories, J. Autom. Reason., 47, 3, 251-289, (2011) · Zbl 1243.68268
[36] Kneuss, E.; Kuraj, I.; Kuncak, V.; Suter, P., Synthesis modulo recursive functions, (Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’13, (2013), ACM New York, NY, USA), 407-426
[37] Knuth, D. E., The art of computer programming, vol. 3: sorting and searching, (1998), Addison Wesley Longman Publishing Redwood City, CA, USA
[38] Konev, B.; Jebelean, T., Solution lifting method for handling meta-variables in theorema, (Maruster, S.; Buchberger, B.; Negru, V.; Jebelean, T., Proceedings of SYNASC01, (October 2001), Mirton Timisoara, Romania), 15-23
[39] Kowalski, R.; Kuehner, D., Linear resolution with selection function, Artif. Intell., 2, (1971) · Zbl 0234.68037
[40] McCasland, R. L.; Bundy, A., Mathsaid: A mathematical theorem discovery tool, (Negru, V.; Petcu, D.; Zaharie, D.; Abraham, A.; Buchberger, B.; Cicortas, A.; Gorgan, D.; Quinqueton, J., 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2006, 26-29 September 2006, (2006), IEEE Computer Society Timisoara, Romania), 17-22
[41] Montano-Rivas, O.; McCasland, R.; Dixon, L.; Bundy, A., Scheme-based theorem discovery and concept invention, Expert Syst. Appl., 39, 2, 1637-1646, (2012)
[42] Mordechai, B., Mathematical logic for computer science, (2004), Springer
[43] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL — A proof assistant for higher-order logic, Lecture Notes in Computer Science, vol. 2283, (2002), Springer · Zbl 0994.68131
[44] Pelletier, F. J., A history of natural deduction and elementary logic textbooks, (Logical Consequence: Rival Approaches, vol. 1, (2000)), 105-138
[45] Smith, D. R., Generating programs plus proofs by refinement, (Meyer, B.; Woodcock, J., Verified Software: Theories, Tools, Experiments, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Lecture Notes in Computer Science, vol. 4171, (2005), Springer), 182-188
[46] Stratulat, S., A unified view of induction reasoning for first-order logic, (Voronkov, A., Turing-100, The Alan Turing Centenary Conference, EPiC Series, vol. 10, (2012), EasyChair), 326-352
[47] Stratulat, S., Mechanically certifying formula-based Noetherian induction reasoning, J. Symb. Comput., 80, Part 1, 209-249, (2017) · Zbl 1356.68202
[48] Wirth, N., Program development by stepwise refinement, Commun. ACM, 14, 4, 221-227, (Apr. 1971)
[49] Wolfram, S., The Mathematica book, (2003), Wolfram Media Inc
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.