람다 대수

**람다 대수**(λ代數, lambda calculus) 또는 **λ-대수** 또는 **람다 계산**(λ計算) 또는 **람다 계산법**(λ計算法)은 추상화와 함수 적용 등의 논리 연산을 다루는 형식 체계이다.lccn=2004102307 람다 대수의 항은 변수와 추상화 및 적용 연산을 통해 구성되며 (비순수 람다 대수에서는 상수 역시 구성에 참여한다), 추상화의 기호로는 그리스 문자 람다(λ)가 사용된다. 람다 대수의 항들에 대하여 알파 동치와 베타 축약 등의 연산을 수행할 수 있다. 알파 동치는 제한 변수를 변경하는 변환으로서 이름 충돌을 방지하기 위해 사용되며, 드 브루인 첨수를 사용할 경우 이는 필요 없다. 베타 축약은 함수 적용을 적절한 치환 연산 결과로 대신하는 변환이며, 베타 축약에 대한 주어진 항의 표준형이 (존재할 경우) 알파 동치 아래 유일하다는 사실은 처치-로서 정리의 따름정리이다. 1930년대 알론조 처치가 수학기초론을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 유형 없는 람다 대수라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 유형 람다 대수를 도입하였다. 람다 대수는 튜링 완전성을 만족시키며, 보편 튜링 기계와 동치이다. 람다 대수는 프로그래밍 언어 이론에서 중요한 역할을 하며, 리스프를 비롯한 함수형 프로그래밍 언어의 기반이 된다. 람다 대수는 그 밖에도 논리학, 철학,Coquand, Thierry, "Type Theory", *The Stanford Encyclopedia of Philosophy* (Summer 2013 Edition), Edward N. Zalta (ed.). 언어학,isbn=9789067653879 컴퓨터 과학 등의 여러 분야에서 응용된다.
# 역사
람다 대수는 수학자 알론조 처치에 의해 수학기초론 연구의 일환으로 1930년대 소개됐다.jstor=1968337For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006). 최초의 시스템은 스티븐 클레이니와 존 버클리 로서가 클리네-로저 역설을 제창하면서 1935년 논리적 모순을 보이기 위해 도입됐다.doi=10.2307/1968646jstor=2268117 그 후인 1936년 처치는 독립적으로 현재에는 유형 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다.jstor=2371045 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 단순 유형 람다 대수이다.jstor=2266170 1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 리처드 몬터규와 언어학자들이 λ-대수를 자연어(natural language)의 의미론에 적용한 덕에, λ-대수는 언어학과publisher=Springer 컴퓨터 과학Alama, Jesse "The Lambda Calculus", *The Stanford Encyclopedia of Philosophy* (Summer 2013 Edition), Edward N. Zalta (ed.). 양쪽 분야에서 인정받는 위치를 차지했다.
# 도입

## 함수의 표현
함수는 컴퓨터 과학과 수학의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다. 예를 들어 항등 함수 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)*이라고 한다. 위의 함수 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 하나이다.
# 정의
람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 (후술할) 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 (이후 정의할) 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 (후술할) 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다. 구체적으로, 다음과 같은 데이터가 주어졌다고 하자. * 가산 무한 정렬 전순서 집합 (I,\le). 또한 I는 최대 원소를 갖지 않아야 한다. * 집합 J 만약 J=\varnothing일 경우, 이 람다 대수를 **순수 람다 대수**(純粹λ代數, pure lambda calculus)라고 한다. (여기서 I가 최대 원소를 갖지 않는 정렬 전순서 집합이어야 하는 것은 치환의 정의에서 주어진 모든 변수들보다 큰 변수들의 집합의 최소 원소를 취할 수 있어야 하기 때문이다.) 그렇다면, (I,J)에 대한 람다 대수의 언어는 다음과 같은 기호들로 구성된다. * 각 i\in I에 대하여, 변수 \mathsf x_i * 각 j\in J에 대하여, 상수 \mathsf a_j * 람다 기호 \lambda * 괄호 () 및 온점 . **람다 항**(λ項, lambda term)은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는, 람다 대수 기호들의 문자열이다. 즉, 이는 다음과 같은 문법을 따른다. * 모든 변수와 상수는 람다 항이다. * 두 람다 항 M, N에 대하여, 문자열 (MN)은 람다 항이다. 이를 N에 대한 M의 **적용**(適用, application)이라고 한다. * 람다 항 M 및 변수 x에 대하여, 문자열 (\lambda x.M)은 람다 항이다. 이를 x에 대한 M의 **추상화**(抽象化, abstraction)라고 한다. 괄호 사용을 줄이기 위해 단순히 M_1M_2\cdots M_n은 (\cdots((M_1M_2)M_3)\cdots M_n)을 나타내고, \lambda x.M_1\cdots M_n은 (\lambda x.(\cdots((M_1M_2)M_3)\cdots M_n))을, \lambda x_1.\cdots\lambda x_n.M (또는 \lambda x_1\cdots x_n.M)은 (\lambda x_1.\cdots(\lambda x_{n-1}.(\lambda x_n.M))\cdots)을 나타내는 데 사용할 수 있다. 예를 들어, 변수 x, y, z에 대하여, :\lambda x.x\lambda x.\lambda y.xyz 는 :(\lambda x.(x(\lambda x.(\lambda y.((xy)z))))) 를 나타낸다.
# 연산

