Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design

16.05.2023

Partial bounding for recursive function synthesis

verfasst von: Azadeh Farzan, Victor Nicolet

Erschienen in: Formal Methods in System Design

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Quantifier bounding is a standard approach in inductive program synthesis to deal with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis problem is specified by an input reference (recursive) function and a recursion skeleton. The goal is to synthesize a recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton. In this context, we illustrate that it is possible to selectively bound a subset of the recursively typed parameters, each by a suitable bound. The choices are guided by counterexamples. The evaluation of our strategy on a broad set of benchmarks shows that it succeeds in efficiently synthesizing non-trivial recursive functions where standard across-the-board bounding would fail.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
2
This example is from [25], which calls this data type zipper.
 
Literatur
1.
Abrahamsson O, Myreen MO (2018) Automatically introducing tail recursion in CakeML. In: Trends in functional programming, lecture notes in computer science. Springer International Publishing, pp 118–134
2.
Ahmad MBS, Cheung A (2018) Automatically leveraging mapreduce frameworks for data-intensive applications. In: Proceedings of the 2018 international conference on management of data, SIGMOD ’18. ACM
3.
Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: Computer aided verification, lecture notes in computer science. Springer, pp 934–950
4.
Alur R, Bodik R, Juniwal G, et al (2013) Syntax-guided synthesis. In: 2013 Formal methods in computer-aided design. IEEE, pp 1–8
5.
Barrett C, Conway CL, Deters M et al (2011) CVC4. Computer aided verification. In: Lecture notes in computer science. Springer, pp 171–177
6.
7.
de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science. Springer, pp 337–340
8.
Farzan A, Nicolet V (2017) Synthesis of divide and conquer parallelism for loops. In: Proceedings of the 38th ACM conference on programming language design and implementation, PLDI ’17
9.
Fedyukovich G, Ahmad MBS, Bodik R (2017) Gradual synthesis for static parallelization of single-pass array-processing programs. In: Proceedings of the 38th ACM conference on programming language design and implementation, PLDI 2017
10.
Feldman YMY, Padon O, Immerman N, et al (2017) Bounded quantifier instantiation for checking inductive invariants. In: Tools and algorithms for the construction and analysis of systems, lecture notes in computer science, pp 76–95
11.
Feser JK, Chaudhuri S, Dillig I (2015) Synthesizing data structure transformations from input–output examples. In: Proceedings of the 36th ACM conference on programming language design and implementation, PLDI ’15
12.
Frankle J, Osera PM, Walker D, et al (2016) Example-directed synthesis: a type-theoretic interpretation. In: Proceedings of the 43rd ACM symposium on principles of programming languages, POPL’16
13.
Hamilton GW, Jones ND (2012) Distillation with labelled transition systems. In: Proceedings of the ACM 2012 workshop on partial evaluation and program manipulation, PEPM ’12. ACM, pp 15–24
14.
Huet G (1997) The zipper. J Funct Program 7(5)
15.
Inala JP, Polikarpova N, Qiu X, et al (2017) Synthesis of recursive ADT transformations from reusable templates. In: Tools and algorithms for the construction and analysis of systems, lecture notes in computer science
16.
Itzhaky S, Singh R, Solar-Lezama A, et al (2016) Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In: Proceedings of the 2016 ACM conference on object-oriented programming, systems, languages, and applications. ACM, pp 145–164
17.
Katayama S (2012) An analytical inductive functional programming system that avoids unintended programs. In: Proceedings of the 2012 workshop on partial evaluation and program manipulation, PEPM’12
18.
Kitzelmann E, Schmid U (2006) Inductive synthesis of functional programs: an explanation based generalization approach. J Mach Learn Res 7(15):429–454MathSciNetMATH
19.
Kneuss E, Kuraj I, Kuncak V, et al (2013) Synthesis modulo recursive functions. In: Proceedings of the 2013 international conference on object oriented programming systems languages and applications, OOPSLA’13
20.
Kobayashi N (2009) Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of the 36th ACM symposium on principles of programming languages, POPL’09
21.
Kobayashi N, Tabuchi N, Unno H (2010) Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of the 37th ACM symposium on principles of programming languages, POPL’10
22.
Kobayashi N, Sato R, Unno H (2011) Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM conference on programming language design and implementation, PLDI’11, pp 222–233
23.
Leroy X, Doligez D, Frisch A, et al (2019) The OCaml system release 4.11: documentation and user’s manual. p 823
24.
Morihata A, Matsuzaki K (2010) Automatic parallelization of recursive functions using quantifier elimination. In: Proceedings of the 10th international conference on functional and logic programming, FLOPS’10
25.
Morihata A, Matsuzaki K, Hu Z, et al (2009) The third homomorphism theorem on trees: downward and upward lead to divide-and-conquer. In: Proceedings of the 36th ACM symposium on principles of programming languages, POPL’09
26.
27.
Ong CHL, Ramsay SJ (2011) Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of the 38th ACM symposium on principles of programming languages, POPL’11
28.
Osera PM, Zdancewic S (2015) Type-and-example-directed program synthesis. In: Proceedings of the 36th ACM conference on programming language design and implementation, PLDI’15
29.
Padhi S, Polgreen E, Raghothaman M, et al (2019) The SyGuS language standard version 2.1
30.
Polikarpova N, Kuraj I, Solar-Lezama A (2016) Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM conference on programming language design and implementation, PLDI’16
31.
Ramsay SJ, Neatherway RP, Ong CHL (2014) A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of the 41st ACM symposium on principles of programming languages, POPL’14
32.
Reynolds A, Deters M, Kuncak V, et al (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification, lecture notes in computer science, pp 198–216
33.
Solar-Lezama A (2008) Program synthesis by sketching. University of California, Berkeley
34.
Solar-Lezama A, Tancau L, Bodik R, et al (2006) Combinatorial sketching for finite programs. In: Proceedings of the 12th international conference on architectural support for programming languages and operating systems, ASPLOS XII. pp 404–415
35.
Solar-Lezama A, Arnold G, Tancau L, et al (2007) Sketching stencils. In: Proceedings of the 28th ACM conference on programming language design and implementation, PLDI’07
36.
Solar-Lezama A, Jones CG, Bodik R (2008) Sketching concurrent data structures. In: Proceedings of the 29th ACM conference on programming language design and implementation, PLDI’08
37.
38.
Yang W, Fedyukovich G, Gupta A (2019) Lemma synthesis for automating induction over algebraic data types. In: Principles and practice of constraint programming, lecture notes in computer science, pp 600–617
Metadaten
Titel
Partial bounding for recursive function synthesis
verfasst von
Azadeh Farzan
Victor Nicolet
Publikationsdatum
16.05.2023
Verlag
Springer US
Erschienen in
Formal Methods in System Design
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-023-00417-y

Premium Partner

    Bildnachweise