4.3 람다 대수(Lambda Calculus)의 구문론적 정의

1. 람다 대수의 개관

람다 대수(Lambda Calculus)는 처치(Alonzo Church)가 1932–1936년에 개발한 형식적 계산 체계로서, 함수의 정의(Function Definition)와 함수의 적용(Function Application)만을 기본 연산으로 사용한다. 람다 대수는 수학적으로 가능한 가장 단순한 프로그래밍 언어로 간주되며, 함수형 프로그래밍(Functional Programming)의 이론적 기반이다.

순수 람다 대수(Pure Lambda Calculus)는 자연수, 불 값, 조건문, 반복문 등의 기본 데이터 유형이나 제어 구조를 포함하지 않으며, 오직 함수만을 다룬다. 그럼에도 불구하고 이 체계는 튜링 완전(Turing Complete)하며, 임의의 계산 가능 함수를 표현할 수 있다.

2. 람다 항(Lambda Term)의 구문론적 정의

람다 대수의 표현을 람다 항(Lambda Term) 또는 람다 식(Lambda Expression)이라 한다. 람다 항은 다음의 귀납적(Inductive) 정의에 의해 생성된다.

2.1 BNF 문법

람다 항의 집합 \Lambda는 변수(Variable)의 가산 무한 집합 \mathcal{V} = \{x, y, z, x_1, x_2, \ldots\}에 대해 다음의 BNF(Backus-Naur Form) 문법으로 정의된다:

M ::= x \mid (\lambda x. M) \mid (M \; M)

여기서 x \in \mathcal{V}이다.

세 가지 구성 형태

1. 변수(Variable): x \in \mathcal{V}

변수는 람다 대수의 원자적(Atomic) 표현이다. 변수는 값의 이름(Name)을 나타내며, 다른 람다 항에 의해 대체(Substitution)될 수 있는 자리표시자(Placeholder) 역할을 한다.

2. 추상(Abstraction): (\lambda x. M)

추상은 함수의 정의를 나타낸다. \lambda는 함수 정의 기호이고, x는 매개변수(Parameter, 또는 속박 변수, Bound Variable)이며, M은 함수의 본체(Body)이다.

(\lambda x. M)은 “입력 x를 받아 M을 계산하는 함수“를 나타낸다. 예를 들어:

• \lambda x. x: 항등 함수(Identity Function). 입력을 그대로 반환한다.
• \lambda x. \lambda y. x: 두 인자 중 첫 번째를 반환하는 함수.

3. 적용(Application): (M \; N)

적용은 함수 M에 인자(Argument) N을 적용하는 것을 나타낸다. (M \; N)은 “함수 M을 인자 N에 적용한 결과“이다. 예를 들어:

• ((\lambda x. x) \; y): 항등 함수에 y를 적용. 결과는 y.

구문론적 관례(Syntactic Conventions)

표기의 간결성을 위해 다음의 관례가 사용된다.

괄호의 생략

최외곽 괄호를 생략한다: (\lambda x. M)을 \lambda x. M으로, (M \; N)을 M \; N으로 표기한다.

적용의 좌결합성(Left Associativity)

적용은 좌결합적이다: M \; N \; P는 ((M \; N) \; P)로 해석된다. 즉, 적용은 왼쪽에서 오른쪽으로 순차적으로 수행된다.

추상의 본체 확장

\lambda 기호의 본체는 가능한 한 오른쪽으로 확장된다: \lambda x. M \; N은 \lambda x. (M \; N)으로 해석된다. 즉, (\lambda x. M) \; N이 아니다.

연속 추상의 축약

\lambda x. \lambda y. \lambda z. M을 \lambda xyz. M으로 축약한다.

자유 변수와 속박 변수

속박 변수(Bound Variable)

추상 \lambda x. M에서 변수 x는 속박 변수이다. x는 M 내에서 \lambda x에 의해 “속박(Bound)“되어 있으며, 함수의 매개변수 역할을 한다.

