Boltzmann Samplers for Closed Simply-Typed Lambda Terms
Boltzmann Samplers for Closed Simply-Typed Lambda Terms
复制标题
用于封闭式简单类型 Lambda 项的玻尔兹曼采样器
DOI：
10.1007/978-3-319-51676-9_8
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Paul Tarau
中科院分区：
文献类型：
--
作者：
Maciej Bendkowski;Katarzyna Grygiel;Paul Tarau
简单类型的lambda术语经常用于编译器和证明助手的内部语言中，对于这些语言，生成大型均匀分布的随机术语有助于测试正确性和可扩展性。最近，玻尔兹曼采样器已经能够均匀随机生成属于几个具有规则结构的组合对象家族的大项，这些对象适合分析组合学的方法。不幸的是，没有封闭的公式或生成函数促进这种方法是已知的封闭的简单类型的lambda项。此外，考虑到它们在封闭lambda项族中的渐近稀疏性，在由玻尔兹曼采样器生成的更大的项集中过滤简单类型的项变得很快难以处理。通过利用逻辑变量之间的协同作用，统一与发生检查和有效的回溯，在今天的Prolog系统，我们推进这项技术的长期规模感兴趣的不仅是正确性，而且可扩展性测试，通过推导玻尔兹曼采样器返回在几秒钟内简单类型的随机lambda条款的大小120及以上。我们还将我们的技术的均匀随机封闭的简单类型的正规形式的生成，并通过并行执行算法进一步推动他们的一些提示。
Simply-typed lambda terms are often used in the internal language of compilers and proof assistants, for which generation of large, uniformly distributed random terms is instrumental for testing correctness and scalability. Recently, Boltzmann samplers have enabled uniform random generation of large terms belonging to several families of combinatorial objects that have a regular structure, amenable to methods from analytic combinatorics. Unfortunately, no closed formula or generating function facilitating such methods is known for closed simply-typed lambda terms. Moreover, given their asymptotic sparsity in the family of closed lambda terms, filtering simply-typed terms in the much larger set of terms generated by a Boltzmann sampler becomes quickly intractable. By taking advantage of the synergy between logic variables, unification with occurs check and efficient backtracking in today’s Prolog systems we advance this technique to term sizes interesting not only for correctness but also for scalability tests, by deriving Boltzmann samplers returning in a few seconds simply-typed random lambda terms of size 120 and above. We also apply our techniques to the generation of uniformly random closed simply-typed normal forms and give some hints on pushing them further via parallel execution algorithms.