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

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

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

becomes

λλλ 3 ((2 1) d)

where d is some natural number >=4. Since it is unbound in the expression, we can't really tell which 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 + denotes string concatenation and * means repetition. Systematically applying this, we get

  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, the open parentheses are encoded as 01 while the close parens are not needed in this encoding.