[잘라먹는 프로그래밍 언어론] 변수가 스스로의 이름을 지키는 법 (de Bruijn index/level)

이 글은 프로그램에서 이름 충돌을 피하고 코드를 정확하게 평가하기 위한 방법으로 de Bruijn index를 소개한다. 변수 이름으로 인한 혼란을 해결하기 위해 α-변환을 설명하고, de Bruijn level과 index를 통해 변수를 숫자로 표현하는 방법을 제시한다. 특히, de Bruijn index는 변수가 얼마나 바깥 스코프를 참조하는지 나타내어, 형식적 증명에서 이름 없는 변수들을 다루는 데 유용함을 강조한다. 이를 통해 코드의 본질을 명확히 하고, 형식적 증명 과정에서 동일한 것을 쉽게 식별할 수 있게 된다.