4.5 자유 변수와 묶인 변수의 구분 및 알파 변환(α-conversion)

1. 자유 변수와 속박 변수의 구분

1.1 변수의 출현(Occurrence)

람다 항 내에서 변수의 각 출현(Occurrence)은 자유 출현(Free Occurrence) 또는 속박 출현(Bound Occurrence)으로 분류된다.

속박 출현: 변수 $x$ 의 출현이 어떤 추상화 $\lambda x$ 의 본체 내에 위치하면, 해당 출현은 그 $\lambda x$ 에 의해 속박(Bound)된다.

자유 출현: 어떤 $\lambda x$ 에 의해서도 속박되지 않은 변수의 출현을 자유 출현이라 한다.

동일한 변수가 같은 항 내에서 자유 출현과 속박 출현을 동시에 가질 수 있다. 예를 들어, $(\lambda x. x) \; x$ 에서 첫 번째 $x$ (본체 내)는 속박 출현이고, 두 번째 $x$ (인자)는 자유 출현이다.

1.2 자유 변수 집합의 귀납적 정의

람다 항 $M$ 의 자유 변수 집합 $FV(M)$ :

$FV(x) = \{x\}$
$FV(\lambda x. M) = FV(M) \setminus \{x\}$
$FV(M \; N) = FV(M) \cup FV(N)$

구체적 예시

람다 항	자유 변수	속박 변수
$x$	$\{x\}$	$\emptyset$
$\lambda x. x$	$\emptyset$	$\{x\}$
$\lambda x. y$	$\{y\}$	$\{x\}$
$\lambda x. x \; y$	$\{y\}$	$\{x\}$
$(\lambda x. x) \; x$	$\{x\}$	$\{x\}$ (본체 내)
$\lambda x. \lambda y. x \; y \; z$	$\{z\}$	$\{x, y\}$
$(\lambda x. x \; y) \; (\lambda y. y)$	$\{y\}$	$\{x, y\}$

마지막 예시에서, 첫 번째 $y$ ( $\lambda x. x \; y$ 의 $y$ )는 자유 출현이고, 두 번째 $y$ ( $\lambda y. y$ 의 $y$ )는 속박 출현이다.

프로그래밍 언어에서의 대응

자유 변수와 속박 변수의 구분은 프로그래밍 언어의 유효 범위(Scope) 규칙에 직접 대응한다.

속박 변수 → 지역 변수(Local Variable): 함수 정의 내에서 선언되고, 함수의 본체 내에서만 유효하다.
자유 변수 → 비지역 변수(Non-Local Variable) 또는 전역 변수(Global Variable): 현재 함수 정의 외부에서 정의된 변수로, 클로저(Closure)를 통해 참조된다.

알파 변환(α-Conversion)

정의

알파 변환(Alpha Conversion, α-Conversion)은 추상화에서 속박 변수의 이름을 다른 이름으로 일관되게 변경하는 연산이다. 알파 변환은 람다 항의 의미를 변화시키지 않으며, 변환 전후의 항은 알파 동치(Alpha Equivalent, $\equiv_\alpha$ )로 간주된다.

형식적으로:

$\lambda x. M \rightarrow_\alpha \lambda y. M[x := y]$

단, $y$ 는 $M$ 에서 자유롭지 않아야 한다( $y \notin FV(M)$ ). 이 조건은 이름 변경이 기존의 자유 변수를 의도치 않게 속박하는 변수 포획(Variable Capture)을 방지한다.

1.3 알파 동치의 예시

$\lambda x. x \equiv_\alpha \lambda y. y \equiv_\alpha \lambda z. z$

세 항은 모두 항등 함수를 나타내며, 매개변수의 이름만 다르다.

$\lambda x. \lambda y. x \; y \equiv_\alpha \lambda a. \lambda b. a \; b$

두 항은 모두 “첫 번째 인자를 두 번째 인자에 적용하는 함수“를 나타낸다.

