Automated Synthesis of Some Algorithms on Finite Sets

Isabela Dramnesc

Abstract: Program synthesis is currently a very active area of programming language and verification communities. We address the problem of synthesizing algorithms operating on finite sets.

We start from the sets theory axioms and we represent sets by monotone lists (sorted lists without duplications). For this we define a representation function R and its reverse S and in order to synthesize the implementation of the essential corresponding predicates and functions over sets we apply a proof-based method. Each synthesis starts as an inductive constructive proof which applies specific strategies and inference rules. In the process of proving we use properties from the theory of sets and we also add other necessary properties in the knowledge base. In this way we explore the theory of sets (represented as monotone lists). The program synthesis and the corresponding theory exploration are carried out in the frame of the Theorema system.

One of the major advantage of our approach is that the algorithms for operating on sets represented as monotone lists are more simple than the ones for operating with usual sets.