encoding - Binary Lambda Calculus はどのように括弧をエンコードしますか?

Question

BLC はどのように括弧をエンコードしますか? たとえば、これは次のようになります。

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

BLC でエンコードされますか?

注: ウィキペディアの記事は、なじみのない表記法を使用しており、括弧を含まない単純な例と、分析が難しい非常に複雑な例を 1 つしか提供していないため、あまり役に立ちません。その点では論文も同様です。

Answer 1

ウィキペディアで説明されている De Bruijn インデックスに基づくバイナリ エンコーディングを意味する場合、それは実際には非常に単純です。最初に De Bruijn エンコーディングを行う必要があります。これは、変数とその λ バインダーの間の λ バインダーの数を表す自然数で変数を置き換えることを意味します。この表記では、

λ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このエンコーディングでは必要ありませんが、閉じ括弧は必要ありません。