2017-12

Random generation of closed simply-typed λ-terms: a synergy between logic programming and Boltzmann samplers

Maciej Bendkowski, Katarzyna Grygiel Jagiellonian University, Kraków, Poland

Paul Tarau University of North Texas, Denton, TX, USA

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


PDF Version

Bibtex

@article{LABEL,
author = {Maciej Bendkowski and Katarzyna Grygiel and Paul Tarau},
title = {Random generation of closed simply-typed λ-terms: a synergy between logic programming and Boltzmann samplers},
journal = {Theory and Practice of Logic Programming},
volume = {},
number = {},
pages = {},
year = {TO APPEAR}
}