Binary Lambda Calculus如何编码括号？

Question

BLC如何编码括号？例如,这将是怎样的:

?a.?b.?c.(a ((b c) d))

用BLC编码？

注意:维基百科的文章不是很有用,因为它使用了一个不熟悉的符号,只提供了一个不涉及括号的简单示例,以及一个很难分析的非常复杂的示例.该论文在这方面是相似的.

Answer 1

如果你的意思是基于维基百科中讨论的De Bruijn索引的二进制编码,那实际上非常简单.首先需要进行De Bruijn编码,这意味着用自然数替换变量,表示变量与其λBinder之间的λ结合数.在这种表示法中,

?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

where +表示字符串连接,*表示重复.系统地应用这个,我们得到

  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在此编码中不需要紧密的parens.