람다 대수

람다 대수(λ代數, 영어: lambda calculus) 또는 λ-대수 또는 람다 계산(λ計算) 또는 람다 계산법(λ計算法)은 추상화와 함수 적용 등의 논리 연산을 다루는 형식 체계이다.^[1] 람다 대수의 항은 변수와 추상화 및 적용 연산을 통해 구성되며 (비순수 람다 대수에서는 상수 역시 구성에 참여한다), 추상화의 기호로는 그리스 문자 람다(λ)가 사용된다. 람다 대수의 항들에 대하여 알파 동치와 베타 축약 등의 연산을 수행할 수 있다. 알파 동치는 제한 변수를 변경하는 변환으로서 이름 충돌을 방지하기 위해 사용되며, 드 브루인 첨수를 사용할 경우 이는 필요 없다. 베타 축약은 함수 적용을 적절한 치환 연산 결과로 대신하는 변환이며, 베타 축약에 대한 주어진 항의 표준형이 (존재할 경우) 알파 동치 아래 유일하다는 사실은 처치-로서 정리의 따름정리이다.

1930년대 알론조 처치가 수학기초론을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 유형 없는 람다 대수라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 유형 람다 대수를 도입하였다.

람다 대수는 튜링 완전성을 만족시키며, 보편 튜링 기계와 동치이다. 람다 대수는 프로그래밍 언어 이론에서 중요한 역할을 하며, 리스프를 비롯한 함수형 프로그래밍 언어의 기반이 된다. 람다 대수는 그 밖에도 논리학, 철학,^[2] 언어학,^[3][4] 컴퓨터 과학^[5] 등의 여러 분야에서 응용된다.

람다 대수는 수학자 알론조 처치에 의해 수학기초론 연구의 일환으로 1930년대 소개됐다.^[6][7] 최초의 시스템은 스티븐 클레이니와 존 버클리 로서가 클리네-로저 역설을 제창하면서 1935년 논리적 모순을 보이기 위해 도입됐다.^[8][9]

그 후인 1936년 처치는 독립적으로 현재에는 유형 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다.^[10] 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 단순 유형 람다 대수이다.^[11]

1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 감사하게도 리처드 몬터규와 언어학자들이 λ-대수를 자연어 (natural language)의 의미론에 적용함으로써, λ-대수는 언어학과^[12]컴퓨터 과학^[13] 양쪽 분야에서 인정받는 위치를 차지했다.

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

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

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

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

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

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

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

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

람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 (후술할) 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 (이후 정의할) 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 (후술할) 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다. 구체적으로, 다음과 같은 데이터가 주어졌다고 하자.

• 가산 무한 정렬 전순서 집합 ${\displaystyle (I,\leq )}$. 또한 ${\displaystyle I}$는 최대 원소를 갖지 않아야 한다.
• 집합 ${\displaystyle J}$ 만약 ${\displaystyle J=\varnothing }$일 경우, 이 람다 대수를 순수 람다 대수(純粹λ代數, 영어: pure lambda calculus)라고 한다.

(여기서 ${\displaystyle I}$가 최대 원소를 갖지 않는 정렬 전순서 집합이어야 하는 것은 치환의 정의에서 주어진 모든 변수들보다 큰 변수들의 집합의 최소 원소를 취할 수 있어야 하기 때문이다.) 그렇다면, ${\displaystyle (I,J)}$에 대한 람다 대수의 언어는 다음과 같은 기호들로 구성된다.

• 각 ${\displaystyle i\in I}$에 대하여, 변수 ${\displaystyle {\mathsf {x}}_{i}}$
• 각 ${\displaystyle j\in J}$에 대하여, 상수 ${\displaystyle {\mathsf {a}}_{j}}$
• 람다 기호 ${\displaystyle \lambda }$
• 괄호 ${\displaystyle ()}$ 및 온점 ${\displaystyle .}$

람다 항(λ項, 영어: lambda term)은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는, 람다 대수 기호들의 문자열이다. 즉, 이는 다음과 같은 문법을 따른다.

