Proving properties of functional programs by equality saturation
Sergei Alexandrovich Grechanik · Programming and Computer Software · 2015
The present paper shows how the idea of equality saturation can be used to prove algebraic properties of programs written in a non-total non-strict first-order functional language. We adapt equality saturation approach to a functional language by using transformations borrowed mainly from supercompilation. Proof by induction is performed via a special transformation called merging by bisimilarity. We compare our experimental prover based on this method with a supercompiler HOSC and inductive provers HipSpec and Zeno.