Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Program Synthesis with Equivalence Reduction

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)

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

Abstract

We introduce program synthesis with equivalence reduction, a synthesis methodology that utilizes relational specifications over components of a given synthesis domain to reduce the search space. Leveraging a blend of classic and modern techniques from term rewriting, we use relational specifications to discover a canonical representative per equivalence class of programs. We show how to design synthesis procedures that only consider programs in normal form, thus pruning the search space. We discuss how to implement equivalence reduction using efficient data structures, and demonstrate the significant reductions it can achieve in synthesis time.

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

Notes

  1. 1.

    https://docs.python.org/3/library/stdtypes.html.

  2. 2.

    We also consider two other works: Big\(\lambda \) [36] is implemented in Python and not competitive with our baseline, while Myth [30] expects data types to be specified from first principles, and does not have, e.g., integers or strings by default.

References

  1. Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-17796-5_12

    Chapter  Google Scholar 

  2. Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 934–950. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_67

    Chapter  Google Scholar 

  3. Alur, R., et al.: Syntax-guided synthesis. In: FMCAD (2013)

    Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  5. Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. Resolut. Eqn. Algebraic Struct. 2, 1–30 (1989)

    MathSciNet  Google Scholar 

  6. Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6–21. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13977-2_3

    Chapter  Google Scholar 

  7. Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS 1997, pp. 26–34. IEEE (1997)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)

    Google Scholar 

  9. De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae, Proceedings, vol. 75, pp. 381–392. Elsevier (1972)

    Google Scholar 

  10. Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. In: OSDI (2004)

    Google Scholar 

  11. Dechter, E., Malmaud, J., Adams, R.P., Tenenbaum, J.B.: Bootstrap learning via modular concept discovery. In: IJCAI (2013)

    Google Scholar 

  12. Dershowitz, N.: Synthesis by completion. Urbana 51, 61801 (1985)

    Google Scholar 

  13. Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: PLDI (2015)

    Google Scholar 

  14. Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: POPL (2016)

    Google Scholar 

  15. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 281–286. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_24

    Chapter  Google Scholar 

  16. Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. CACM 55(8), 97–105 (2012)

    Article  Google Scholar 

  17. Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: PLDI (2013)

    Google Scholar 

  18. Hillenbrand, T., Buch, A., Vogt, R., Löchner, B.: Waldmeister-high-performance equational deduction. J. Autom. Reason. 18(2), 265–270 (1997)

    Article  Google Scholar 

  19. Klein, D., Hirokawa, N.: Maximal completion. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 10. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2011)

    Google Scholar 

  20. Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)

    Google Scholar 

  21. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. SYMBOLIC, pp. 342–376. Springer, Heidelberg (1983). https://doi.org/10.1007/978-3-642-81955-1_23

    Chapter  Google Scholar 

  22. Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02348-4_21

    Chapter  Google Scholar 

  23. Kurihara, M., Kondo, H.: Completion for multiple reduction orderings. J. Autom. Reason. 23(1), 25–42 (1999)

    Article  MathSciNet  Google Scholar 

  24. Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. Mach. Learn. 53(1–2), 111–156 (2003)

    Article  Google Scholar 

  25. Liang, P., Jordan, M.I., Klein, D.: Learning programs: a hierarchical Bayesian approach. In: Proceedings of the 27th International Conference on Machine Learning, ICML 2010, pp. 639–646 (2010)

    Google Scholar 

  26. Löchner, B.: Things to know when implementing KBO. J. Autom. Reason. 36(4), 289–310 (2006)

    Article  MathSciNet  Google Scholar 

  27. McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147–167 (1992). https://doi.org/10.1007/BF00245458

    Article  MathSciNet  MATH  Google Scholar 

  28. Menon, A.K., Tamuz, O., Gulwani, S., Lampson, B.W., Kalai, A.: A machine learning framework for programming by example. In: ICML (2013)

    Google Scholar 

  29. Novikov, P.S.: On the algorithmic unsolvability of the word problem in group theory. Trudy Matematicheskogo Instituta imeni VA Steklova 44, 3–143 (1955)

    Google Scholar 

  30. Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: PLDI (2015)

    Google Scholar 

  31. Otto, F.: On the connections between rewriting and formal language theory. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 332–355. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48685-2_27

    Chapter  MATH  Google Scholar 

  32. Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 297–310. ACM (2016)

    Google Scholar 

  33. Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 522–538. ACM (2016)

    Article  Google Scholar 

  34. Reddy, U.S.: Rewriting techniques for program synthesis. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 388–403. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51081-8_121

    Chapter  Google Scholar 

  35. Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. ACM SIGPLAN Not. 48(4), 305–316 (2013)

    Article  Google Scholar 

  36. Smith, C., Albarghouthi, A.: MapReduce program synthesis. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 326–340. ACM (2016)

    Google Scholar 

  37. Smith, C., Ferns, G., Albarghouthi, A.: Discovering relational specifications. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 616–626. ACM (2017)

    Google Scholar 

  38. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS (2006)

    Google Scholar 

  39. Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: TRANSIT: specifying protocols with concolic snippets. ACM SIGPLAN Not. 48(6), 287–296 (2013)

    Article  Google Scholar 

  40. Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. Proc. ACM Program. Lang. 2(POPL), 63 (2017)

    Google Scholar 

  41. Wehrman, I., Stump, A., Westbrook, E.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287–296. Springer, Heidelberg (2006). https://doi.org/10.1007/11805618_22

    Chapter  Google Scholar 

  42. White, T.: Hadoop - The Definitive Guide: Storage and Analysis at Internet Scale (2015)

    Google Scholar 

  43. Winkler, S., Middeldorp, A.: Termination tools in ordered completion. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 518–532. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_43

    Chapter  Google Scholar 

  44. Yu, Y., et al.: DryadLINQ: a system for general-purpose distributed data-parallel computing using a high-level language. In: OSDI (2008)

    Google Scholar 

  45. Zaharia, M., et al.: Resilient distributed datasets: a fault-tolerant abstraction for in-memory cluster computing. In: NSDI (2012)

    Google Scholar 

  46. Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. J. Autom. Reason. 43(2), 173–201 (2009)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgement

This work is supported by the National Science Foundation CCF under awards 1566015 and 1652140.

Author information

Authors and Affiliations

  1. University of Wisconsin–Madison, Madison, WI, USA

    Calvin Smith & Aws Albarghouthi

Authors
  1. Calvin Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aws Albarghouthi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Calvin Smith .

Editor information

Editors and Affiliations

  1. IRIF, University Paris Diderot and CNRS, Paris, France

    Constantin Enea

  2. Yale University, New Haven, CT, USA

    Ruzica Piskac

1 Electronic supplementary material

Below is the link to the electronic supplementary material.

Supplementary material 1 (pdf 542 KB)

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Smith, C., Albarghouthi, A. (2019). Program Synthesis with Equivalence Reduction. In: Enea, C., Piskac, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2019. Lecture Notes in Computer Science(), vol 11388. Springer, Cham. https://doi.org/10.1007/978-3-030-11245-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-11245-5_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-11244-8

  • Online ISBN: 978-3-030-11245-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation