×

Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms. (English) Zbl 1497.68088

Summary: 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.

MSC:

68N17 Logic programming
03B40 Combinatory logic and lambda calculus

Software:

Automath; OEIS
PDFBibTeX XMLCite
Full Text: DOI

References:

[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.), LogicBased 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-31963139-4. doi:10.1007/978-3-319-63139-4\14. , Best paper award. · Zbl 1485.68044
[2] Barendregt HP. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984. ISBN:9780444875082, 9780080933757. · Zbl 0551.03007
[3] Hindley JR, Seldin JP. Lambda-calculus and combinators: an introduction, volume 13. Cambridge University Press Cambridge, 2008. ISBN-10:0521898854, 13:978-0521898850. · Zbl 1149.03016
[4] Barendregt HP. Lambda Calculi with Types. In: Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991. · Zbl 1159.03304
[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. · Zbl 1311.68045
[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). · Zbl 1278.03034
[10] Bodini O, Gardy D, Gittenberger B. Lambda-terms of Bounded Unary Height. In: ANALCO. SIAM, 2011 pp. 23-32. · Zbl 1429.68155
[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. · Zbl 1278.03034
[12] Flajolet P, Sedgewick R. Analytic Combinatorics. Cambridge University Press, New York, NY, USA, 1 edition, 2009. ISBN-0521898064, 9780521898065. · Zbl 1165.05001
[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-206158 8 · Zbl 1417.68028
[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/. · Zbl 1417.68028
[18] Tarau P. A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations.CoRR, 2015.abs/1507.06944. URLhttp://arxiv.org/abs/1507.06944.
[19] Stanley RP. Enumerative Combinatorics. Wadsworth Publ. Co., Belmont, CA, USA, 1986. ISBN-0-53406546-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. · Zbl 0411.03049
[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. · Zbl 1244.68023
[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. · Zbl 1244.68017
[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. · Zbl 1507.68073
[28] Garc´ıa-P´erez ´A, Nogueira P. The full-reducing Krivine abstract machine KN simulates pure normalorder reduction in lockstep: A proof via corresponding calculus.J. Funct. Program., 2019.29:e7. doi:10.1017/S0956796819000017. · Zbl 1493.68085
[29] Lescanne P. Boltzmann samplers for random generation of lambda terms.CoRR, 2014.abs/1404.3875. URLhttp://arxiv.org/abs/1404.3875.
[30] Tromp J. Binary Lambda Calculus and Combinatory Logic, 2018. Published electronically athttps: //tromp.github.io/cl/LC.pdf. · Zbl 1137.68020
[31] Grygiel K, Lescanne P. Counting and generating terms in the binary lambda calculus.J. Funct. Program., 2015.25. doi:10.1017/S0956796815000271. · Zbl 1419.68039
[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 ofLecture Notes in Computer Science. Springer 2016 pp. 183-194. ISBN-978-3-662-49191-1. doi:10.1007/978-3-662-49192-8 15. · Zbl 1428.68095
[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 ofLecture Notes in Computer Science. Springer 2007 pp. 100-109. ISBN-978-3-540-68084-0. doi: 10.1007/978-3-540-68103-8\7. · Zbl 1136.68009
[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. URLhttps://doi. org/10.1017/S147106841700045X. · Zbl 1425.68054
[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. · Zbl 1508.68036
[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 ofLecture 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. · Zbl 1328.68041
[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.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.