是否有任何有效的算法可以在简单类型的lambda演算和自然数的良好类型,闭合项之间进行映射？例如,使用bruijn索引(可能是错误的顺序)：

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

相关问题：是否存在一种算法,可以在简单类型的lambda演算的自然数和标准化项之间进行映射？此外,相同的问题适用于无类型的lambda演算.

最佳答案 二元Lambda微积分定义了无类型lambda演算中任何闭合项的二进制编码,并且还建议自然数和二进制字符串之间的双射,但前者不是满射的.

论文
http://arxiv.org/abs/1401.0379

“计算Binary Lambda微积分中的术语”

可能会产生有效的排名/排名映射.