## 자유 변수와 제한 변수
람다 항에 등장하는 변수들은 **자유 변수**(自由變數, free variable)와 **제한 변수**(制限變數, bound variable)로 분류된다. 람다 항 M과 변수 x에 대하여, 만약 M에 등장하는 모든 x가 M 속 \lambda x.N과 같은 꼴의 부분 람다 항에 등장한다면 x는 제한 변수이며, 만약 적어도 한 x가 \lambda x.N과 같은 꼴의 부분 람다 항에 등장하지 않는다면 x는 자유 변수이다. 즉, 람다 항 M의 자유 변수의 집합 \operatorname{FV}(M)는 M의 구조에 따라 다음과 같이 재귀적으로 정의된다. * 변수 x에 대하여, \operatorname{FV}(x)=\\{x\\} * 상수 a에 대하여, \operatorname{FV}(a)=\varnothing * 두 람다 항 M, N에 대하여, \operatorname{FV}(MN)=\operatorname{FV}(M)\cup\operatorname{FV}(N) * 람다 항 M 및 변수 x에 대하여, \operatorname{FV}(\lambda x.M)=\operatorname{FV}(M)\setminus\\{x\\} 람다 항 M에 등장하는 변수 가운데 자유 변수가 아닌 것들을 M의 제한 변수라고 한다. 자유 변수를 갖지 않는 람다 항을 **닫힌 람다 항**(닫힌λ項, closed lambda term)이라고 한다. 예를 들어, 변수 x, y, z에 대하여, :(\lambda x.\lambda y.xyz)x 의 자유 변수의 집합은 \\{x,z\\}이며, 제한 변수의 집합은 \\{y\\}이다.
## 치환
주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 **치환**(置換, substitution)하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다 (이는 아래 네 번째 조건의 세 번째 경우에 해당한다). 구체적으로, 람다 항 M, N 및 변수 x에 대하여, x를 N으로 치환한 M의 **치환 실례**(置換實例, substitution instance) M[N/x]는 M의 구조에 따라 다음과 같이 재귀적으로 정의된다. * 변수 y에 대하여,y[N/x]=\begin{cases} N&y;=x\\\ y&y;\ne x \end{cases} * 상수 a에 대하여, a[N/x]=a * 람다 항 M, M'에 대하여, (MM')[N/x]=(M[N/x])(M'[N/x]) * 람다 항 M 및 변수 y에 대하여,(\lambda y.M)[N/x]=\begin{cases} \lambda y.M&y;=x\\\ \lambda y.(M[N/x])&(y\ne x)\land(y\not\in\operatorname{FV}(N)\lor x\not\in\operatorname{FV}(M))\\\ \lambda z.(M[z/y][N/x])&(y\ne x)\land(y\in\operatorname{FV}(N)\land x\in\operatorname{FV}(M))\land(z=\min\\{w\in I\colon w>\max(\operatorname{FV}(M)\cup\operatorname{FV}(N))\\}) \end{cases} 예를 들어, : ((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw) : ((\lambda x.\lambda y.xyz)x)[yw/z]=(\lambda x.\lambda v.xvyw)x\qquad(v=\min\\{u\in I\colon u>\max\\{x,y,z,w\\}\\}) 이다.
## 알파 동치
**알파 동치**(α同値, alpha equivalence)는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항 M이 부분 람다 항 \lambda x.P를 가질 경우, 이를 P의 자유 변수가 아닌 변수 y에 대하여 \lambda y.P[y/x]로 바꾸면 새로운 람다 항을 얻는다. 이와 같은 과정을 유한 번 거듭하여 람다 항 N를 얻을 경우, 두 람다 항 M, N이 서로 **알파 동치**라고 하며, M\equiv_\alpha N라고 표기한다. 예를 들어, :\begin{align}(\lambda x.xy)(\lambda y.yx) &\equiv_\alpha (\lambda z.zy)(\lambda y.yx)\\\ &\equiv_\alpha (\lambda z.zy)(\lambda w.wx)\\\ \end{align} 이다.
## 베타 축약
**베타 축약**(β縮約, beta reduction)은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항 M가 부분 람다 항 (\lambda x.P)Q를 가질 경우, 이를 P[Q/x]로 대신하여 새로운 람다 항 N를 얻을 수 있다. 이 경우 M\vartriangleright_{\beta,1}N이라고 표기한다. 두 람다 항 M, N이 다음 조건을 만족시키면, N이 M의 **베타 축약**이라고 하며, M\vartriangleright_\beta N이라고 표기한다. * 다음 조건을 만족시키는 람다 항의 열 M=M_0,M_1,\dots,M_n=N이 존재한다. ** 임의의 k\in\\{0,\dots,n-1\\}에 대하여, M_k\equiv_\alpha M_{k+1}이거나 M_k\vartriangleright_{\beta,1}N_{k+1} 두 람다 항 M, N에 대하여, 다음 두 조건이 서로 동치이며, 이를 만족시키는 M, N을 서로 **베타 동치**(β同値, beta equivalence)라고 하며, M\equiv_\beta N이라고 표기한다. * 다음 조건을 만족시키는 람다 항의 열 M=M_0,M_1,\dots,M_n=N이 존재한다. ** 임의의 k\in\\{0,\dots,n-1\\}에 대하여, M_k\vartriangleright_\beta M_{k+1}이거나 M_k\vartriangleleft_\beta M_{k+1} * (처치-로서 정리) M\vartriangleright_\beta P이며 N\vartriangleright_\beta P인 람다 항 P가 존재한다. 람다 항 N이 (\lambda x.P)Q와 같은 꼴의 부분 람다 항을 가지지 않는다면, N을 **베타 표준형**(β標準型, beta normal form)이라고 한다. 베타 표준형 N이 람다 항 M의 베타 축약이라면 (즉, M\vartriangleright_\beta N이라면), N을 M의 **베타 표준형**이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.
# 응용
\mathbb N이 음이 아닌 정수의 집합이라고 하자.
## 산술의 표현
람다 대수의 언어를 사용하여 자연수의 페아노 산술을 다음과 같이 표현할 수 있다. * (처치 숫자, Church numeral) \bar n=\lambda f.\lambda x.f^nx\qquad(n\in\mathbb N) * \operatorname{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx) * \operatorname{times}=\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x 여기서 :f^n=\underbrace{f\cdots f}_n 이다.
## μ-재귀 함수의 표현
μ-재귀 함수는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수 f\colon(\mathbb N_\bullet)^d\to\mathbb N_\bullet에 대하여, 다음 두 조건을 만족시키는 람다 항 \bar f가 존재한다.332, §43.8, Definition 276 (여기서 \mathbb N_\bullet=\mathbb N\sqcup\\{\bullet_{\mathbb N}\\}는 점을 가진 집합이다.) * 임의의 (n_1,\dots,n_d)\in\mathbb N_\bullet^d에 대하여, 만약 f(n_1,\dots,n_d)=\bullet_{\mathbb N}이라면, \bar f{\bar n}_1\cdots{\bar n}_d는 베타 표준형을 갖지 않는다. * 임의의 (n_1,\dots,n_d)\in\mathbb N_\bullet^d에 대하여, 만약 f(n_1,\dots,n_d)\in\mathbb N이라면, \bar f{\bar n}_1\cdots{\bar n}_d는 \overline{f(n_1,\dots,n_d)}를 베타 표준형으로 갖는다.