Title
Random generation of closed simply-typed $λ$-terms: a synergy between logic programming and Boltzmann samplers.
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 typeable $\lambda$-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typeable $\lambda$-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 $\lambda$-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. Under consideration in Theory and Practice of Logic Programming (TPLP).
Year
Venue
DocType
2016
CoRR
Journal
Volume
Citations 
PageRank 
abs/1612.07682
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Maciej Bendkowski100.34
Katarzyna Grygiel2446.95
Paul Tarau31529113.14