람다 대수

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

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

설명과 적용

람다 대수는 임의의 튜링 기계 (Turing machine)를 시뮬레이션 할 수 있는 보편적인 계산 모델로서 튜링 완전 (Turing complete)하다. 이름에 관하여는, 람다 표현식과 람다 항목 의 람다는 그리스 문자 람다 (λ)로서 어떤 함수 내에 어떤 변수를 종속 시키는 것을 나타내기 위하여 이용된다.

람다 대수는 수학, 철학, 언어학, and 컴퓨터 과학. 등의 여러 분야에 적용될 수 있다. 람다 대수는 프로그래밍 언어 이론의 발달에 중요한 역할을 했다. 람다 대수는 함수형 프로그래밍을 사용하여 구현된다. 또한, 람다 대수는 현재 범주론의 연구 토픽에 포함된다.

수학사에서 람다 대수

람다 대수는 알론조 처치에 의해 1930년대 소개됐다. 최초의 시스템은 스테펜 클리네와 존 버클리 로서가 클리네-로저 역설을 제창하면서 1935년 논리적 결점을 보이기 위해 도입됐다. 그 후인 1936년 처치는 독립적으로 현재에는 타입 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다. 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 단순 타입 람다 대수이다.

함수의 표현

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

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

1. 함수가 반드시 이름을 가질 필요는 없다. 함수 $s$는 이름을 제거하고 $(x,y)\mapsto x\times x+y\times y$ 와 같은 형태로 쓸 수 있다. 또한 항등 함수 $I(x)=x$는 $x\mapsto x$ 의 형태로 쓸 수 있다.
2. 함수의 입력 변수의 이름 또한 필요 없다. $x\mapsto x$ 와 $y\mapsto y$ 는 변수의 이름은 다르지만 같은 항등 함수를 의미한다. 또한 $(x,y)\mapsto x\times x+y\times y$ 와 $(u,v)\mapsto u\times u+v\times v$ 는 같은 함수를 나타낸다.
3. 두 개 이상의 입력을 받는 함수는 하나의 입력을 받아 또다른 함수를 출력하는 함수로 다시 쓸 수 있다. 예를 들어, $(x,y)\mapsto x\times x+y\times y$ 는 $x\mapsto (y\mapsto x\times x+y\times y)$ 와 같은 형태로 다시 쓸 수 있다. 함수를 이와 같이 변환하는 것을 커링 (currying)이라고 한다. 위의 함수 $s(x,y)$는 다음과 같이 단일 입력 함수를 두 번 적용하는 것으로 이해할 수 있다.

$(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 x.t$는 단일 입력 $x$를 받아 $t$의 표현으로 치환하는 익명의 함수를 지칭한다. 예를 들어 $\lambda x.x^{2}+2$는 함수 $f(x)=x^{2}+2$의 람다 추상화이다. 람다 추상화를 통해 함수를 정의한다는 것은 함수를 정의하기만 하고 함수를 수행(호출)하지는 않는다는 것을 의미한다. 람다 추상화를 통해 변수 $x$는 표현 $t$에 속박된다.

자유 변수

자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.

• $x$의 자유 변수는 $x$뿐이다.
• $\lambda x.t$의 자유변수는 $x$를 제외하고 $t$에 등장하는 변수들이다.
• 두 표현 $t$와 $s$의 결합 $ts$의 자유변수의 집합은 $t$의 자유변수의 집합과 $s$의 자유변수의 집합의 합집합이다.

예를 들어, $\lambda x.x$에는 자유 변수가 없지만, $\lambda x.x+y$에는 자유변수가 $y$ 하나이다.

축약

람다 대수식의 의미는 식이 어떻게 축약될 수 있는지에 따라 정의된다. 람다 대수식 축약에는 세 가지가 있다.

• 알파-변환(α-conversion): 속박 변수를 바꿈
• 베타-축약(β-reduction): 식의 인수에 함수를 적용
• 에타-변환(η-conversion): 외연성을 통해 축약 (겉으로 보이는 행동이 같은 함수는 동일 함수로 간주함)

베타-축약을 통해 같은 식으로 변환되면 베타-동치(β-equivalent)라 부른다. 다른 축약도 마찬가지로 각각 알파-동치(α-equivalent), 에타-동치(η-equivalent)로 정의된다. 축약할 수 있는 식(reducible expression)을 줄여서 redex라고 부른다.

알파-변환

알파-리네이밍(alpha-renaming)이라고 불리기도 하는 알파-변환은 속박 변수의 이름이 바뀌는 것을 허용한다. 예를 들어, $\lambda x.x$가 $\lambda y.y$로 바뀌어도 알파-동치이다. 알파-변환은 일반적으로 동치임을 확인하기 위해 사용된다. 정확한 알파-변환의 규칙은 완전히 사소하지 않다. 첫 번째로 추상화로 알파-변환을 수행할 때, 한 변수는 같은 추상화에 속한 경우만 새롭게 이름 붙일 수 있다. 예를 들어, $\lambda x.\lambda x.x$의 알파-변환은 $\lambda y.\lambda x.x$가 될 수 있으나, $\lambda y.\lambda x.y$은 될 수 없다. 두 번째로 다른 추상화에 의해 변수가 캡쳐되어 있을 경우 알파-변환을 할 수 없다. 예를 들어, $\lambda x.\lambda y.x$은 $\lambda y.\lambda y.y$로 알파-변환될 수 없다. 정적인 스코프를 가지는 프로그래밍 언어에서, 알파-변환은 이름 없는 변수의 이름을 해당 변수를 포함하는 스코프에서 결정하는 이름 분석(name resolution)을 통해 변수의 이름을 결정할 수 있다.

치환

$E[V:=R]$ 형태로 쓰여지는 치환은 변수 $V$를 식 $R$과 함께 $E$에 대입하는 과정이다. 치환은 다음과 같은 성질을 가진다. x와 y는 변수, M과 N은 λ 형태의 식이다.

x[x := N] ≡ N

y[x := N] ≡ y (만약 x ≠ y 일 경우,)

(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])

(λx.M)[x := N] ≡ λx.M

(λy.M)[x := N] ≡ λy.(M[x := N]) (만약 x ≠ y 이고, y ∉ FV(N) 일 경우,)

람다 추상화에 치환하기 위해서는 알파-변환이 필요하다. 예를 들어, $\lambda x.y[y:=x]$를 치환했을 경우 $\lambda x.x$는 정확하지 않다. $\lambda z.x$로 치환되어야 알파-동치를 이룰 수 있다.

타입 없는 람다 대수

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

$\lambda$ 변수 $.$ 수식

위에서 살펴본 항등함수 $I$는 람다 대수로 표현하면 $\lambda x.x$ 가 된다.

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

$(\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로 치환한 것으로 표현할 수 있다. 이와 같이 치환 등을 통해 수식을 축약하는 것은 베타 축약의 한 예이다.

같이 보기

• 처치-로서 정리

참고 문헌

• Church, Alonzo; Rosser, J. Barkley (May 1936), “Some properties of conversion”, 《Transactions of the American Mathematical Society》 39 (3): 472–482, JSTOR 1989762 .