[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Jeopardy: An Invertible Functional Programming Language

  • Conference paper
  • First Online:
Reversible Computation (RC 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14680))

Included in the following conference series:

  • 181 Accesses

Abstract

Reversible programming languages guarantee that their programs are invertible at the cost of restricting the permissible operations to those which are locally invertible. However, writing programs in a reversible style can be cumbersome, and may produce significantly different implementations than the conventional – even when the implemented algorithm is, in fact, invertible. We introduce Jeopardy, a functional programming language that guarantees global program invertibility without imposing local invertibility. In particular, Jeopardy allows the limited use of uninvertible – and even nondeterministic – operations, provided that they are used in a way that can be statically determined to be globally invertible. To this end, we outline an implicitly available arguments analysis and further approaches that can give a partial static guarantee to the (generally difficult) problem of guaranteeing invertibility.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Similar content being viewed by others

Notes

  1. 1.

    Often (as in Janus) local invertibility only guarantees invertibility of partial functions. This comes from the fact that control structures (like conditional and loops) require assertion of specific values.

  2. 2.

    It will never be possible to write an invertible implementation of the Fibonacci function that does not include something extra in its output, since the first couple of outputs has to be \(\texttt {[suc [zero]]}\) for two different inputs.

  3. 3.

    The problem of extending an invertible (or even a reversible) programming language with (real) higher order functions will be worthy of its own paper.

