自然数和有效类型的lambda演算项之间的映射是什么？
自然数和有效类型的lambda演算项之间的映射是什么？
提问于 2015-02-23 23:00:03
在简单类型λ演算的类型化、闭项和自然数之间有什么有效的算法吗？例如，使用bruijn索引(可能顺序不正确)：
0 → (λ 0)
1 → (λ (λ (0 1)))
2 → (λ (λ (1 0)))
3 → (λ 0 (λ 0))
4 → (λ (λ 0) 0)
5 → (λ (λ 1) 0)
6 → ... so on相关问题:是否有一种算法在自然数和标准化的项之间映射简单类型的lambda演算？同样的问题也适用于非类型化的lambda演算。
回答 2
Stack Overflow用户
回答已采纳
发布于 2015-04-14 18:13:50
二元Lambda演算为非类型化lambda演算中的任何闭项定义了二进制编码，并提出了自然数和二进制串之间的双射，但前者不是满射的。尽管如此，论文http://arxiv.org/abs/1401.0379“二进制Lambda中的计数项”可能会产生有效的排序/未排序映射。
Stack Overflow用户
发布于 2015-11-23 15:33:32
由于类型化lambda演算对上下文高度敏感，如果有一个有效的算法，或者更确切地说是一个“自然”高效算法，我会感到惊讶。
本论文有很好的计算非类型化λ项的公式，并由此导出了一个用于枚举非类型化项的相当简单的函数。它们还提供了一个正常形式的计数函数，它也很容易适应生成函数。不幸的是，他们只通过过滤那些昂贵得离谱的东西(论文的结果之一就是它是多么的荒谬)才能产生一个类型化的生成器功能。
至于一种更有效地生成类型化术语的方法，我的建议是生成类型派生，而不是术语，然后键入检查它们。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/28685232
复制相关文章
相似问题
腾讯云开发者
