How does binary lambda encode brackets?

Question

How does the BLC code brackets? For example, how to do this:

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

Be encoded in BLC?

Note. The Wikipedia article is not very useful as it uses an unfamiliar notation and provides only one simple example that does not include brackets and a very complex example that is difficult to analyze. In this aspect, the paper is similar.

Answer 1

If you mean binary encoding based on the De Bruijn indices discussed on Wikipedia, this is actually quite simple. First you need to do the encoding De Bruijn, which means replacing the variables with natural numbers, denoting the number of λ-binders between the variable and its λ-binder. In these notation

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

becomes

 λλλ 3 ((2 1) d) 

where d is some natural number> = 4. Since it is not connected in the expression, we cannot determine exactly what number it should be.

Then the encoding itself, defined recursively as

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

where + stands for string concatenation and * stands for repetition. Systematically applying this, we obtain

  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) 

and, as you can see, open parentheses are encoded as 01 , while close encodings are not needed in this encoding.