The aim of the work is to investigate the possibility of using a combination of equality saturation methods and multi-result supercompilation to identify and prove the properties of programs in a non-strict functional language of the first order. The present work shows that, based on the method of saturation with equalities and transformations from supercompilation, it is possible to construct a system of transformation of functional programs applicable for proving equivalence. It is shown that this avoids the problem associated with a combinatorial explosion of the number of functions that differ only in the order of the arguments. It was also shown that the principle of induction can be formulated as a special transformation that works within the framework of the saturation system.

functional programs, the method of saturation with equalities, supercompilation, multi-result supercompilation

Programming, parallel computing, multimedia