4.7 에타 변환(η-conversion)과 함수 외연성

1. 에타 변환의 정의

에타 변환(Eta Conversion, η-conversion)은 람다 대수에서 함수의 외연적 동등성(Extensional Equality)을 포착하는 변환 규칙이다.

1.1 에타 축약(η-reduction)

$\lambda x. (M \; x) \rightarrow_\eta M \quad \text{단, } x \notin FV(M)$

$x$ 가 $M$ 의 자유 변수가 아닐 때, $\lambda x. (M \; x)$ 는 $M$ 과 동일한 함수를 나타낸다. 왜냐하면 임의의 인자 $N$ 에 대해:

$(\lambda x. (M \; x)) \; N \rightarrow_\beta M \; N$

이므로, $\lambda x. (M \; x)$ 와 $M$ 은 모든 입력에 대해 동일한 결과를 산출한다.

1.2 에타 확장(η-expansion)

에타 축약의 역방향:

$M \rightarrow_\eta \lambda x. (M \; x) \quad \text{단, } x \notin FV(M)$

에타 확장은 임의의 함수적 표현을 명시적 추상화 형태로 변환한다.

함수의 외연성(Extensionality)

외연성 원리

함수의 외연성 원리(Principle of Extensionality)는 다음과 같이 진술된다:

두 함수 $f$ 와 $g$ 가 모든 인자에 대해 동일한 결과를 산출하면, $f$ 와 $g$ 는 동일하다.

$(\forall x. \; f \; x = g \; x) \implies f = g$

이 원리는 함수를 입력-출력 대응(Input-Output Mapping)으로 동일시하는 관점이다. 함수의 “내부 구조“가 아니라 “외부 행동“에 의해 함수의 정체성이 결정된다.

1.3 내포성 대 외연성

내포적 동등성(Intensional Equality): 두 함수가 동일한 정의(Definition)를 가질 때 동등하다고 판단한다. 동일한 입출력 관계를 가지더라도 정의가 다르면 다른 함수로 간주한다. 예를 들어, $\lambda x. x + x$ 와 $\lambda x. 2 \times x$ 는 내포적으로 다르다.

외연적 동등성(Extensional Equality): 두 함수가 모든 입력에 대해 동일한 출력을 산출하면 동등하다고 판단한다. $\lambda x. x + x$ 와 $\lambda x. 2 \times x$ 는 외연적으로 동등하다.

에타 변환은 외연적 동등성의 한 측면을 람다 대수 내에서 형식적으로 포착한다.

2. 에타 변환의 예시

2.1 기본 예시

$\lambda x. (\text{succ} \; x) \rightarrow_\eta \text{succ}$

$\text{succ}$ 가 후자 함수(Successor Function)일 때, $\lambda x. (\text{succ} \; x)$ 는 $\text{succ}$ 와 외연적으로 동등하다. 에타 축약에 의해 불필요한 추상화를 제거할 수 있다.

$\lambda f. \lambda x. (f \; x) \rightarrow_\eta \lambda f. f \rightarrow_\eta \mathbf{I}$

여기서 $\mathbf{I} = \lambda f. f$ 는 항등 함수이다.

2.2 조건 확인의 중요성

$\lambda x. (x \; x) \not\rightarrow_\eta x$

여기서 $M = x$ 이고, $x \in FV(M) = \{x\}$ 이므로 에타 축약의 조건 $x \notin FV(M)$ 을 위반한다. 이 축약은 허용되지 않는다.

이 조건이 필수적인 이유: $\lambda x. (x \; x)$ 는 자기 적용 함수로서, 자유 변수 $x$ 자체와는 전혀 다른 함수이다.

에타 동치(η-equivalence)

정의

에타 동치는 에타 변환(에타 축약과 에타 확장 모두)에 의해 연결되는 항들의 동등 관계이다.

$M =_\eta N \iff M \text{과 } N \text{이 에타 변환의 열에 의해 연결됨}$

2.3 베타-에타 동치(βη-equivalence)

실제로 람다 대수에서 가장 일반적으로 사용되는 동등 관계는 베타 변환과 에타 변환을 모두 포함하는 베타-에타 동치( $=_{\beta\eta}$ )이다. 두 람다 항 $M$ 과 $N$ 이 베타-에타 동치라 함은, 베타 축약, 에타 축약, 그리고 이들의 역방향(베타 확장, 에타 확장)의 유한 열에 의해 $M$ 에서 $N$ 에 도달 가능함을 의미한다.

3. 에타 변환과 프로그래밍

3.1 포인트프리 스타일(Point-Free Style)

에타 축약은 함수형 프로그래밍에서 포인트프리 스타일(Point-Free Style) 또는 암묵적 프로그래밍(Tacit Programming)의 이론적 기반이다. 포인트프리 스타일에서는 함수의 인자를 명시적으로 기술하지 않고, 함수의 합성으로만 프로그램을 작성한다.

예: Haskell에서

-- 포인트풀 스타일
f x = g (h x)
-- 포인트프리 스타일 (에타 축약 적용)
f = g . h

$f = \lambda x. g \; (h \; x)$ 에서 에타 축약을 적용하면(적절한 변환 후) $f = g \circ h$ 가 된다.

3.2 부분 적용(Partial Application)

에타 확장은 부분 적용(Partial Application)의 형식적 기반이다. 이항 함수 $f$ 에 하나의 인자만 제공하여 단항 함수를 생성하는 것은 에타 확장의 역으로 해석된다.

4. 에타 변환과 범주론

범주론(Category Theory)적 관점에서, 에타 변환은 카르테시안 폐쇄 범주(Cartesian Closed Category)에서 지수 대상(Exponential Object)의 보편 성질(Universal Property)에 대응한다. 구체적으로, 에타 축약은 함수 적용(Evaluation)과 커링(Currying) 사이의 수반(Adjunction) 관계를 반영한다.

에타 변환은 람다 대수에서 함수의 외연적 동등성을 포착하는 규칙이며, 함수형 프로그래밍에서의 코드 단순화, 최적화, 추상화의 이론적 기반을 제공한다.