Mã nhị phân lambda Calculus mã hóa dấu ngoặc đơn như thế nào?

Question

Mã hóa BLC như thế nào? Ví dụ: cách này:

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

Được mã hóa trong BLC? Ghi chú: Bài viết Wikipedia không hữu ích vì nó sử dụng một ký hiệu lạ và chỉ cung cấp một ví dụ đơn giản, không liên quan đến dấu ngoặc đơn và một ví dụ rất phức tạp, khó phân tích. Giấy tương tự ở khía cạnh đó.

Answer 1

Nếu bạn ngụ ý mã hóa nhị phân dựa trên các chỉ số De Bruijn được thảo luận trong Wikipedia, điều đó thực sự khá đơn giản. Trước tiên, bạn cần phải làm mã hóa De Bruijn, có nghĩa là thay thế các biến bằng các số tự nhiên biểu thị số lượng các liên kết giữa biến và giá trị của nó. Trong ký hiệu này,

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

trở thành

λλλ 3 ((2 1) d) 

nơi d là một số số tự nhiên> = 4. Vì nó không bị ràng buộc trong biểu thức, chúng ta không thể thực sự biết số đó nên là gì.

Sau đó mã hóa riêng của mình, được định nghĩa đệ quy như

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

nơi + biểu thị chuỗi nối và * có nghĩa là lặp lại. Có hệ thống áp dụng này, chúng tôi nhận

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) 

và như bạn có thể thấy, các dấu ngoặc đơn mở được mã hóa như 01 trong khi Parens gần không cần thiết trong bảng mã này.