이름은 프로그램에서 대상을 부를 때 필연적으로 등장하는 개념이다.

모듈, 함수, 변수, 상수. 그 모든 것들은 이름을 필요로 하고, 제한된 어휘 속에 결국 충돌하고 만다.

그렇기에 사람은 지역을 나누어 그 안에서만 고유한 이름을 주고, 그 외에는 신경을 쓰지 않아왔다.

하지만, 어째서 컴파일러가 그 모든 코드를 모아서 단일 아티팩트를 냈음에도 그들은 충돌하지 않고 평가가 가능한 걸까? 여러 방법이 있지만, 형식적 증명에서 자주 쓰는 방법을 소개해보고자 한다.

const sum = x => (y => x + y)

let x = 4;
sum(2)(4 + x)

위 JS 코드를 평가해보자.

let x = 4;
sum(2)(4 + x)
// ==> sum 치환
let x = 4;
(x => (y => x + y))(2)(4 + x)
// ==> 함수 적용
let x = 4;
((y => x + y)(4 + x))[x = 2]
// ==> 함수 적용
let x = 4;
((x + y)[y = 4 + x])[x = 2]
// ==> x 치환
let x = 4;
((2 + y)[y = 4 + 2])
// ... 잠깐!

y가 참조해야 할 바깥 let x = 4 선언이 아니라, 인자 x에게 납치당해 2로 치환당했다! 변수 이름을 고쳐서 충돌을 피해보자.

정의 "α-변환": 아무도 안 쓰는 이름 b가 있다면, a => E(a)는 b => E(b)로 고칠 수 있다 (이름이 달라도 같은 위치를 가리키기 때문이다).

let x = 4;
sum(2)(4 + x)
// ==> sum 치환
let x = 4;
(x => (y => x + y))(2)(4 + x)
// ==> x를 α-변환
let x = 4;
(_1 => (y => _1 + y))(2)(4 + x)
// ==> y를 α-변환
let x = 4;
(_1 => (_2 => _1 + _2))(2)(4 + x)
// ==> 함수 적용
let x = 4;
((_2 => _1 + _2)(4 + x))[_1 = 2]
// ==> 함수 적용
let x = 4;
((_1 + _2)[_2 = 4 + x])[_1 = 2]
// ==> _1 치환
let x = 4;
(2 + _2)[_2 = 4 + x]
// ==> _2 치환
let x = 4;
2 + (4 + x)

지루한 치환 끝에 원하던 결과를 얻었다. 이제 우리는 어떤 변수명을 쓰든 상관 없이 잘 치환하는 법을 배웠다.

우리가 했던 것처럼 가장 바깥 변수부터 숫자를 부여하면 de Bruijn level이 된다. 이 체계에서는 안쪽이 얼마나 깊든 바깥쪽 변수가 이미 번호를 잘 부여받았기에, 같은 변수를 참조한다면, 같은 이름으로 참조하게 된다.

하지만, 바깥쪽에 람다 표현식이 감싸진다면 모든 변수를 한 칸 밀어야 하기에 표현식 조작에 부적합하다. 반대로 de Bruijn index는 실제로 쓰는 곳에서 얼마나 바깥의 변수를 참조하는지 말하는 방식이다.

// de Bruijn level
     y => z => y //  λλ1
     y => z => z //  λλ2
     1    2
x => y => z => x // λλλ1
x => y => z => y // λλλ2
x => y => z => z // λλλ3
1    2    3

// de Bruijn index
     y => z => y //  λλ2
     y => z => z //  λλ1
     2    1    |
     ^    ^    |
     +----+----+
x => y => z => x // λλλ3
x => y => z => y // λλλ2
x => y => z => z // λλλ1
3    2    1    |
^    ^    ^    |
+----+----+----+

나아가, 이름 없는 de Bruijn index 세계에선 x => y => x와 y => x => y가 모두 λλ2로 같다.

같은 것을 쉽게 같다고 할 수 있기에 형식적 증명 세계는 이름을 지우고, 본질을 되새긴다.