Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema

We demonstrate the deduction based synthesis of element deletion algorithms for [sorted] lists and [sorted] binary trees, by first developing the necessary theory which is multi–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are “pattern matching”, namely sets of conditional equalities, and we also demonstrate their transformation into functional algorithms and, for lists, into tail recursive algorithms. This work constitutes a case study first in theory exploration and second in automated synthesis and transformation of algorithms synthesized on the basis of natural style proofs, which allows to investigate the heuristics of theory construction on multiple types, as well as the natural style inferences and strategies for constructing human readable synthesis proofs. The experiments are performed in the frame of the Theorema system.