Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers*. Issue 1 (13th October 2017)

• Record Type: Journal Article
• Authors: BENDKOWSKI, MACIEJ; GRYGIEL, KATARZYNA; TARAU, PAUL
• Is Part Of: Theory and practice of logic programming. Volume 18:Issue 1(2018)
• Page Start: 97
• Page End: 119
• Publication Date: 2017-10-13
• Subjects: Boltzmann samplers, -- random generation of simply typed λ-terms, -- type inference, -- combinatorics of λ-terms, -- random generation of simply typed normal forms, -- parallel implementation of Boltzmann samplers; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S147106841700045X
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: 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 λ-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable λ-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 λ-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.