Inductive Prover Based on Equality Saturation for a Lazy Functional Language

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8974)

Abstract

The present paper shows how the idea of equality saturation can be used to build an inductive prover for a non-total first-order lazy functional language. We adapt equality saturation approach to a functional language by using transformations borrowed from supercompilation. A special transformation called merging by bisimilarity is used to perform proof by induction of equivalence between nodes of the E-graph. Equalities proved this way are just added to the E-graph. We also experimentally compare our prover with HOSC and HipSpec.

Keywords

Equivalence Class Pattern Match Variable Node Outgoing Edge Reduction Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
  2. 2.
    Abel, A., Altenkrich, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1–41 (2002)CrossRefMATHGoogle Scholar
  3. 3.
    Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392–406. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  4. 4.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM: J. ACM 52(3), 365–473 (2005)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Dovier, A., Piazza, C.: The subgraph bisimulation problem. IEEE Trans. Knowl. Data Eng. 5(4), 1055–1056 (2003). Publisher: IEEE, USACrossRefGoogle Scholar
  6. 6.
    Grechanik, S.A.: Overgraph representation for multi-result supercompilation. In: Klimov, A., Romanenko, S. (eds.) Proceedings of the Third International Valentin Turchin Workshop on Metacomputation, pp. 48–65. Ailamazyan University of Pereslavl, Pereslavl-Zalessky (2012)Google Scholar
  7. 7.
    Hamilton, G.W.: Distillation: extracting the essence of programs. In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61–70. ACM Press, New York (2007)Google Scholar
  8. 8.
    Klyuchnikov, I.: Supercompiler HOSC 1.0: under the hood. Preprint 63, Keldysh Institute of Applied Mathematics, Moscow (2009)Google Scholar
  9. 9.
    Klyuchnikov, I.: Towards effective two-level supercompilation. Preprint 81, Keldysh Institute of Applied Mathematics (2010). http://library.keldysh.ru/preprint.asp?id=2010-81&lg=e
  10. 10.
    Klyuchnikov, I., Romanenko, S.: Proving the equivalence of higher-order terms by means of supercompilation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 193–205. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  11. 11.
    Klyuchnikov, I., Romanenko, S.: Towards higher-level supercompilation. In: Second International Workshop on Metacomputation in Russia (2010)Google Scholar
  12. 12.
    Klyuchnikov, I., Romanenko, S.A.: Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 210–226. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  13. 13.
    Lisitsa, A., Webster, M.: Supercompilation for equivalence testing in metamorphic computer viruses detection. In: Proceedings of the First International Workshop on Metacomputation in Russia (2008)Google Scholar
  14. 14.
    Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM: J. ACM 27(2), 356–364 (1980)CrossRefMATHMathSciNetGoogle Scholar
  15. 15.
    Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Trans. Program. Lang. Syst. 18(2), 175–234 (1996)CrossRefMathSciNetGoogle Scholar
  16. 16.
    Sørensen, M., Glück, R., Jones, N.: A positive supercompiler. J. Funct. Program. 6(6), 811–838 (1993)CrossRefGoogle Scholar
  17. 17.
    Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737–742. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  18. 18.
    Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. SIGPLAN Not. 44, 264–276 (2009)CrossRefGoogle Scholar
  19. 19.
    Turchin, V.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292–325 (1986)CrossRefMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.Keldysh Institute of Applied MathematicsRussian Academy of SciencesMoscowRussia

Personalised recommendations