Getting There and Back Again

• Autorzy: Danvy Olivier

Identyfikatory

DOI

10.3233/FI-222106

• Języki publikacji: EN

Abstrakty

EN

"There and Back Again" (TABA) is a programming pattern where the recursive calls traverse one data structure and the subsequent returns traverse another. This article presents new TABA examples, refines existing ones, and formalizes both their control flow and their data flow using the Coq Proof Assistant. Each formalization mechanizes a pen-and-paper proof, thus making it easier to "get" TABA. In addition, this article identifies and illustrates a tail-recursive variant of TABA, There and Forth Again (TAFA) that does not come back but goes forth instead with more tail calls.

Słowa kluczowe

EN

continuations; Coq Proof Assistant; defunctionalization and refunctionalization; eta redexes; lambda-lifting and lambda-dropping; lightweight fusion and lightweight fission; list processing; recursion pattern; symbolic convolutions; TABA; There and Forth Again (TAFA)

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 185, nr 2
• Strony: 185--199
• Opis fizyczny: Bibliogr. 46 poz., tab.

Twórcy

autor

Danvy Olivier

• Yale-NUS College & School of Computing, National University of Singapore

Bibliografia

• [1] Danvy O, Goldberg M. There and back again. Fundamenta Informaticae, 2005. 66(4):397-413.
• [2] Danvy O, Millikin K. Refunctionalization at Work. Science of Computer Programming, 2009. 74(8):534-549. doi:10.1016/j.scico.2007.10.007.
• [3] Fernandes JP, Saraiva J. Tools and libraries to model and manipulate circular programs. In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2007). ACM Press, Nice, France, 2007 pp. 102-111. doi:10.1145/1244381.1244399.
• [4] Miranda-Perea F. Some Remarks on Type Systems for Course-of-value Recursion. Electronic Notes in Theoretical Computer Science, 2009. 247:103-121. doi:10.1016/j.entcs.2009.07.051.
• [5] Sergey I. Programs and Proofs: Mechanizing Mathematics with Dependent Types. JetBrains/SPbSU Summer School, 2014. https://ilyasergey.net/pnp-2014/.
• [6] Shivers O, Fisher D. Multi-return function call. Journal of Functional Programming, 2006. 4-5(16):547-582. doi:10.1017/S0956796806006009.
• [7] Morihatao A, Kakehi K, Hu Z, Takeichi M. Swapping Arguments and Results of Recursive Functions. In:Mathematics of Program Construction, 8th International Conference, MPC 2006, number 4014 in Lecture Notes in Computer Science. Springer, Kuressaare, Estonia, 2006 pp. 379-396. doi:10.1007/11783596 22.
• [8] Nguyen K. Langage de combinateurs pour XML: Conception, Typage, et Implantation. PhD thesis, LRI, Universit´e Paris Sud, Orsay, France, 2008. In English.
• [9] Foner K. ‘There and Back Again’ and What Happened After. In: Compose Conference, http://www.composeconference.org/2016/program/. 2016 https://www.youtube.com/watch?v=u_OsUlwkmBQ, URL http://www.composeconference.org/2016/program/.
• [10] Hemann J, Friedman DP. Deriving Pure, Naturally-Recursive Operations for Processing Tail-Aligned Lists. In: Scheme and Functional Programming Workshop, Co-located with ICFP 2016. Nara, Japan, 2016 http://www.schemeworkshop.org/2016/.
• [11] Amin N, Rompf T. Collapsing Towers of Interpreters. Proceedings of the ACM on Programming Languages, 2018. 2(POPL):52:1-52:33. doi:10.1145/3158140.
• [12] Brunel A, Mazza D, Pagani M. Backpropagation in the simply typed lambda-calculus with linear negation. Proceedings of the ACM on Programming Languages, 2019. 4(POPL):64:1-64:27. doi:10.1145/3158140.
• [13] Wang F, Decker J, Wu X, Essertel G, Rompf T. Backpropagation with Callbacks: Foundations for Efficient and Expressive Differentiable Programming. In: Advances in Neural Information Processing Systems 31, pp. 10180-10191. Curran Associates, Inc., 2018. ID:53989384.
• [14] Wang F, Zheng D, Decker JM, Wu X, Essertel GM, Rompf T. Demystifying differentiable programming: shift/reset the penultimate backpropagator. Proceedings of the ACM on Programming Languages, 2019.3(ICFP):96:1-96:31. doi:10.1145/3341700.
• [15] Filliâtre JC. Two puzzles from Danvy and Goldberg’s “There and back again”. 2013. http://toccata.lri.fr/gallery/there_and_back_again.en.html.
• [16] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development. Springer, 2004. ISBN-10:3540208542, 13:978-3540208549.
• [17] Bird R, Wadler P. Introduction to Functional Programming. Prentice-Hall International, London, UK, 1stedition, 1988. ISBN-10:0134841972, 13:978-0134841977.
• [18] Burstall RM, Landin PJ. Programs and their proofs: An algebraic approach. In: Meltzer B, Michie D (eds.), Machine Intelligence, volume 4. Edinburgh University Press, 1969 pp. 17-43. ID:60873698.
• [19] Manna Z. Mathematical Theory of Computation. McGraw-Hill, 1974. ISBN-10:0070854661, 13:978-0070854666.
• [20] Nolan C. Tenet. Warner Bros. Pictures, 2020.
• [21] Dijkstra EW. Recursive Programming. In: Rosen S (ed.), Programming Systems and Languages, chapter 3C, pp. 221-227. McGraw-Hill, New York, 1960. doi:10.1007/BF01386223.
• [22] Ohori A, Sasano I. Lightweight fusion by fixed point promotion. In: Proceedings of the Thirty-Fourth Annual ACM Symposium on Principles of Programming Languages, SIGPLAN Notices, Vol. 42, No. 1. ACM Press, Nice, France, 2007 pp. 143-154. doi:10.1145/1190215.1190241.
• [23] Danvy O, Schultz UP. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. Theoretical Computer Science, 2000. 248(1-2):243-287. doi:10.1016/S0304-3975(00)00054-2
• [24] Danvy O, Goldberg M. There and back again. In: Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming (ICFP’02), SIGPLAN Notices, Vol. 37, No. 9. ACM Press, Pittsburgh, Pennsylvania, 2002 pp. 230-234. doi:10.1145/583852.581500.
• [25] Danvy O, Filinski A. Abstracting Control. In: Proceedings of the 1990 ACM Conference on Lisp and Functional Programming. ACM Press, Nice, France, 1990 pp. 151-160. doi:10.1145/91556.91622.
• [26] Asai K. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation, 2009. 22(3):275-291. doi:10.1007/s10990-009-9049-5.
• [27] Materzok M, Biernacki D. Subtyping Delimited Continuations. In: Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages. ACM Press, Portland, Oregon, 1994 pp. 446-457. doi:10.1145/174675.178047.
• [28] de Bruijn NG. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 1972. 34(5):381-392. doi:10.1016/1385-7258(72)90034-0.
• [29] Dybvig RK. The development of Chez Scheme. In: Proceedings of the 2006 ACM SIGPLAN International Conference on Functional Programming (ICFP’06). Invited talk. ACM Press, Portland, Oregon, 2006 pp. 1-12. doi:10.1145/1159803.1159805.
• [30] Barron DW, Strachey C. Programming. In: Fox L (ed.), Advances in Programming and Non-Numerical Computation, pp. 49-82. Pergammon Press, 1966. doi:10.1016/C2013-0-01911-1
• [31] Kidney DO. Typing TABA, 2020. URL https://doisinkidney.com/posts/2020-02-15-taba.html.
• [32] Peyton Jones SL. Personal communication at ICFP, Pittsburgh, Pennsylvania, 2002.
• [33] Danvy O. Back to Direct Style. Science of Computer Programming, 1994. 22(3):183-195. doi:10.1016/0167-6423(94)00003-4.
• [34] Danvy O. Sur un Exemple de Patrick Greussay. Research Report BRICS RS-04-41, Department of Computer Science, Aarhus University, Aarhus, Denmark, 2004. doi:10.7146/brics.v11i41.21866.
• [35] Danvy O, Lawall JL. Back to Direct Style II: First-Class Continuations. In: Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1. ACM Press, San Francisco, California, 1992 pp. 299-310. doi:10.1145/141471.141564.
• [36] Felleisen M, Friedman DP. Control Operators, the SECD Machine, and the λ-Calculus. In: Wirsing M (ed.), Formal Description of Programming Concepts III, pp. 193-217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986. ID:57760323.
• [37] Filinski A. Representing Monads. In: Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages. ACM Press, Portland, Oregon, 1994 pp. 446-457. doi:10.1145/ 174675.178047.
• [38] Johnsson T. Lambda Lifting: Transforming Programs to Recursive Equations. In: Functional Programming Languages and Computer Architecture, number 201 in Lecture Notes in Computer Science. Springer-Verlag, Nancy, France, 1985 pp. 190-203. doi:10.1007/3-540-15975-4 37.
• [39] Landin PJ. The Mechanical Evaluation of Expressions. The Computer Journal, 1964. 6(4):308-320. doi:10.1093/comjnl/6.4.308
• [40] Peyton Jones SL. The Implementation of Functional Programming Languages. Prentice Hall International Series in Computer Science. Prentice-Hall International, 1987. ISBN-13:978-0134533339, 10:013453333X.
• [41] Reynolds JC. Definitional Interpreters for Higher-Order Programming Languages. In: Proceedings of 25th ACM National Conference. Boston, Massachusetts, 1972 pp. 717-740. Reprinted in Higher-Order and Symbolic Computation 11(4):363-397, 1998, with a foreword [42]. doi:10.1145/800194.805852.
• [42] Reynolds JC. Definitional Interpreters Revisited. Higher-Order and Symbolic Computation, 1998. 11(4):355-361. doi:10.1023/A:1010075320153.
• [43] Schmidt DA. State-Transition Machines for Lambda-Calculus Expressions. Higher-Order and Symbolic Computation, 2007. 20(3):319-332. Journal version of [45], with a foreword [44]. doi:10.1007/s10990-007-9012-2.
• [44] Schmidt DA. State-Transition Machines, Revisited. Higher-Order and Symbolic Computation, 2007. 20(3):319-332. doi:10.1007/s10990-007-9017-x.
• [45] Schmidt DA. State transition machines for lambda calculus expressions. In: Semantics-Directed Compiler Generation, number 94 in Lecture Notes in Computer Science. Springer-Verlag, Aarhus, Denmark, 1980 pp. 415-440. doi:10.1007/3-540-10250-7 32.
• [46] Strachey C. Handwritten Notes, 1961. Archive of working papers and correspondence. Bodleian Library, Oxford, Catalogue no. MS. Eng. misc. b.267

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL).