跨越数量级的徒步之旅：推导闭简单类型lambda项与范式的高效生成器
编程语言
2016-08-16 v1 计算机科学中的逻辑
摘要
与若干其他lambda项族不同，对于给定大小的闭简单类型lambda项集合，既无已知的闭式公式或生成函数，且当前解析组合学中设计的精细技术也无法用于计数或生成该集合。此外，它们在闭lambda项集合中的渐近稀缺性使得通过暴力生成和类型推断进行计数很快变得难以处理，先前发表的工作仅展示了大小不超过10的计数。通过利用当今Prolog系统中逻辑变量、带出现检查的合一（unification with occurs check）与高效回溯之间的协同作用，我们推导出逐步更快的霍恩子句（Horn Clause）程序，生成和/或计数大小不超过14的闭简单类型lambda项集合，从而将先前已知计数提升了4个数量级。类似地，我们也推导了闭简单类型范式直至大小14的计数。关键词：逻辑编程变换，类型推断，lambda项组合学，简单类型lambda演算，简单类型范式。
引用
@article{arxiv.1608.03912,
title = {A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms},
author = {Paul Tarau},
journal= {arXiv preprint arXiv:1608.03912},
year = {2016}
}
备注
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)