Skip to main content
SpringerLink
Log in

Inductive Prover Based on Equality Saturation for a Lazy Functional Language

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8974))

  • 527 Accesses

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.

Supported by Russian Foundation for Basic Research grant No. 12-01-00972-a and RF President grant for leading scientific schools No. NSh-4307.2012.9.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Graphsc source code and the test suite. https://github.com/sergei-grechanik/supercompilation-hypergraph

  2. Abel, A., Altenkrich, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1–41 (2002)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  4. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM: J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

  5. Dovier, A., Piazza, C.: The subgraph bisimulation problem. IEEE Trans. Knowl. Data Eng. 5(4), 1055–1056 (2003). Publisher: IEEE, USA

    Article  Google Scholar 

  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. 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. Klyuchnikov, I.: Supercompiler HOSC 1.0: under the hood. Preprint 63, Keldysh Institute of Applied Mathematics, Moscow (2009)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  11. Klyuchnikov, I., Romanenko, S.: Towards higher-level supercompilation. In: Second International Workshop on Metacomputation in Russia (2010)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM: J. ACM 27(2), 356–364 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  15. Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Trans. Program. Lang. Syst. 18(2), 175–234 (1996)

    Article  MathSciNet  Google Scholar 

  16. Sørensen, M., Glück, R., Jones, N.: A positive supercompiler. J. Funct. Program. 6(6), 811–838 (1993)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  18. Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. SIGPLAN Not. 44, 264–276 (2009)

    Article  Google Scholar 

  19. Turchin, V.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292–325 (1986)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Keldysh Institute of Applied Mathematics, Russian Academy of Sciences, 4 Miusskaya sq., Moscow, 125047, Russia

    Sergei Grechanik

Authors
  1. Sergei Grechanik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sergei Grechanik .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

  2. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Irina Virbitskaite

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grechanik, S. (2015). Inductive Prover Based on Equality Saturation for a Lazy Functional Language. In: Voronkov, A., Virbitskaite, I. (eds) Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science(), vol 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46823-4_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46822-7

  • Online ISBN: 978-3-662-46823-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation