计算和生成lambda项
Counting and generating lambda terms
摘要：
λ演算是函数式编程和高阶证明助手的基础。然而，很少有人知道的组合特性的lambda条款，特别是，他们的渐近分布和随机生成。本文试图回答这样的问题：有多少项的给定大小？什么是简单类型术语的“典型”结构？尽管表面上看起来很简单，但这些问题仍然没有答案，而这些问题的解决方案对于测试编译器和优化程序至关重要，这些程序的预期效率取决于术语的大小。我们解决上述问题的方法以后可以扩展到任何具有约束变量的语言，即，范围和声明。本文提出了两种互补的方法：一种是理论的，使用复分析和生成函数，另一种是实验的，是基于一个发电机上的的frida项。由于德Bruijn指数，我们提供了三个家庭的公式的数量封闭的lambda条款的一个给定的大小，我们给这些数字之间的关系，有有趣的组合解释。作为计数公式的一个副产品，我们设计了一个生成lambda项的算法。执行的测试为我们提供了实验数据，如绑定变量的平均深度和头变量的平均数量。我们还为各种术语创建随机生成器。此后，我们进行实验，回答这样的问题：什么是简单类型的条款中的所有条款的比例？(Very小！）简单类型的lambda术语如何分布在所有lambda术语中？（可类型化的术语几乎总是以抽象开始。在本文中，抽象和应用程序的大小为1，变量的大小为0。
英文摘要：
Lambda calculus is the basis of functional programming and higher order proof assistants. However, little is known about combinatorial properties of lambda terms, in particular, about their asymptotic distribution and random generation. This paper tries to answer questions like: How many terms of a given size are there? What is a "typical" structure of a simply typable term? Despite their ostensible simplicity, these questions still remain unanswered, whereas solutions to such problems are essential for testing compilers and optimizing programs whose expected efficiency depends on the size of terms. Our approach toward the afore-mentioned problems may be later extended to any language with bound variables, i.e., with scopes and declarations. This paper presents two complementary approaches: one, theoretical, uses complex analysis and generating functions, the other, experimental, is based on a generator of lambda-terms. Thanks to de Bruijn indices, we provide three families of formulas for the number of closed lambda terms of a given size and we give four relations between these numbers which have interesting combinatorial interpretations. As a by-product of the counting formulas, we design an algorithm for generating lambda terms. Performed tests provide us with experimental data, like the average depth of bound variables and the average number of head lambdas. We also create random generators for various sorts of terms. Thereafter, we conduct experiments that answer questions like: What is the ratio of simply typable terms among all terms? (Very small!) How are simply typable lambda terms distributed among all lambda terms? (A typable term almost always starts with an abstraction.) In this paper, abstractions and applications have size 1 and variables have size 0.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
