Deductive Synthesis of Min-Max-Sort Using Multisets in Theorema
Isabela Drămnesc, Tudor Jebelean · 2020
We demonstrate the deductive synthesis of the Min-Max-Sort algorithm using multisets in the frame of the Theorema system. Starting from the logical specification of the sorting function (input and output conditions), we show how to construct a synthesis conjecture, from whose proof the algorithm can be constructed. For the proof we choose those inference methods and induction principles such that the synthesized algorithm consists of selecting at each step the minimum and the maximum of the list, and moving them at the ends of the list. We also show how to add, on a logical basis, a specific flag in order to stop the recursion as soon as the list is already sorted. During the main proof new conjectures are produced for the synthesis of auxiliary algorithms, and this process repeats in a cascading fashion until all necessary algorithms are produced. Our proof techniques, which are in natural style, include a novel approach using multisets and the use of cover sets for realizing Noetherian induction. The later has the advantage that the concrete induction hypotheses are created dynamically during the proof of the corresponding induction conclusion, thus no concrete induction principle or algorithm scheme is needed in advance. The synthesis mechanism is implemented in the frame of the Theorema system which allows the construction of mathematical theories, proving in natural style, and computing with the synthesized algorithms.