Binary Lambda Calculusはカッコをどのようにエンコードしますか？

Question

BLCはカッコをどのようにエンコードしますか？たとえば、次のようになります。

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

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

注：Wikipediaの記事はあまり知られていない表記法を使用しており、括弧を含まない単純な例と分析が難しい非常に複雑な例を提供しています。この論文は、その面で似ています。

Answer 1

Wikipediaで議論されたDe Bruijnインデックスに基づくバイナリエンコーディングを意味するならば、実際は非常に簡単です。最初にDe Bruijnエンコーディングを行う必要があります。これは、変数とそのλバインダーの間のλバインダーの数を表す自然数で変数を置き換えることを意味します。この表記では、

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

はDは、いくつかの自然数> = 4である

λλλ 3 ((2 1) d) 

なります。それは表現の中で束縛されていないので、実際にどの数字にすべきかは分かりません。そして

+が文字列連結を表し、*繰り返しを意味

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としてエンコードされています。