自然数和有效的简单类型 lambda 演算项之间的映射是什么？答案

【问题标题】：What is a mapping between natural numbers and valid simply typed lambda calculus terms?自然数和有效的简单类型 lambda 演算项之间的映射是什么？
【发布时间】：2015-02-23 23:00:03
【问题描述】：

是否有任何有效的算法可以在简单类型的 lambda 演算的类型良好的封闭项和自然数之间进行映射？例如，使用 bruijn 索引（并且可能顺序不正确）：

0 → (λ 0)
1 → (λ (λ (0 1)))
2 → (λ (λ (1 0)))
3 → (λ 0 (λ 0))
4 → (λ (λ 0) 0)
5 → (λ (λ 1) 0)
6 → ... so on

相关问题：是否有一种算法可以在自然数和简单类型 lambda 演算的规范化项之间进行映射？此外，同样的问题也适用于无类型 lambda 演算。

【问题讨论】：

它必须是双射的吗？如果是这样，我不相信有任何有效的解决方案。
如果识别归一化项不可计算，那么您可能对枚举算法不满意。
您所说的“地图之间”是指两个地图，每个方向一个地图（可能它们彼此相反，使其成为同构）？此外，您是否希望它仅限于 Church 数字，还是希望它适用于任意 lambda 项？听起来您正在寻找后者，后者（如果我问的第一件事是正确的）似乎在询问所有 lambda 演算项的集合是否可数。
是的，两张地图。函数“natToLambda”及其反函数“lambdaToNat”。是的，我想要后者。是可数的！
你需要lambdaToNat 是满射的吗？

标签： algorithm search functional-programming enumeration lambda-calculus

【解决方案1】：

Binary Lambda Calculus 为无类型 lambda 演算中的任何闭项定义了二进制编码，并且还暗示了自然数和二进制字符串之间的双射，但前者不是满射的。尽管如此，论文http://arxiv.org/abs/1401.0379 “二进制 Lambda 演算中的计数项” 可能会产生有效的排名/非排名映射。

【讨论】：

约翰，没有任何算法可以接受一个 int（一个 nat...）并将其转换为一个 lambda 项，并且它是相反的吗？所以每个 nat 都有一个对应的 lambda 项，反之亦然？

【解决方案2】：

由于类型化 lambda 演算的高度上下文敏感特性，如果有一种有效的算法，或者更确切地说是一种“自然的”高效算法，我会感到惊讶。

This paper 有很好的公式来计算 无类型 lambda 项，并从中派生出一个相当简单的函数来枚举无类型项。它们还为范式提供了计数功能，这也应该很容易适应生成函数。不幸的是，他们只通过过滤非常昂贵的东西来制作一个类型化的生成器函数（论文的结果之一就是它是多么荒谬）。

至于生成类型化术语的更有效方法，我的建议是生成类型化派生而不是术语，然后对它们进行类型检查。

【讨论】：