References

  1. Abramov, S., Glück, R.: The universal resolving algorithm and its correctness: inverse computation in a functional language. Sci. Comput. Program. 43(2–3), 193–229 (2002)

    Article  MathSciNet  Google Scholar 

  2. Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. 17(6), 525–532 (1973)

    Article  MathSciNet  Google Scholar 

  3. Carette, J., Heunen, C., Kaarsgaard, R., Sabry, A.: With a few square roots, quantum computing is as easy as Pi. Proc. ACM Program. Lang. 8(POPL), 546–574 (2024)

    Google Scholar 

  4. Dijkstra, E.W.: Program Inversion, pp. 54–57. Springer, Heidelberg (1979). https://doi.org/10.1007/BFb0014657

    Book  Google Scholar 

  5. Futamura, Y.: Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds.) RIMS Symposia on Software Science and Engineering. LNCS, vol. 147, pp. 1–35. Springer, Heidelberg (1983). https://doi.org/10.1007/3-540-11980-9_13

    Chapter  Google Scholar 

  6. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_26

    Chapter  Google Scholar 

  7. Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)

    Article  MathSciNet  Google Scholar 

  8. Glück, R., Yokoyama, T.: Reversible computing from a programming language perspective. Theor. Comput. Sci. 953, 113429 (2023)

    Article  MathSciNet  Google Scholar 

  9. Heunen, C., Kaarsgaard, R.: Bennett and Stinespring, together at last. In: Proceedings 18th International Conference on Quantum Physics and Logic (QPL 2021). Electronic Proceedings in Theoretical Computer Science, vol. 343, pp. 102–118. OPA (2021)

    Google Scholar 

  10. Heunen, C., Kaarsgaard, R.: Quantum information effects. Proc. ACM Program. Lang. 6(POPL) (2022)

    Google Scholar 

  11. Heunen, C., Kaarsgaard, R., Karvonen, M.: Reversible effects as inverse arrows. In: Mathematical Foundations of Programming Semantics XXXIV, Proceedings. Electronic Notes in Theoretical Computer Science, vol. 341, pp. 179–199. Elsevier (2018)

    Google Scholar 

  12. Huffman, D.A.: Canonical forms for information-lossless finite-state logical machines. IRE Trans. Inf. Theory 5(5), 41–59 (1959)

    Article  Google Scholar 

  13. Jacobsen, P.A.H., Kaarsgaard, R., Thomsen, M.K.: \(\sf CoreFun\): a typed functional reversible core language. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 304–321. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99498-7_21

    Chapter  Google Scholar 

  14. James, R.P., Sabry, A.: Theseus: a high level language for reversible computing (2014). Work in progress paper at RC 2014. www.cs.indiana.edu/~sabry/papers/theseus.pdf

  15. Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K.: Branching execution symmetry in jeopardy by available implicit arguments analysis. In: Norwegian Informatics Conference, NIK, vol. 1. 34th Norwegian ICT Conference for Research and Education, NIKT 2022 (2022, to appear)

    Google Scholar 

  16. Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K.: Tail recursion transformation for invertible functions. In: Kutrib, M., Meyer, U. (eds.) RC 2023. LNCS, vol. 13960, pp. 73–88. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38100-3_6

    Chapter  Google Scholar 

  17. Landauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5(3), 261–269 (1961)

    Article  MathSciNet  Google Scholar 

  18. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_16

    Chapter  Google Scholar 

  19. Laursen, J.S., Schultz, U.P., Ellekilde, L.P.: Automatic error recovery in robot assembly operations using reverse execution. In: 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1785–1792. IEEE (2015)

    Google Scholar 

  20. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Symposium on Principles of Programming Languages, POPL 2001, pp. 81–92. ACM (2001)

    Google Scholar 

  21. Lutz, C., Derby, H.: Janus: a time-reversible language. A letter to R. Landauer (1986). http://tetsuo.jp/ref/janus.pdf

  22. Matsuda, K., Wang, M.: SPARCL: a language for partially invertible computation. J. Funct. Program. 34, e2 (2024). https://doi.org/10.1017/S0956796823000126

    Article  MathSciNet  Google Scholar 

  23. McCarthy, J.: The inversion of functions defined by turing machines. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies. Princeton University Press (1956)

    Google Scholar 

  24. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2015)

    Google Scholar 

  25. Schordan, M., Jefferson, D., Barnes, P., Oppelstrup, T., Quinlan, D.: Reverse code generation for parallel discrete event simulation. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 95–110. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_6

    Chapter  Google Scholar 

  26. Schordan, M., Oppelstrup, T., Thomsen, M.K., Glück, R.: Reversible languages and incremental state saving in optimistic parallel discrete event simulation. In: Ulidowski, I., Lanese, I., Schultz, U.P., Ferreira, C. (eds.) RC 2020. LNCS, vol. 12070, pp. 187–207. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-47361-7_9

    Chapter  Google Scholar 

  27. Schultz, U., Bordignon, M., Stoy, K.: Robust and reversible execution of self-reconfiguration sequences. Robotica 29(1), 35–57 (2011)

    Article  Google Scholar 

  28. Thomsen, M.K., Axelsen, H.B.: Interpretation and programming of the reversible functional language. In: Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, pp. 8:1–8:13. ACM (2016)

    Google Scholar 

  29. Thomsen, M.K., Kaarsgaard, R., Soeken, M.: Ricercar: a language for describing and rewriting reversible circuits with ancillae and its permutation semantics. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 200–215. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_13

    Chapter  Google Scholar 

  30. Voichick, F., Li, L., Rand, R., Hicks, M.: Qunity: a unified language for quantum and classical computing. Proc. ACM Program. Lang. 7(POPL), 921–951 (2023)

    Google Scholar 

  31. Wadler, P.: Linear types can change the world! In: IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 347–359. North Holland (1990)

    Google Scholar 

  32. Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a reversible functional language. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 14–29. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_2

    Chapter  Google Scholar 

  33. Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: Partial Evaluation and Program Manipulation, PEPM 2007, pp. 144–153. ACM (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, University of Oslo, Oslo, Norway

    Joachim Tilsted Kristensen & Michael Kirkedal Thomsen

  2. University of University of Southern Denmark, Odense, Denmark

    Robin Kaarsgaard

  3. Department of Computer Science, University of Copenhagen, Copenhagen, Denmark

    Michael Kirkedal Thomsen

Authors
  1. Joachim Tilsted Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robin Kaarsgaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Kirkedal Thomsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joachim Tilsted Kristensen .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Copenhagen, Copenhagen Ø, Denmark

    Torben Ægidius Mogensen

  2. Faculty of Mathematics and Computer Science, Nicolaus Copernicus University, Toruń, Poland

    Łukasz Mikulski

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K. (2024). Jeopardy: An Invertible Functional Programming Language. In: Mogensen, T.Æ., Mikulski, Ł. (eds) Reversible Computation. RC 2024. Lecture Notes in Computer Science, vol 14680. Springer, Cham. https://doi.org/10.1007/978-3-031-62076-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-62076-8_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-62075-1

  • Online ISBN: 978-3-031-62076-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation