Inductive synthesis of encoding for algebraic abstract data types

Abstract

The method announced in this paper develops the inductive approach for implementing algebraic ADT. We tried to describe here some framework for this approach and to demonstrate it and its problems on simple examples.

The concept of the partial model seems for us to be a very interesting object for inductive synthesis as there exist good inductive synthesis algorithms for applicable classes of ADT.

Another point of interest in the described method was the use of indication functions in the optimizing of encoding. It seems to be worthwhile to develop this approach, too.

And at the end it should be noted, that there is a lot of possibilities in this approach to combine inductive methods with deductive ones. For instance, we can try to prove that the encoding function satisfies the ADT axioms. Another use of deductive methods here is to generate type operations directly from the encoding function.