Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms

• Autorzy: Tarau Paul

Identyfikatory

DOI

10.3233/FI-2020-1994

• Języki publikacji: EN

Abstrakty

EN

Contrary to several other families of lambda terms, no closed formula or generating function is known and none of the sophisticated techniques devised in analytic combinatorics can currently help with counting or generating the set of simply-typed closed lambda terms of a given size. Moreover, their asymptotic scarcity among the set of closed lambda terms makes counting them via brute force generation and type inference quickly intractable, with previous published work showing counts for them only up to size 10. By taking advantage of the synergy between logic variables, unification with occurs check and efficient backtracking in today’s Prolog systems, we climb 4 orders of magnitude above previously known counts by deriving progressively faster sequential Prolog programs that generate and/or count the set of closed simply-typed lambda terms of sizes up to 14. Similar counts for closed simply-typed normal forms are also derived up to size 14. Finally, we devise several parallel execution algorithms, based on generating code to be uniformly distributed among the available cores, that push the counts for simply typed terms up to size 15 and simply typed normal forms up to size 16. As a remarkable feature, our parallel algorithms are linearly scalable with the number of available cores.

Słowa kluczowe

EN

simply-typed lambda terms; normal forms; parallel combinatorial generation algorithms; sequential combinatorial generation algorithms; type inference; prolog multi-threadinglogic programming transformations

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 177, nr 3/4
• Strony: 385--415
• Opis fizyczny: Bibliogr. 40 poz., tab.

Twórcy

autor

Tarau Paul

• Department of Computer Science and Engineering, University of North Texas, Denton, Texas, USA

Bibliografia

