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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
For binary functions one may use simultaneous induction on both arguments.
- 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.
We use LHS for left hand side and RHS for right hand side.
- 4.
- 5.
Note that this introduces exceptions to antisymmetry and transitivity when the empty composite object is involved.
- 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
Blizard, W.D.: Multiset theory. Notre Dame J. Formal Logic 30(1), 36–66 (1989). https://doi.org/10.1305/ndjfl/1093634995
Buchberger, B.: Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica XXXVII(2), 9–32 (2000)
Buchberger, B.: Algorithm invention and verification by lazy thinking. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 41–70 (2003)
Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: using problem schemes. In: Proceedings of SYNASC, pp. 90–106 (2004)
Buchberger, B., et al.: The theorema project: a progress report. In: Calculemus 2000, pp. 98–113. A.K. Peters, Natick (2000)
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
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
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
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)
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
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
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
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
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
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
Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Boston (1998). https://doi.org/10.1137/1012065
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
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
Manna, Z., Waldinger, R.: The Logical Basis for Computer Programming, vol. 1: Deductive Reasoning. Addison-Wesley, Boston (1985). https://doi.org/10.2307/2275898
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
Radoaca, A.: Properties of multisets compared to sets. In: SYNASC 2015, pp. 187–188 (2015). https://doi.org/10.1109/SYNASC.2015.37
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
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
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
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)