Comment Binary Lambda Calculus code-t-il les parenthèses?

Question

Comment le BLC code-t-il les parenthèses? Par exemple, comment cela serait-il:

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

Être codé en BLC? Note: l'article Wikipédia n'est pas très utile car il utilise une notation peu familière et ne fournit qu'un exemple simple, qui n'implique pas de parenthèse, et un exemple très complexe, difficile à analyser. Le papier est similaire dans cet aspect.

Answer 1

Si vous voulez dire que le codage binaire basé sur De Bruijn indices discuté dans Wikipedia, qui est en fait assez simple. Vous devez d'abord faire le codage De Bruijn, qui consiste à remplacer les variables par des nombres naturels indiquant le nombre de liants X entre la variable et son liant λ. Dans cette notation,

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

devient

λλλ 3 ((2 1) d) 

où d est un nombre naturel> = 4. Comme il n'est pas lié dans l'expression, nous ne pouvons pas vraiment dire quel nombre il devrait être.

le codage lui-même, défini récursivement comme

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

où + représente la concaténation de chaîne et * signifie répétition. appliquer ce Systématiquement, nous obtenons

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) 

et comme vous pouvez le voir, les parenthèses ouvertes sont encodées comme 01 alors que les parens proches ne sont pas nécessaires dans ce codage.