• [1] Tarau P. A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms. In: Hermenegildo MV, Lopez-Garcia P (eds.), Logic-Based Program Synthesis and Transformation: 26th International Symposium, LOPSTR 2016, Edinburgh, UK, Revised Selected Papers. Springer LNCS, volume 10184. 2017 pp. 240-255. ISBN-978-3-319-63139-4. doi:10.1007/978-3-319-63139-4\_14. Best paper award.
• [2] Barendregt HP. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984. ISBN:9780444875082, 9780080933757.
• [3] Hindley JR, Seldin JP. Lambda-calculus and combinators: an introduction, volume 13. Cambridge University Press Cambridge, 2008. ISBN-10:0521898854, 13:978-0521898850.
• [4] Barendregt HP. Lambda Calculi with Types. In: Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991.
• [5] Howard W. The Formulae-as-types Notion of Construction. In: Seldin J, Hindley J (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479-490. Academic Press, London, 1980. Howard80.pdf.
• [6] Wadler P. Propositions as types. Commun. ACM, 2015. 58:75-84. doi:10.1145/2699407.
• [7] Palka MH, Claessen K, Russo A, Hughes J. Testing an Optimising Compiler by Generating Random Lambda Terms. In: Proceedings of the 6th International Workshop on Automation of Software Test, AST’11. ACM, New York, NY, USA, 2011 pp. 91-97. doi:10.1145/1982595.1982615.
• [8] Grygiel K, Lescanne P. Counting and generating lambda terms. J. Funct. Program., 2013. 23(5):594-628. doi:10.1017/S0956796813000178.
• [9] David R, Raffalli C, Theyssier G, Grygiel K, Kozik J, Zaionc M. Some properties of random lambda terms. Logical Methods in Computer Science, 2009. 9(1).
• [10] Bodini O, Gardy D, Gittenberger B. Lambda-terms of Bounded Unary Height. In: ANALCO. SIAM, 2011 pp. 23-32.
• [11] David R, Grygiel K, Kozik J, Raffalli C, Theyssier G, Zaionc M. Asymptotically almost all λ-terms are strongly normalizing. Preprint: arXiv: math. LO/0903.5505 v3, 2010.
• [12] Flajolet P, Sedgewick R. Analytic Combinatorics. Cambridge University Press, New York, NY, USA, 1 edition, 2009. ISBN-0521898064, 9780521898065.
• [13] Sloane NJA. The On-Line Encyclopedia of Integer Sequences. 2020. Published electronically at https://oeis.org/.
• [14] Tarau P. On Logic Programming Representations of Lambda Terms: de Bruijn Indices, Compression, Type Inference, Combinatorial Generation, Normalization. In: Pontelli E, Son TC (eds.), Proceedings of the Seventeenth International Symposium on Practical Aspects of Declarative Languages PADL’15. Springer, LNCS 8131, Portland, Oregon, USA, 2015 pp. 115-131. doi:10.1007/978-3-319-19686-2_9.
• [15] Tarau P. Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices. In: Kerber M, Carette J, Kaliszyk C, Rabe F, Sorge V (eds.), Proceedings of the 8th Conference on Intelligent Computer Mathematics. Springer, LNAI 9150, Washington, D.C., USA, 2015 pp. 118-133. doi:10.1007/978-3-319-20615-8_8.
• [16] Tarau P. On a Uniform Representation of Combinators, Arithmetic, Lambda Terms and Types. In: Albert E (ed.), PPDP’15: Proceedings of the 17th international ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. ACM, New York, NY, USA, 2015 pp. 244-255. doi:10.1145/2790449.2790526.
• [17] Tarau P. On Type-directed Generation of Lambda Terms. In: De Vos M, Eiter T, Lierler Y, Toni F (eds.), 31st International Conference on Logic Programming (ICLP 2015), Technical Communications. CEUR, Cork, Ireland, 2015 Available online at http://ceur-ws.org/Vol-1433/.
• [18] Tarau P. A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations. CoRR, 2015. abs/1507.06944. URL http://arxiv.org/abs/1507.06944.
• [19] Stanley RP. Enumerative Combinatorics. Wadsworth Publ. Co., Belmont, CA, USA, 1986. ISBN-0-534-06546-5.
• [20] Statman R. Intuitionistic Propositional Logic is Polynomial-Space Complete. Theor. Comput. Sci., 1979. 9:67-72. doi:10.1016/0304-3975(79)90006-9.
• [21] Wielemaker J, Schrijvers T, Triska M, Lager T. SWI-Prolog. Theory and Practice of Logic Programming, 2012. 12:67-96. doi:10.1017/S1471068411000494.
• [22] Costa VS, Rocha R, Damas L. The YAP Prolog system. Theory and Practice of Logic Programming, 2012. 12:5-34. doi:10.1017/S1471068411000512.
• [23] Tarau P. An Efficient Specialization of the WAM for Continuation Passing Binary Programs. In: Proceedings of the 1993 ILPS Conference. MIT Press, Vancouver, Canada, 1993 Poster.
• [24] Tarau P, Demoen B. Higher-Order Programming in an OR-intensive Style. In: Hermenegildo M, Lopez P (eds.), Proceedings of the 1995 COMPULOG-NET Workshop and Area Meeting on Parallelism and Implementation Technology. 1995.
• [25] Gupta G, Pontelli E, Ali KAM, Carlsson M, Hermenegildo MV. Parallel execution of prolog programs: a survey. ACM Trans. Program. Lang. Syst., 2001. 23(4):472-602. doi:10.1145/504083.504085.
• [26] Wielemaker J. Native Preemptive Threads in SWI-Prolog. In: Palamidessi C (ed.), Practical Aspects of Declarative Languages. Springer Verlag, Berlin, Germany, 2003 pp. 331-345. LNCS 2916. doi:10.1007/978-3-540-24599-5_23.
• [27] Kiselyov O. λ to SKI, Semantically - Declarative Pearl. In: Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings, volume 10818 of Lecture Notes in Computer Science. 2018 pp. 33-50. doi:10.1007/978-3-319-90686-7_3.
• [28] García-Pérez Á, Nogueira P. The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus. J. Funct. Program., 2019. 29:e7. doi:10.1017/S0956796819000017.
• [29] Lescanne P. Boltzmann samplers for random generation of lambda terms. CoRR, 2014. abs/1404.3875. URL http://arxiv.org/abs/1404.3875.
• [30] Tromp J. Binary Lambda Calculus and Combinatory Logic, 2018. Published electronically at https://tromp.github.io/cl/LC.pdf.
• [31] Grygiel K, Lescanne P. Counting and generating terms in the binary lambda calculus. J. Funct. Program., 2015. 25. doi:10.1017/S0956796815000271.
• [32] Bendkowski M, Grygiel K, Lescanne P, Zaionc M. A Natural Counting of Lambda Terms. In: Freivalds RM, Engels G, Catania B (eds.), SOFSEM 2016: Theory and Practice of Computer Science - 42nd International Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 23-28, 2016, Proceedings, volume 9587 of Lecture Notes in Computer Science. Springer 2016 pp. 183-194. ISBN-978-3-662-49191-1. doi:10.1007/978-3-662-49192-8_15.
• [33] Fetscher B, Claessen K, Palka MH, Hughes J, Findler RB. Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System. In: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 2015 pp. 383-405.
• [34] Genitrini A, Kozik J, Zaionc M. Intuitionistic vs. Classical Tautologies, Quantitative Comparison. In: Miculan M, Scagnetto I, Honsell F (eds.), Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, volume 4941 of Lecture Notes in Computer Science. Springer 2007 pp. 100-109. ISBN-978-3-540-68084-0. doi:10.1007/978-3-540-68103-8\_7.
• [35] Bendkowski M, Grygiel K, Tarau P. Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers. TPLP, 2018. 18(1):97-119. URL https://doi.org/10.1017/S147106841700045X.
• [36] Bodini O, Tarau P. On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms. In: Fioravanti F, Gallagher JP (eds.), Logic-Based Program Synthesis and Transformation, LNCS 10855. Springer International Publishing 2018 pp. 252-268. ISBN-978-3-319-94460-9.
• [37] Tarau P. On k-colored Lambda Terms and their Skeletons. In: Calimeri F, Hamlen KW, Leone N (eds.), Practical Aspects of Declarative Languages - 20th International Symposium, PADL 2018, Los Angeles, CA, USA, January 8-9, 2018, Proceedings, volume 10702 of Lecture Notes in Computer Science. Springer 2018 pp. 116-131. ISBN-978-3-319-73304-3. doi:10.1007/978-3-319-73305-0\_8.
• [38] Fioravanti F, Proietti M, Senni V. Efficient generation of test data structures using constraint logic programming and program transformation. Journal of Logic and Computation, 2015. 25(6):1263-1283. doi:10.1093/logcom/ext071.
• [39] Kuraj I, Kuncak V, Jackson D. Programming with Enumerable Sets of Structures. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015. ACM, New York, NY, USA 2015 pp. 37-56. ISBN-978-1-4503-3689-5. doi:10.1145/2814270.2814323.
• [40] Tarau P. A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers. In: Alferes JJ, Johansson M (eds.), Practical Aspects of Declarative Languages - 21th International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings, volume 11372 of Lecture Notes in Computer Science. Springer 2019 pp. 115-132. ISBN 978-3-030-05997-2.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).