• 모든 변수와 상수는 람다 항이다.
• 두 람다 항 ${\displaystyle M}$, ${\displaystyle N}$에 대하여, 문자열 ${\displaystyle (MN)}$은 람다 항이다. 이를 ${\displaystyle N}$에 대한 ${\displaystyle M}$의 적용(適用, 영어: application)이라고 한다.
• 람다 항 ${\displaystyle M}$ 및 변수 ${\displaystyle x}$에 대하여, 문자열 ${\displaystyle (\lambda x.M)}$은 람다 항이다. 이를 ${\displaystyle x}$에 대한 ${\displaystyle M}$의 추상화(抽象化, 영어: abstraction)라고 한다.

괄호 사용을 줄이기 위해 단순히 ${\displaystyle M_{1}M_{2}\cdots M_{n}}$은 ${\displaystyle (\cdots ((M_{1}M_{2})M_{3})\cdots M_{n})}$을 나타내고, ${\displaystyle \lambda x.M_{1}\cdots M_{n}}$은 ${\displaystyle (\lambda x.(\cdots ((M_{1}M_{2})M_{3})\cdots M_{n}))}$을, ${\displaystyle \lambda x_{1}.\cdots \lambda x_{n}.M}$ (또는 ${\displaystyle \lambda x_{1}\cdots x_{n}.M}$)은 ${\displaystyle (\lambda x_{1}.\cdots (\lambda x_{n-1}.(\lambda x_{n}.M))\cdots )}$을 나타내는 데 사용할 수 있다. 예를 들어, 변수 ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$에 대하여,

${\displaystyle \lambda x.x\lambda x.\lambda y.xyz}$

는

${\displaystyle (\lambda x.(x(\lambda x.(\lambda y.((xy)z)))))}$

를 나타낸다.

람다 항에 등장하는 변수들은 자유 변수(自由變數, 영어: free variable)와 제한 변수(制限變數, 영어: bound variable)로 분류된다. 람다 항 ${\displaystyle M}$과 변수 ${\displaystyle x}$에 대하여, 만약 ${\displaystyle M}$에 등장하는 모든 ${\displaystyle x}$가 ${\displaystyle M}$ 속 ${\displaystyle \lambda x.N}$과 같은 꼴의 부분 람다 항에 등장한다면 ${\displaystyle x}$는 제한 변수이며, 만약 적어도 한 ${\displaystyle x}$가 ${\displaystyle \lambda x.N}$과 같은 꼴의 부분 람다 항에 등장하지 않는다면 ${\displaystyle x}$는 자유 변수이다. 즉, 람다 항 ${\displaystyle M}$의 자유 변수의 집합 ${\displaystyle \operatorname {FV} (M)}$는 ${\displaystyle M}$의 구조에 따라 다음과 같이 재귀적으로 정의된다.

• 변수 ${\displaystyle x}$에 대하여, ${\displaystyle \operatorname {FV} (x)=\{x\}}$
• 상수 ${\displaystyle a}$에 대하여, ${\displaystyle \operatorname {FV} (a)=\varnothing }$
• 두 람다 항 ${\displaystyle M}$, ${\displaystyle N}$에 대하여, ${\displaystyle \operatorname {FV} (MN)=\operatorname {FV} (M)\cup \operatorname {FV} (N)}$
• 람다 항 ${\displaystyle M}$ 및 변수 ${\displaystyle x}$에 대하여, ${\displaystyle \operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\setminus \{x\}}$

람다 항 ${\displaystyle M}$에 등장하는 변수 가운데 자유 변수가 아닌 것들을 ${\displaystyle M}$의 제한 변수라고 한다. 자유 변수를 갖지 않는 람다 항을 닫힌 람다 항(닫힌λ項, 영어: closed lambda term)이라고 한다.

예를 들어, 변수 ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$에 대하여,

${\displaystyle (\lambda x.\lambda y.xyz)x}$

의 자유 변수의 집합은 ${\displaystyle \{x,z\}}$이며, 제한 변수의 집합은 ${\displaystyle \{y\}}$이다.

