람다 대수(Lambda Calculus)는 함수 추상화와 적용만으로 모든 계산을 표현하는 형식 체계다. 처치(Alonzo Church)가 1930년대 창안했으며 함수형 프로그래밍의 이론적 토대다.
기본 문법
항(Term):
e ::= x (변수)
| λx. e (추상, 람다 추상)
| e₁ e₂ (적용)
예:
λx. x (항등 함수)
λf. λx. f x (함수 적용)
λx. λy. x (상수 함수, K 컴비네이터)
β-환원 (Beta Reduction)
(λx. e) v →_β e[x := v]
(변수 x를 값 v로 치환)
예:
(λx. x + 1) 3
→ 3 + 1
→ 4
정규 순서(Normal Order): 가장 바깥/왼쪽 환원자 먼저
적용 순서(Applicative Order): 인자 먼저 환원 (대부분의 언어)
처치-로서 정리: 정규형이 존재하면 정규 순서로 도달 가능
자유 변수와 바인딩
자유 변수 FV:
FV(x) = {x}
FV(λx. e) = FV(e) - {x}
FV(e₁ e₂) = FV(e₁) ∪ FV(e₂)
α-변환: λx.x ≡ λy.y (바인딩 변수 이름 변경)
η-변환: λx. f x ≡ f (x ∉ FV(f) 일 때)
Y 컴비네이터
재귀를 명시적 자기 참조 없이 구현.
Y = λf. (λx. f (x x)) (λx. f (x x))
Y f = f (Y f) (고정점)
-- Haskell 버전 (lazy evaluation 필요)
y :: (a -> a) -> a
y f = let x = f x in x
-- 팩토리얼 예시
fact = Y (\self n -> if n == 0 then 1 else n * self (n-1))
fact 5 -- 120
처치 인코딩
자연수, 불리언을 람다 항으로 인코딩.
처치 숫자:
0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
n = λf. λx. fⁿ x
SUCC = λn. λf. λx. f (n f x)
ADD = λm. λn. λf. λx. m f (n f x)
MULT = λm. λn. λf. m (n f)
처치 불리언:
TRUE = λx. λy. x
FALSE = λx. λy. y
IF = λb. λt. λf. b t f
AND = λp. λq. p q p
OR = λp. λq. p p q
관련 개념
