Как двоичное исчисление лямбда закодирует скобки?

Question

Как кодировать скобки BLC? Например, как это делается:

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

Может быть закодирован в BLC?

Примечание: статья Википедии не очень полезна, так как использует незнакомую нотацию и предоставляет только один простой пример, который не включает скобки, и очень сложный пример, который трудно анализировать. В этом аспекте бумага аналогична.

Answer 1

Если вы имеете в виду двоичную кодировку на основе индексов De Bruijn, обсуждаемых в Википедии, это на самом деле довольно просто. Сначала вам нужно сделать кодировку De Bruijn, что означает замену переменных натуральными числами, обозначающими число λ-связующих между переменной и ее λ-связующим. В этих обозначениях

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

становится

λλλ 3 ((2 1) 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 в то время как близкие круглые скобки не нужны в этой кодировке.