{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T03:21:05Z","timestamp":1649128865455},"reference-count":20,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T00:00:00Z","timestamp":1507852800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques automating this labour-intensive process. A prominent example is the successful use of randomness, in particular, random typable \u03bb-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable \u03bb-terms, no effective uniform sampling method is known, setting it as a fundamental open problem in the random software testing approach. In this paper, we combine the framework of Boltzmann samplers, a powerful technique of random combinatorial structure generation, with today's Prolog systems offering a synergy between logic variables, unification with occurs check and efficient backtracking. This allows us to develop a novel sampling mechanism able to construct uniformly random closed simply typed \u03bb-terms of up size 120. We apply our techniques to the generation of uniformly random closed simply typed normal forms and design a parallel execution mechanism pushing forward the achievable term size to 140.<\/jats:p>","DOI":"10.1017\/s147106841700045x","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T04:37:07Z","timestamp":1507869427000},"page":"97-119","source":"Crossref","is-referenced-by-count":1,"title":["Random generation of closed simply typed \u03bb-terms: A synergy between logic programming and Boltzmann samplers"],"prefix":"10.1017","volume":"18","author":[{"given":"MACIEJ","family":"BENDKOWSKI","sequence":"first","affiliation":[]},{"given":"KATARZYNA","family":"GRYGIEL","sequence":"additional","affiliation":[]},{"given":"PAUL","family":"TARAU","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,10,13]]},"reference":[{"key":"S147106841700045X_ref18","doi-asserted-by":"crossref","unstructured":"Tarau P. 2015a. On logic programming representations of lambda terms: de Bruijn indices, compression, type inference, combinatorial generation, normalization. In Proc. 7th International Symposium on Practical Aspects of Declarative Languages PADL'15, E. Pontelli and T. C. Son , Eds. Lecture Notes in Computer Science, vol. 8131. Springer, Portland, Oregon, USA, 115\u2013131.","DOI":"10.1007\/978-3-319-19686-2_9"},{"key":"S147106841700045X_ref1","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1991"},{"key":"S147106841700045X_ref17","unstructured":"Sloane N. J. A. 2014. The on-line encyclopedia of integer sequences. URL: https:\/\/oeis.org\/. [Accessed on August 6, 2017]."},{"key":"S147106841700045X_ref7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:2)2013"},{"key":"S147106841700045X_ref15","volume-title":"The University of Nottingham","author":"Koopman","year":"2006"},{"key":"S147106841700045X_ref2","first-page":"183","volume-title":"SOFSEM","author":"Bendkowski","year":"2016"},{"key":"S147106841700045X_ref19","unstructured":"Tarau P. 2015b. On type-directed generation of lambda terms. In 31st International Conference on Logic Programming (ICLP 2015), Technical Communications, M. De Vos , T. Eiter , Y. Lierler and F. Toni , Eds. CEUR, Cork, Ireland. URL: http:\/\/ceur-ws.org\/Vol-1433\/."},{"key":"S147106841700045X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44854-3_6"},{"key":"S147106841700045X_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S147106841700045X_ref3","doi-asserted-by":"crossref","unstructured":"Bendkowski M. , Grygiel K. and Tarau P. 2017. Boltzmann samplers for closed simply-typed lambda terms. In Proc. of Practical Aspects of Declarative Languages \u2013 19th International Symposium, PADL 2017. Paris, France, January 16\u201317, 2017.","DOI":"10.1007\/978-3-319-51676-9_8"},{"key":"S147106841700045X_ref20","volume-title":"Generatingfunctionology","author":"Wilf","year":"2006"},{"key":"S147106841700045X_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655"},{"key":"S147106841700045X_ref6","doi-asserted-by":"crossref","unstructured":"Claessen K. and Hughes J. 2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In ICFP '00: Proc. of 5th ACM SIGPLAN International Conference on Functional Programming, ACM, New York, NY, USA, 268\u2013279.","DOI":"10.1145\/351240.351266"},{"key":"S147106841700045X_ref4","doi-asserted-by":"crossref","unstructured":"Bodini O. , Gardy D. and Gittenberger B. 2011. Lambda terms of bounded unary height. In Proc. of the 8th Workshop on Analytic Algorithmics and Combinatorics (ANALCO), 23\u201332.","DOI":"10.1137\/1.9781611973013.3"},{"key":"S147106841700045X_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835"},{"key":"S147106841700045X_ref5","doi-asserted-by":"publisher","DOI":"10.1515\/puma-2015-0012"},{"key":"S147106841700045X_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000271"},{"key":"S147106841700045X_ref16","unstructured":"Pa\u0142ka M. H. , Claessen K. , Russo A. and Hughes J. 2011. Testing an optimising compiler by generating random lambda terms. In Proc. of the 6th International Workshop on Automation of Software Test, AST'11. ACM, New York, NY, USA, 91\u201397."},{"key":"S147106841700045X_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000178"},{"key":"S147106841700045X_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0963548304006315"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S147106841700045X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,15]],"date-time":"2019-04-15T16:53:05Z","timestamp":1555347185000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106841700045X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,13]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["S147106841700045X"],"URL":"https:\/\/doi.org\/10.1017\/s147106841700045x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,13]]}}}