Advertisement

Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema

  • Isabela DrămnescEmail author
  • Tudor Jebelean
Conference paper
  • 20 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11989)

Abstract

We demonstrate the automatic proof–based synthesis of merging and inserting algorithms for [sorted] binary trees, using the notion of multisets, in the Theorema system. Each algorithm is extracted from the proof of the conjecture based on the specification of the desired function, in the form of a list of [conditional] equalities, which can be directly executed. The proofs are performed in natural style, using general techniques, but most importantly efficient inference rules and strategies specific for the domains involved. In particular we present specific techniques for the construction of arbitrarily nested recursive algorithms by general Noetherian induction, as well as a systematic method for the generation of the conjectures and consequently of the algorithms for the auxiliary functions needed in the main function.

Keywords

Algorithm synthesis Binary trees Multisets Theorema 

References

  1. 1.
    Blizard, W.D.: Multiset theory. Notre Dame J. Formal Logic 30(1), 36–66 (1989).  https://doi.org/10.1305/ndjfl/1093634995MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Buchberger, B.: Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica XXXVII(2), 9–32 (2000)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Buchberger, B.: Algorithm invention and verification by lazy thinking. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 41–70 (2003)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: using problem schemes. In: Proceedings of SYNASC, pp. 90–106 (2004)Google Scholar
  5. 5.
    Buchberger, B., et al.: The theorema project: a progress report. In: Calculemus 2000, pp. 98–113. A.K. Peters, Natick (2000)Google Scholar
  6. 6.
    Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: computer-assisted natural-style mathematics. J. Formal. Reason. 9(1), 149–185 (2016).  https://doi.org/10.6092/issn.1972-5787/4568MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. Electron. Notes Theor. Comput. Sci. 153, 3–21 (2006).  https://doi.org/10.1016/j.entcs.2005.08.003CrossRefGoogle Scholar
  8. 8.
    Dramnesc, I., Jebelean, T.: Synthesis of list algorithms by mechanical proving. J. Symb. Comput. 68, 61–92 (2015).  https://doi.org/10.1016/j.jsc.2014.09.030MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Dramnesc, I., Jebelean, T.: Case studies on algorithm discovery from proofs: the delete function on lists and binary trees using multisets. In: SISY 2019, pp. 213–220. IEEE Xplore (2019)Google Scholar
  10. 10.
    Dramnesc, I., Jebelean, T.: Proof-based synthesis of sorting algorithms using multisets in theorema. In: FROM 2019, EPTCS 303, pp. 76–91 (2019).  https://doi.org/10.4204/EPTCS.303.6
  11. 11.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Combinatorial techniques for proof-based synthesis of sorting algorithms. In: SYNASC 2015, pp. 137–144 (2015).  https://doi.org/10.1109/SYNASC.2015.30
  12. 12.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Theory exploration of binary trees. In: SISY 2015, pp. 139–144. IEEE (2015).  https://doi.org/10.1109/SISY.2015.7325367
  13. 13.
    Dramnesc, I., Jebelean, T., Stratulat, S.: A case study on algorithm discovery from proofs: the insert function on binary trees. In: SACI 2016, pp. 231–236. IEEE (2016).  https://doi.org/10.1109/SACI.2016.7507376
  14. 14.
    Drămnesc, I., Jebelean, T., Stratulat, S.: Proof–based synthesis of sorting algorithms for trees. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 562–575. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30000-9_43CrossRefGoogle Scholar
  15. 15.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. J. Symb. Comput. 90, 3–41 (2019).  https://doi.org/10.1016/j.jsc.2018.04.002MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Boston (1998).  https://doi.org/10.1137/1012065CrossRefzbMATHGoogle Scholar
  17. 17.
    Korukhova, Y.: Automatic deductive synthesis of lisp programs in the system ALISA. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 242–252. Springer, Heidelberg (2006).  https://doi.org/10.1007/11853886_21CrossRefzbMATHGoogle Scholar
  18. 18.
    Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980).  https://doi.org/10.1145/357084.357090CrossRefzbMATHGoogle Scholar
  19. 19.
    Manna, Z., Waldinger, R.: The Logical Basis for Computer Programming, vol. 1: Deductive Reasoning. Addison-Wesley, Boston (1985).  https://doi.org/10.2307/2275898CrossRefzbMATHGoogle Scholar
  20. 20.
    Manna, Z., Waldinger, R.: Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18(8), 674–704 (1992).  https://doi.org/10.1109/32.153379CrossRefGoogle Scholar
  21. 21.
    Radoaca, A.: Properties of multisets compared to sets. In: SYNASC 2015, pp. 187–188 (2015).  https://doi.org/10.1109/SYNASC.2015.37
  22. 22.
    Smith, D.R.: Kids: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024–1043 (1990).  https://doi.org/10.1109/32.578788CrossRefGoogle Scholar
  23. 23.
    Traugott, J.: Deductive synthesis of sorting programs. J. Symb. Comput. 7(6), 533–572 (1989).  https://doi.org/10.1016/S0747-7171(89)80040-9CrossRefzbMATHGoogle Scholar
  24. 24.
    Windsteiger, W.: Theorema 2.0: a system for mathematical theory exploration. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 49–52. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44199-2_9CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.West UniversityTimişoaraRomania
  2. 2.Johannes Kepler UniversityLinzAustria

Personalised recommendations