Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Mathematical Aspects of Computer and Information Sciences (MACIS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For binary functions one may use simultaneous induction on both arguments.

  2. 2.

    The construction of the object desired for the synthesis uses only the objects which are already present in the proof, and does not try to decompose some of them.

  3. 3.

    We use LHS for left hand side and RHS for right hand side.

  4. 4.

    https://isabelle.in.tum.de/library/HOL/HOL-Library/Sorting_Algorithms.html.

  5. 5.

    Note that this introduces exceptions to antisymmetry and transitivity when the empty composite object is involved.

  6. 6.

    This means that the input condition is the logical constant True and the implication from the synthesis conjecture reduces to O[X, Y, Z].

References

  1. Blizard, W.D.: Multiset theory. Notre Dame J. Formal Logic 30(1), 36–66 (1989). https://doi.org/10.1305/ndjfl/1093634995

    Article  MathSciNet  MATH  Google Scholar 

  2. Buchberger, B.: Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica XXXVII(2), 9–32 (2000)

    MathSciNet  MATH  Google Scholar 

  3. Buchberger, B.: Algorithm invention and verification by lazy thinking. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 41–70 (2003)

    MathSciNet  MATH  Google Scholar 

  4. Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: using problem schemes. In: Proceedings of SYNASC, pp. 90–106 (2004)

    Google Scholar 

  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. 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/4568

    Article  MathSciNet  MATH  Google Scholar 

  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.003

    Article  Google Scholar 

  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.030

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. 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. 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. 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_43

    Chapter  Google Scholar 

  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.002

    Article  MathSciNet  MATH  Google Scholar 

  16. Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Boston (1998). https://doi.org/10.1137/1012065

    Book  MATH  Google Scholar 

  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_21

    Chapter  MATH  Google Scholar 

  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.357090

    Article  MATH  Google Scholar 

  19. Manna, Z., Waldinger, R.: The Logical Basis for Computer Programming, vol. 1: Deductive Reasoning. Addison-Wesley, Boston (1985). https://doi.org/10.2307/2275898

    Book  MATH  Google Scholar 

  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.153379

    Article  Google Scholar 

  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. Smith, D.R.: Kids: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024–1043 (1990). https://doi.org/10.1109/32.578788

    Article  Google Scholar 

  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-9

    Article  MATH  Google Scholar 

  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_9

    Chapter  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. West University, Timişoara, Romania

    Isabela Drămnesc

  2. Johannes Kepler University, Linz, Austria

    Tudor Jebelean

Authors
  1. Isabela Drămnesc
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tudor Jebelean
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Isabela Drămnesc .

Editor information

Editors and Affiliations

  1. AIT Austrian Institute of Technology, Vienna, Austria

    Daniel Slamanig

  2. IMJ-PRG, Sorbonne University, Paris, France

    Elias Tsigaridas

  3. Institute of Information Technologies, Gebze Technical University, Gebze, Turkey

    Zafeirakis Zafeirakopoulos

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Drămnesc, I., Jebelean, T. (2020). Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema . In: Slamanig, D., Tsigaridas, E., Zafeirakopoulos, Z. (eds) Mathematical Aspects of Computer and Information Sciences. MACIS 2019. Lecture Notes in Computer Science(), vol 11989. Springer, Cham. https://doi.org/10.1007/978-3-030-43120-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-43120-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-43119-8

  • Online ISBN: 978-3-030-43120-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation