람다 대수

람다 대수(λ -, lambda -)는 이론 컴퓨터과학 및 수리논리학에서 함수 정의, 함수 적용, 귀납적 함수를 추상화한 형식 체계이다. 1930년대 알론조 처치가 수학기초론을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 타입 없는 람다 대수 (untyped lambda calculus)라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 타입 람다 대수 (simply typed lambda calculus)를 도입하였다.

람다 대수는 계산 이론, 언어학 등에 중요한 역할을 하며, 특히 프로그래밍 언어 이론의 발전에 크게 기여했다. 리스프와 같은 함수형 프로그래밍 언어는 람다 대수로부터 직접적인 영향을 받아 탄생했으며, 단순 타입 람다 대수는 현대 프로그래밍 언어의 타입 이론의 기초가 되었다.

함수의 표현

함수는 컴퓨터 과학과 수학의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다.

예를 들어 항등 함수 $I(x)=x$ 는 하나의 입력 $x$를 받아 다시 $x$를 결과로 내놓는다. 한편 함수 $s(x,y)=x\times x+y\times y$ 는 입력 $x$와 $y$를 받아 두 수의 제곱의 합을 내놓는다. 두 가지 예제로부터 세 가지 유용한 사실을 알아낼 수 있다.

첫 번째는 함수가 꼭 이름을 가질 필요는 없다는 것이다. 함수 $s$는 이름을 제거하고 $(x,y)\mapsto x\times x+y\times y$ 와 같은 형태로 쓸 수 있다. 또한 항등 함수 $I(x)=x$는 $x\mapsto x$ 의 형태로 쓸 수 있다.

두 번째는 함수의 입력 변수의 이름 또한 필요 없다는 것이다. $x\mapsto x$ 와 $y\mapsto y$ 는 변수의 이름은 다르지만 같은 항등 함수를 의미한다. 또한 $(x,y)\mapsto x\times x+y\times y$ 와 $(u,v)\mapsto u\times u+v\times v$ 는 같은 함수를 나타낸다.

마지막으로, 두 개나 그 이상의 입력을 받는 함수는 하나의 입력을 받아 또다른 함수를 출력하는 함수로 다시 쓸 수 있다는 것이다. 예를 들어, $(x,y)\mapsto x\times x+y\times y$ 는 $x\mapsto (y\mapsto x\times x+y\times y)$ 와 같은 형태로 다시 쓸 수 있다. 함수를 이와 같이 변환하는 것을 커리잉 (currying)이라고 한다. 이 함수는 다음과 같이 이해할 수 있다.

$(x\mapsto (y\mapsto x\times x+y\times y))(5)(2)$
$=(y\mapsto 5\times 5+y\times y)(2)$
$=5\times 5+2\times 2$

타입 없는 람다 대수

타입 없는 람다 대수는 이와 같은 고찰을 바탕으로 함수를 다음과 같은 형식으로 다시 표현한다.

$\lambda$ 변수 $.$ 수식

위에서 살펴본 항등함수 $I$는 람다 대수로 표현하면 $\lambda x.x$ 가 되고, 제곱의 합을 구하는 함수 $s$는 $\lambda xy.x\times x+y\times y$ 가 된다.

함수를 실제로 계산하는 것은 베타 축약이라는 과정을 통해 이루어진다. 베타 축약은 다음과 같은 규칙을 갖는다.

$(\lambda V.E)E'$: 수식 $E$에서 모든 변수 $V$를 수식 $E'$으로 대치한다.

예를 들어 입력값 $n$에 대해 수식 $E=n\times 2$를 리턴하는 함수 $(\lambda n.n\times 2)$가 있다고 하자. 이 함수에 입력 $E'=7$을 적용하는 과정은 $(\lambda n.n\times 2)7\rightarrow 7\times 2$와 같이 수식 내의 모든 $n$을 7로 치환한 것으로 표현할 수 있다. 이와 같이 치환 등을 통해 수식을 축약하는 것을 베타 축약이다.