BLC是如何编码括号的?例如,这将如何:
λa.λb.λc.(a ((b c) d))
用BLC编码?
注意: Wikipedia的文章没有多大帮助,因为它使用了一个不熟悉的符号,只提供了一个不涉及括号的简单示例,以及一个非常复杂的示例,很难分析。本论文在这方面也是类似的。
发布于 2013-08-03 08:34:13
如果你指的是基于维基百科中讨论的De索引的二进制编码,那实际上很简单。首先需要进行denoting编码,这意味着用表示变量与其λ绑定之间的λ绑定数的自然数替换变量。在这个符号里,
λ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
,而在这种编码中不需要关闭父母。
https://stackoverflow.com/questions/18034246
复制