자유 변수(Free Variable)

어떤 \lambda 추상에 의해서도 속박되지 않는 변수를 자유 변수(Free Variable)라 한다. 람다 항 M의 자유 변수 집합 FV(M)은 다음과 같이 귀납적으로 정의된다:

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

예를 들어:

• FV(\lambda x. x \; y) = \{y\}: x는 속박, y는 자유.
• FV(\lambda x. \lambda y. x \; y \; z) = \{z\}: x, y는 속박, z는 자유.

2.2 폐쇄 항(Closed Term, Combinator)

자유 변수가 없는 람다 항, 즉 FV(M) = \emptyset인 항을 폐쇄 항(Closed Term) 또는 결합자(Combinator)라 한다. 폐쇄 항은 자기 완결적(Self-Contained)이며, 외부 환경에 의존하지 않는다.

중요한 결합자의 예:

• \mathbf{I} = \lambda x. x (항등 결합자, Identity)
• \mathbf{K} = \lambda x. \lambda y. x (상수 결합자, Constant)
• \mathbf{S} = \lambda x. \lambda y. \lambda z. x \; z \; (y \; z) (대입 결합자, Substitution)

\mathbf{S}와 \mathbf{K}만으로 모든 폐쇄 람다 항을 표현할 수 있으며(\mathbf{SK} 기저), 이는 \{\mathbf{S}, \mathbf{K}\}가 결합자 논리(Combinatory Logic)에서 기능적으로 완전함을 의미한다.

3. 알파 동치(Alpha Equivalence)

속박 변수의 이름은 의미론적으로 무관하다. 속박 변수의 이름만이 다른 두 람다 항은 알파 동치(Alpha Equivalent)라 하며, 동일한 항으로 간주한다.

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

형식적으로, \lambda x. M에서 M 내의 x의 모든 자유 출현(Free Occurrence)을 새로운 변수 y(M에서 자유롭지 않은)로 일관되게 대체한 \lambda y. M[x := y]는 원래 항과 알파 동치이다.

알파 동치는 프로그래밍 언어에서 변수의 이름 변경(Renaming)이 프로그램의 의미를 변화시키지 않는 것에 대응한다.

대입(Substitution)

대입(Substitution) M[x := N]은 람다 항 M 내의 변수 x의 모든 자유 출현을 람다 항 N으로 대체하는 연산이다. 대입은 다음과 같이 귀납적으로 정의된다:

x[x := N] = N
y[x := N] = y \quad (y \neq x)
(\lambda x. M)[x := N] = \lambda x. M \quad (x\text{는 속박되므로 대체하지 않음})
(\lambda y. M)[x := N] = \lambda y. (M[x := N]) \quad (y \neq x \text{ 이고 } y \notin FV(N))
(M_1 \; M_2)[x := N] = (M_1[x := N]) \; (M_2[x := N])

y \in FV(N)인 경우, 대입 전에 알파 변환(Alpha Conversion)을 수행하여 변수 포획(Variable Capture)을 방지해야 한다.

4. 람다 항의 구문 트리

람다 항은 추상 구문 트리(Abstract Syntax Tree, AST)로 표현된다. 트리의 잎(Leaf) 노드는 변수이고, 내부 노드는 추상(\lambda) 또는 적용(@)이다.

예: \lambda x. x \; y의 구문 트리:

  λx
   |
   @
  / \
 x   y

구문 트리는 람다 항의 구조를 모호하지 않게 표현하며, 컴파일러와 인터프리터에서 람다 항의 내부 표현으로 사용된다.

람다 대수의 구문론적 정의는 변수, 추상, 적용이라는 세 가지 구성 형태만으로 튜링 완전한 계산 체계를 구축하며, 이 극도의 단순성이 람다 대수의 이론적 분석력과 실용적 표현력의 기반이다.