按 De Bruijn 表示的加权长度枚举 Lambda 项

John Tromp 引入了所谓的“二进制 lambda 演算”，作为一种利用 de Bruijn 表示及加权方案将 lambda 项编码为 0-1 字符串的方法。后来，Grygiel 和 Lescanne 猜想，具有 $m$ 个自由指标且大小为 $n$ 的二进制 lambda 项（编码为长度为 $n$ 的二进制字，并依据 Tromp 的权重）的数量对于 $\tau \approx 1.963448\ldots$ 为 $o(n^{-3/2} \tau^{-n})$。我们推广了所提出的大小概念，并证明对于包括具有 $m$ 个自由指标的二进制 lambda 项在内的几类 lambda 项，大小为 $n$ 的项数为 $\Theta{n^{-3/2} \rho^{-n}}$，其中 $\rho$ 为依赖于类的常数，这尤其反驳了上述猜想。所用方法是为 lambda 项类建立生成函数。这些生成函数是无限嵌套根式，随后通过奇点分析加以研究。我们进一步展示了如何分析随机 lambda 项的某些性质，并给出了一种以极高效率均匀随机抽样 lambda 项的方法。这使得能够在合理时间内生成大小超过一百万的项，显著优于迄今文献中提出的采样器。