1.4 변수 포획의 문제

알파 변환에서 변수 포획 방지 조건이 왜 필요한지를 예시로 설명한다.

$\lambda x. x \; y$ 에서 $x$ 를 $y$ 로 변경하면 $\lambda y. y \; y$ 가 된다. 원래 항에서 두 번째 $y$ 는 자유 변수였으나, 변경 후에는 $\lambda y$ 에 의해 속박되어 버린다. 이로 인해 항의 의미가 변한다:

원래 항 $\lambda x. x \; y$ : 입력 $x$ 를 자유 변수 $y$ 에 적용
변경 후 $\lambda y. y \; y$ : 입력 $y$ 를 자기 자신에 적용 (자기 적용)

두 항의 의미가 완전히 달라졌으므로, 이 변경은 올바른 알파 변환이 아니다.

1.5 변수 포획 방지

알파 변환 시 새 변수 이름은 다음의 조건을 만족해야 한다:

$y \notin FV(M)$ : 새 변수 $y$ 가 본체 $M$ 에서 자유 출현하지 않아야 한다.
$y$ 는 $M$ 내의 다른 속박 변수와 충돌하지 않는 것이 바람직하다(필수는 아니지만 명확성을 위해 권장).

이 조건을 만족하는 변수를 신선 변수(Fresh Variable)라 한다.

2. 드 브라윈 인덱스(De Bruijn Index)

2.1 동기

알파 변환의 필요성은 변수의 이름(Name)에 의존하는 표기법의 불편함에서 기인한다. 이름 기반 표기에서는 동일한 함수가 매개변수 이름에 따라 다르게 표기되며, 대입 시 변수 포획을 회피하기 위한 알파 변환이 반복적으로 필요하다.

2.2 드 브라윈 인덱스의 정의

드 브라윈(Nicolaas Govert de Bruijn)은 1972년 변수에 이름 대신 자연수 인덱스를 부여하는 무명(Nameless) 표기법을 제안하였다. 속박 변수의 인덱스는 해당 변수를 속박하는 $\lambda$ 까지의 거리(중첩 $\lambda$ 의 수)를 나타낸다.

예시:

$\lambda x. x$ → $\lambda. 0$ (변수가 가장 가까운 $\lambda$ 에 속박, 거리 0)
$\lambda x. \lambda y. x$ → $\lambda. \lambda. 1$ (변수가 두 번째로 가까운 $\lambda$ 에 속박, 거리 1)
$\lambda x. \lambda y. x \; y$ → $\lambda. \lambda. 1 \; 0$

2.3 드 브라윈 인덱스의 이점

드 브라윈 인덱스에서는 알파 동치인 항이 동일한 표현을 갖는다:

$\lambda x. x = \lambda y. y = \lambda z. z \quad \text{모두} \quad \lambda. 0$

따라서 알파 변환이 불필요해지며, 항의 동치 판정이 단순한 문자열 비교로 환원된다. 이 이점 때문에 드 브라윈 인덱스는 컴퓨터에 의한 람다 항의 처리(정리 증명기, 컴파일러 등)에서 널리 사용된다.

자유 변수와 속박 변수 구분의 이론적 의의

자유 변수와 속박 변수의 구분, 그리고 알파 변환은 다음의 이론적 의의를 갖는다.

첫째, 추상화의 본질: 속박 변수는 함수의 매개변수이며, 그 이름은 관례에 불과하다. 알파 동치는 이 관례적 성격을 형식적으로 포착한다.

둘째, 대입의 정확성: 베타 축약(Beta Reduction)에서의 대입이 의미론적으로 올바르게 수행되려면, 변수 포획을 방지해야 한다. 알파 변환은 이를 보장하는 기제이다.

셋째, 프로그래밍 언어의 유효 범위: 현대 프로그래밍 언어에서 변수의 유효 범위(Lexical Scope) 규칙은 자유 변수와 속박 변수의 구분에 직접 기반한다.