무타입 $\lambda$-대수 (Untyped Lambda Calculus)
1. 개요
무타입 $\lambda$-대수(Untyped Lambda Calculus)는 알론조 처치(Alonzo Church)가 1930년대에 제안한 함수 정의, 함수 적용, 그리고 변수 바인딩을 다루는 형식 체계로, [계산 가능성]을 연구하기 위한 수학적 모델이자 현대 함수형 프로그래밍 언어의 이론적 기초가 되는 체계이다.
2. 기본 문법과 정의
$\lambda$-대수에서는 모든 것이 '함수'로 취급된다. $\lambda$-식(Lambda Term)은 다음과 같은 세 가지 기본 규칙에 의해 재귀적으로 정의된다.
2.1. 구성 요소
- 변수 (Variable): $x, y, z$와 같이 식별자로 표현되는 값이다.
- 추상화 (Abstraction): 함수를 정의하는 과정이다. $\lambda x. M$으로 표기하며, 이는 "입력 $x$를 받아 식 $M$을 반환하는 함수"를 의미한다. 여기서 $x$는 바인딩 변수(Bound Variable)가 된다.
- 적용 (Application): 정의된 함수에 인자를 전달하는 과정이다. $(M N)$으로 표기하며, 함수 $M$에 인자 $N$을 적용함을 의미한다.
2.2. 변수의 구분
$\lambda$-식 내에서 변수는 그 상태에 따라 두 가지로 구분된다.
- 결합 변수 (Bound Variable): $\lambda$ 추상화에 의해 범위가 지정된 변수이다. 예를 들어 $\lambda x. x$에서 $x$는 결합 변수이다.
- 자유 변수 (Free Variable): 어떤 $\lambda$ 추상화에 의해서도 묶이지 않은 변수이다. 예를 들어 $\lambda x. y$에서 $x$는 결합 변수이지만, $y$는 자유 변수이다.
3. 계산 및 축약 규칙
$\lambda$-대수에서의 계산은 식을 더 단순한 형태로 변형하는 '축약(Reduction)' 과정을 통해 이루어진다.
3.1. $\alpha$-변환 ($\alpha$-conversion)
변수의 이름이 바뀌어도 함수의 의미는 변하지 않는다는 원칙이다. 이는 변수 이름의 충돌(Name Clash)을 방지하기 위해 사용된다.
- 예시: $\lambda x. x \equiv \lambda y. y$
3.2. $\beta$-축약 ($\beta$-reduction)
함수 적용의 핵심 규칙으로, 함수의 인자 자리에 실제 값을 대입하는 과정이다. $(\lambda x. M) N$ 형태의 식에서 $M$ 내의 모든 결합 변수 $x$를 $N$으로 치환한다.
주의: 변수 포착(Variable Capture) 문제
단순히 치환을 수행할 때, 치환되는 식 $N$에 포함된 자유 변수가 $M$의 결합 변수와 이름이 같으면, 치환 후 해당 변수가 의도치 않게 묶이는 '변수 포착' 현상이 발생한다.
- 예시: $(\lambda x. \lambda y. x y) y$에서 $x$를 $y$로 단순히 치환하면 $\lambda y. y y$가 되어, 원래 자유 변수였던 $y$가 결합 변수로 바뀌어 의미가 변질된다.
- 해결책: 이를 방지하기 위해 $\beta$-축약 전 $\alpha$-변환을 통해 $M$의 결합 변수 이름을 $N$의 자유 변수와 겹치지 않게 변경해야 한다. (예: $\lambda y. x y \rightarrow \lambda z. x z$로 변경 후 치환 $\rightarrow \lambda z. y z$)
3.3. $\eta$-축약 ($\eta$-reduction)
함수의 외형적 중복을 제거하는 규칙이다. $\lambda x. (f x)$ 형태의 식이 있고 $x$가 $f$에서 자유 변수일 때, 이를 단순히 $f$로 축약할 수 있다. 이는 "함수 $f$에 $x$를 적용하는 함수는 결국 $f$ 그 자체와 같다"는 [외연성] 원리를 반영한다.
- 예시: $\lambda x. (f x) \rightarrow f$
3.4. 정규형과 정규화 전략
더 이상 축약할 수 없는 상태의 식을 정규형(Normal Form)이라고 한다. 정규형에 도달하기 위한 순서(전략)에 따라 결과의 수렴 여부가 달라질 수 있다.
| 전략 |
설명 |
특징 |
| 정상 순서 (Normal Order) |
가장 바깥쪽의 $\lambda$-적용을 먼저 수행 |
정규형이 존재한다면 반드시 찾아냄 (안전함) |
| 적용 순서 (Applicative Order) |
인자(내부 식)를 먼저 완전히 축약한 후 적용 |
계산 효율이 좋으나, 무한 루프에 빠질 위험이 있음 |
4. 처치 부호화 (Church Encoding)
무타입 $\lambda$-대수에는 기본 데이터 타입(정수, 불리언 등)이 없다. 따라서 모든 데이터를 함수들의 조합으로 표현하는데, 이를 처치 부호화라고 한다.
4.1. 처치 숫자 (Church Numerals)
자연수 $n$을 "함수를 $n$번 적용하는 [고차 함수]"로 정의한다.
- $0 \equiv \lambda f. \lambda x. x$
- $1 \equiv \lambda f. \lambda x. f x$
- $2 \equiv \lambda f. \lambda x. f (f x)$
- $n \equiv \lambda f. \lambda x. f^n(x)$
기본 연산: Successor (다음 수)
숫자 $n$을 받아 $n+1$을 만드는 함수 $\text{SUCC}$는 다음과 같이 정의된다.
- $\text{SUCC} \equiv \lambda n. \lambda f. \lambda x. f (n f x)$
- 작동 예시: $\text{SUCC } 1 \rightarrow (\lambda n. \lambda f. \lambda x. f (n f x)) (\lambda f. \lambda x. f x) \rightarrow \lambda f. \lambda x. f ((\lambda f. \lambda x. f x) f x) \rightarrow \lambda f. \lambda x. f (f x) \equiv 2$
4.2. 불리언 및 조건문
참과 거짓을 "두 개의 인자 중 하나를 선택하는 함수"로 정의한다.
| 개념 |
$\lambda$-식 표현 |
설명 |
| True |
$\lambda x. \lambda y. x$ |
첫 번째 인자를 선택 |
| False |
$\lambda x. \lambda y. y$ |
두 번째 인자를 선택 |
| IF |
$\lambda p. \lambda a. \lambda b. p a b$ |
조건 $p$가 True면 $a$, False면 $b$ 반환 |
5. 고정점 조합자와 재귀 (Fixed-point Combinators)
$\lambda$-대수의 함수는 이름이 없으므로(익명 함수), 자기 자신을 직접 호출하는 일반적인 재귀 정의가 불가능하다. 이를 해결하기 위해 고정점 조합자(Fixed-point Combinator)를 사용한다.
5.1. Y 조합자 (Y Combinator)
Y 조합자는 임의의 함수 $F$에 대해 $F(Y F) = Y F$를 만족하는 고정점을 찾아주는 특수한 함수이다.
- 정의식: $Y = \lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))$
작동 원리 (유도 과정):
$Y F$를 적용했을 때 어떻게 $F(Y F)$로 전개되는지 단계별로 살펴보면 다음과 같다.
1. $Y F = (\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))) F$
2. $f$ 자리에 $F$를 대입: $(\lambda x. F (x x)) (\lambda x. F (x x))$
3. 앞의 $(\lambda x. F (x x))$에 인자 $(\lambda x. F (x x))$를 적용:
- $x$ 자리에 $(\lambda x. F (x x))$를 대입 $\rightarrow F ((\lambda x. F (x x)) (\lambda x. F (x x)))$
4. 여기서 괄호 안의 $(\lambda x. F (x x)) (\lambda x. F (x x))$는 위 2번 단계의 $Y F$와 동일하다.
5. 따라서, $Y F = F (Y F)$ 가 성립한다.
5.2. 재귀 구현 원리
재귀 함수를 만들고 싶다면, 재귀 호출 부분을 인자로 받는 고차 함수 $F$를 정의한 뒤, 이를 $Y$ 조합자에 적용한다.
- 구조: $\text{RecursiveFunction} = Y F$
- 이를 통해 함수가 자기 자신의 복사본을 계속해서 생성하며 재귀적으로 동작하게 된다.
무타입 $\lambda$-대수는 튜링 기계(Turing Machine)와 계산 능력이 동등함이 증명되었으며, 이를 통해 [튜링 완전]한 체계임이 입증되었다. 즉, $\lambda$-대수로 표현 가능한 모든 계산은 알고리즘적으로 구현 가능하다.
6.1. 현대 언어에 미친 영향
- Lisp: $\lambda$-대수의 핵심 개념(고차 함수, 익명 함수)을 프로그래밍 언어에 최초로 도입한 언어 중 하나로, S-표현식과 함수적 프로그래밍의 기틀을 마련했다.
- Haskell / ML: 강타입 $\lambda$-대수(Typed Lambda Calculus)를 기반으로 하며, 순수 함수형 프로그래밍의 패러다임을 정립했다.
- 현대 범용 언어: Python의
lambda, JavaScript의 화살표 함수, Java의 람다식 등 대부분의 현대 언어들이 $\lambda$-대수의 추상화 개념을 채택하고 있다.
# 무타입 $\lambda$-대수 (Untyped Lambda Calculus)
## 1. 개요
무타입 $\lambda$-대수(Untyped Lambda Calculus)는 알론조 처치(Alonzo Church)가 1930년대에 제안한 함수 정의, 함수 적용, 그리고 변수 바인딩을 다루는 형식 체계로, [[계산 가능성]](Computability)을 연구하기 위한 수학적 모델이자 현대 함수형 프로그래밍 언어의 이론적 기초가 되는 체계이다.
## 2. 기본 문법과 정의
$\lambda$-대수에서는 모든 것이 '함수'로 취급된다. $\lambda$-식(Lambda Term)은 다음과 같은 세 가지 기본 규칙에 의해 재귀적으로 정의된다.
### 2.1. 구성 요소
1. **변수 (Variable)**: $x, y, z$와 같이 식별자로 표현되는 값이다.
2. **추상화 (Abstraction)**: 함수를 정의하는 과정이다. $\lambda x. M$으로 표기하며, 이는 "입력 $x$를 받아 식 $M$을 반환하는 함수"를 의미한다. 여기서 $x$는 바인딩 변수(Bound Variable)가 된다.
3. **적용 (Application)**: 정의된 함수에 인자를 전달하는 과정이다. $(M N)$으로 표기하며, 함수 $M$에 인자 $N$을 적용함을 의미한다.
### 2.2. 변수의 구분
$\lambda$-식 내에서 변수는 그 상태에 따라 두 가지로 구분된다.
- **결합 변수 (Bound Variable)**: $\lambda$ 추상화에 의해 범위가 지정된 변수이다. 예를 들어 $\lambda x. x$에서 $x$는 결합 변수이다.
- **자유 변수 (Free Variable)**: 어떤 $\lambda$ 추상화에 의해서도 묶이지 않은 변수이다. 예를 들어 $\lambda x. y$에서 $x$는 결합 변수이지만, $y$는 자유 변수이다.
## 3. 계산 및 축약 규칙
$\lambda$-대수에서의 계산은 식을 더 단순한 형태로 변형하는 '축약(Reduction)' 과정을 통해 이루어진다.
### 3.1. $\alpha$-변환 ($\alpha$-conversion)
변수의 이름이 바뀌어도 함수의 의미는 변하지 않는다는 원칙이다. 이는 변수 이름의 충돌(Name Clash)을 방지하기 위해 사용된다.
- **예시**: $\lambda x. x \equiv \lambda y. y$
### 3.2. $\beta$-축약 ($\beta$-reduction)
함수 적용의 핵심 규칙으로, 함수의 인자 자리에 실제 값을 대입하는 과정이다. $(\lambda x. M) N$ 형태의 식에서 $M$ 내의 모든 결합 변수 $x$를 $N$으로 치환한다.
**주의: 변수 포착(Variable Capture) 문제**
단순히 치환을 수행할 때, 치환되는 식 $N$에 포함된 자유 변수가 $M$의 결합 변수와 이름이 같으면, 치환 후 해당 변수가 의도치 않게 묶이는 '변수 포착' 현상이 발생한다.
- **예시**: $(\lambda x. \lambda y. x y) y$에서 $x$를 $y$로 단순히 치환하면 $\lambda y. y y$가 되어, 원래 자유 변수였던 $y$가 결합 변수로 바뀌어 의미가 변질된다.
- **해결책**: 이를 방지하기 위해 $\beta$-축약 전 $\alpha$-변환을 통해 $M$의 결합 변수 이름을 $N$의 자유 변수와 겹치지 않게 변경해야 한다. (예: $\lambda y. x y \rightarrow \lambda z. x z$로 변경 후 치환 $\rightarrow \lambda z. y z$)
### 3.3. $\eta$-축약 ($\eta$-reduction)
함수의 외형적 중복을 제거하는 규칙이다. $\lambda x. (f x)$ 형태의 식이 있고 $x$가 $f$에서 자유 변수일 때, 이를 단순히 $f$로 축약할 수 있다. 이는 "함수 $f$에 $x$를 적용하는 함수는 결국 $f$ 그 자체와 같다"는 [[외연성]](Extensionality) 원리를 반영한다.
- **예시**: $\lambda x. (f x) \rightarrow f$
### 3.4. 정규형과 정규화 전략
더 이상 축약할 수 없는 상태의 식을 **정규형(Normal Form)**이라고 한다. 정규형에 도달하기 위한 순서(전략)에 따라 결과의 수렴 여부가 달라질 수 있다.
| 전략 | 설명 | 특징 |
| :--- | :--- | :--- |
| **정상 순서 (Normal Order)** | 가장 바깥쪽의 $\lambda$-적용을 먼저 수행 | 정규형이 존재한다면 반드시 찾아냄 (안전함) |
| **적용 순서 (Applicative Order)** | 인자(내부 식)를 먼저 완전히 축약한 후 적용 | 계산 효율이 좋으나, 무한 루프에 빠질 위험이 있음 |
## 4. 처치 부호화 (Church Encoding)
무타입 $\lambda$-대수에는 기본 데이터 타입(정수, 불리언 등)이 없다. 따라서 모든 데이터를 함수들의 조합으로 표현하는데, 이를 처치 부호화라고 한다.
### 4.1. 처치 숫자 (Church Numerals)
자연수 $n$을 "함수를 $n$번 적용하는 [[고차 함수]](Higher-order function)"로 정의한다.
- $0 \equiv \lambda f. \lambda x. x$
- $1 \equiv \lambda f. \lambda x. f x$
- $2 \equiv \lambda f. \lambda x. f (f x)$
- $n \equiv \lambda f. \lambda x. f^n(x)$
**기본 연산: Successor (다음 수)**
숫자 $n$을 받아 $n+1$을 만드는 함수 $\text{SUCC}$는 다음과 같이 정의된다.
- $\text{SUCC} \equiv \lambda n. \lambda f. \lambda x. f (n f x)$
- **작동 예시**: $\text{SUCC } 1 \rightarrow (\lambda n. \lambda f. \lambda x. f (n f x)) (\lambda f. \lambda x. f x) \rightarrow \lambda f. \lambda x. f ((\lambda f. \lambda x. f x) f x) \rightarrow \lambda f. \lambda x. f (f x) \equiv 2$
### 4.2. 불리언 및 조건문
참과 거짓을 "두 개의 인자 중 하나를 선택하는 함수"로 정의한다.
| 개념 | $\lambda$-식 표현 | 설명 |
| :--- | :--- | :--- |
| **True** | $\lambda x. \lambda y. x$ | 첫 번째 인자를 선택 |
| **False** | $\lambda x. \lambda y. y$ | 두 번째 인자를 선택 |
| **IF** | $\lambda p. \lambda a. \lambda b. p a b$ | 조건 $p$가 True면 $a$, False면 $b$ 반환 |
## 5. 고정점 조합자와 재귀 (Fixed-point Combinators)
$\lambda$-대수의 함수는 이름이 없으므로(익명 함수), 자기 자신을 직접 호출하는 일반적인 재귀 정의가 불가능하다. 이를 해결하기 위해 **고정점 조합자(Fixed-point Combinator)**를 사용한다.
### 5.1. Y 조합자 (Y Combinator)
Y 조합자는 임의의 함수 $F$에 대해 $F(Y F) = Y F$를 만족하는 고정점을 찾아주는 특수한 함수이다.
- **정의식**: $Y = \lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))$
**작동 원리 (유도 과정)**:
$Y F$를 적용했을 때 어떻게 $F(Y F)$로 전개되는지 단계별로 살펴보면 다음과 같다.
1. $Y F = (\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x))) F$
2. $f$ 자리에 $F$를 대입: $(\lambda x. F (x x)) (\lambda x. F (x x))$
3. 앞의 $(\lambda x. F (x x))$에 인자 $(\lambda x. F (x x))$를 적용:
- $x$ 자리에 $(\lambda x. F (x x))$를 대입 $\rightarrow F ((\lambda x. F (x x)) (\lambda x. F (x x)))$
4. 여기서 괄호 안의 $(\lambda x. F (x x)) (\lambda x. F (x x))$는 위 2번 단계의 $Y F$와 동일하다.
5. 따라서, $Y F = F (Y F)$ 가 성립한다.
### 5.2. 재귀 구현 원리
재귀 함수를 만들고 싶다면, 재귀 호출 부분을 인자로 받는 고차 함수 $F$를 정의한 뒤, 이를 $Y$ 조합자에 적용한다.
- **구조**: $\text{RecursiveFunction} = Y F$
- 이를 통해 함수가 자기 자신의 복사본을 계속해서 생성하며 재귀적으로 동작하게 된다.
## 6. 튜링 완전성과 영향
무타입 $\lambda$-대수는 튜링 기계(Turing Machine)와 계산 능력이 동등함이 증명되었으며, 이를 통해 [[튜링 완전]](Turing Complete)한 체계임이 입증되었다. 즉, $\lambda$-대수로 표현 가능한 모든 계산은 알고리즘적으로 구현 가능하다.
### 6.1. 현대 언어에 미친 영향
- **Lisp**: $\lambda$-대수의 핵심 개념(고차 함수, 익명 함수)을 프로그래밍 언어에 최초로 도입한 언어 중 하나로, S-표현식과 함수적 프로그래밍의 기틀을 마련했다.
- **Haskell / ML**: 강타입 $\lambda$-대수(Typed Lambda Calculus)를 기반으로 하며, 순수 함수형 프로그래밍의 패러다임을 정립했다.
- **현대 범용 언어**: Python의 `lambda`, JavaScript의 화살표 함수, Java의 람다식 등 대부분의 현대 언어들이 $\lambda$-대수의 추상화 개념을 채택하고 있다.