람다 대수

람다 대수는 1930년대 수학자 알론조 처치에 의해 수학기초론 연구 과정에서 소개되었다. 처치는 1936년 결정 문제(Entscheidungsproblem)를 해결하기 위해 계산 가능성의 개념을 정의하는 수학적 모델로 이를 활용하였다. 초기 체계는 논리적 오류가 발견되기도 하였으나, 이후 계산과 관련된 부분만을 추출한 '유형 없는 람다 대수(untyped lambda calculus)'와 논리적 모순을 해결한 '단순 유형 람다 대수(simply typed lambda calculus)'로 발전하였다.

람다 대수의 항(term)은 변수, 추상화, 적용의 세 가지 요소를 통해 재귀적으로 정의된다.

• 변수(Variable): $x, y, z$와 같은 식별자이다.
• 추상화(Abstraction): $\lambda x. M$과 같이 표현하며, 변수 $x$를 인자로 받는 함수를 정의한다. 기호 $\lambda$는 함수 선언을 의미한다.
• 적용(Application): $M N$과 같이 표현하며, 함수 $M$에 인자 $N$을 적용하여 계산을 수행한다.

이 체계에서는 함수에 이름이 없는 익명 함수를 기본으로 하며, 여러 개의 인자를 받는 함수는 하나의 인자를 받아 또 다른 함수를 반환하는 방식인 커링(Currying)을 통해 표현한다.

람다 대수에는 항을 변형하고 계산하기 위한 주요 규칙이 존재한다.

1. 알파 동치($\alpha$-equivalence): 이름 충돌을 방지하기 위해 묶인 변수의 이름을 변경하는 규칙이다. 예를 들어 $\lambda x. x$와 $\lambda y. y$는 동일한 함수로 간주한다.
2. 베타 축약($\beta$-reduction): 함수 적용을 실제 치환 연산으로 대신하는 과정이다. $(\lambda x. M) N$을 $M$ 내부의 $x$를 $N$으로 치환한 결과로 변환한다.
3. 에타 변환($\eta$-conversion): 두 함수가 모든 인자에 대해 동일한 결과를 내면 두 함수를 같다고 보는 외연성의 개념을 다룬다.

베타 축약을 통해 더 이상 축약할 수 없는 상태에 도달하면 이를 '정규형(normal form)'이라고 한다. 처치-로서 정리에 따르면, 정규형이 존재할 경우 그 결과는 유일하다.

람다 대수는 앨런 튜링의 튜링 기계와 계산 능력이 동일하다는 사실이 증명되었다. 이는 람다 대수로 표현 가능한 모든 함수가 계산 가능하다는 것을 의미한다. 람다 대수 내에서는 자연수(처치 수), 불(Boolean) 진릿값, 산술 연산, 조건문, 재귀 함수 등을 모두 함수 형태로 부호화하여 표현할 수 있다.

현대 컴퓨터 과학에서 람다 대수는 리스프(Lisp), 하스켈(Haskell), ML 등 함수형 프로그래밍 언어의 이론적 근간이 된다. 또한 프로그래밍 언어의 의미론 연구와 자료형 이론(Type Theory)의 발전에도 핵심적인 역할을 수행한다.