Làm thế nào để sử dụng ngữ cảnh đặt tên để tìm chỉ số de Bruijn của các biến miễn phí?

Question

Trong "Loại và Ngôn ngữ lập trình", mục 6.1.2, chúng nói về ngữ cảnh đặt tên được sử dụng để đánh số tự do trong biểu thức lambda. Sử dụng lược đồ ví dụ mà họ đã cung cấp, cả hai λx.xb và λx.xx sẽ có biểu diễn de Bruijn của chúng là λ.00 khi chúng có các cụm từ rõ ràng khác nhau. Cái này hoạt động ra sao?

Answer 1

Như bạn đã đề cập, sách sử dụng ngữ cảnh đặt tên để ánh xạ các biến số n miễn phí tới các số từ 0 đến n-1. Tuy nhiên, nếu bạn xem xét kỹ các ví dụ trong cuốn sách, bạn sẽ nhận thấy rằng nó không sử dụng những con số đó trực tiếp để đại diện cho các biến. Ví dụ: nó đại diện cho λw. y w là λ. 4 0 mặc dù ánh xạ cho y là 3, không phải là 4.

Điều đang xảy ra ở đây là thêm chiều sâu lồng của biến vào số. I E. nếu một biến miễn phí v được lồng trong d lambdas, nó sẽ nhận được chỉ mục Γ(v)+d, không chỉ Γ(v).

Vì vậy, trong ví dụ của bạn, sử dụng ngữ cảnh Γ {b -> 0}λx.xb sẽ được biểu thị là λ. 0 1, chứ không phải là λ. 0 0. Do đó không có sự mơ hồ.