CoCaml: Functional Programming with Regular Coinductive Types

• Autorzy: Jeannin J.-B. , Kozen D. , Silva A.

Identyfikatory

DOI

10.3233/FI-2017-1473

• Języki publikacji: EN

Abstrakty

EN

Functional languages offer a high level of abstraction, which results in programs that are elegant and easy to understand. Central to the development of functional programming are inductive and coinductive types and associated programming constructs, such as pattern-matching. Whereas inductive types have a long tradition and are well supported in most languages, coinductive types are subject of more recent research and are less mainstream. We present CoCaml, a functional programming language extending OCaml, which allows us to define recursive functions on regular coinductive datatypes. These functions are defined like usual recursive functions, but parameterized by an equation solver. We present a full implementation of all the constructs and solvers and show how these can be used in a variety of examples, including operations on infinite lists, infinitary γ-terms, and p-adic numbers.

Słowa kluczowe

EN

functional programming; coinductive types; recursive types; coalgebra

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 3/4
• Strony: 347--377
• Opis fizyczny: Bibliogr. 50 poz., rys.

Twórcy

autor

Jeannin J.-B.

• Samsung Research America, USA

autor

Kozen D.

• Department of Computer Science, Cornell University, USA

autor

Silva A.

• Department of Computer Science, University College London, UK

Bibliografia

