具有指定De Bruijn表示大小的λ项数目

John Tromp引入了所谓的“二进制lambda演算”作为用二进制字编码lambda项的方法。后来，Grygiel和Lescanne猜想，具有 $m$ 个自由指标且大小为 $n$（编码为长度为 $n$ 的二进制字）的二进制lambda项的数目对于 $\tau \approx 1.963448\ldots$ 为 $o(n^{-3/2} \tau^{-n})$。我们推广了所提出的大小概念，并证明对于几类lambda项，包括具有 $m$ 个自由指标的二进制lambda项，大小为 $n$ 的项的数目为 $\Theta(n^{-3/2} \rho^{-n})$，其中 $\rho$ 为依赖于类的常数，这尤其反驳了上述猜想。给出了一种获得首项附近常数上下界的方法，并给出了之前引入的几类lambda项的数值结果。