encoding - How does Binary Lambda Calculus encode parenthesis?

Question

How does the BLC encode parenthesis? For example, how would this:

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

Be encoded in BLC?

Note: the Wikipedia article is not very helpful as it uses an unfamiliar notation and provides only one simple example, which doesn't involve parenthesis, and a very complex example, which is hard to analyze. The paper is similar in that aspect.

Answer 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在此编码中不需要右括号。