Document Open Access Logo

Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

Authors Kostia Chardonnet, Louis Lemonnier , Benoît Valiron

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2024.19.pdf
  • Filesize: 0.87 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Reversible programming
  • functional programming
  • Computability
  • Denotational Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.

Cite As Get BibTex

Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSCD.2024.19

Author Details

Kostia Chardonnet
  • Department of Computer Science and Engineering, University of Bologna, Italy
Louis Lemonnier
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France
Benoît Valiron
  • Université Paris-Saclay, CNRS, CentraleSupélec, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Funding

This work has been partially funded by the French National Research Agency (ANR) by the projects ANR-21-CE48-0019, ANR-19-CE48-0014, ANR-22-CE47-0012, and within the framework of "Plan France 2030", under the project ANR-22-PETQ-0007, ANR-22-PNCQ-0001.
  • Chardonnet, Kostia: is partially supported by the MIUR FARE project CAFFEINE, "Compositional and Effectful Program Distances", R20LW7EJ7L.

Acknowledgements

The authors thank Vladimir Zamdzhiev for his expert insight on specific parts of the denotational semantics.

References

  1. Holger Bock Axelsen and Robert Glück. A simple and efficient universal reversible turing machine. In Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, editors, Language and Automata Theory and Applications, pages 117-128, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-21254-3_8.
  2. Holger Bock Axelsen and Robin Kaarsgaard. Join inverse categories as models of reversible recursion. In Bart Jacobs and Christof Löding, editors, Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'16), volume 9634 of Lecture Notes in Computer Science, pages 73-90, Eindhoven, The Netherlands, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49630-5_5.
  3. Henk Barendregt. ’the lambda calculus: its syntax and semantics’. Studies in logic and the foundations of Mathematics, 1984. Google Scholar
  4. Charles H Bennett. Logical reversibility of computation. IBM Journal of Research and Development, 17(6):525-532, 1973. URL: https://doi.org/10.1147/rd.176.0525.
  5. Antoine Bérut, Artak Arakelyan, Artyom Petrosyan, Sergio Ciliberto, Raoul Dillenschneider, and Eric Lutz. Experimental verification of landauer’s principle linking information and thermodynamics. Nature, 483(7388):187-189, 2012. Google Scholar
  6. Kostia Chardonnet. Towards a Curry-Howard Correspondence for Quantum Computation. Theses, Université Paris-Saclay, January 2023. URL: https://theses.hal.science/tel-03959403.
  7. Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Categorical semantics of reversible pattern-matching. Electronic Proceedings in Theoretical Computer Science, 351:18-33, December 2021. URL: https://doi.org/10.4204/eptcs.351.2.
  8. Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard correspondence for linear, reversible computation. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.13.
  9. J. Robin B. Cockett and Stephen Lack. Restriction categories I: Categories of partial maps. Theoretical Computer Science, 270(1):223-259, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00382-0.
  10. J. Robin B. Cockett and Stephen Lack. Restriction categories ii: partial map classification. Theoretical Computer Science, 294(1):61-102, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00245-6.
  11. Robin Cockett and Stephen Lack. Restriction categories III: Colimits, partial limits and extensivity. Mathematical Structures in Computer Science, 17(4):775-817, 2007. URL: https://doi.org/10.1017/S0960129507006056.
  12. M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, 2004. URL: https://books.google.co.uk/books?id=rsIAmbc2cIoC.
  13. Brett Gordon Giles. An Investigation of Some Theoretical Aspects of Reversible Computing. PhD thesis, University of Calgary, 2014. URL: https://doi.org/10.11575/PRISM/24917.
  14. Robert Glück and Robin Kaarsgaard. A categorical foundation for structured reversible flowchart languages: Soundness and adequacy. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:16)2018.
  15. Robert Glück, Robin Kaarsgaard, and Tetsuo Yokoyama. Reversible programs have reversible semantics. In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II, volume 12233 of Lecture Notes in Computer Science, pages 413-427. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54997-8_26.
  16. Xiuzhan Guo. Products, Joins, Meets, and Ranges in Restriction Categories. PhD thesis, University of Calgary, 2012. URL: https://doi.org/10.11575/PRISM/4745.
  17. Chris Heunen, Robin Kaarsgaard, and Martti Karvonen. Reversible effects as inverse arrows. In Sam Staton, editor, Proceedings of the 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV), volume 341 of Electronic Notes in Theoretical Computer Science, pages 179-199, Dalhousie University, Halifax, Canada, 2018. Elsevier. URL: https://doi.org/10.1016/j.entcs.2018.11.009.
  18. Chris Heunen and Martti Karvonen. Reversible monadic computing. In Dan Ghica, editor, Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI), volume 319 of Electronic Notes in Theoretical Computer Science, pages 217-237, Nijmegen, The Netherlands, 2015. URL: https://doi.org/10.1016/j.entcs.2015.12.014.
  19. Petur Andrias Højgaard Jacobsen, Robin Kaarsgaard, and Michael Kirkedal Thomsen. CoreFun: A typed functional reversible core language. In Jarkko Kari and Irek Ulidowski, editors, Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 304-321. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_21.
  20. Rosham P. James and Amr Sabry. Theseus: A high-level language for reversible computing. Draft, available at https://legacy.cs.indiana.edu/~sabry/papers/theseus.pdf, 2014.
  21. Xiaodong Jia, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. Commutative monads for probabilistic programming languages. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, June 2021. URL: https://doi.org/10.1109/lics52264.2021.9470611.
  22. Robin Kaarsgaard. Condition/decision duality and the internal logic of extensive restriction categories. In Barbara König, editor, Proceedings of the 35th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXV), volume 347 of Electronic Notes in Theoretical Computer Science, pages 179-202, London, UK, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.010.
  23. Robin Kaarsgaard. Inversion, iteration, and the art of dual wielding. In Michael Kirkedal Thomsen and Mathias Soeken, editors, Proceedings of the 11th International Conference on Reversible Computation (RC 2019), volume 11497 of Lecture Notes in Computer Science, pages 34-50, Lausanne, Switzerland, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-21500-2_3.
  24. Robin Kaarsgaard, Holger Bock Axelsen, and Robert Glück. Join inverse categories and reversible recursion. Journal of Logical and Algebraic Methods in Programming, 87:33-50, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.08.003.
  25. Robin Kaarsgaard and Mathys Rennela. Join inverse rig categories for reversible functional programming, and beyond. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of Electronic Proceedings in Theoretical Computer Science, pages 152-167. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.351.10.
  26. Robin Kaarsgaard and Niccolò Veltri. En garde! unguarded iteration for reversible computation in the delay monad. In Graham Hutton, editor, Proceedings of the 13th International Conference on Mathematics of Program Construction (MPC 2019), volume 11825 of Lecture Notes in Computer Science, pages 366-384, Porto, Portugal, October 2019. Springer Verlag. URL: https://doi.org/10.1007/978-3-030-33636-3_13.
  27. J. Kastl. Inverse categories. In Algebraische Modelle, Kategorien und Gruppoide, Studien zur Algebra und ihre Anwendungen, Band 7, pages 51-60. Berlin, Akademie-Verlag, 1979. Google Scholar
  28. G.M Kelly. Tensor products in categories. Journal of Algebra, 2(1):15-37, 1965. URL: https://doi.org/10.1016/0021-8693(65)90022-0.
  29. Max Kelly. Basic concepts of enriched category theory, volume 64. CUP Archive, 1982. Google Scholar
  30. Rolf Landauer. Irreversibility and heat generation in the computing process. IBM Journal of Research and Development., 5(3):183-191, 1961. URL: https://doi.org/10.1147/rd.53.0183.
  31. Christopher Lutz. Janus: a time-reversible language. Letter to Rolf Landauer, posted online by Tetsuo Yokoyama on http://www.tetsuo.jp/ref/janus.html, 1986.
  32. Ian Mackie. The geometry of interaction machine. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'95, pages 198-208. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199483.
  33. J.-M. Maranda. Formal categories. Canadian Journal of Mathematics, 17:758-801, 1965. URL: https://doi.org/10.4153/CJM-1965-076-0.
  34. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2002. Google Scholar
  35. Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 647-658, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535879.
  36. Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From symmetric pattern-matching to quantum control. In Christel Baier and Ugo Dal Lago, editors, Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FOSSACS'18), volume 10803 of Lecture Notes in Computer Science, pages 348-364, Thessaloniki, Greece, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89366-2_19.
  37. Michael Kirkedal Thomsen and Holger Bock Axelsen. Interpretation and programming of the reversible functional language RFUN. In Ralf Lämmel, editor, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, Koblenz, Germany, September 14-16, 2015, pages 8:1-8:13. ACM, 2015. URL: https://doi.org/10.1145/2897336.2897345.
  38. Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück. Towards a reversible functional language. In Alexis De Vos and Robert Wille, editors, Revised Papers of the Third International Workshop on Reversible Computation (RC'11), volume 7165 of Lecture Notes in Computer Science, pages 14-29, Gent, Belgium, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-29517-1_2.
  39. Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück. Fundamentals of reversible flowchart languages. Theoretical Computer Science, 611:87-115, 2016. URL: https://doi.org/10.1016/j.tcs.2015.07.046.
  40. Tetsuo Yokoyama and Robert Glück. A reversible programming language and its invertible self-interpreter. In G. Ramalingam and Eelco Visser, editors, Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2007, Nice, France, January 15-16, 2007, pages 144-153, 2007. URL: https://doi.org/10.1145/1244381.1244404.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact