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

Question

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

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

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

Answer 1

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