• [1] Adámek J, Milius S, Velebil J. Elgot Algebras, Log. Methods Comput. Sci., 2006; 2 (5:4) 1-31. doi: 10.2168/LMCS-2(5:4)2006.
• [2] Ancona D. Regular corecursion in Prolog, SAC (S. Ossowski, P. Lecca, Eds.), ACM, 2012, ISBN 978-1-4503-0857-1. doi: 10.1145/2245276.2232088.
• [3] Ancona D, Zucca E. Translating Corecursive Featherweight Java in Coinductive Logic Programming Co-LP 2012 - A workshop on Coinductive Logic Programming, 2012.
• [4] Ghani N, Hamana M, Uustalu T, Vene V. Representing cyclic structures as nested datatypes. Proc. of 7th Symp. on Trends in Functional Programming, TFP 2006 (H. Nilsson, Ed.), Univ. of Nottingham, 2006.
• [5] Jeannin JB, Kozen D, Silva A. Language Constructs for Non-Well-Founded Computation, 22nd European Symposium on Programming (ESOP 2013) (M. Felleisen, P. Gardner, Eds.), 7792, Springer. Rome, Italy, March 2013. doi: 10.1007/978-3-642-37036-6_4.
• [6] Adámek J, Lücke D, Milius S. Recursive Coalgebras of Finitary Functors, Theoretical Informatics and Applications, 2007; 41: 447-462. doi : 10.1051/ita:2007028.
• [7] Adámek J., Milius, S., Velebil, J.: Iterative algebras at work, Mathematical Structures in Comp. Sci., December 2006; 16 (6): 1085-1131. doi: 10.1017/S0960129506005706.
• [8] Ancona D., Zucca E. Corecursive Featherweight Java, FTfJP’012 - Formal Techniques for Java-like Programs, 2012. doi: 10.1145/2318202.2318205.
• [9] Capretta V, Uustalu T, Vene V. Corecursive Algebras: A Study of General Structured Corecursion, Formal Methods: Foundations and Applications, 12th Brazilian Symp. Formal Methods (SBMF 2009) (M. V. M. Oliveira, J. Woodcock, Eds.), 5902, Springer, Berlin, 2009. doi: 10.1007/978-3-642-10452-7_7.
• [10] Fegaras L, Sheard T. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space), Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL’96, ACM, New York, NY, USA, 1996. doi: 10.1145/237721.237792.
• [11] Simon L, Mallya A, Bansal A, Gupta G. Co-logic programming: Extending logic programming with coinduction, 34th Int. Colloq. Automata, Languages and Programming (ICALP 2007) (L. Arge, C. Cachin, T Jurdzinski, A. Tarlecki, Eds.), 4596, Springer, July 2007. doi: 10.1007/978-3-540-73420-8_42.
• [12] Turbak FA, Wells JB. Cycle Therapy: A Prescription for Fold and Unfold on Regular Trees, PPDP, ACM, 2001, ISBN: 1-58113-388-X. doi: 10.1145/773184.773200.
• [13] Widemann BT. Coalgebraic Semantics of Recursion on Circular Data Structures, CALCO Young Researchers Workshop (CALCO-jnr 2011) (C. Cirstea, M. Seisenberger, T. Wilkinson, Eds.), August 2011.
• [14] Wright JB, Thatcher JW, Wagner EG, Goguen JA. Rational Algebraic Theories and Fixed-Point Solutions, FOCS, IEEE Computer Society, 1976. doi: 10.1109/SFCS.1976.24.
• [15] Zucca E, Ancona D. Safe Corecursion in coFJ, FTfJP’012 - Formal Techniques for Java-like Programs. 2013, 2013. doi: 10.1145/2489804.2489807.
• [16] Goguen JA, Thatcher JW. Initial Algebra Semantics, 15th Symp. Switching and Automata Theory, IEEE, 1974. doi: 10.1109/SWAT.1974.13.
• [17] Garrigue J. Relaxing the Value Restriction, Proceedings of the 7th International Symposium on Functional and Logic Programming, FLOPS 2004, Nara, Japan, April 7-9, 2004. (Y. Kameyama, P. J. Stuckey, Eds.), Springer, Berlin, Heidelberg, 2004, ISBN: 978-3-540-24754-8. doi: 10.1007/978-3-540-24754-8_15.
• [18] Jeannin JB, Kozen D. Computing with Capsules, J. Automata, Languages and Combinatorics, 2012; 17 (2-4): 185-204.
• [19] Hirschowitz T, Leroy X, Wells JB. Compilation of extended recursion in call-by-value functional languages, PPDP 2003, 2003. doi: 10.1145/888251.888267.
• [20] Sperber M. Thiemann P. ML and the Address Operator, 1998 ACM SIGPLAN Workshop on ML, September 1998.
• [21] Syme D. Initializing Mutually Referential Abstract Objects: The Value Recursion Challenge, Proc. ACM-SIGPLAN Workshop on ML (2005), Elsevier, March 2006. doi: 10.1016/j.entcs.2005.11.038.
• [22] Boudol G, Zimmer P. Recursion in the call-by-value lambda-calculus, FICS (Z. Ésik, A. Ingólfsdóttir, Eds.), NS-02-2, University of Aarhus, 2002.
• [23] Kozen D. New, Proc. 28th Conf. Math. Found. Programming Semantics (MFPS XXVIII) (U. Berger, M. Mislove, Eds.), Elsevier Electronic Notes in Theoretical Computer Science, Bath, England, June 2012. doi: 10.1016/j.entcs.2012.08.003.
• [24] Jeannin JB. Capsules and Closures, Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII) (M. Mislove, J. Ouaknine, Eds.), Elsevier Electronic Notes in Theoretical Computer Science. Pittsburgh, PA, May 2011. doi: 10.1016/j.entcs.2011.09.022.
• [25] Eppendahl A. Coalgebra-to-Algebra Morphisms, Electronic Notes in Theoretical Computer Science, 29, 1999. doi: 10.1016/S1571-0661(05)80305-6.
• [26] Taylor P. Practical Foundations of Mathematics, Number 59 in Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1999.
• [27] Simon L, Mallya A, Bansal A, Gupta G. Coinductive logic programming, 22nd Int. Conf. Logic Programming (ICLP 2006) (S. Etalle, M. Truszczyński, Eds.), 4079, Springer, August 2006. doi: 10.1007/11799573_25.
• [28] Jeannin JB, Kozen D, Silva A. Well-Founded Coalgebras, Revisited, Math. Structures in Computer Science, FirstView: l-21, February 2016. doi: 10.1017/S0960129515000481.
• [29] Hopcroft JE, Karp RM. A linear algorithm for testing equivalence of finite automata, Technical report, Cornell University, 1971.
• [30] Pottier F. Lazy Least Fixed Points in ML, URL pauillac.inria.fr/~fpottier/publis/fpottier-fix.pdf.
• [31] Capretta V. Coalgebras in functional programming and type theory, Theor. Comput. Sci., 2011; 412 (38): 5006-5024. doi: 10.1016/j.tcs.2011.04.024.
• [32] Silva A, Rutten JJ. Behavioural Differential Equations and Coinduction for Binary Trees, WoLLIC (D. Leivant, R. J. G. B. de Queiroz, Eds.), 4576, Springer, 2007, p. 322-336. ISBN: 978-3-540-73443-7. doi: 10.1007/978-3-540-73445-1_23.
• [33] Silva A, Rutten JJ. A coinductive calculus of binary trees, Inf. Comput., 2010; 208 (5): 578-593. doi: 10.1016/j.ic.2008.08.006.
• [34] Baker A. An Introduction to p-adic Numbers and p-adic Analysis, URL http://www.maths.gla.ac.uk/~ajb/dvi-ps/padicnotes.pdf, March 2011, School of Mathematics and Statistics, University of Glasgow.
• [35] URL https://forge.ocamlcore.org/projects/ocaml-cyclist/, June 2010. Hehner ECR, Horspool RNS. A new representation of the rational numbers for fast easy arithmetic, SIAM J. Comput., 1979; 8 (2): 124-134. doi: 10.1137/0208011.
• [36] Wikipedia: p-adic numbers, URL http://en.wikipedia.org/w/index.php?title=P-adic_number&oldid=553107165, 2012.
• [37] Felleisen M, Hieb R. The Revised Report on the Syntactic Theories of Sequential Control and State, Theoretical Computer Science, 1992; 103: 235-271. doi: 10.1016/0304-3975(92)90014-7.
• [38] Abel A, Pientka B. Wellfounded recursion with copatterns: a unified approach to termination and productivity, ICFP, 2013. doi: 10.1145/2500365.2500591.
• [39] Abel A, Pientka B, Thibodeau D, Setzer A. Copatterns: programming infinite structures by observations, POPL, 2013. doi: 10.1145/2429069.2429075.
• [40] Grebeniuk D. Library ocaml-cyclist, URL https://forge.ocamlcore.org/projects/ocaml-cyclist/, June 2010.
• [41] Caspi P, Pouzet M. A Co-iterative Characterization of Synchronous Stream Functions, Electr. Notes Theor. Comput. Sci., 1998; 11: 1-21. doi: 10.1016/S1571-0661(04)00050-7.
• [42] Adams MD, Dybvig RK. Efficient nondestructive equality checking for trees and graphs, Proc. 13 ACM SIGPLAN Int. Conf. Functional Programming, 2008. doi: 10.1145/1411204.1411230.
• [43] Gaquand T. Infinite Objects in Type Theory, TYPES, 1993. doi: 10.1007/3-540-58085-9_72.
• [44] Giménez E. Structural Recursive Definitions in Type Theory, ICALP, 1998. doi: 10.1007/BFb0055070.
• [45] Bertot Y, Komendantskaya E. Inductive and Coinductive Components of Corecursive Functions in Coq, Electr. Notes Theor. Comput. Sci., 2008; 203 (5): 25-47. doi: 10.1016/j.entcs.2008.05.018.
• [46] Danielsson NA. Beating the Productivity Checker Using Embedded Languages, PAR, 2010. doi: 10.4204/EPTCS.43.3.
• [47] Hur CK, Neis G, Dreyer D, Vafeiadis V. The power of parameterization in coinductive proof, POPL, 2013. doi: 10.1145/2429069.2429093.
• [48] Niqui M. Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme, TYPES, 2008. doi: 10.1007/978-3-642-02444-3_17.
• [49] Oliveira, Bruno CdS, Cook WR. Functional programming with structured graphs, ICFP (P. Thiemann, R. B. Findler, Eds.), ACM, 2012, p. 77-88. ISBN 978-1-4503-1054-3. doi: 10.1145/2364527.2364541.
• [50] Leino KRM, Moskal M. Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier, Technical report, Microsoft Research, 2013.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).