{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:49Z","timestamp":1747173469637,"version":"3.40.5"},"reference-count":90,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2024,1,26]],"date-time":"2024-01-26T00:00:00Z","timestamp":1706227200000},"content-version":"unspecified","delay-in-days":25,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer\/deserializer, parser\/printer, redo\/undo, compressor\/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on <jats:italic>partially invertible<\/jats:italic> functions\u2014functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.<\/jats:p>\n\t  <jats:p>We develop a language <jats:sc>Sparcl<\/jats:sc> for programming such functions in a natural way, where partial invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the \u201cpartially\u201d part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language <jats:sc>Sparcl<\/jats:sc> is linear-typed and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language and prove that <jats:sc>Sparcl<\/jats:sc> correctly guarantees invertibility for its programs. We demonstrate the expressiveness of <jats:sc>Sparcl<\/jats:sc> with examples including tree rebuilding from preorder and inorder traversals, Huffman coding, arithmetic coding, and LZ77 compression.<\/jats:p>","DOI":"10.1017\/s0956796823000126","type":"journal-article","created":{"date-parts":[[2024,1,26]],"date-time":"2024-01-26T08:20:21Z","timestamp":1706257221000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["<scp>Sparcl<\/scp>: A language for partially invertible computation"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9747-4899","authenticated-orcid":false,"given":"KAZUTAKA","family":"MATSUDA","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-630X","authenticated-orcid":false,"given":"MENG","family":"WANG","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,1,26]]},"reference":[{"key":"S0956796823000126_ref54","doi-asserted-by":"crossref","unstructured":"Matsuda, K. & Wang, M. (2018c) HOBiT: Programming lenses without using lens combinators. In ESOP. Springer, pp. 31\u201359.","DOI":"10.1007\/978-3-319-89884-1_2"},{"key":"S0956796823000126_ref63","doi-asserted-by":"crossref","unstructured":"Mu, S. & Bird, R. S. (2003) Rebuilding a tree from its traversals: A case study of program inversion. In Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27\u201329, 2003, Proceedings, Ohori, A. (ed). Lecture Notes in Computer Science, vol. 2895. Springer, pp. 265\u2013282.","DOI":"10.1007\/978-3-540-40018-9_18"},{"key":"S0956796823000126_ref85","doi-asserted-by":"crossref","unstructured":"Wang, M. , Gibbons, J. , Matsuda, K. & Hu, Z. (2013) Refactoring pattern matching. Sci. Comput. Program. 78(11), 2216\u20132242. Special section on Mathematics of Program Construction (MPC 2010) and Special section on methodological development of interactive systems from Interaccion 2011.","DOI":"10.1016\/j.scico.2012.07.014"},{"key":"S0956796823000126_ref33","unstructured":"Jones, N. D. , Gomard, C. K. & Sestoft, P. (1993) Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice Hall."},{"key":"S0956796823000126_ref14","doi-asserted-by":"crossref","unstructured":"Chen, C. & Sabry, A. (2021) A computational interpretation of compact closed categories: Reversible programming with negative and fractional types. Proc. ACM Program. Lang. 5(POPL), 1\u201329.","DOI":"10.1145\/3434290"},{"key":"S0956796823000126_ref13","doi-asserted-by":"crossref","unstructured":"Capretta, V. (2005) General recursion via coinductive types. Logical Methods Comput. Sci. 1(2), Article number 1.Please provide page number for \u201cCapretta (2005)\u201d.","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"S0956796823000126_ref24","first-page":"3_108","article-title":"A linear-time self-interpreter of a reversible imperative language","volume":"33","author":"Gl\u00fcck","year":"2016","journal-title":"Comput. Softw."},{"key":"S0956796823000126_ref71","first-page":"1","volume-title":"Haskell","author":"Rendel","year":"2010"},{"key":"S0956796823000126_ref2","unstructured":"Abramov, S. M. , Gl\u00fcck, R. & Klimov, Y. A. (2006) An universal resolving algorithm for inverse computation of lazy languages. In Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27\u201330, 2006. Papers, Revised , Virbitskaite, I. & Voronkov, A. (eds), Lecture Notes in Computer Science, vol. 4378. Springer, pp. 27\u201340."},{"key":"S0956796823000126_ref39","unstructured":"Kristensen, J. T. , Kaarsgaard, R. & Thomsen, M. K. (2022b) Jeopardy: An invertible functional programming language. CoRR. abs\/2209.02422."},{"key":"S0956796823000126_ref40","doi-asserted-by":"crossref","unstructured":"K\u00fchnemann, A. , Gl\u00fcck, R. & Kakehi, K. (2001) Relating accumulative and non-accumulative functional programs. In RTA. Springer, pp. 154\u2013168.","DOI":"10.1007\/3-540-45127-7_13"},{"key":"S0956796823000126_ref56","doi-asserted-by":"crossref","unstructured":"Mazurak, K. , Zhao, J. & Zdancewic, S. (2010) Lightweight linear types in system fdegree. In TLDI. ACM, pp. 77\u201388.","DOI":"10.1145\/1708016.1708027"},{"key":"S0956796823000126_ref11","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1147\/rd.176.0525","article-title":"Logical reversibility of computation","volume":"17","author":"Bennett","year":"1973","journal-title":"IBM J. Res. Dev."},{"key":"S0956796823000126_ref42","doi-asserted-by":"crossref","unstructured":"Launchbury, J. & Jones, S. L. P. (1994) Lazy functional state threads. In Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, USA, June 20\u201324, 1994. ACM, pp. 24\u201335.","DOI":"10.1145\/178243.178246"},{"key":"S0956796823000126_ref7","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. & Grattage, J. (2005) A functional quantum programming language. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26\u201329 June 2005, Chicago, IL, USA, Proceedings. IEEE Computer Society, pp. 249\u2013258.","DOI":"10.1109\/LICS.2005.1"},{"key":"S0956796823000126_ref68","unstructured":"Nishida, N. & Vidal, G. (2011) Program inversion for tail recursive functions. In RTA. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 283\u2013298."},{"key":"S0956796823000126_ref3","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/j.tcs.2005.07.002","article-title":"A structural approach to reversible computation","volume":"347","author":"Abramsky","year":"2005","journal-title":"Theor. Comput. Sci."},{"key":"S0956796823000126_ref46","doi-asserted-by":"crossref","unstructured":"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\u20133, 2007. ACM, pp. 47\u201358.","DOI":"10.1145\/1291151.1291162"},{"key":"S0956796823000126_ref72","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1010027404223","article-title":"Definitional interpreters for higher-order programming languages","volume":"11","author":"Reynolds","year":"1998","journal-title":"Higher-Order Symb. Comput."},{"volume":"55","volume-title":"Cambridge Tracts in Theoretical Computer Science","year":"2003","key":"S0956796823000126_ref79"},{"key":"S0956796823000126_ref28","doi-asserted-by":"crossref","unstructured":"Hu, Z. , Iwasaki, H. , Takeichi, M. & Takano, A. (1997) Tupling calculation eliminates multiple data traversals. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP\u201997), Amsterdam, The Netherlands, June 9\u201311, 1997. ACM, pp. 164\u2013175.","DOI":"10.1145\/258949.258964"},{"key":"S0956796823000126_ref38","unstructured":"Kristensen, J. T. , Kaarsgaard, R. & Thomsen, M. K. (2022a) Branching execution symmetry in jeopardy by available implicit arguments analysis. CoRR. abs\/2212.03161."},{"key":"S0956796823000126_ref45","doi-asserted-by":"crossref","unstructured":"Matsuda, K. (2020) Modular inference of linear types for multiplicity-annotated arrows. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25\u201330, 2020, Proceedings. Springer. pp. 456\u2013483. The full version is available on: http:\/\/arxiv.org\/abs\/1911.00268v2.","DOI":"10.1007\/978-3-030-44914-8_17"},{"key":"S0956796823000126_ref82","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1017\/S0956796811000098","article-title":"OutsideIn(X) modular type inference with local assumptions","volume":"21","author":"Vytiniotis","year":"2011","journal-title":"J. Funct. Program."},{"key":"S0956796823000126_ref80","doi-asserted-by":"crossref","unstructured":"Tov, J. A. & Pucella, R. (2011) Practical affine types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011. ACM, pp. 447\u2013458.","DOI":"10.1145\/1926385.1926436"},{"key":"S0956796823000126_ref16","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/382780.382785","article-title":"A modal analysis of staged computation","volume":"48","author":"Davies","year":"2001","journal-title":"J. ACM"},{"key":"S0956796823000126_ref37","doi-asserted-by":"crossref","unstructured":"Kirkeby, M. H. & Gl\u00fcck, R. (2020) Inversion framework: Reasoning about inversion by conditional term rewriting systems. In PPDP\u201920: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9\u201310 September, 2020. ACM, pp. 9:1\u20139:14.","DOI":"10.1145\/3414080.3414089"},{"key":"S0956796823000126_ref67","doi-asserted-by":"crossref","unstructured":"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\u201321, 2005, Proceedings. Springer, pp. 264\u2013278.","DOI":"10.1007\/978-3-540-32033-3_20"},{"key":"S0956796823000126_ref86","doi-asserted-by":"crossref","unstructured":"Xi, H. & Pfenning, F. (1998) Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN\u201998 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17\u201319, 1998. ACM, pp. 249\u2013257.","DOI":"10.1145\/277650.277732"},{"key":"S0956796823000126_ref23","doi-asserted-by":"crossref","unstructured":"Gl\u00fcck, R. & Kawabe, M. (2004) Derivation of deterministic inverse programs based on LR parsing. In FLOPS. Springer, pp. 291\u2013306.","DOI":"10.1007\/978-3-540-24754-8_21"},{"key":"S0956796823000126_ref22","doi-asserted-by":"crossref","unstructured":"Gl\u00fcck, R. & Kawabe, M. (2003) A program inverter for a functional language with equality and constructors. In Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27\u201329, 2003, Proceedings, Ohori, A. (ed). Lecture Notes in Computer Science, vol. 2895. Springer, pp. 246\u2013264.","DOI":"10.1007\/978-3-540-40018-9_17"},{"key":"S0956796823000126_ref17","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. & Mitra, S. (1999) Jeopardy. In Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2\u20134, 1999, Proceedings. Springer, pp. 16\u201329.","DOI":"10.1007\/3-540-48685-2_2"},{"key":"S0956796823000126_ref47","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10990-013-9097-8","article-title":"Polynomial-time inverse computation for accumulative functions with multiple data traversals","volume":"25","author":"Matsuda","year":"2012","journal-title":"Higher-Order Symb. Comput."},{"key":"S0956796823000126_ref57","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796807006326","article-title":"Applicative programming with effects","volume":"18","author":"McBride","year":"2008","journal-title":"J. Funct. Program."},{"key":"S0956796823000126_ref34","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1017\/S0305004100074338","article-title":"Traced monoidal categories","volume":"119","author":"Joyal","year":"1996","journal-title":"Math. Proc. Cambridge Philos. Soc"},{"key":"S0956796823000126_ref53","doi-asserted-by":"crossref","unstructured":"Matsuda, K. & Wang, M. (2018b) Embedding invertible languages with binders: A case of the FliPpr language. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27\u201317, 2018. ACM, pp. 158\u2013171.","DOI":"10.1145\/3242744.3242758"},{"key":"S0956796823000126_ref87","doi-asserted-by":"crossref","unstructured":"Yokoyama, T. , Axelsen, H. B. & Gl\u00fcck, R. (2008) Principles of a reversible programming language. In Proceedings of the 5th Conference on Computing Frontiers, 2008, Ischia, Italy, May 5\u20137, 2008. ACM, pp. 43\u201354.","DOI":"10.1145\/1366230.1366239"},{"key":"S0956796823000126_ref75","doi-asserted-by":"crossref","unstructured":"Rondon, P. M. , Kawaguchi, M. & Jhala, R. (2008) Liquid types. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7\u201313, 2008. ACM, pp. 159\u2013169.","DOI":"10.1145\/1379022.1375602"},{"key":"S0956796823000126_ref1","doi-asserted-by":"crossref","unstructured":"Abel, A. & Chapman, J. (2014) Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014, pp. 51\u201367.","DOI":"10.4204\/EPTCS.153.4"},{"key":"S0956796823000126_ref59","unstructured":"Mogensen, T. \u00c6. (2006) Report on an implementation of a semi-inverter. In Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27\u201330, 2006. Revised Papers, Virbitskaite, I. & Voronkov, A. (eds). Lecture Notes in Computer Science, vol. 4378. Springer, pp. 322\u2013334."},{"key":"S0956796823000126_ref62","doi-asserted-by":"crossref","unstructured":"Morris, J. G. (2016) The best of both worlds: linear functional programming without compromise. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18\u201322, 2016. ACM, pp. 448\u2013461.","DOI":"10.1145\/3022670.2951925"},{"key":"S0956796823000126_ref74","doi-asserted-by":"crossref","unstructured":"Romanenko, A. (1991) Inversion and metacomputation. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM\u201991, Yale University, New Haven, Connecticut, USA, June 17\u201319, 1991. ACM, pp. 12\u201322.","DOI":"10.1145\/115865.115868"},{"key":"S0956796823000126_ref21","doi-asserted-by":"crossref","unstructured":"Gibbons, J. (2002) Calculating functional programs. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Backhouse, R. , Crole, R. & Gibbons, J. (eds). Lecture Notes in Computer Science, vol. 2297. Springer-Verlag, pp. 148\u2013203. Available at: http:\/\/www.cs.ox.ac.uk\/people\/jeremy.gibbons\/publications\/acmmpc-calcfp.pdf.","DOI":"10.1007\/3-540-47797-7_5"},{"key":"S0956796823000126_ref35","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1017\/S0956796812000263","article-title":"Every bit counts: The binary representation of typed data and programs","volume":"22","author":"Kennedy","year":"2012","journal-title":"J. Funct. Program."},{"key":"S0956796823000126_ref55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3409000","article-title":"Sparcl: A language for partially-invertible computation","volume":"4","author":"Matsuda","year":"2020","journal-title":"Proc. ACM Program. Lang"},{"key":"S0956796823000126_ref49","doi-asserted-by":"crossref","unstructured":"Matsuda, K. & Wang, M. (2013) FliPpr: A prettier invertible printing system. In ESOP. Springer, pp. 101\u2013120.","DOI":"10.1007\/978-3-642-37036-6_6"},{"key":"S0956796823000126_ref77","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1017\/S0960129506005238","article-title":"A lambda calculus for quantum computation with classical control","volume":"16","author":"Selinger","year":"2006","journal-title":"Math. Struct. Comput. Sci."},{"key":"S0956796823000126_ref58","doi-asserted-by":"crossref","unstructured":"Mogensen, T. \u00c6. (2005) Semi-inversion of guarded equations. In Generative Programming and Component Engineering, 4th International Conference, GPCE 2005, Tallinn, Estonia, September 29\u2013October 1, 2005, Proceedings. Springer, pp. 189\u2013204.","DOI":"10.1007\/11561347_14"},{"key":"S0956796823000126_ref31","doi-asserted-by":"crossref","unstructured":"James, R. P. & Sabry, A. (2012) Information effects. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22\u201328, 2012. ACM, pp. 73\u201384.","DOI":"10.1145\/2103656.2103667"},{"key":"S0956796823000126_ref64","doi-asserted-by":"crossref","unstructured":"Mu, S. , Hu, Z. & Takeichi, M. (2004a) An algebraic approach to bi-directional updating. In Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4\u20136, 2004. Proceedings. Springer, pp. 2\u201320.","DOI":"10.1007\/978-3-540-30477-7_2"},{"key":"S0956796823000126_ref5","doi-asserted-by":"crossref","unstructured":"Almendros-Jim\u00e9nez, J. M. & Vidal, G. (2006) Automatic partial inversion of inductively sequential functions. In Implementation and Application of Functional Languages, 18th International Symp osium, IFL 2006, Budapest, Hungary, September 4\u20136, 2006, Revised Selected Papers. Springer, pp. 253\u2013270.","DOI":"10.1007\/978-3-540-74130-5_15"},{"key":"S0956796823000126_ref41","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1147\/rd.53.0183","article-title":"Irreversibility and heat generation in the computing process","volume":"5","author":"Landauer","year":"1961","journal-title":"IBM J. Res. Dev."},{"key":"S0956796823000126_ref15","doi-asserted-by":"crossref","unstructured":"Chin, W. (1993) Towards an automated tupling strategy. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM\u201993, Copenhagen, Denmark, June 14\u201316, 1993. ACM, pp. 119\u2013132.","DOI":"10.1145\/154630.154643"},{"key":"S0956796823000126_ref51","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.scico.2014.07.008","article-title":"\u201cBidirectionalization for free\u201d for monomorphic transformations","volume":"111","author":"Matsuda","year":"2015","journal-title":"Sci. Comput. Program."},{"volume-title":"Undergraduate Topics in Computer Science","year":"2008","author":"Salomon","key":"S0956796823000126_ref76"},{"key":"S0956796823000126_ref81","doi-asserted-by":"crossref","unstructured":"Virbitskaite, I. & Voronkov, A. (eds) (2007) Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27\u201330, 2006. Revised Papers. Lecture Notes in Computer Science, vol. 4378. Springer.","DOI":"10.1007\/978-3-540-70881-0"},{"key":"S0956796823000126_ref73","doi-asserted-by":"crossref","unstructured":"Rios, F. & Selinger, P. (2017) A categorical model for a quantum circuit description language. In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3\u20137 July 2017, pp. 164\u2013178.","DOI":"10.4204\/EPTCS.266.11"},{"volume-title":"Cambridge Tracts in Theoretical Computer Science","year":"1992","author":"Nielson","key":"S0956796823000126_ref66"},{"key":"S0956796823000126_ref84","unstructured":"Walker, D. (2004) Substractural type systems. In Advanced Topics in Types and Programming Languages, Pierce, B. C. (ed). MIT, pp. 3\u201343."},{"key":"S0956796823000126_ref12","first-page":"5:1","article-title":"Linear haskell: Practical linearity in a higher-order polymorphic language","volume":"2","author":"Bernardy","year":"2018","journal-title":"PACMPL"},{"key":"S0956796823000126_ref4","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1017\/S0960129502003730","article-title":"Geometry of interaction and linear combinatory algebras","volume":"12","author":"Abramsky","year":"2002","journal-title":"Math. Struct. Comput. Sci."},{"key":"S0956796823000126_ref18","unstructured":"Eppstein, D. (1985) A heuristic approach to program inversion. In IJCAI, pp. 219\u2013221."},{"key":"S0956796823000126_ref8","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1145\/347476.347484","article-title":"A needed narrowing strategy","volume":"47","author":"Antoy","year":"2000","journal-title":"J. ACM."},{"key":"S0956796823000126_ref19","doi-asserted-by":"crossref","DOI":"10.1145\/1232420.1232424","article-title":"Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem","volume":"29","author":"Foster","year":"2007","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"S0956796823000126_ref36","doi-asserted-by":"crossref","unstructured":"Kirkeby, M. H. & Gl\u00fcck, R. (2019) Semi-inversion of conditional constructor term rewriting systems. In Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8\u201310, 2019, Revised Selected Papers. Springer, pp. 243\u2013259.","DOI":"10.1007\/978-3-030-45260-5_15"},{"key":"S0956796823000126_ref9","doi-asserted-by":"crossref","unstructured":"Axelsen, H. B. , Gl\u00fcck, R. & Yokoyama, T. (2007) Reversible machine code and its abstract processor architecture. In Computer Science \u2013 Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3\u20137, 2007, Proceedings. Springer, pp. 56\u201369.","DOI":"10.1007\/978-3-540-74510-5_9"},{"key":"S0956796823000126_ref60","doi-asserted-by":"crossref","unstructured":"Mogensen, T. \u00c6. (2008) Semi-inversion of functional parameters. In Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2008, San Francisco, California, USA, January 7\u20138, 2008. ACM, pp. 21\u201329.","DOI":"10.1145\/1328408.1328413"},{"key":"S0956796823000126_ref26","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1017\/S0956796800000058","article-title":"A partial evaluator for the untyped lambda-calculus","volume":"1","author":"Gomard","year":"1991","journal-title":"J. Funct. Program."},{"key":"S0956796823000126_ref44","unstructured":"Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd ed. Graduate Texts in Matheematics, vol. 5. Springer."},{"key":"S0956796823000126_ref6","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. , Chapman, J. & Uustalu, T. (2010) Monads need not be endofunctors. In Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20\u201328, 2010. Proceedings. Springer, pp. 297\u2013311.","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"S0956796823000126_ref20","unstructured":"Frank, M. P. (1997) The R programming language and compiler. MIT Reversible Computing Project Memo #M8, MIT AI Lab. Available on: https:\/\/github.com\/mikepfrank\/Rlang-compiler\/blob\/master\/docs\/MIT-RCP-MemoM8-RProgLang.pdf."},{"key":"S0956796823000126_ref50","doi-asserted-by":"crossref","unstructured":"Matsuda, K. & Wang, M. (2015a) Applicative bidirectional programming with lenses. In ICFP. ACM, pp. 62\u201374.","DOI":"10.1145\/2858949.2784750"},{"key":"S0956796823000126_ref52","doi-asserted-by":"crossref","first-page":"e15","DOI":"10.1017\/S0956796818000096","article-title":"Applicative bidirectional programming: Mixing lenses and semantic bidirectionalization","volume":"28","author":"Matsuda","year":"2018","journal-title":"J. Funct. Program."},{"volume-title":"Qualified Types: Theory and Practice","year":"1995","author":"Jones","key":"S0956796823000126_ref32"},{"key":"S0956796823000126_ref83","doi-asserted-by":"crossref","unstructured":"Wadler, P. (1993) A taste of linear logic. In Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS\u201993, Gdansk, Poland, August 30\u2013September 3, 1993, Proceedings. Springer, pp. 185\u2013210.","DOI":"10.1007\/3-540-57182-5_12"},{"key":"S0956796823000126_ref29","doi-asserted-by":"crossref","unstructured":"Hu, Z. , Mu, S. & Takeichi, M. (2004) A programmable editor for developing structured documents based on bidirectional transformations. In Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004, Verona, Italy, August 24\u201325, 2004. ACM, pp. 178\u2013189.","DOI":"10.1145\/1014007.1014025"},{"key":"S0956796823000126_ref65","doi-asserted-by":"crossref","unstructured":"Mu, S. , Hu, Z. & Takeichi, M. (2004b) An injective language for reversible computation. In Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12\u201314, 2004, Proceedings. Springer, pp. 289\u2013313.","DOI":"10.1007\/978-3-540-27764-4_16"},{"key":"S0956796823000126_ref78","doi-asserted-by":"crossref","unstructured":"Srivastava, S. , Gulwani, S. , Chaudhuri, S. & Foster, J. S. (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\u20138, 2011. ACM, pp. 492\u2013503.","DOI":"10.1145\/1993498.1993557"},{"key":"S0956796823000126_ref27","doi-asserted-by":"crossref","unstructured":"Hidaka, S. , Hu, Z. , Inaba, K. , Kato, H. , Matsuda, K. & Nakano, K. (2010) Bidirectionalizing graph transformations. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27\u201329, 2010. ACM, pp. 205\u2013216.","DOI":"10.1145\/1932681.1863573"},{"key":"S0956796823000126_ref89","first-page":"5","article-title":"Optimizing reversible simulation of injective functions","volume":"18","author":"Yokoyama","year":"2012","journal-title":"Multiple-Valued Logic Soft Comput."},{"key":"S0956796823000126_ref61","doi-asserted-by":"crossref","unstructured":"Moggi, E. (1998) Functor categories and two-level languages. In Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS\u201998, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201998, Lisbon, Portugal, March 28\u2013April 4, 1998, Proceedings. Springer, pp. 211\u2013225.","DOI":"10.1007\/BFb0053552"},{"key":"S0956796823000126_ref69","doi-asserted-by":"crossref","unstructured":"Ohori, A. (ed) (2003) Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27\u201329, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2895. Springer.","DOI":"10.1007\/b94290"},{"key":"S0956796823000126_ref10","doi-asserted-by":"crossref","unstructured":"Baker, H. G. (1992) NREVERSAL of fortune - the thermodynamics of garbage collection. In Memory Management, International Workshop IWMM 92, St. Malo, France, September 17\u201319, 1992, Proceedings. Springer, pp. 507\u2013524.","DOI":"10.1007\/BFb0017210"},{"key":"S0956796823000126_ref43","unstructured":"Lutz, C. (1986) Janus: A time-reversible language. Letter to R. Landauer. Available on: http:\/\/tetsuo.jp\/ref\/janus.pdf."},{"key":"S0956796823000126_ref30","doi-asserted-by":"crossref","unstructured":"Jacobsen, P. A. H. , Kaarsgaard, R. & Thomsen, M. K. (2018) CoreFun: A typed functional reversible core language. In Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12\u201314, 2018, Proceedings. Springer, pp. 304\u2013321.","DOI":"10.1007\/978-3-319-99498-7_21"},{"key":"S0956796823000126_ref90","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1109\/TIT.1977.1055714","article-title":"A universal algorithm for sequential data compression","volume":"23","author":"Ziv","year":"1977","journal-title":"IEEE Trans. Inf. Theory"},{"key":"S0956796823000126_ref70","first-page":"300","volume-title":"In MPC","author":"Paterson","year":"2012"},{"key":"S0956796823000126_ref25","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/j.ipl.2019.03.002","article-title":"Constructing a binary tree from its traversals by reversible recursion and iteration","volume":"147","author":"Gl\u00fcck","year":"2019","journal-title":"Inf. Process. Lett."},{"key":"S0956796823000126_ref88","first-page":"14","volume-title":"In RC","author":"Yokoyama","year":"2011"},{"key":"S0956796823000126_ref48","doi-asserted-by":"crossref","unstructured":"Matsuda, K. , Mu, S.-C. , Hu, Z. & Takeichi, M. (2010) A grammar-based approach to invertible programs. In ESOP. Springer, pp. 448\u2013467.","DOI":"10.1007\/978-3-642-11957-6_24"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796823000126","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,26]],"date-time":"2024-01-26T08:21:05Z","timestamp":1706257265000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796823000126\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":90,"alternative-id":["S0956796823000126"],"URL":"https:\/\/doi.org\/10.1017\/s0956796823000126","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e2"}}