Abstract
Tail recursive functions allow for a wider range of optimisations than general recursive functions. For this reason, much research has gone into the transformation and optimisation of this family of functions, in particular those written in continuation passing style (CPS).
Though the CPS transformation, capable of transforming any recursive function to an equivalent tail recursive one, is deeply problematic in the context of reversible programming (as it relies on troublesome features such as higher-order functions), we argue that relaxing (local) reversibility to (global) invertibility drastically improves the situation. On this basis, we present an algorithm for tail recursion conversion specifically for invertible functions. The key insight is that functions introduced by program transformations that preserve invertibility, need only be invertible in the context in which the functions subject of transformation calls them. We show how a bespoke data type, corresponding to such a context, can be used to transform invertible recursive functions into a pair of tail recursive function acting on this context, in a way where calls are highlighted, and from which a tail recursive inverse can be straightforwardly extracted.
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
References
Abramov, S., Robert, G.: The universal resolving algorithm and its correctness: inverse computation in a functional language. Sci. Comput. Program. 43(23), 193–229 (2002). https://doi.org/10.1016/S0167-6423(02)00023-0. Mathematics of Program Construction (MPC 2000)
Axelsen, H.B.: Clean translation of an imperative reversible programming language. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 144–163. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19861-8_9
Glück, R., Kaarsgaard, R.: A categorical foundation for structured reversible flowchart languages: soundness and adequacy. Logical Methods Comput. Sci. 14(3) (2018). https://doi.org/10.1016/j.entcs.2018.03.021
Glück, R., Kaarsgaard, R., Yokoyama, T.: From reversible programming languages to reversible metalanguages. Theoret. Comput. Sci. 920, 46–63 (2022). https://doi.org/10.1016/j.tcs.2022.02.024
Glück, R., Kawabe, M.: A program inverter for a functional language with equality and constructors. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 246–264. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40018-9_17
Glück, R., Kawabe, M.: Derivation of deterministic inverse programs based on LR parsing. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 291–306. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24754-8_21
Glück, R., Kawabe, M.: A method for automatic program inversion based on LR(0) parsing. Fund. Inform. 66(4), 367–395 (2005)
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
James, R.P., Sabry, A.: Theseus: a high level language for reversible computing (2014). Work in progress paper at RC 2014. https://www.cs.indiana.edu/sabry/papers/theseus.pdf
Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K.: Branching execution symmetry in Jeopardy by available implicit arguments analysis. In: Rutle, A. (ed.) Proceedings of 34th Norwegian ICT Conference for Research and Education, NIKT 2022. No. 1 (2022)
Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K.: Jeopardy: an invertible functional programming language (2022). https://doi.org/10.48550/ARXIV.2209.02422. Work-in-progress paper presented at 34th Symposium on Implementation and Application of Functional Languages
Lutz, C., Derby, H.: Janus: a time-reversible language. A letter to R. Landauer (1986). http://tetsuo.jp/ref/janus.pdf
Matsuda, K., Mu, S.-C., Hu, Z., Takeichi, M.: A grammar-based approach to invertible programs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 448–467. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_24
McCarthy, J.: The inversion of functions defined by Turing machines. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies. Annals of Mathematics Studies, Princeton University Press, Princeton (1956)
Mogensen, T.Æ.: Semi-inversion of guarded equations. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 189–204. Springer, Heidelberg (2005). https://doi.org/10.1007/11561347_14
Mogensen, T.Æ.: Semi-inversion of functional parameters. In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 2008, pp. 21–29. ACM (2008). https://doi.org/10.1145/1328408.1328413
Nishida, N., Vidal, G.: Conversion to tail recursion in term rewriting. J. Logic Algebraic Program. 83(1), 53–63 (2014). https://doi.org/10.1016/j.jlap.2013.07.001
Nishida, N., Vidal, G.: Program inversion for tail recursive functions. In: 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, vol. 10, pp. 283–298 (2011)
Romanenko, A.: The generation of inverse functions in REFAL. In: Proceedings of the International Workshop on Partial Evaluation and Mixed Computation, vol. 427. North-Holland, Amsterdam (1988). https://cir.nii.ac.jp/crid/1571135649260521472
Thomsen, M.K., Axelsen, H.B.: Interpretation and programming of the reversible functional language. In: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, pp. 8:1–8:13. ACM (2016). https://doi.org/10.1145/2897336.2897345
Thomsen, M.K., Axelsen, H.B., Glück, R.: A reversible processor architecture and its reversible logic design. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 30–42. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_3
Vieri, C.J.: Reversible computer engineering and architecture. Ph.D. thesis, MIT, EECS (1999)
Yokoyama, T., Axelsen, H.B., Glück, R.: Reversible flowchart languages and the structured reversible program theorem. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 258–270. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_22
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., 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). https://doi.org/10.1145/1244381.1244404
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Kristensen, J.T., Kaarsgaard, R., Thomsen, M.K. (2023). Tail Recursion Transformation for Invertible Functions. In: Kutrib, M., Meyer, U. (eds) Reversible Computation. RC 2023. Lecture Notes in Computer Science, vol 13960. Springer, Cham. https://doi.org/10.1007/978-3-031-38100-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-031-38100-3_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-38099-0
Online ISBN: 978-3-031-38100-3
eBook Packages: Computer ScienceComputer Science (R0)