주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 치환(置換, 영어: substitution)하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다 (이는 아래 네 번째 조건의 세 번째 경우에 해당한다). 구체적으로, 람다 항 ${\displaystyle M}$, ${\displaystyle N}$ 및 변수 ${\displaystyle x}$에 대하여, ${\displaystyle x}$를 ${\displaystyle N}$으로 치환한 ${\displaystyle M}$의 치환 실례(置換實例, 영어: substitution instance) ${\displaystyle M[N/x]}$는 ${\displaystyle M}$의 구조에 따라 다음과 같이 재귀적으로 정의된다.

• 변수 ${\displaystyle y}$에 대하여,
  ${\displaystyle y[N/x]={\begin{cases}N&y=x\\y&y\neq x\end{cases}}}$
• 상수 ${\displaystyle a}$에 대하여, ${\displaystyle a[N/x]=a}$
• 람다 항 ${\displaystyle M}$, ${\displaystyle M'}$에 대하여, ${\displaystyle (MM')[N/x]=(M[N/x])(M'[N/x])}$
• 람다 항 ${\displaystyle M}$ 및 변수 ${\displaystyle y}$에 대하여,
  ${\displaystyle (\lambda y.M)[N/x]={\begin{cases}\lambda y.M&y=x\\\lambda y.(M[N/x])&(y\neq x)\land (y\not \in \operatorname {FV} (N)\lor x\not \in \operatorname {FV} (M))\\\lambda z.(M[z/y][N/x])&(y\neq 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}}}$

예를 들어,

${\displaystyle ((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw)}$

${\displaystyle ((\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)는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항 ${\displaystyle M}$이 부분 람다 항 ${\displaystyle \lambda x.P}$를 가질 경우, 이를 ${\displaystyle P}$의 자유 변수가 아닌 변수 ${\displaystyle y}$에 대하여 ${\displaystyle \lambda y.P[y/x]}$로 바꾸면 새로운 람다 항을 얻는다. 이와 같은 과정을 유한 번 거듭하여 람다 항 ${\displaystyle N}$를 얻을 경우, 두 람다 항 ${\displaystyle M}$, ${\displaystyle N}$이 서로 알파 동치라고 하며, ${\displaystyle M\equiv _{\alpha }N}$라고 표기한다.

예를 들어,

${\displaystyle {\begin{aligned}(\lambda x.xy)(\lambda y.yx)&\equiv _{\alpha }(\lambda z.zy)(\lambda y.yx)\\&\equiv _{\alpha }(\lambda z.zy)(\lambda w.wx)\\\end{aligned}}}$

이다.

베타 축약(β縮約, 영어: beta reduction)은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항 ${\displaystyle M}$가 부분 람다 항 ${\displaystyle (\lambda x.P)Q}$를 가질 경우, 이를 ${\displaystyle P[Q/x]}$로 대신하여 새로운 람다 항 ${\displaystyle N}$를 얻을 수 있다. 이 경우 ${\displaystyle M\vartriangleright _{\beta ,1}N}$이라고 표기한다. 두 람다 항 ${\displaystyle M}$, ${\displaystyle N}$이 다음 조건을 만족시키면, ${\displaystyle N}$이 ${\displaystyle M}$의 베타 축약이라고 하며, ${\displaystyle M\vartriangleright _{\beta }N}$이라고 표기한다.

• 다음 조건을 만족시키는 람다 항의 열 ${\displaystyle M=M_{0},M_{1},\dots ,M_{n}=N}$이 존재한다.
  • 임의의 ${\displaystyle k\in \{0,\dots ,n-1\}}$에 대하여, ${\displaystyle M_{k}\equiv _{\alpha }M_{k+1}}$이거나 ${\displaystyle M_{k}\vartriangleright _{\beta ,1}N_{k+1}}$

두 람다 항 ${\displaystyle M}$, ${\displaystyle N}$에 대하여, 다음 두 조건이 서로 동치이며, 이를 만족시키는 ${\displaystyle M}$, ${\displaystyle N}$을 서로 베타 동치(β同値, 영어: beta equivalence)라고 하며, ${\displaystyle M\equiv _{\beta }N}$이라고 표기한다.

• 다음 조건을 만족시키는 람다 항의 열 ${\displaystyle M=M_{0},M_{1},\dots ,M_{n}=N}$이 존재한다.
  • 임의의 ${\displaystyle k\in \{0,\dots ,n-1\}}$에 대하여, ${\displaystyle M_{k}\vartriangleright _{\beta }M_{k+1}}$이거나 ${\displaystyle M_{k}\vartriangleleft _{\beta }M_{k+1}}$
• (처치-로서 정리) ${\displaystyle M\vartriangleright _{\beta }P}$이며 ${\displaystyle N\vartriangleright _{\beta }P}$인 람다 항 ${\displaystyle P}$가 존재한다.

람다 항 ${\displaystyle N}$이 ${\displaystyle (\lambda x.P)Q}$와 같은 꼴의 부분 람다 항을 가지지 않는다면, ${\displaystyle N}$을 베타 표준형(β標準型, 영어: beta normal form)이라고 한다. 베타 표준형 ${\displaystyle N}$이 람다 항 ${\displaystyle M}$의 베타 축약이라면 (즉, ${\displaystyle M\vartriangleright _{\beta }N}$이라면), ${\displaystyle N}$을 ${\displaystyle M}$의 베타 표준형이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.

${\displaystyle \mathbb {N} }$이 음이 아닌 정수의 집합이라고 하자.

람다 대수의 언어를 사용하여 자연수의 페아노 산술을 다음과 같이 표현할 수 있다.

• (처치 숫자, 영어: Church numeral) ${\displaystyle {\bar {n}}=\lambda f.\lambda x.f^{n}x\qquad (n\in \mathbb {N} )}$
• ${\displaystyle \operatorname {plus} =\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)}$
• ${\displaystyle \operatorname {times} =\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x}$

여기서

${\displaystyle f^{n}=\underbrace {f\cdots f} _{n}}$

이다.

μ-재귀 함수는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수 ${\displaystyle f\colon (\mathbb {N} _{\bullet })^{d}\to \mathbb {N} _{\bullet }}$에 대하여, 다음 두 조건을 만족시키는 람다 항 ${\displaystyle {\bar {f}}}$가 존재한다.^{[1]:332, §43.8, Definition 276} (여기서 ${\displaystyle \mathbb {N} _{\bullet }=\mathbb {N} \sqcup \{\bullet _{\mathbb {N} }\}}$는 점을 가진 집합이다.)

• 임의의 ${\displaystyle (n_{1},\dots ,n_{d})\in \mathbb {N} _{\bullet }^{d}}$에 대하여, 만약 ${\displaystyle f(n_{1},\dots ,n_{d})=\bullet _{\mathbb {N} }}$이라면, ${\displaystyle {\bar {f}}{\bar {n}}_{1}\cdots {\bar {n}}_{d}}$는 베타 표준형을 갖지 않는다.
• 임의의 ${\displaystyle (n_{1},\dots ,n_{d})\in \mathbb {N} _{\bullet }^{d}}$에 대하여, 만약 ${\displaystyle f(n_{1},\dots ,n_{d})\in \mathbb {N} }$이라면, ${\displaystyle {\bar {f}}{\bar {n}}_{1}\cdots {\bar {n}}_{d}}$는 ${\displaystyle {\overline {f(n_{1},\dots ,n_{d})}}}$를 베타 표준형으로 갖는다.

• 데카르트 닫힌 범주
• 클로저 (프로그래밍 언어)
• 도메인 이론
• 평가 전략 (컴퓨터 프로그래밍)
• 함수형 프로그래밍
• 클레이니-로서 역설
• 재작성

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

• Alama, Jesse; Korbmacher, Johannes. “The Lambda Calculus”. 《Stanford Encyclopedia of Philosophy》. ISSN 1095-5054.