람다 대수

위키백과, 우리 모두의 백과사전.
이동: 둘러보기, 검색

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

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

수학사에서 람다 대수[편집]

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

함수의 표현[편집]

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

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

  1. 함수가 반드시 이름을 가질 필요는 없다. 함수 s는 이름을 제거하고 (x, y) \mapsto x \times x + y \times y 와 같은 형태로 쓸 수 있다. 또한 항등 함수 I(x) = xx \mapsto x 의 형태로 쓸 수 있다.
  2. 함수의 입력 변수의 이름 또한 필요 없다. x \mapsto xy \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 yx \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에 등장하는 변수들이다.
  • 두 표현 ts의 결합 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 (만약 xy 일 경우,)
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
x.M)[x := N] ≡ λx.M
y.M)[x := N] ≡ λy.(M[x := N]) (만약 xy 이고, 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로 치환한 것으로 표현할 수 있다. 이와 같이 치환 등을 통해 수식을 축약하는 것은 베타 축약의 한 예이다.

같이 보기[편집]

참고 문헌[편집]

  • (May 1936) 《Some properties of conversion》, 472–482쪽. JSTOR 1989762.