Binary Lambda Calculus 如何编码括号？答案

【问题标题】：How does Binary Lambda Calculus encode parenthesis?Binary Lambda Calculus 如何编码括号？
【发布时间】：2013-08-03 15:11:52
【问题描述】：

BLC 如何编码括号？例如，这将如何：

λa.λb.λc.(a ((b c) d))

用 BLC 编码？

注意：维基百科的文章不是很有帮助，因为它使用了一种不熟悉的符号，并且只提供了一个不涉及括号的简单示例，以及一个非常复杂的示例，难以分析。这篇论文在这方面是相似的。

【问题讨论】：

标签： encoding lambda functional-programming lambda-calculus

【解决方案1】：

如果您指的是基于 Wikipedia 中讨论的 De Bruijn 索引的二进制编码，那实际上非常简单。您首先需要进行 De Bruijn 编码，这意味着用自然数替换变量，表示变量与其 λ 绑定器之间的 λ 绑定器的数量。在这种表示法中，

λa.λb.λc.(a ((b c) d))

变成

λλλ 3 ((2 1) d)

其中 d 是某个自然数 >=4。由于它在表达式中是未绑定的，因此我们无法确定它应该是哪个数字。

然后是编码本身，递归定义为

enc(λM) = 00 + enc(M)
enc(MN) = 01 + enc(M) + enc(N)
enc(i) = 1*i + 0

其中+ 表示字符串连接，* 表示重复。系统地应用它，我们得到

  enc(λλλ 3 ((2 1) d))
= 00 + enc(λλ 3 ((2 1) d))
= 00 + 00 + enc(λ 3 ((2 1) d))
= 00 + 00 + 00 + enc(3 ((2 1) d))
= 00 + 00 + 00 + 01 + enc(3) + enc((2 1) d)
= 00 + 00 + 00 + 01 + enc(3) + 01 + enc(2 1) + enc(d)
= 00 + 00 + 00 + 01 + enc(3) + 01 + 01 + enc(2) + enc(1) + enc(d)
= 000000011110010111010 + enc(d)

如您所见，左括号被编码为01，而在此编码中不需要右括号。

【讨论】：

很棒的答案，谢谢。所以括号不是必需的，因为 01 已经意味着二进制应用程序。只是一个问题，这是最优的吗？因为这种编码数字的方式看起来很浪费。
@Viclib：你说得对，这是使用一元数字表示（计数标记），二进制编码可能更适合复杂的公式。不过，这将更难定义，我现在不打算尝试它——您需要确保它不会与表示 λ 和应用程序的位字符串发生冲突。