Abstract
This paper presents \(\mathsf {CoreFun}\), a typed reversible functional language, which seeks to reduce typed reversible functional programming to its essentials. We present a complete formal definition of the language, including its formal semantics and type system, the latter of which is based on a combined reasoning logical system of unrestricted and relevantly typed terms, and allows special support for ancillary (read-only) variables through its unrestricted fragment. We show how, in many cases, the type system provides the possibility to statically check for the reversibility of programs. Finally, we detail how higher-level language features such as variants and type classes may be incorporated into \(\mathsf {CoreFun}\) as syntactic sugar, such that \(\mathsf {CoreFun}\) may be used as a core language for a reversible functional language in a more modern style.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A rank-1 polymorphic system may not instantiate type variables with polymorphic types.
References
Anderson, A.R., Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, vol. 1. Princeton University Press, Princeton (1975)
Axelsen, H.B., Glück, R.: On reversible turing machines and their function universality. Acta Informatica 53(5), 509–543 (2016)
Dunn, J.M., Restall, G.: Relevance logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 6, pp. 1–192. Springer, Dordrecht (2002). https://doi.org/10.1007/978-94-017-0460-1_1
Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)
Glück, R., Kaarsgaard, R.: A categorical foundation for structured reversible flowchart languages. In: Silva, A. (ed.) Mathematical Foundations of Programming Semantics (MFPS XXXIII). Electronic Notes in Theoretical Computer Science, vol. 336, pp. 155–171. Elsevier (2018)
Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Conference on Programming Language Design and Implementation, PLDI, PLDI 2013, pp. 333–342. ACM (2013)
Huffman, D.A.: Canonical forms for information-lossless finite-state logical machines. IRE Trans. Inf. Theory 5(5), 41–59 (1959)
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
Landauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5(3), 183–191 (1961)
Lecerf, Y.: Machines de Turing réversibles. Comptes Rendus Hebdomadaires des Séances de l’Académie des Sciences 257, 2597–2600 (1963)
Lutz, C., Derby, H.: Janus: a time-reversible language. A letter to R. Landauer (1986). http://tetsuo.jp/ref/janus.pdf
Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Polakow, J.: Ordered Linear Logic and Applications. Ph.D. thesis. Carnegie Mellon University (2001)
Sabry, A., Valiron, B., Vizzotto, J.K.: From Symmetric pattern-matching to quantum control. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 348–364. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_19
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
Schultz, U.P., Laursen, J.S., Ellekilde, L.-P., Axelsen, H.B.: Towards a domain-specific language for reversible assembly sequences. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 111–126. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_7
Thomsen, M.K.: A functional language for describing reversible logic. In: Specification & Design Languages, FDL 2012, pp. 135–142. IEEE (2012)
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)
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)
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
Yokoyama, T., Axelsen, H.B., GlĂĽck, R.: Fundamentals of reversible flowchart languages. Theor. Comput. Sci. (2015) (in Press), https://doi.org/10.1016/j.tcs.2015.07.046
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)
Acknowledgements
This work was partly supported by the European COST Action IC 1405: Reversible Computation—Extending Horizons of Computing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Jacobsen, P.A.H., Kaarsgaard, R., Thomsen, M.K. (2018). \(\mathsf {CoreFun}\): A Typed Functional Reversible Core Language. In: Kari, J., Ulidowski, I. (eds) Reversible Computation. RC 2018. Lecture Notes in Computer Science(), vol 11106. Springer, Cham. https://doi.org/10.1007/978-3-319-99498-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-99498-7_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99497-0
Online ISBN: 978-3-319-99498-7
eBook Packages: Computer ScienceComputer Science (R0)