Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Tate, R., Stepp, M., Tatlock, Z., and Lerner, S., Equality saturation: a new approach to optimization, SIGPLAN Not., 2009, vol. 44, pp. 264–276.
Detlefs, D., Nelson, D., and Saxe, J.,, Simplify: a theorem prover for program checking, JACM, 2005, vol. 52, no. 3, pp. 365–473.
Nelson, G. and Oppen D.C.,, Fast decision procedures based on congruence closure, JACM, 1980, vol. 27, no. 2, pp. 356–364.
Stepp, M., Tate, R., and Lerner, S., Equality-based translation validator for LLVM, Gopalakrishnan, Ganesh and Qadeer, Shaz, Eds., Computer Aided Verification—23rd International Conference, CAV 2011 (USA, UT, Snowbird, 2011), Springer, 2011, vol. 6806, pp. 737–742.
Turchin, V.F., The concept of a supercompiler, ACM Trans. Program. Lang. Syst. (TOPLAS), 1986, vol. 8, no. 3, pp. 292–325.
Sørensen, M.H., Glück, R., and Jones, N.D., A positive supercompiler, J. Funct. Program., 1993, vol. 6, no. 6, pp. 811–838.
Claessen, K., Johansson, M., Rosén, D., and Smallbone, N., Automating inductive proofs using theory exploration, Maria Paola Bonacina, Ed., Automated Deduction—CADE-24—24th International Conference on Automated Deduction (USA, NY, Lake Placid, 2013), 2013, vol. 7898, pp. 392–406.
Sonnex, W., Drossopoulou, S., and Eisenbach, S., Zeno: an automated prover for properties of recursive data structures, in TACAS, Lecture Notes in Computer Science, 2012.
Abel, A., Termination Checker for Simple Functional Programs, 1998.
Abel, A. and Altenkrich, T., A predicative analysis of structural recursion, J. Funct. Program., 2002, vol. 12, pp. 1–41.
Graphsc source code and the test suite, https://github.com/sergei-grechanik/supercompilation-hypergraph.
Sands, D., Total correctness by local improvement in the transformation of functional programs, ACM Trans. Program. Lang. Syst., 1996, vol. 18, no. 2, pp. 175–234.
Klyuchnikov, I. and Romanenko, S., Towards higherlevel supercompilation, Second International Workshop on Metacomputation in Russia, 2010.
Dovier, A. and Piazza, C., The subgraph bisimulation problem, IEEE Transactions on Knowledge and Data Engineering, USA: IEEE, 2003, vol. 15, no. 4, pp. 1055–1056.
Klyuchnikov, I., Supercompiler HOSC 1.0: under the hood, Preprint of Keldysh Institute of Applied Mathematics, Moscow, 2009, no. 63.
Lisitsa, A.P. and Webster, M., Supercompilation for equivalence testing in metamorphic computer viruses detection, Proceedings of the First International Workshop on Metacomputation (Russia, 2008).
Klyuchnikov, I. and Romanenko, S., Proving the equivalence of higher-order terms by means of supercompilation, in Perspectives of Systems Informatics, 2010, vol. 5947, pp. 193–205.
Klyuchnikov, I., Towards effective two-level supercompilation, Preprint of Keldysh Institute of Applied Mathematics, Moscow, 2010, no. 81; URL: http://library.keldysh.ru/preprint.asp?id=2010-81&lg=e.
Claessen, K., Smallbone, N., and Hughes, J., Quickspec: Guessing formal specifications using testing, Fraser, G. and Gargantini, A., Eds., Tests and Proofs, 4th International Conference, TAP 2010 (Spain, Mälaga, 2010), Springer, 2010, vol. 6143, pp. 6–21.
Grechanik, S.A., Overgraph representation for multiresult supercompilation, Klimov, A.V. and Romanenko, S.A., Eds., Proceedings of the Third International Valentin Turchin Workshop on Metacomputation (Russia, Pereslavl-Zalessky, 2012), Pereslavl-Zalessky: Ailamazyan University of Pereslavl, pp. 48–65.
Klyuchnikov, I.G. and Romanenko, S.A., Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions, Clarke, Virbitskaite, I. and Voronkov, A., Eds., Perspectives of Systems Informatics, 8th Andrei Ershov Informatics Conference, PSI 2011 (Novosibirsk, Akademgorodok, Russia, 2011), Springer, 2012, vol. 7162, pp. 210–226.
Hamilton, G.W., Distillation: extracting the essence of programs, Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, N.Y.: ACM Press, 2007, pp. 61–70.
Author information
Authors and Affiliations
Corresponding author
Additional information
Original Russian Text © S.A. Grechanik, 2015, published in Programmirovanie, 2015, Vol. 41, No. 3.
The article was translated by the authors.
Rights and permissions
About this article
Cite this article
Grechanik, S.A. Proving properties of functional programs by equality saturation. Program Comput Soft 41, 149–161 (2015). https://doi.org/10.1134/S0361768815030056
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S0361768815030056