Synbit: synthesizing bidirectional programs using unidirectional sketches
Pages 198 - 247
Abstract
We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus input/output examples. The core ideas are: (1) constructing a sketch using the given unidirectional program as a specification, and (2) filling the sketch in a modular fashion by exploiting the properties of bidirectional programs. These ideas are enabled by our choice of programming language, HOBiT, which is specifically designed to maintain the unidirectional program structure in bidirectional programming, and keep the parts that control bidirectional behavior modular. To evaluate our approach, we implemented it in a tool called Synbit and used it to generate bidirectional programs for intricate microbenchmarks, as well as for a few larger, more realistic problems. We also compared Synbit to a state-of-the-art unidirectional synthesis tool on the task of synthesizing backward computations. This is an extended version of the paper “Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches”, published at OOPSLA 2021. In addition to the OOPSLA’21 paper, this journal will contain additional formalization and detailed examples.
References
[1]
Bancilhon F and Spyratos N Update semantics of relational views ACM Trans Database Syst 1981 6 4 557-575
[2]
Hegner SJ (1990) Foundations of canonical update support for closed database views. In: ICDT, pp 422–436.
[3]
Stevens P In: Lämmel R, Visser J, Saraiva J (eds) (2008) A landscape of bidirectional model transformations. Springer, Berlin, Heidelberg, pp 408–424.
[4]
Foster JN, Greenwald MB, Moore JT, Pierce BC, and Schmitt A Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem ACM Trans Program Lang Syst 2007 10 1145/1232420 1232424
[5]
Matsuda K, Hu Z, Nakano K, Hamana M, Takeichi M (2007) Bidirectionalization transformation based on automatic derivation of view complement functions. In: Proceedings of the 12th ACM SIGPLAN international conference on functional programming, ICFP 2007, Freiburg, Germany, October 1–3, 2007, pp 47–58.
[6]
Bohannon A, Foster JN, Pierce BC, Pilkiewicz A, Schmitt A (2008) Boomerang: resourceful lenses for string data. In: Necula GC, Wadler P (eds) Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp 407–419 .
[7]
Voigtländer J (2009) Bidirectionalization for free! (pearl). In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. POPL ’09. Association for Computing Machinery, New York, NY, USA, pp 165–176.
[8]
Pacheco H, Hu Z, Fischer S (2014) Monadic combinators for "putback" style bidirectional programming. In: Proceedings of the ACM SIGPLAN 2014 Workshop on partial evaluation and program manipulation, PEPM 2014, January 20–21, 2014, San Diego, California, USA, pp 39–50.
[9]
Matsuda K, Wang M (2018) Hobit: Programming lenses without using lens combinators. In: Ahmed A (ed) Programming languages and systems—27th European symposium on programming, ESOP 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, pp 31–59.
[10]
Matsuda K, Wang M (2015) Applicative bidirectional programming with lenses. In: Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP 2015, Vancouver, BC, Canada, September 1–3, 2015, pp 62–74.
[11]
Matsuda K and Wang M “Bidirectionalization for free” for monomorphic transformations Sci Comput Program 2015 111 79-109
[12]
Chong N, Cook B, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M, Tuttle MR (2020) Code-level model checking in the software development workflow. In: ICSE-SEIP 2020: 42nd international conference on software engineering, software engineering in practice, Seoul, South Korea, 27 June–19 July, 2020, pp 11–20.
[13]
Lubin J, Collins N, Omar C, Chugh R (2020) Program sketching with live bidirectional evaluation. In: Proceedings of the ACM on Programming Languages 4(ICFP), pp 109–110929.
[14]
Gulwani S (2011) Automating string processing in spreadsheets using input-output examples. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26–28, 2011, pp 317–330.
[15]
Solar-Lezama A (2009) The sketching approach to program synthesis. In: Hu Z (ed) Programming languages and systems, 7th Asian symposium, APLAS 2009, Seoul, Korea, December 14–16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5904, pp 4–13.
[16]
Lutz C (1986) Janus: a time-reversible language. Letter to R. Landauer. Available on: http://tetsuo.jp/ref/janus.pdf
[17]
Yokoyama T, Axelsen H.B, Glück R (2011) Towards a reversible functional language. In: RC, pp 14–29.
[18]
Ko H, Zan T, Hu Z (2016) BiGUL: a formally verified core language for putback-based bidirectional programming. In: Proceedings of the 2016 ACM SIGPLAN Workshop on partial evaluation and program manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20–22, 2016, pp 61–72.
[19]
Hu Z, Ko H (2016) Principles and practice of bidirectional programming in BiGUL. In: Bidirectional transformations—international summer school, Oxford, UK, July 25–29, 2016, Tutorial Lectures, pp 100–150.
[20]
Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM/IEEE international conference on software engineering—Volume 1, ICSE 2010, Cape Town, South Africa, 1–8 May 2010, pp 215–224.
[21]
Feng Y, Martins R, Wang Y, Dillig I, Reps TW (2017) Component-based synthesis for complex APIs. In: Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages, POPL 2017, Paris, France, January 18–20, 2017, pp 599–612. http://dl.acm.org/citation.cfm?id=3009851
[22]
Davies R and Pfenning F A modal analysis of staged computation J ACM 2001 48 3 555-604
[23]
Osera P, Zdancewic S (2015) Type-and-example-directed program synthesis. In: Grove D, Blackburn SM (eds) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15–17, 2015, pp 619–630.
[24]
Fischer S, Kiselyov O, and Shan C Purely functional lazy nondeterministic programming J Funct Program 2011 21 4–5 413-465
[25]
Albarghouthi A, Gulwani S, Kincaid Z (2013) Recursive program synthesis. In: Computer aided verification—25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, pp 934–950.
[26]
Damas L, Milner R (1982) Principal type-schemes for functional programs. In: Conference record of the ninth annual ACM symposium on principles of programming languages, Albuquerque, New Mexico, USA, January 1982, pp 207–212.
[27]
Matsuda K, Inaba K, Nakano K (2012) Polynomial-time inverse computation for accumulative functions with multiple data traversals. In: Proceedings of the ACM SIGPLAN 2012 workshop on partial evaluation and program manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23–24, 2012, pp 5–14.
[28]
Nishida N, Vidal G (2011) Program inversion for tail recursive functions. In: Proceedings of the 22nd international conference on rewriting techniques and applications, RTA 2011, May 30–June 1, 2011, Novi Sad, Serbia, pp 283–298.
[29]
de Jonge M, Visser E (2011) An algorithm for layout preservation in refactoring transformations. In: Software language engineering—4th international conference, SLE 2011, Braga, Portugal, July 3–4, 2011, Revised Selected Papers, pp 40–59.
[30]
Kort J, Lämmel R (2003) Parse-tree annotations meet re-engineering concerns. In: 3rd IEEE International workshop on source code analysis and manipulation (SCAM 2003), 26–27 September 2003, Amsterdam, The Netherlands, p 161.
[31]
Pombrio J, Krishnamurthi S (2014) Resugaring: lifting evaluation sequences through syntactic sugar. In: ACM SIGPLAN Conference on programming language design and implementation, PLDI ’14, Edinburgh, United Kingdom—June 09–11, 2014, pp 361–371.
[32]
Miltner A, Fisher K, Pierce BC, Walker D, Zdancewic S (2018) Synthesizing bijective lenses. In: Proceedings of the ACM on Programming Languages 2(POPL), pp 1–1130.
[33]
Maina S, Miltner A, Fisher K, Pierce BC, Walker D, Zdancewic S (2018) Synthesizing quotient lenses. In: Proceedings of the ACM on Programming Languages 2(ICFP), pp 80–18029.
[34]
Miltner A, Maina S, Fisher K, Pierce BC, Walker D, Zdancewic S (2019) Synthesizing symmetric lenses. In: Proceedings of the ACM on Programming Languages 3(ICFP), pp 95–19528.
[35]
Hofmann M, Pierce BC, Wagner D (2011) Symmetric lenses. In: Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26–28, 2011, pp 371–384.
[36]
Foster JN, Pilkiewicz A, Pierce BC (2008) Quotient lenses. In: Proceeding of the 13th ACM SIGPLAN international conference on functional programming, ICFP 2008, Victoria, BC, Canada, September 20–28, 2008, pp 383–396.
[37]
Barbosa DMJ, Cretin J, Foster N, Greenberg M, Pierce BC (2010) Matching lenses: alignment and view update. In: Hudak P, Weirich S (eds) Proceeding of the 15th ACM SIGPLAN international conference on functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27–29, 2010, pp 193–204. ACM,.
[38]
Voigtländer J (2012) Ideas for connecting inductive program synthesis and bidirectionalization. In: Proceedings of the ACM SIGPLAN 2012 workshop on partial evaluation and program manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23–24, 2012, pp 39–42.
[39]
Srivastava S, Gulwani S, Chaudhuri S, Foster JS (2011) Path-based inductive synthesis for program inversion. In: Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI 2011, San Jose, CA, USA, June 4–8, 2011, pp 492–503.
[40]
Korf RE (1981) Inversion of applicative programs. In: IJCAI, pp 1007–1009
[41]
Yokoyama T, Axelsen HB, Glück R (2008) Principles of a reversible programming language. In: Proceedings of the 5th conference on computing frontiers, 2008, Ischia, Italy, May 5–7, 2008, pp 43–54.
[42]
Gries D The science of programming, chapter 21 inverting programs 1981 Berlin Springer
[43]
Glück R and Kawabe M Revisiting an automatic program inverter for lisp SIGPLAN Not 2005 40 5 8-17
[44]
Matsuda K, Mu S-C, Hu Z, Takeichi M (2010) A grammar-based approach to invertible programs. In: ESOP, pp 448–467
[45]
Nishida N, Sakai M, Sakabe T (2005) Partial inversion of constructor term rewriting systems. In: Term rewriting and applications, 16th international conference, RTA 2005, Nara, Japan, April 19–21, 2005, Proceedings, pp 264–278.
[46]
Gomard CK and Jones ND A partial evaluator for the untyped lambda-calculus J Funct Program 1991 1 1 21-69
[47]
Almendros-Jiménez JM, Vidal G (2006) Automatic partial inversion of inductively sequential functions. In: Implementation and application of functional languages, 18th international symposium, IFL 2006, Budapest, Hungary, September 4–6, 2006, Revised Selected Papers, pp 253–270.
[48]
Matsuda K, Wang M (2020) Sparcl: a language for partially-invertible computation. In: Proceedings of the ACM on Programming Languages 4(ICFP), pp 118–111831.
[49]
Wadler P Deforestation: transforming programs to eliminate trees Theor Comput Sci 1990 73 2 231-248
[50]
Voigtländer J (2009) Bidirectionalization for free! (pearl). In: Proceedings of the 36th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2009, Savannah, GA, USA, January 21–23, 2009, pp 165–176.
[51]
Wadler P (1989) Theorems for free! In: Proceedings of the fourth international conference on functional programming languages and computer architecture, FPCA 1989, London, UK, September 11–13, 1989, pp 347–359.
[52]
Reynolds JC (1983) Types, abstraction and parametric polymorphism. In: Information processing 83, proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19–23, 1983, pp 513–523
[53]
Voigtländer J, Hu Z, Matsuda K, and Wang M Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins J Funct Program 2013 23 5 515-551
[54]
Matsuda K and Wang M Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization J Funct Program 2018 28 15
[55]
Solar-Lezama A, Jones CG, Bodík R (2008) Sketching concurrent data structures. In: PLDI, pp 136–148.
[56]
David C, Kesseli P, Kroening D, and Lewis M Program synthesis for program analysis ACM Trans Program Lang Syst 2018 40 2 5-1545
[57]
David C, Kroening D, Lewis M (2015) Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek J (ed) Programming languages and systems—24th European symposium on programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9032, pp 183–204.
[58]
Abate A, Bessa I, Cattaruzza D, Cordeiro L.C, David C, Kesseli P, Kroening D, Polgreen E (2017) Automated formal synthesis of digital controllers for state-space physical plants. In: Majumdar R, Kuncak V (eds) Computer aided verification—29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp 462–482.
[59]
Kneuss E, Kuraj I, Kuncak V, Suter P (2013) Synthesis modulo recursive functions. In: Hosking AL, Eugster PT, Lopes CV (eds) Proceedings of the 2013 ACM SIGPLAN international conference on object oriented programming systems languages & applications, OOPSLA 2013, Part of SPLASH 2013, Indianapolis, IN, USA, October 26–31, 2013, pp 407–426.
[60]
Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Chockler H, Weissenbacher G (eds) Computer aided verification—30th international conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp 270–288.
[61]
Katayama S (2005) Systematic search for lambda expressions. In: van Eekelen MCJD (ed) Revised selected papers from the sixth symposium on trends in functional programming, TFP 2005, Tallinn, Estonia, 23–24 September 2005. Trends in Functional Programming, vol. 6, pp 111–126
[62]
Feser JK, Chaudhuri S, Dillig I (2015) Synthesizing data structure transformations from input-output examples. In: Grove D, Blackburn SM (eds) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15–17, 2015, pp 229–239.
[63]
Smith C, Albarghouthi A (2019) Program synthesis with equivalence reduction. In: Enea C, Piskac R (eds) Verification, model checking, and abstract interpretation—20th international conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11388, pp 24–47.
[64]
Koukoutos M, Kneuss E, Kuncak V (2016) An update on deductive synthesis and repair in the leon tool. In: Piskac R, Dimitrova R (eds) Proceedings fifth workshop on synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016. EPTCS, vol. 229, pp 100–111.
Recommendations
Synbit: synthesizing bidirectional programs using unidirectional sketches
We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus a few input/output examples. The core ideas are: (1) constructing a sketch using the given unidirectional program as a specification, and (2) ...
Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular Examples
Logic-Based Program Synthesis and TransformationAbstractIn the database community, many synthesizers have been proposed to synthesize unidirectional programs (queries) from tabular examples, but it remains as a challenge to synthesize bidirectional programs (view update strategies) from examples over ...
Synthesizing transformations on hierarchically structured data
PLDI '16This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s) 2024.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 29 January 2024
Accepted: 19 June 2023
Received: 01 April 2022
Author Tags
Qualifiers
- Research-article
Funding Sources
- Royal Society
- EPSRC
- Royal Society
- JSPS KAKENHI
- JSPS KAKENHI
- JSPS Bilateral Program
- Kayamori Foundation of Informational Science Advancement
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 22 Dec 2024