In che modo Binary Lambda Calculus codifica parentesi?

Question

In che modo BLC codifica la parentesi? Ad esempio, come sarebbe questo:

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

Essere codificato in BLC?

Nota: l'articolo di Wikipedia non è molto utile in quanto utilizza una notazione non familiare e fornisce solo un semplice esempio, che non include parentesi, e un esempio molto complesso, che è difficile da analizzare. La carta è simile in questo aspetto.

Answer 1

Se si intende la codifica binaria basata su indici De Bruijn discussi in Wikipedia, in realtà è piuttosto semplice. È necessario prima eseguire la codifica De Bruijn, che significa sostituire le variabili con numeri naturali che indicano il numero di leganti λ tra la variabile e il suo raccoglitore λ. In questa notazione,

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

diventa

λλλ 3 ((2 1) d) 

dove d è un numero naturale> = 4. Dal momento che non è legato nell'espressione, non possiamo veramente dire quale numero dovrebbe essere.

Poi la codifica stessa, definito ricorsivamente come

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

dove + indica concatenazione di stringhe e * mezzi di ripetizione. Sistematicamente l'applicazione di questo, otteniamo

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) 

e come si può vedere, le parentesi aperte sono codificati come 01 mentre le parentesi stretti non sono necessari in questa codifica.