람다 대수

[[컴퓨터공학|컴퓨터 과학 & 공학

Computer Science & Engineering

]]

[ 펼치기 · 접기 ]

||<tablebgcolor=#fff,#1c1d1f><tablecolor=#373a3c,#ddd><colbgcolor=#0066DC><colcolor=white> 기반 학문 ||수학(해석학 · 이산수학 · 수리논리학 · 선형대수학 · 미적분학 · 미분방정식 · 대수학(환론 · 범주론) · 정수론) · 이론 컴퓨터 과학 · 암호학 · 전자공학 · 언어학(형태론 · 통사론 · 의미론 · 화용론 · 음운론) · 인지과학 ||

하드웨어 구성	SoC · CPU · GPU(그래픽 카드 · GPGPU) · ROM · RAM · SSD · HDD · 참조: 틀:컴퓨터 부품
기술	기계어 · 어셈블리어 · C/C++ · C# · Java · Python · BIOS · 절차적 프로그래밍 · 객체 지향 프로그래밍 · 해킹 · ROT13 · 일회용 비밀번호 · 사물인터넷 · 와이파이 · GPS · 임베디드 · 인공신경망 · OpenGL · EXIF · 마이크로아키텍처 · ACPI · UEFI · NERF · gRPC · 리버스 엔지니어링 · HCI · UI · UX · 대역폭 · DBMS · NoSQL · 해시(SHA · 브루트 포스 · 레인보우 테이블 · salt · 암호화폐) · RSA 암호화 · 하드웨어 가속
연구 및 기타	논리 회로(보수기 · 가산기 · 논리 연산 · 불 대수 · 플립플롭) · 정보이론 · 임베디드 시스템 · 운영 체제 · 데이터베이스 · 프로그래밍 언어{컴파일러(어셈블러 · JIT) · 인터프리터 · 유형 이론 · 파싱 · 링커 · 난해한 프로그래밍 언어} · 메타데이터 · 기계학습 · 빅데이터 · 폰노이만 구조 · 양자컴퓨터 · 행위자 모델 · 인코딩(유니코드 · MBCS) · 네트워크 · 컴퓨터 보안 · OCR · 슈퍼컴퓨터 · 튜링 머신 · FPGA · 딥러닝 · 컴퓨터 구조론 · 컴퓨터 비전 · 컴퓨터 그래픽스 · 인공지능 · 시간 복잡도(최적화) · 소프트웨어 개발 방법론 · 디자인 패턴 · 정보처리이론 · 재귀 이론 · 자연어 처리(기계 번역 · 음성인식) · 버전 (버전 관리 시스템 · Git · GitHub)

'''이론 컴퓨터 과학 {{{#!wiki style="display: inline-block; font-family:Times New Roman, serif;font-style:italic"'''
{{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px"	<colbgcolor=#a36> 이론
기본 대상	수학기초론{수리논리학(논리 연산) · 계산 가능성 이론 · 범주론 · 집합론} · 이산수학(그래프 이론) · 수치해석학 · 확률론 및 통계학 · 선형대수학
다루는 대상과 주요 토픽
계산 가능성 이론	재귀함수 · 튜링 머신 · 람다대수 · 처치-튜링 명제 · 바쁜 비버
오토마타 이론	FSM · 푸시다운 · 튜링 머신(폰노이만 구조) · 정규 표현식 · 콘웨이의 생명 게임 · 형식언어
계산 복잡도 이론	점근 표기법 · 튜링 기계^^{고전, 양자, 비결정론적, 병렬 임의접근 기계}^ · 알고리즘 · 자료구조 · 알고리즘 패러다임(그리디 알고리즘, 동적 계획법)
정보이론	데이터 압축(무손실 압축 포맷 · 손실 압축 포맷) · 채널 코딩(채널 용량) · 알고리즘 정보 이론(AIT) · 양자정보과학
프로그래밍 언어이론	프로그래밍 언어(함수형 언어 · 객체 지향 프로그래밍 · 증명보조기) · 메타 프로그래밍 · 유형 이론 · 프로그래밍 언어 의미론 · 파싱 · 컴파일러 이론
주요 알고리즘 및 자료구조
기초	정렬 알고리즘 · 순서도 · 탐색 알고리즘
추상적 자료형 및 구현	배열^^벡터^ · 리스트^^{연결 리스트}^ · 셋(set)^^{레드-블랙 트리, B-트리}^ · 우선순위 큐^^{힙, 피보나치 힙}^
수학적 최적화	조합 최적화	외판원 순회 문제 · 담금질 기법 · 유전 알고리즘 · 기계학습
	볼록 최적화	내부점 방법 · 경사하강법
	선형계획법	심플렉스법
계산 수론 및 암호학	밀러-라빈 소수판별법 · Pollard-rho 알고리즘 · 쇼어 알고리즘 · LLL 알고리즘 · 해시(MD5 · 암호화폐 · 사전 공격(레인보우 테이블) · SHA) · 양자 암호
	대칭키 암호화 방식	블록 암호 알고리즘(AES · ARIA · LEA · Camellia) · 스트림 암호 알고리즘(RC4)
	공개키 암호화 방식	공개키 암호 알고리즘(타원 곡선 암호 · RSA) · 신원 기반 암호 알고리즘(SM9)
계산기하학	볼록 껍질 · 들로네 삼각분할 및 보로노이 도형^^{Fortune의 line-sweeping 알고리즘}^ · 범위 탐색^^{vp-tree, R-tree}^ · k-NN
그래프 이론	탐색^^{BFS, DFS, 다익스트라 알고리즘, A* 알고리즘}^ · 에드몬드-카프 · 크루스칼 알고리즘 · 위상 정렬 · 네트워크 이론
정리
정지 문제^{대각선 논법} · 암달의 법칙 · P-NP 문제^미해결 · 콜라츠 추측^미해결
틀:이산수학 · 틀:수학기초론 · 틀:컴퓨터공학			}}}}}}}}}

1. 개요2. 번역어 논란3. 설명

3.1. 기본 개념

3.1.1. 익명 함수3.1.2. 커링

3.2. 정의

3.2.1. 람다 항과 대입 연산3.2.2. 변환 규칙3.2.3. 정규형

3.3. 계산 이론

4. 응용

4.1. 부호화

4.1.1. 자연수4.1.2. 불 진릿값4.1.3. 술어4.1.4. 쌍4.1.5. 재귀 함수4.1.6. 기타

4.2. 프로그래밍 언어

4.2.1. 익명 함수4.2.2. 자료형

1. 개요

lambda calculus

람다 대수란 계산을 함수와 함수의 연산으로 추상화한 체계이다. 다른 계산 모델인 튜링 기계와는 동치이며, 모든 기계적인 계산은 람다 대수로 표현할 수 있다고 믿어진다. 미국의 수학자이자 컴퓨터 과학자 알론조 처치(Alonzo Church)가 1930년대에 수학 기초론을 연구하며 고안했다.

2. 번역어 논란

이 번역어에 대한 논란이 있다. 순수 수학 및 응용 수학은 말할 것도 없고 컴퓨터 과학에서도 대수라는 용어는 대부분 algebra에 대응되는 용어로 쓰이지만, 유독 lambda calculus에서까지 혼동될 만한 '대수'라는 역어가 쓰이고 있다. calculus라는 말이 수학에서는 미분 적분학을 가리키는 의미로 쓰이지만 이 분야는 전혀 미적분과 상관없는 분야이기 때문에 20세기 대한민국 수학자 및 전산학자들이 일부러 대수라는 용어를 가져다 쓴 것으로 추측된다. 이런 혼동 때문에 일부러 람다 대수라는 명칭을 기피하고 람다 계산술, 람다 셈법 등의 다른 용어를 쓰거나 아예 람다 캘큘러스라는 발음을 그대로 읽는 사람들도 많다.
서울대학교 이광근 교수는 프로그래밍 언어론 강의 노트에서 람다 계산법이라는 용어를 사용했다.[1]

3. 설명

3.1. 기본 개념

3.1.1. 익명 함수

수학에서 일반적으로 함수를 정의할 때는 이름을 붙여 나타낸다. 예를 들어, 자연수 [math(n)]과 수열[2] [math(f)]에 대해 제[math(0)]항부터 제[math(n)]항까지의 수열의 합은 다음과 같이 나타낼 수 있다.

[math(\displaystyle\sum_{k=0}^nf(k)=f(0)+f(1)+\cdots+f(n))]

이때 [math(\sum)]는 함수의 집합을 정의역으로 하는 고차 함수라고 생각할 수 있으며[3], 위 식에서는 [math(\sum)]의 매개 변수를 나타내기 위해 [math(f)]라는 이름을 붙였다.

하지만, 실제로 [math(\sum)]를 사용할 때 항상 함수에 이름을 붙이지는 않는다. 예를 들어, 다음 항등식을 생각하자.

[math(\displaystyle\sum_{k=0}^n(2k+1)=(n+1)^2)]

위 식 내의 [math(2k+1)]은 그냥 식이 아니라, [math(k)]를 입력받아 [math(2k+1)]을 출력하는 함수를 나타낸다고 볼 수 있다. 이 함수를 나타내기 위해 굳이 [math(f(x)=2x+1)]이라고 함수 [math(f)]를 따로 정의한 후 [math(\sum)]에 대입하지 않았음에 주목하자. 그러면 함수를 정의할 때 함수의 이름은 중요하지 않음을 알 수 있을 것이다.

여기서 익명 함수의 개념이 등장한다. 굳이 이름을 붙이지 않고, 매개 변수와 매개 변수를 사용한 식만으로 함수를 정의하겠다는 뜻이다. 익명 함수는 [math(\lambda)](매개 변수)[math(.)](함수식)의 꼴로 나타낸다. 예를 들어, 위에서 본 함수를 다음과 같이 적는다.

[math(\lambda x.2x+1)]

이렇게 함수를 익명 함수로 만드는 이유는 이 함수를 마치 값처럼 쓰기 위해서이다. 아래에서 보겠지만 람다 대수에서는 입출력이 모두 함수인 함수에 대해서 다룬다.

3.1.2. 커링

다음과 같이 정의된 함수 [math(f:\R^2\to\R)]를 생각해 보자.

[math(f(x,y)=x^2+y^2)]

이 함수는 매개 변수가 2개인 다변수 함수이다. 이를 익명 함수로 나타내고자 하는데, 익명 함수에는 매개 변수가 하나만 들어갈 수 있다. 물론 익명 함수가 여러 개의 매개 변수를 가질 수 있도록 정의를 수정해도 되겠지만, 굳이 그러지 않아도 함수를 다음과 같이 변형하면 문제되지 않는다.

[math(\begin{aligned}f(x,y)&=g(x)(y)\\g(x)&=g_x\\g_x(y)&=x^2+y^2\end{aligned})]

여기서 [math(g)]는 [math(\R)]에서 [math(\mathcal F(\R,\R))][4]로 가는 함수이며, [math(g_x)]는 [math(\R)]에서 [math(\R)]로 가는 함수이다. 즉, 실수의 순서쌍 [math((x,y))]를 입력받아 실수 [math(x^2+y^2)]을 출력하는 다변수 함수 [math(f)]를, 실수 [math(x)]를 입력받아 함수 [math(g_x)]를 출력하는 일변수 함수 [math(g)]와, 실수 [math(y)]를 입력받아 실수[math(x^2+y^2)]을 출력하는 일변수 함수 [math(g_x)]로 나눈 것이다. 이런 방식으로 다변수 함수를 일변수 함수들로 나누는 과정을 커링(Currying)이라고 한다. 커링이라는 용어는 미국의 수학자이자 논리학자 해스컬 커리(Haskell Curry)의 이름에서 따왔다.[5]

이제 이를 익명 함수로 나타내 보자. 먼저 [math(g_x)]를 나타내면 다음과 같다.

[math(\begin{aligned}&&g_x(y)&=x^2+y^2\\\Rightarrow&&g_x&=\lambda y.x^2+y^2\end{aligned})]

이제 이를 통해 [math(g)]를 나타낸다. [math(g)]의 함숫값은 함수인데, 이 함수는 위에서 익명 함수로 이미 나타냈다. 따라서 이를 값처럼 쓸 수 있다.

[math(\begin{aligned}&&g(x)&=g_x\\&&&=\lambda y.x^2+y^2\\\Rightarrow&&g&=\lambda x.\lambda y.x^2+y^2\end{aligned})]

참고로 이 식은 다음 순서로 해석해야 한다.

[math(\lambda x.{\left(\lambda y.{\left(x^2+y^2\right)}\right)})]

3.2. 정의

람다 대수는 람다 항과 변환 규칙으로 구성된다.

3.2.1. 람다 항과 대입 연산

람다 항\[lambda term\]은 다음 3가지 재귀적 정의로 정의된다.

람다 항의 정의

[math(x)]는 람다 항이고, 이를 변수\[variable\]라고 한다.
변수 [math(x)]와 람다 항 [math(t)]에 대해, [math(\lambda x.t)]는 람다 항이고, 이를 추상화\[abstraction\]라고 한다.
람다 항 [math(t)], [math(s)]에 대해, [math(ts)]는 람다 항이고, 이를 적용\[application\]이라고 한다.

람다 대수에서는 모든 것을 함수라고 생각할 수 있다. 그래서 변수 또한 함수이며, 변수에 다른 람다 항을 대입하는 것도 당연히 가능하다. 추상화는 위에서 봤듯 함수를 정의하는 것으로 이해할 수 있다. 적용은 함수에 값을 대입하는 것인데, 쉽게 말해 일반적인 수학에서 [math(t(s))]라고 적는 것을 [math(ts)]라고 적는다고 보면 된다.

람다 항 연산 순서의 기본 원칙은 다음과 같다.

추상화 내의 람다 항은 가능한 최대로 한다.
적용은 맨 앞에서부터 진행한다.

원하는 계산 순서가 이 원칙에 어긋나지 않는다면 괄호를 생략할 수 있다. 예를 들어, 다음 람다 항을 생각하자.

[math(\lambda f.(\lambda x.f(xx))\lambda x.f(xx))]

이 람다 항은 다음과 같이 해석해야 한다.

[math(\lambda f.((\lambda x.(f(xx)))(\lambda x.(f(xx)))))]

자유 변수\[free variable\]란 람다 항 내에서 어떤 함수의 매개 변수로 쓰이지 않은 변수를 뜻한다. 자유 변수의 집합 [math(\mathrm{FV})]는 다음과 같이 정의한다.

자유 변수의 정의

변수 [math(x)]에 대해, [math(\mathrm{FV}(x)=\{x\})]
변수 [math(x)]와 람다 항 [math(t)]에 대해, [math(\mathrm{FV}(\lambda x.t)=\mathrm{FV}(t)\setminus\{x\})]
람다 항 [math(t)], [math(s)]에 대해, [math(\mathrm{FV}(ts)=\mathrm{FV}(t)\cup\mathrm{FV}(s))]

변수는 추상화의 매개 변수로 쓰일 때만 자유 변수가 아니게 된다. 그래서 추상화 [math(\lambda x.t)]는 변수 [math(x)]를 묶는다\[bind\]고 표현한다.

대입\[substitution\] 연산은 자유 변수를 람다 항으로 대체하는 연산이다. 변수 [math(x)]에 람다 항 [math(t)]를 대입하는 것은 [math([x:=t])]로 표현하며, 다음과 같이 정의된다.

대입 연산의 정의

변수 [math(y)]에 대해, [math(y[x:=t]=\begin{cases}t,&\text{if }y=x\\y,&\text{if }y\ne x\end{cases})]
변수 [math(y)]와 람다 항 [math(s)]에 대해, [math((\lambda y.s)[x:=t]=\begin{cases}\lambda y.s,&\text{if }y=x\\\lambda y.(s[x:=t]),&\text{if }y\ne x\land y\notin\mathrm{FV}(t)\end{cases})]
람다 항 [math(s)], [math(u)]에 대해, [math((su)[x:=t]=(s[x:=t])(u[x:=t]))]

변수 [math(y)]와 람다 항 [math(s)]에 대해, [math(y\ne x)]이고 [math(y\in\mathrm{FV}(t))]인 경우의 [math((\lambda y.s)[x:=t])]는 위에서는 정의돼 있지 않다. 이때는 후술할 α 전환을 통해 위에서 정의된 두 경우 중 하나로 변환한 후 대입하면 된다.

3.2.2. 변환 규칙

α 전환\[α-conversion\]은 다음과 같은 변환 규칙이다.

[math(\lambda x.t[x]\Rightarrow\lambda y.t[y])]

이는 함수의 매개 변수를 바꾸는 규칙이다. 예를 들어, [math(\lambda x.x)]는 [math(\lambda y.y)]로 변환할 수 있다. 매개 변수로 무엇을 쓰든 함수의 내용에는 영향을 주지 않는다. 두 람다 항 [math(x)], [math(y)]에 대해, [math(x)]에 α 전환을 적용해 [math(y)]를 만들 수 있으면 두 람다 항은 α 동치 관계에 있다고 한다.

α 전환에서 주의해야 할 점이 있는데, α 전환으로 서로 다른 변수가 같아지거나 하면 안 된다는 것이다. 예를 들어, [math(\lambda x.y)] 내의 [math(x)]를 [math(z)]로 전환해 [math(\lambda z.y)]로 변환하는 것은 가능하지만, [math(y)]로 전환해 [math(\lambda y.y)]로 변환할 수는 없다. 또 다른 예시로, [math(\lambda x.\lambda y.x)] 내의 [math(x)]를 [math(y)]로 전환해 [math(\lambda y.\lambda y.y)]로 변환하는 것도 불가능하다.

이제 약간 헷갈릴 수 있는 경우를 보자. 다음 변환은 가능하다.

[math(\lambda y.y\lambda x.x\Rightarrow\lambda x.x\lambda x.x)]

이는 이 식의 [math(x)]를 다음과 같이 구별할 수 있기 때문이다.

[math(\lambda{\color{Red}x}.{\color{Red}x}\lambda{\color{Blue}x}.{\color{Blue}x})]

변수는 가장 가까운 함수에 묶인다는 점에서, 헷갈릴 수는 있어도 [math(\color{Red}x)]와 [math(\color{Blue}x)]가 서로 다른 변수임을 확실히 알 수 있다. 두 [math(x)]가 서로 다름을 안다면 다음 변환도 가능함을 알 수 있다.

[math(\lambda x.x\lambda x.x\Rightarrow\lambda y.y\lambda x.x)]

당연히 [math(\lambda x.x\lambda x.x\Rightarrow\lambda y.y\lambda x.y)] 같은 건 안 된다는 것도 짚고 넘어가자.

β 축약\[β-reduction\]은 다음과 같은 변환 규칙이다.

[math((\lambda x.t)s\Rightarrow t[x:=s])]

이는 함수에 값을 대입하는 규칙으로, [math(x)]를 매개 변수로 하는 함수 [math(\lambda x.t)]에 [math(s)]를 대입하면 함수식 [math(t)] 내의 [math(x)]를 [math(s)]로 치환한 값을 출력하는 것을 나타낸다. 예를 들어, [math((\lambda x.x)y)]는 [math(y)]로 변환된다. 여기서 [math(\lambda x.x)]는 항등 함수임을 알 수 있다. 두 람다 항 [math(x)], [math(y)]에 대해, [math(x)]에 β 축약을 적용해 [math(y)]를 만들 수 있거나, [math(y)]에 β 축약을 적용해 [math(x)]를 만들 수 있으면 두 람다 항은 β 동치 관계에 있다고 한다.

β 축약에서도 주의해야 할 점이 있는데, 일부 β 축약은 α 전환을 요할 때가 있다는 점이다. 예를 들어, 다음 식을 생각하자.

[math((\lambda x.\lambda{\color{Red}y}.x{\color{Red}y}){\color{Blue}y})]

위 식에 β 축약을 그냥 적용하면 [math(\lambda y.yy)]가 되면서, 자유 변수 [math(\color{Blue}y)]가 함수 [math(\lambda{\color{Red}y}.x{\color{Red}y})]에 묶이게 된다. 따라서 이 경우, 먼저 α 전환을 한 후 β 축약을 적용해야 한다.

[math(\begin{aligned}&(\lambda x.\lambda y.xy)y\\\Rightarrow&(\lambda x.\lambda z.xz)y&&\text{(α-conversion)}\\\Rightarrow&\lambda z.yz&&\text{(β-reduction)}\end{aligned})]

η 축약\[η-reduction\]은 다음과 같은 변환 규칙이다.

[math(\lambda x.tx\Rightarrow t\;\;\;\;\text{if }x\notin\mathrm{FV}(t))]

이는 임의의 입력에 대해 같은 출력을 내는 함수는 같음을 나타내는 규칙으로, 양변에 임의의 람다 항 [math(z)]를 적용하면 [math((\lambda x.tx)z\Rightarrow tz)]에서 서로 β 동치 관계에 있음을 알 수 있다. 물론 이는 [math(x)]가 [math(t)]의 자유 변수가 아니어야 성립한다. 두 람다 항 [math(x)], [math(y)]에 대해, [math(x)]에 η 축약을 적용해 [math(y)]를 만들 수 있거나, [math(y)]에 η 축약을 적용해 [math(x)]를 만들 수 있으면 두 람다 항은 η 동치 관계에 있다고 한다. 이렇게 어떤 동치 관계에 있는 두 람다 항을 이제 같다고 표현하도록 한다.

3.2.3. 정규형

어떤 람다 항에 대해 β 축약이 가능하려면 람다 항 내부에 [math((\lambda x.t)s)] 꼴이 포함돼 있어야 하고, η 축약이 가능하려면 람다 항 내부에 [math(\lambda x.tx)] 꼴이 포함돼 있어야 한다. 이런 형태의 식을 리덱스(redex, REDucible EXpression)라고 한다. 또, 리덱스가 없어 축약이 불가능한 람다 항을 정규형\[normal form\]이라고 한다.

다음 람다 항을 보자.

[math((\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)\lambda u.u)\lambda f.\lambda x.fx)]

이 긴 람다 항은 다음과 같이 β 축약을 통해 정규형으로 변환할 수 있다.

[math(\begin{aligned}&(\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)\lambda u.u)\lambda f.\lambda x.fx\\\Rightarrow&\lambda f.\lambda x.(\lambda f.\lambda x.fx)(\lambda g.\lambda h.h(gf))(\lambda u.x)\lambda u.u&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.(\lambda x.(\lambda g.\lambda h.h(gf))x)(\lambda u.x)\lambda u.u&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.(\lambda g.\lambda h.h(gf))(\lambda u.x)\lambda u.u&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.(\lambda h.h((\lambda u.x)f))\lambda u.u&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.(\lambda u.u)((\lambda u.x)f)&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.(\lambda u.x)f&&\text{(β-reduction)}\\\Rightarrow&\lambda f.\lambda x.x&&\text{(β-reduction)}\end{aligned})]

이번에는 다음 람다 항을 보자.

[math((\lambda x.xx)\lambda x.xx)]

이 람다 항은 변환을 아무리 하더라도 형태가 달라지지 읺아 정규형으로 변환할 수 없다.

[math(\begin{aligned}&(\lambda x.xx)\lambda x.xx\\\Rightarrow&(\lambda x.xx)\lambda x.xx&&\text{(β-reduction)}\\\Rightarrow&(\lambda x.xx)\lambda x.xx&&\text{(β-reduction)}\\\Rightarrow&(\lambda x.xx)\lambda x.xx&&\text{(β-reduction)}\\\Rightarrow&\cdots\end{aligned})]

다음 람다 항은 조금 특이하다.

[math((\lambda x.f(xx))\lambda x.f(xx))]

이 람다 항은 변환할수록 오히려 더 길어진다.

[math(\begin{aligned}&(\lambda x.f(xx))\lambda x.f(xx)\\\Rightarrow&f((\lambda x.f(xx))\lambda x.f(xx))&&\text{(β-reduction)}\\\Rightarrow&f(f((\lambda x.f(xx))\lambda x.f(xx)))&&\text{(β-reduction)}\\\Rightarrow&f(f(f((\lambda x.f(xx))\lambda x.f(xx))))&&\text{(β-reduction)}\\\Rightarrow&\cdots\end{aligned})]

위의 세 람다 항으로부터 모든 람다 항을 정규형으로 변환할 수 있는 것은 아님을 알 수 있다.

이번에는 다음 람다 항을 생각하자.

[math((\lambda z.y)((\lambda x.f(xx))\lambda x.f(xx)))]

이 람다 항은 가장 바깥쪽 리덱스에 β 축약을 적용하면 바로 정규형으로 바뀐다.

[math(\begin{aligned}&(\lambda z.y)((\lambda x.f(xx))\lambda x.f(xx))\\\Rightarrow&y&&\text{(β-reduction)}\end{aligned})]

하지만, 이 람다 항에 β 축약을 가장 안쪽 리덱스부터 적용하려 하면 영원히 정규형에 도달하지 않는다.

[math(\begin{aligned}&(\lambda z.y)((\lambda x.f(xx))\lambda x.f(xx))\\\Rightarrow&(\lambda z.y)(f((\lambda x.f(xx))\lambda x.f(xx)))&&\text{(β-reduction)}\\\Rightarrow&(\lambda z.y)(f(f((\lambda x.f(xx))\lambda x.f(xx))))&&\text{(β-reduction)}\\\Rightarrow&(\lambda z.y)(f(f(f((\lambda x.f(xx))\lambda x.f(xx)))))&&\text{(β-reduction)}\\\Rightarrow&\cdots\end{aligned})]

여기서 정규형으로 변환할 때 β 축약의 순서가 중요함을 알 수 있다.

람다 대수에서는 다음 정리가 증명돼 있다.

처치·로서 정리(Church–Rosser Theorem)
어떤 람다 항 [math(a)]에 서로 다른, 변환 규칙의 나열을 적용해 각각 람다 항 [math(b)], [math(c)]를 얻었다고 하자. 그러면 [math(b)]로부터 어떤 변환 규칙의 나열을 적용해서도 얻을 수 있고, [math(c)]로부터 어떤 변환 규칙의 나열을 적용해서도 얻을 수 있는 람다 항 [math(d)]가 존재한다.

처치·로서 정리는 람다 항이 정규형을 가지고 있다면 유일함을 보여준다. 정규형이 존재한다면 유일하다는 건 알았으니, 이젠 이 정규형을 찾는 방법이 필요하다. 그리고 이 방법은 매우 간단하다. β 축약을 가장 바깥쪽, 가장 왼쪽 리덱스부터 적용하는 것을 정규 순서\[normal order\]라고 하자. 이름에서부터 알 수 있듯 이 순서로 변환을 진행하면 정규형이 있는 경우 언젠간 정규형에 도달함이 증명돼 있다. 정규형 문단 위쪽 세 람다식은 모두 정규 순서로 변환을 진행한 예시이고, 정규형이 존재하는 첫 번째 람다식은 정규형에 도달했음을 확인할 수 있다.

3.3. 계산 이론

람다 대수는 기계적인 계산을 추상화한 계산 모델이다. 유명한 계산 모델 중에는 튜링 기계가 있는데, 람다 대수는 튜링 기계와 같은 계산 능력을 가진다. 즉, 임의의 튜링 기계에 대해 같은 일을 하는 람다 항이 존재하며, 그 역도 성립한다. 따라서 우리가 현대 컴퓨터로 할 수 있는 모든 계산은 람다 대수를 이용해서도 가능하다. 어떻게 가능한지는 아래 문단에서 다루기로 하고, 여기서는 몇 가지 이론을 먼저 보도록 한다.

어떤 함수를 같은 계산을 하는 람다 항으로 표현할 수 있다면 이 함수는 λ 계산 가능하다고 한다. 또 어떤 함수를 같은 계산을 하는 튜링 기계로 표현할 수 있다면 이 함수는 튜링 계산 가능하다고 한다. 이에 대해 다음과 같은 명제가 있다.

처치·튜링 명제(Church–Turing Thesis)
어떤 함수가 기계적으로 계산 가능하다는 것의 필요충분조건은 해당 함수가 튜링 계산 가능하다는 것이고, 해당 함수가 λ 계산 가능하다는 것이다.

기계적으로 계산 가능하다는 것이 무엇인지 엄밀하게 정의돼 있지 않아 위 명제를 증명할 수는 없으며, 그래서 정리가 아니라 명제라고 부른다. 하지만 지금까지는 인간이 기계적이라고 생각할 수 있는 방식으로 튜링 계산 불가능한 함수, λ 계산 불가능한 함수를 계산한 경우가 없으므로 이를 기계적으로 계산 가능하다는 것의 정의로 보기도 한다. 현대 컴퓨터는 이 명제를 바탕으로 연구·개발되고 있다.

어떤 함수가 λ 계산 가능하다는 것이 의미가 있으려면 λ 계산 불가능한 함수가 존재해야 할 것이다. 이러한 함수 중 대표적인 함수는 람다 항 하나를 받아 해당 함수가 정규형을 가지고 있는지 판단하는 함수이다. 이러한 함수가 λ 계산 불가능함을 다음과 같이 증명할 수 있다.

정리
주어진 람다 항이 정규형을 가지는지를 계산하는 함수는 λ 계산 불가능하다.

증명
증명 방법으로 귀류법을 사용한다. 그러한 함수가 λ 계산 가능하다고 가정하자. 그러면 다음과 같이 입력이 정규형을 가지는지에 따라 출력이 다른 람다 항 [math(X)]가 존재한다.

[math(Xt=\begin{cases}\lambda x.\lambda y.x,&\text{if }t\text{ has normal form}\\\lambda x.\lambda y.y,&\text{if }t\text{ does not have normal form}\end{cases})]

정규형을 가지는 람다 항 [math(M)]과 정규형을 가지지 않는 람다 항 [math(N)]에 대해, 다음과 같은 람다 항 [math(e)]를 생각하자.

[math(e:=\lambda f.X(ff)NM)]

람다 항 [math(ee)]는 정규형을 가지거나 가지지 않는다. 각 경우에 대해 [math(X(ee))]를 생각한다.

[math(ee)]가 정규형을 가진다고 가정하자. 그러면 [math(X)]의 정의에 의해 [math(X(ee)=\lambda x.\lambda y.x)]이다. 이때

{{{#!wiki style="text-align:center;"

[math(\begin{aligned}ee&=(\lambda f.X(ff)NM)e&&\text{(definition)}\\&=X(ee)NM&&\text{(β-reduction)}\\&=(\lambda x.\lambda y.x)NM&&\text{(definition)}\\&=(\lambda y.N)M&&\text{(β-reduction)}\\&=N&&\text{(β-reduction)}\end{aligned})]}}}

에서 [math(X(ee)=XN=\lambda x.\lambda y.y)]이다. 이는 모순이다.
1. [math(ee)]가 정규형을 가지지 않는다고 가정하자. 그러면 [math(X)]의 정의에 의해 [math(X(ee)=\lambda x.\lambda y.y)]이다. 이때

{{{#!wiki style="text-align:center;"

[math(\begin{aligned}ee&=(\lambda f.X(ff)NM)e&&\text{(definition)}\\&=X(ee)NM&&\text{(β-reduction)}\\&=(\lambda x.\lambda y.y)NM&&\text{(definition)}\\&=(\lambda y.y)M&&\text{(β-reduction)}\\&=M&&\text{(β-reduction)}\end{aligned})]}}}

에서 [math(X(ee)=XM=\lambda x.\lambda y.x)]이다. 이는 모순이다.

모든 경우에서 모순이 발생하므로 모순이다. 따라서 주어진 람다 항이 정규형을 가지는지를 계산하는 함수는 λ 계산 불가능하다.

람다 대수가 튜링 기계와 동치라는 점에서 생각해 보면, 이 함수는 정지 문제와 닮았음을 알 수 있다. 람다 항을 정규형으로 바꾸는 변환 과정은 튜링 기계가 작동하는 과정으로, 정규형을 튜링 기계의 정지 상태로 생각하면 해당 함수는 튜링 기계가 정지하는지를 판별하는 튜링 기계, 즉, 정지 문제를 푸는 튜링 기계로 생각할 수 있다. 이 점에서 증명 과정을 보면 정지 문제의 계산 불가능성 증명 과정과도 비슷함을 느낄 수 있을 것이다.[6]

위 함수 외에도 많은 함수가 λ 계산 불가능하다. 또 다른 대표적인 예시로는 람다 항 2개를 받아 두 람다 항이 동치인지 판단하는 함수가 있다.

4. 응용

4.1. 부호화

위에서 람다 대수가 튜링 기계와 동치라고 했다. 이제 람다 대수로 간단한 계산이 어떻게 이뤄지는지를 보도록 한다. 처음 개념을 설명할 때는 그냥 수학에서 써 왔듯 [math(\lambda x.\lambda y.x^2+y^2)] 같은 식을 그냥 사용했다. 하지만, 정의 문단에서 보듯 람다 항에는 지수도, 덧셈도 없다. 심지어 숫자조차 없다. 이런 상황에서 람다 항으로 계산을 하려면 자연수 같은 연산의 대상, 덧셈 같은 연산을 정의해야 한다. 즉, 계산에 필요한 것들을 부호화[encoding]해야 한다. 이는 컴퓨터에서는 [math(0)]과 [math(1)]로 구성된 비트밖에 없지만, 이런 비트를 몇 개씩 묶어서 자연수, 실수부터 여러 연산까지 부호화해 CPU가 할 수 있는 몇 개의 연산만으로 수많은 계산을 해낼 수 있는 것과 비슷하다. 여기서는 대부분 처치 부호화\[Church encoding\]를 사용하도록 한다. 이 부호화는 처치가 처음 사용했다고 이런 이름이 붙었다.

4.1.1. 자연수

편의성을 위해 수학의 합성 함수를 가져와 다음을 정의하자.

합성 함수의 정의
람다 항 [math(f)], [math(x)]와 자연수 [math(n)]에 대해

[math(f^nx=\begin{cases}x,&n=0\\f{\left(f^{n-1}x\right)},&n>0\end{cases})]

그러면 다음 성질을 만족한다는 것은 쉽게 알 수 있다.

합성 함수의 성질
람다 항 [math(f)], [math(x)]와 자연수 [math(m)], [math(n)]에 대해

[math(f^n{\left(f^mx\right)}=f^{m+n}x)]
[math({\left(f^m\right)}^nx=f^{mn}x)]

자연수는 다음과 같이 정의한다.

처치 부호화 한 자연수의 정의

[math(\begin{aligned}0&:=\lambda f.\lambda x.x&&=\lambda f.\lambda x.f^0x\\1&:=\lambda f.\lambda x.fx&&=\lambda f.\lambda x.f^1x\\2&:=\lambda f.\lambda x.f(fx)&&=\lambda f.\lambda x.f^2x\\3&:=\lambda f.\lambda x.f(f(fx))&&=\lambda f.\lambda x.f^3x\\&\vdots\\n&:=\lambda f.\lambda x.\underbrace{f(\cdots f(f(f}_nx))\cdots)&&=\lambda f.\lambda x.f^nx\end{aligned})]

자연수는 함수 [math(f)]와 [math(x)]를 받아 [math(x)]에 [math(f)]를 원하는 자연수만큼 합성하는 함수로 나타내는데, 이런 부호화는 어떤 함수를 주어진 자연수만큼 반복해야 할 때 유용하게 사용된다. 자연수에 반복할 함수를 대입하면 되기 때문이다.

이제 자연수에 대한 연산을 정의하자. 1번째 연산은 다음 수 연산 [math(\mathrm{succ})]이다. 처치 부호화 한 자연수 [math(n)]에 대해, [math(\mathrm{succ}\,n)]의 결과는 처치 부호화 한 [math(n+1)]이다. 즉, [math(\mathrm{succ})]에 [math(\lambda f.\lambda x.f^nx)]를 대입하면 [math(\lambda f.\lambda x.f^{n+1}x)]로 변환돼야 한다. 이는 자연수가 어떻게 부호화됐는지를 생각하면 쉽다. 크게 2가지 방식이 있는데, 하나는 [math(f^nx)] 바깥에 [math(f)]를 씌우는 것이고, 다른 하나는 [math(n)]의 [math(x)]에 [math(fx)]를 대입하는 것이다. 두 방식 모두 처치 부호화 한 자연수에 대해서는 결과가 동일하다. 여기서는 전자의 방식을 사용하기로 하자. [math(\mathrm{succ})]은 다음과 같이 정의된다.

다음 수 연산의 정의

[math(\mathrm{succ}:=\lambda n.\lambda f.\lambda x.f(nfx))]

예시로 [math(\mathrm{succ}\,2)]를 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{succ}\,2&=(\lambda n.\lambda f.\lambda x.f(nfx))2&&\text{(definition)}\\&=\lambda f.\lambda x.f(2fx)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f{\left({\left(\lambda f.\lambda x.f^2x\right)}fx\right)}&&\text{(definition)}\\&=\lambda f.\lambda x.f{\left({\left(\lambda x.f^2x\right)}x\right)}&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f{\left(f^2x\right)}&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^3x&&\text{(definition)}\\&=3&&\text{(definition)}\end{aligned})]

2번째로는 덧셈 연산 [math(\mathrm{add})]를 정의하기로 하자. 처치 부호화 한 자연수 [math(m)], [math(n)]에 대해, [math(\mathrm{add}\,mn)]의 결과는 처치 부호화 한 [math(m+n)]이다. 즉, [math(\mathrm{add})]에 [math(\lambda f.\lambda x.f^mx)], [math(\lambda f.\lambda x.f^nx)]를 순서대로 대입하면 [math(\lambda f.\lambda x.f^{m+n}x)]로 변환돼야 한다. 이를 구현하는 방식도 여러 가지이다. 여기서는 [math(\mathrm{succ})]과 같은 방식으로, [math(f^mx)] 바깥에 [math(f)]를 [math(n)]번 씌우는 방법으로 구현하겠다. 위에서 언급했듯 이런 방식에서 처치 부호화 한 자연수의 강점이 드러난다.

덧셈 연산의 정의

[math(\mathrm{add}:=\lambda m.\lambda n.\lambda f.\lambda x.nf(mfx))]

예시로 [math(\mathrm{add}\,2\,3)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{add}\,2\,3&=(\lambda m.\lambda n.\lambda f.\lambda x.nf(mfx))2\,3&&\text{(definition)}\\&=(\lambda n.\lambda f.\lambda x.nf(2fx))3&&\text{(β-reduction)}\\&=\lambda f.\lambda x.3f(2fx)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.{\left(\lambda f.\lambda x.f^3x\right)}f(2fx)&&\text{(definition)}\\&=\lambda f.\lambda x.{\left(\lambda x.f^3x\right)}(2fx)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^3(2fx)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^3{\left({\left(\lambda f.\lambda x.f^2x\right)}fx\right)}&&\text{(definition)}\\&=\lambda f.\lambda x.f^3{\left({\left(\lambda x.f^2x\right)}x\right)}&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^3{\left(f^2x\right)}&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^5x&&\text{(property)}\\&=5&&\text{(definition)}\end{aligned})]

3번째로는 곱셈 연산 [math(\mathrm{mul})]을 정의한다. 처치 부호화 한 자연수 [math(m)], [math(n)]에 대해, [math(\mathrm{mul}\,mn)]의 결과는 처치 부호화 한 [math(mn)]이다. 즉, [math(\mathrm{mul})]에 [math(\lambda f.\lambda x.f^mx)], [math(\lambda f.\lambda x.f^nx)]를 순서대로 대입하면 [math(\lambda f.\lambda x.f^{mn}x)]로 변환돼야 한다. 이는 [math(f^{mn}={\left(f^m\right)}^n)]임을 이용하면 된다. 즉, [math(f^nx)]의 [math(f)]에 [math(f^m)]을 대입하면 된다. 이렇게 정의하면 다음과 같다.

곱셈 연산의 정의

[math(\mathrm{mul}:=\lambda m.\lambda n.\lambda f.\lambda x.n(mf)x)]

예시로 [math(\mathrm{mul}\,2\,3)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{mul}\,2\,3&=(\lambda m.\lambda n.\lambda f.\lambda x.n(mf)x)2\,3&&\text{(definition)}\\&=(\lambda n.\lambda f.\lambda x.n(2f)x)3&&\text{(β-reduction)}\\&=\lambda f.\lambda x.3(2f)x&&\text{(β-reduction)}\\&=\lambda f.\lambda x.\bigl(\lambda f.\lambda x.f^3x\bigr)(2f)x&&\text{(definition)}\\&=\lambda f.\lambda x.\bigl(\lambda x.(2f)^3x\bigr)x&&\text{(β-reduction)}\\&=\lambda f.\lambda x.(2f)^3x&&\text{(β-reduction)}\\&=\lambda f.\lambda x.2f\bigl((2f)^2x\bigr)&&\text{(definition)}\\&=\lambda f.\lambda x.\bigl(\lambda f.\lambda x.f^2x\bigr)f\bigl((2f)^2x\bigr)&&\text{(definition)}\\&=\lambda f.\lambda x.\bigl(\lambda x.f^2x\bigr)\bigl((2f)^2x\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^2\bigl((2f)^2x\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^2(2f(2fx))&&\text{(definition)}\\&=\lambda f.\lambda x.f^2\bigl(\bigl(\lambda f.\lambda x.f^2x\bigr)f(2fx)\bigr)&&\text{(definition)}\\&=\lambda f.\lambda x.f^2\bigl(\bigl(\lambda x.f^2x\bigr)(2fx)\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^2\bigl(f^2(2fx)\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^4(2fx)&&\text{(property)}\\&=\lambda f.\lambda x.f^4\bigl(\bigl(\lambda f.\lambda x.f^2x\bigr)fx\bigr)&&\text{(definition)}\\&=\lambda f.\lambda x.f^4\bigl(\bigl(\lambda x.f^2x\bigr)x\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^4\bigl(f^2x\bigr)&&\text{(β-reduction)}\\&=\lambda f.\lambda x.f^6x&&\text{(property)}\\&=6&&\text{(definition)}\end{aligned})]

4번째로는 거듭제곱 연산 [math(\mathrm{pow})]를 정의한다. 처치 부호화 한 자연수 [math(m)], [math(n)]에 대해, [math(\mathrm{pow}\,mn)]의 결과는 처치 부호화 한 [math(m^n)]이다. 즉, [math(\mathrm{pow})]에 [math(\lambda f.\lambda x.f^mx)], [math(\lambda f.\lambda x.f^nx)]를 순서대로 대입하면 [math(\lambda f.\lambda x.f^{m^n}x)]로 변환돼야 한다. 가장 간단한 방법은 [math(1)]에 [math(m)]을 [math(n)]번 곱하는 것일 것이다. 이 방식은 매우 직관적이며, 사실 위의 [math(\mathrm{add})]와 [math(\mathrm{mul})]도 같은 방법론을 이용해 각각 [math(\mathrm{succ})]와 [math(\mathrm{add})]로 정의할 수 있다. 이렇게 정의하면 다음과 같다.

거듭제곱 연산의 정의(직관적인 방법)

[math(\mathrm{pow}:=\lambda m.\lambda n.n(\mathrm{mul}\,m)1)]

근데 한번 [math(\lambda f.\lambda x.f^nx)]에 [math(\lambda f.\lambda x.f^mx)]를 대입하고 정리해 보자.

[펼치기·접기]: [math(\begin{aligned}(\lambda f.\lambda x.f^nx)\lambda f.\lambda x.f^mx&=(\lambda f.\lambda x.f^nx)M&&(M:=\lambda f.\lambda x.f^mx)\\&=\lambda x.M^nx&&\text{(β-reduction)}\\&=\lambda x.M\bigl(M^{n-1}x\bigr)&&\text{(definition)}\\&=\lambda x.(\lambda f.\lambda x.f^mx)\bigl(M^{n-1}x\bigr)&&\text{(definition)}\\&=\lambda x.(\lambda f.\lambda y.f^my)\bigl(M^{n-1}x\bigr)&&\text{(α-conversion)}\\&=\lambda x.\lambda y.\bigl(M^{n-1}x\bigr)^my&&\text{(β-reduction)}\\&=\lambda x.\lambda y.\bigl(M\bigl(M^{n-2}x\bigr)\bigr)^my&&\text{(definition)}\\&=\lambda x.\lambda y.\bigl((\lambda f.\lambda x.f^mx)\bigl(M^{n-2}x\bigr)\bigr)^my&&\text{(definition)}\\&=\lambda x.\lambda y.\bigl((\lambda f.\lambda z.f^mz)\bigl(M^{n-2}x\bigr)\bigr)^my&&\text{(α-conversion)}\\&=\lambda x.\lambda y.\bigl(\lambda z.\bigl(M^{n-2}x\bigr)^mz\bigr)^my&&\text{(β-reduction)}\\&=\lambda x.\lambda y.\bigl(\bigl(M^{n-2}x\bigr)^m\bigr)^my&&\text{(η-reduction)}\\&=\lambda x.\lambda y.\bigl(M^{n-2}x\bigr)^{m^2}y&&\text{(property)}\\&=\lambda x.\lambda y.\bigl(M\bigl(M^{n-3}x\bigr)\bigr)^{m^2}y&&\text{(definition)}\\&=\lambda x.\lambda y.\bigl((\lambda f.\lambda x.f^mx)\bigl(M^{n-3}x\bigr)\bigr)^{m^2}y&&\text{(definition)}\\&=\lambda x.\lambda y.\bigl((\lambda f.\lambda z.f^mz)\bigl(M^{n-3}x\bigr)\bigr)^{m^2}y&&\text{(α-conversion)}\\&=\lambda x.\lambda y.\bigl(\lambda z.\bigl(M^{n-3}x\bigr)^mz\bigr)^{m^2}y&&\text{(β-reduction)}\\&=\lambda x.\lambda y.\bigl(\bigl(M^{n-3}x\bigr)^m\bigr)^{m^2}y&&\text{(η-reduction)}\\&=\lambda x.\lambda y.\bigl(M^{n-3}x\bigr)^{m^3}y&&\text{(property)}\\&=\cdots\\&=\lambda x.\lambda y.x^{m^n}y&&\text{(property)}\\&=\lambda f.\lambda y.f^{m^n}y&&\text{(α-conversion)}\\&=\lambda f.\lambda x.f^{m^n}x&&\text{(α-conversion)}\end{aligned})]

놀랍게도 처치 부호화 한 [math(m^n)]이 나온다! 이를 이용하면 [math(\mathrm{pow})]를 다음과 같이 매우 간단하게 정의할 수 있다.

거듭제곱 연산의 정의(간단한 방법)

[math(\mathrm{pow}:=\lambda m.\lambda n.nm)]

자연수는 뺄셈과 나눗셈에 대해 닫혀 있지 않지만, 편의상 다음과 같이 정의할 수 있다.[7]

자연수의 뺄셈과 나눗셈의 정의

[math(\begin{aligned}m-_\N n&:=\begin{cases}m-_\Z n,&m\ge n\\0,&m<n\end{cases}\\m/_\N n&:=\lfloor m/_\mathbb Qn\rfloor\end{aligned})]

자연수의 이전 수 연산 [math(\mathrm{pred})], 뺄셈 연산 [math(\mathrm{sub})], 나눗셈 연산 [math(\mathrm{div})]는 다음과 같이 정의할 수 있다. 이에 대해서는 필요한 연산을 모두 정의한 후 설명하기로 한다.

이전 수 연산과 뺄셈 연산, 나눗셈 연산의 정의

[math(\begin{aligned}\mathrm{pred}&:=\lambda n.\mathrm{first}(n(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0))
\\\mathrm{sub}&:=\lambda m.\lambda n.n\,\mathrm{pred}\,m\\\mathrm{div}&:=Y\lambda f.\lambda m.\lambda n.\mathrm{lt}\,mn0(\mathrm{succ}(f(\mathrm{sub}\,mn)n))\end{aligned})]

4.1.2. 불 진릿값

불 진릿값[Boolean]은 다음과 같이 정의한다.

처치 부호화한 불 진릿값의 정의

[math(\begin{aligned}\mathrm{true}&:=\lambda x.\lambda y.x\\\mathrm{false}&:=\lambda x.\lambda y.y\end{aligned})]

불 진릿값은 함수 2개를 입력받아 참이면 1번째 함수를, 거짓이면 2번째 함수를 출력하는 함수로 부호화한다. 이는 조건문을 만들 때 유용한 형태이다. 예를 들어, 다음과 같은 표현을 생각하자.

[math(\text{if }p\text{ then }q\text{ else }r)]

이때 참이나 거짓의 값을 가지는 [math(p)]를 처치 부호화 하면 람다 항 [math(pqr)]는 [math(p)]가 참이라면 1번째 함수 [math(q)]가, 거짓이라면 2번째 함수 [math(r)]가 출력될 테니 원하는 조건문임을 알 수 있다.

불 대수에서의 연산에는 부정 연산 [math(\mathrm{not})], 논리합 연산 [math(\mathrm{or})], 논리곱 연산 [math(\mathrm{and})] 등이 있다. 여기서는 이 3가지 연산을 보도록 하자.

부정 연산 [math(\mathrm{not})]은 불 진릿값 하나를 입력받아 참이면 거짓, 거짓이면 참을 출력해야 한다. 처치 부호화에서는 참, 거짓을 어떤 함수를 출력하는지로 구분하므로 두 함수의 순서만 바꾸면 된다. 따라서 다음과 같이 정의할 수 있다.

부정 연산의 정의

[math(\mathrm{not}:=\lambda p.\lambda x.\lambda y.pyx)]

예시로 [math(\mathrm{not}\,\mathrm{true})]를 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{not}\,\mathrm{true}&=(\lambda p.\lambda x.\lambda y.pyx)\mathrm{true}&&\text{(definition)}\\&=\lambda x.\lambda y.\mathrm{true}\,yx&&\text{(β-reduction)}\\&=\lambda x.\lambda y.(\lambda x.\lambda y.x)yx&&\text{(definition)}\\&=\lambda x.\lambda y.(\lambda x.\lambda z.x)yx&&\text{(α-conversion)}\\&=\lambda x.\lambda y.(\lambda z.y)x&&\text{(β-reduction)}\\&=\lambda x.\lambda y.y&&\text{(β-reduction)}\\&=\mathrm{false}&&\text{(definition)}\end{aligned})]

논리합 연산 [math(\mathrm{or})]는 불 진릿값 2개를 입력받아 하나만 참이어도 참을, 모두 거짓일 때만 거짓을 출력하는 연산이다. 이는 다음과 같이 조건문으로 생각할 수 있다.

[math(\begin{aligned}p\text{ or }q&=\text{if }p\text{ then true else (if }q\text{ then true else false)}\\&=\text{if }p\text{ then true else }q\\&=\text{if }p\text{ then }p\text{ else }q\end{aligned})]

그러면 이를 다음과 같이 정의할 수 있다.

논리합 연산의 정의

[math(\mathrm{or}:=\lambda p.\lambda q.ppq)]

예시로 [math(\mathrm{or}\,\mathrm{true}\,\mathrm{false})]를 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{or}\,\mathrm{true}\,\mathrm{false}&=(\lambda p.\lambda q.ppq)\mathrm{true}\,\mathrm{false}&&\text{(definition)}\\&=(\lambda q.\mathrm{true}\,\mathrm{true}\,q)\mathrm{false}&&\text{(β-reduction)}\\&=\mathrm{true}\,\mathrm{true}\,\mathrm{false}&&\text{(β-reduction)}\\&=(\lambda x.\lambda y.x)\mathrm{true}\,\mathrm{false}&&\text{(definition)}\\&=(\lambda y.\mathrm{true})\mathrm{false}&&\text{(β-reduction)}\\&=\mathrm{true}&&\text{(β-reduction)}\end{aligned})]

논리곱 연산 [math(\mathrm{and})]는 불 진릿값 2개를 입력받아 모두 참일 때만 참을, 하나만 거짓이어도 거짓을 출력하는 연산이다. 이것도 조건문으로 생각하면 다음과 같다.

[math(\begin{aligned}p\text{ and }q&=\text{if }p\text{ then (if }q\text{ then true else false) else false}\\&=\text{if }p\text{ then }q\text{ else false}\\&=\text{if }p\text{ then }q\text{ else }p\end{aligned})]

그러면 이를 다음과 같이 정의할 수 있다.

논리곱 연산의 정의

[math(\mathrm{and}:=\lambda p.\lambda q.pqp)]

예시로 [math(\mathrm{and}\,\mathrm{true}\,\mathrm{false})]를 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{and}\,\mathrm{true}\,\mathrm{false}&=(\lambda p.\lambda q.pqp)\mathrm{true}\,\mathrm{false}&&\text{(definition)}\\&=(\lambda q.\mathrm{true}\,q\,\mathrm{true})\mathrm{false}&&\text{(β-reduction)}\\&=\mathrm{true}\,\mathrm{false}\,\mathrm{true}&&\text{(β-reduction)}\\&=(\lambda x.\lambda y.x)\mathrm{false}\,\mathrm{true}&&\text{(definition)}\\&=(\lambda y.\mathrm{false})\mathrm{true}&&\text{(β-reduction)}\\&=\mathrm{false}&&\text{(β-reduction)}\end{aligned})]

4.1.3. 술어

이제 진릿값을 나타낼 수 있게 됐으니 특정한 입력에 대해 참, 거짓을 출력하는 함수인 술어\[predicate\]를 생각해 볼 수 있다. 자연수에 대한 몇 가지 술어를 처치 부호화 해 보자.

처음으로 생각할 만한 간단한 술어로는 주어진 자연수가 [math(0)]인지 판단하는 술어 [math(\mathrm{isZero})]가 있다. 이를 부호화하기 위해서는 [math(0)]과 다른 자연수의 차이를 생각해 보면 된다. 자연수는 함수 [math(f)], [math(x)]를 받는 함수로 부호화되는데, [math(0)]을 제외한 자연수는 [math(f)]가 쓰인다는 점을 떠올리면 [math(f)]가 어떤 입력에도 [math(\mathrm{false})]를 출력하는 함수이기만 하면 [math(0)]이 아닌 자연수에 대해 [math(\mathrm{false})]일 것임을 알 수 있다. 따라서 이 술어는 다음과 같이 정의할 수 있다.

술어 [math(\mathrm{isZero})]의 정의

[math(\mathrm{isZero}:=\lambda n.n(\lambda x.\mathrm{false})\mathrm{true})]

예시로 [math(\mathrm{isZero}\,10)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{isZero}\,10&=(\lambda n.n(\lambda x.\mathrm{false})\mathrm{true})10&&\text{(definition)}\\&=10(\lambda x.\mathrm{false})\mathrm{true}&&\text{(β-reduction)}\\&=\bigl(\lambda f.\lambda x.f^{10}x\bigr)(\lambda x.\mathrm{false})\mathrm{true}&&\text{(definition)}\\&=\bigl(\lambda x.(\lambda x.\mathrm{false})^{10}x\bigr)\mathrm{true}&&\text{(β-reduction)}\\&=(\lambda x.\mathrm{false})^{10}\mathrm{true}&&\text{(β-reduction)}\\&=(\lambda x.\mathrm{false})\bigl((\lambda x.\mathrm{false})^9\mathrm{true}\bigr)&&\text{(definition)}\\&=\mathrm{false}&&\text{(β-reduction)}\end{aligned})]

이번에는 주어진 자연수가 짝수/홀수인지 판단하는 술어 [math(\mathrm{isEven})], [math(\mathrm{isOdd})]를 정의해 보자. 이는 매우 간단한데, 부정의 부정은 자기 자신임을 이용하면 된다.

술어 [math(\mathrm{isEven})], [math(\mathrm{isOdd})]의 정의

[math(\begin{aligned}\mathrm{isEven}&:=\lambda n.n\,\mathrm{not}\,\mathrm{true}\\\mathrm{isOdd}&:=\lambda n.n\,\mathrm{not}\,\mathrm{false}\end{aligned})]

예시로 [math(\mathrm{isEven}\,4)]를 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{isEven}\,4&=(\lambda n.n\,\mathrm{not}\,\mathrm{true})4&&\text{(definition)}\\&=4\,\mathrm{not}\,\mathrm{true}&&\text{(β-reduction)}\\&=\bigl(\lambda f.\lambda x.f^4x\bigr)\mathrm{not}\,\mathrm{true}&&\text{(definition)}\\&=\bigl(\lambda x.\mathrm{not}^4x\bigr)\mathrm{true}&&\text{(β-reduction)}\\&=\mathrm{not}^4\mathrm{true}&&\text{(β-reduction)}\\&=\mathrm{not}(\mathrm{not}(\mathrm{not}(\mathrm{not}\,\mathrm{true})))&&\text{(definition)}\\&=\mathrm{not}(\mathrm{not}(\mathrm{not}\,\mathrm{false}))&&\text{(negation)}\\&=\mathrm{not}(\mathrm{not}\,\mathrm{true})&&\text{(negation)}\\&=\mathrm{not}\,\mathrm{false}&&\text{(negation)}\\&=\mathrm{true}&&\text{(negation)}\end{aligned})]

이번에는 두 자연수를 비교하는 술어를 정의해 보자. 함수가 어디가 더 많이 씌워졌는지를 비교하는 것은 어려워 보이지만, 생각보다 쉽게 정의할 수 있다. 자연수의 뺄셈은 뒤쪽이 앞쪽보다 크다면 [math(0)]으로 정의했으므로 자연수 [math(m)], [math(n)]에 대해 [math(m-n=0\Leftrightarrow m\le n)]이 성립한다. 따라서 이하 연산 [math(\mathrm{le})]는 다음과 같이 정의한다.

술어 [math(\mathrm{le})]의 정의

[math(\mathrm{le}:=\lambda m.\lambda n.\mathrm{isZero}(\mathrm{sub}\,mn))]

이제 다른 부등호는 [math(\mathrm{le})]를 이용해 쉽게 정의할 수 있다. 이상 연산 [math(\mathrm{ge})], 초과 연산 [math(\mathrm{gt})], 미만 연산 [math(\mathrm{lt})]는 다음과 같이 정의한다.

술어 [math(\mathrm{ge})], [math(\mathrm{gt})], [math(\mathrm{lt})]의 정의

[math(\begin{aligned}\mathrm{ge}&:=\lambda m.\lambda n.\mathrm{le}\,nm\\\mathrm{gt}&:=\lambda m.\lambda n.\mathrm{not}(\mathrm{le}\,mn)\\\mathrm{lt}&:=\lambda m.\lambda n.\mathrm{not}(\mathrm{le}\,nm)\end{aligned})]

자연수의 상등 연산 [math(\mathrm{eq})]와 부등 연산 [math(\mathrm{ne})]는 위의 비교 연산을 이용해 다음과 같이 정의할 수 있다.

술어 [math(\mathrm{eq})], [math(\mathrm{ne})]의 정의

[math(\begin{aligned}\mathrm{eq}&:=\lambda m.\lambda n.\mathrm{and}(\mathrm{le}\,mn)(\mathrm{ge}\,mn)\\\mathrm{ne}&:=\lambda m.\lambda n.\mathrm{or}(\mathrm{lt}\,mn)(\mathrm{gt}\,mn)\end{aligned})]

예시로 [math(\mathrm{eq}\,2\,3)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{eq}\,2\,3&=(\lambda m.\lambda n.\mathrm{and}(\mathrm{le}\,mn)(\mathrm{ge}\,mn))2\,3&&\text{(definition)}\\&=(\lambda n.\mathrm{and}(\mathrm{le}\,2n)(\mathrm{ge}\,2n))3&&\text{(β-reduction)}\\&=\mathrm{and}(\mathrm{le}\,2\,3)(\mathrm{ge}\,2\,3)&&\text{(β-reduction)}\\&=\mathrm{and}((\lambda m.\lambda n.\mathrm{isZero}(\mathrm{sub}\,m\,n))2\,3)(\mathrm{ge}\,2\,3)&&\text{(definition)}\\&=\mathrm{and}((\lambda n.\mathrm{isZero}(\mathrm{sub}\,2\,n))3)(\mathrm{ge}\,2\,3)&&\text{(β-reduction)}\\&=\mathrm{and}(\mathrm{isZero}(\mathrm{sub}\,2\,3))(\mathrm{ge}\,2\,3)&&\text{(β-reduction)}\\&=\mathrm{and}(\mathrm{isZero}\,0)(\mathrm{ge}\,2\,3)&&\text{(subtraction)}\\&=\mathrm{and}\,\mathrm{true}(\mathrm{ge}\,2\,3)&&\text{(predicate)}\\&=\mathrm{and}\,\mathrm{true}((\lambda m.\lambda n.\mathrm{le}\,nm)2\,3)&&\text{(predicate)}\\&=\mathrm{and}\,\mathrm{true}((\lambda n.\mathrm{le}\,n2)3)&&\text{(β-reduction)}\\&=\mathrm{and}\,\mathrm{true}(\mathrm{le}\,3\,2)&&\text{(β-reduction)}\\&=\mathrm{and}\,\mathrm{true}((\lambda m.\lambda n.\mathrm{isZero}(\mathrm{sub}\,mn))3\,2)&&\text{(definition)}\\&=\mathrm{and}\,\mathrm{true}((\lambda n.\mathrm{isZero}(\mathrm{sub}\,3n))2)&&\text{(β-reduction)}\\&=\mathrm{and}\,\mathrm{true}(\mathrm{isZero}(\mathrm{sub}\,3\,2))&&\text{(β-reduction)}\\&=\mathrm{and}\,\mathrm{true}(\mathrm{isZero}\,1)&&\text{(subtraction)}\\&=\mathrm{and}\,\mathrm{true}\,\mathrm{false}&&\text{(predicate)}\\&=\mathrm{false}&&\text{(conjunction)}\end{aligned})]

4.1.4. 쌍

이번에는 쌍을 부호화해 보고, 이를 이용해 자연수의 뺄셈을 정의해 보겠다. 쌍\[pair\]은 두 대상을 순서대로 묶은 것으로, 묶인 대상을 각각 1번째, 2번째 원소라고 한다. 처치 부호화 한 쌍으로는 임의의 람다 항을 묶을 수 있다. 예를 들어, 처치 부호화 한 두 자연수를 묶을 수도 있고, 자연수 하나와 불 진릿값 하나를 묶을 수도 있고, 심지어 쌍을 묶을 수도 있다. 의미는 없겠지만 처치 부호화와 관계없는 람다 항도 묶을 수 있을 것이다.

두 람다 항 [math(x)], [math(y)]에 대해, 쌍 [math((x,y))]는 다음과 같이 정의한다.

처치 부호화 한 쌍의 정의

[math((x,y):=\lambda f.fxy)]

쌍과 관련된 연산으로는 두 대상을 입력받아 이를 묶은 쌍을 출력하는 쌍 생성 연산 [math(\mathrm{pair})], 쌍을 받아 각각 1번째, 2번째 원소를 출력하는 참조 연산 [math(\mathrm{first})], [math(\mathrm{second})]이 있다. 이는 쌍을 어떻게 부호화했는지를 보면 쉽게 정의할 수 있다.

쌍 생성 연산과 참조 연산의 정의

[math(\begin{aligned}\mathrm{pair}&:=\lambda x.\lambda y.\lambda f.fxy\\\mathrm{first}&:=\lambda p.p(\lambda x.\lambda y.x)\\\mathrm{second}&:=\lambda p.p(\lambda x.\lambda y.y)\end{aligned})]

이제 쌍을 이용해 자연수의 뺄셈을 정의해 보자. 자연수의 뺄셈은 이전 수 연산으로 쉽게 정의할 수 있으므로 사실상 이전 수 연산을 구현하기만 하면 된다. 자연수는 함수의 합성 횟수로 부호화되므로 이를 이용해 부호화하려면 이전 수 연산 [math(f)]는 다음 표를 만족해야 한다.

[math(\begin{array}{c||c|c|c|c|c}n&0&1&2&3&\cdots\\\hline f^n(0)&0&f(0)=0&f(0)=1&f(1)=2&\cdots\\\hline n-1&0&0&1&2&\cdots\end{array})]

하지만 이는 입력 [math(0)]에 대해 어떤 때는 [math(0)]을, 어떤 때는 [math(1)]을 출력해야 할 수도 있으므로 불가능하다. 그러면 이전 수와 다음 수의 이전 수(즉, 자기 자신)까지 가지고 있으면 어떨까? 그러니까 쌍을 이용해 다음과 같이 쌍을 입력받아 쌍을 출력하는 함수 [math(g)]를 생각해 보자는 말이다.

[math(\begin{array}{c||c|c|c|c|c}n&0&1&2&3&\cdots\\\hline g^n(0,0)&(0,0)&g(0,0)=(0,1)&g(0,1)=(1,2)&g(1,2)=(2,3)&\cdots\\\hline n-1&0&0&1&2&\cdots\end{array})]

이제는 같은 입력에 다른 출력을 낼 필요가 없으므로 가능하며, 심지어 구현하기도 쉽다! 쌍을 입력받아 2번째 원소와 2번째 원소의 다음 수를 묶은 쌍을 출력하면 되기 때문이다. 이 함수를 [math((0,0))]에 [math(n)]번 합성하면 [math((n-1,n))]이 출력될 것이고, 이전 수 연산은 이 쌍의 1번째 원소만 불러오면 된다. 이를 이용해 이전 수 연산 [math(\mathrm{pred})]를 정의하면 다음과 같다.

이전 수 연산의 정의

[math(\mathrm{pred}:=\lambda n.\mathrm{first}(n(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0)))]

예시로 [math(\mathrm{pred}\,3)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{pred}\,3&=(\lambda n.\mathrm{first}(n(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0)))3&&\text{(definition)}\\&=\mathrm{first}(3(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0))&&\text{(β-reduction)}\\&=\mathrm{first}\bigl(\bigl(\lambda f.\lambda x.f^3x\bigr)(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0)\bigr)&&\text{(definition)}\\&=\mathrm{first}\bigl(\bigl(\lambda x.(\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))^3x\bigr)(0,0)\bigr)&&\text{(β-reduction)}\\&=\mathrm{first}\bigl((\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))^3(0,0)\bigr)&&\text{(β-reduction)}\\&=\mathrm{first}\bigl(F^3(0,0)\bigr)&&(F:=\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))\\&=\mathrm{first}(F(F(F(0,0))))&&\text{(definition)}\\&=\mathrm{first}(F(F((\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,0))))&&\text{(definition)}\\&=\mathrm{first}(F(F(\mathrm{pair}(\mathrm{second}(0,0))(\mathrm{succ}(\mathrm{second}(0,0))))))&&\text{(β-reduction)}\\&=\mathrm{first}(F(F(\mathrm{pair}\,0(\mathrm{succ}\,0))))&&\text{(referencing)}\\&=\mathrm{first}(F(F(\mathrm{pair}\,0\,1)))&&\text{(successor)}\\&=\mathrm{first}(F(F(0,1)))&&\text{(pairing)}\\&=\mathrm{first}(F((\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(0,1)))&&\text{(definition)}\\&=\mathrm{first}(F(\mathrm{pair}(\mathrm{second}(0,1))(\mathrm{succ}(\mathrm{second}(0,1)))))&&\text{(β-reduction)}\\&=\mathrm{first}(F(\mathrm{pair}\,1(\mathrm{succ}\,1)))&&\text{(referencing)}\\&=\mathrm{first}(F(\mathrm{pair}\,1\,2))&&\text{(successor)}\\&=\mathrm{first}(F(1,2))&&\text{(pairing)}\\&=\mathrm{first}((\lambda p.\mathrm{pair}(\mathrm{second}\,p)(\mathrm{succ}(\mathrm{second}\,p)))(1,2))&&\text{(definition)}\\&=\mathrm{first}(\mathrm{pair}(\mathrm{second}(1,2))(\mathrm{succ}(\mathrm{second}(1,2))))&&\text{(β-reduction)}\\&=\mathrm{first}(\mathrm{pair}\,2(\mathrm{succ}\,2))&&\text{(referencing)}\\&=\mathrm{first}(\mathrm{pair}\,2\,3)&&\text{(successor)}\\&=\mathrm{first}(2,3)&&\text{(pairing)}\\&=2&&\text{(referencing)}\end{aligned})]

뺄셈 연산 [math(\mathrm{sub})]는 이전 수 연산 [math(\mathrm{pred})]로 정의한다.

뺄셈 연산의 정의

[math(\mathrm{sub}:=\lambda m.\lambda n.n\,\mathrm{pred}\,m)]

4.1.5. 재귀 함수

재귀 함수를 구현하려면 일단 고정점 조합자에 대한 배경지식이 필요하다.

함수 [math(f)]에 대해 [math(f(x)=x)]를 만족하는 [math(x)]를 [math(f)]의 고정점\[fixed point\]이라고 한다. 예를 들어, 함수 [math(f(x)=x^2-2)]의 고정점은 [math(2)]와 [math(-1)]이다. 고정점을 가지는 함수를 입력받아 해당 함수의 고정점을 출력하는 함수를 고정점 조합자\[fixed point combinator\]라고 한다. 고정점 조합자 [math(\mathrm{fix})]와 고정점을 가지는 어떤 함수 [math(f)]에 대해 [math(\mathrm{fix}(f))]는 [math(f)]의 고정점이고, 따라서 [math(f(\mathrm{fix}(f))=\mathrm{fix}(f))]를 만족한다.

람다 대수의 모든 람다 항에는 고정점이 존재함이 알려져 있다. 그리고 고정점 조합자도 존재하는데, 다음과 같다.

[math(Y:=\lambda f.(\lambda x.f(xx))\lambda x.f(xx))]

이를 [math(Y)] 조합자라고 한다. 임의의 람다 항 [math(f)]에 대해 [math(Y)]가 잘 작동하는지는 다음과 같이 확인할 수 있다.

[math(\begin{aligned}Yf&=(\lambda f.(\lambda x.f(xx))\lambda x.f(xx))f&&\text{(definition)}\\&=(\lambda x.f(xx))\lambda x.f(xx)&&\text{(β-reduction)}\\&=f((\lambda x.f(xx))\lambda x.f(xx))&&\text{(β-reduction)}\\&=f(Yf)&&(Yf=(\lambda x.f(xx))\lambda x.f(xx))\end{aligned})]

여기서는 중요하지 않으나 람다 대수에서는 [math(Y)] 조합자 외에도 다른 고정점 조합자가 존재한다는 점은 알고 넘어가자.

이제 [math(Y)] 조합자를 이용해 재귀 함수를 정의하고자 한다. 재귀 함수는 함수 정의에서 자기 자신을 이용하는 함수를 뜻한다. 예를 들어, 계승은 다음과 같이 정의되므로 재귀 함수로 정의할 수 있다.

계승의 재귀적 정의

[math(n!=\begin{cases}1,&n=0\\n\times(n-1)!,&n>0\end{cases})]

하지만 람다 대수에서는 함수를 정의할 때 함수에 이름을 붙이지 않으므로 정의 내에 자기 자신을 이용할 수 없다. 이때 고정점 조합자를 이용하게 된다. 람다 대수에서 재귀 함수는 다음 방법으로 정의된다.

자기 자신이 쓰여야 할 곳을 임의의 변수 [math(f)]로 두고 정의하고자 하는 함수를 정의한다. 이 람다 항을 [math(t)]라고 하면 [math(f\in\mathrm{FV}(t))]이다.
[math(f)]를 매개 변수로, [math(t)]를 함수식으로 하는 람다 항 [math(F:=\lambda f.t)]를 정의한다.
[math(F)]를 [math(Y)] 조합자에 대입한 함수 [math(YF)]는 원하는 재귀 함수이다.

2에서 3으로 갑자기 뛰어넘은 것 같지만, 생각보다 쉽게 그 이유를 알 수 있다. [math(F)]는 함수를 입력받아 이를 재귀 함수가 들어가야 할 자리에 넣으므로, 재귀 함수는 [math(F)]에 재귀 함수를 대입한 것과 같아야 함을 알 수 있다. 그런데 고정점 조합자의 성질에서 [math(YF=F(YF))]이므로 [math(YF)]는 [math(F)]의 재귀 함수가 들어갈 자리에 자기 자신 [math(YF)]를 넣은 것과 같다. 그러므로 [math(YF)]는 우리가 원하던 재귀 함수임을 알 수 있다.

예시로 직접 계승 함수 [math(\mathrm{fac})]을 정의해 보자. 계승의 정의를 말로 풀면 다음과 같다.

[math(\mathrm{fac}(n):=\text{if }n=0\text{ then }1\text{ else }n\,\mathrm{fac}(n-1))]

이제 1, 2번 과정을 적용하자.

[math(\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))]

마지막으로 3번 과정까지 적용하면 [math(\mathrm{fac})]은 다음과 같다.

계승의 정의

[math(\mathrm{fac}:=Y\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))]

예시로 [math(\mathrm{fac}\,3)]을 계산하면 다음과 같다.

[펼치기·접기]: [math(\begin{aligned}\mathrm{fac}\,3&=Y(\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))3&&\text{(definition)}\\&=YF\,3&&(F:=\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))\\&=(\lambda f.(\lambda x.f(xx))\lambda x.f(xx))F\,3&&\text{(definition)}\\&=(\lambda x.F(xx))(\lambda x.F(xx))3&&\text{(β-reduction)}\\&=GG\,3&&(G:=\lambda x.F(xx))\\&=F(GG)3&&(GG=YF=F(YF)=F(GG))\\&=(\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))(GG)3&&\text{(definition)}\\&=(\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(GG(\mathrm{pred}\,n))))3&&\text{(β-reduction)}\\&=\mathrm{isZero}\,3\,1(\mathrm{mul}\,3(GG(\mathrm{pred}\,3)))&&\text{(β-reduction)}\\&=\mathrm{false}\,1(\mathrm{mul}\,3(GG(\mathrm{pred}\,3)))&&\text{(predicate)}\\&=\mathrm{mul}\,3(GG(\mathrm{pred}\,3))&&\text{(condition)}\\&=\mathrm{mul}\,3(GG\,2)&&\text{(predecessor)}\\&=\mathrm{mul}\,3(F(GG)2)&&(GG=F(GG))\\&=\mathrm{mul}\,3((\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))(GG)2)&&\text{(definition)}\\&=\mathrm{mul}\,3((\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(GG(\mathrm{pred}\,n))))2)&&\text{(β-reduction)}\\&=\mathrm{mul}\,3(\mathrm{isZero}\,2\,1(\mathrm{mul}\,2(GG(\mathrm{pred}\,2))))&&\text{(β-reduction)}\\&=\mathrm{mul}\,3(\mathrm{false}\,1(\mathrm{mul}\,2(GG(\mathrm{pred}\,2))))&&\text{(predicate)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(GG(\mathrm{pred}\,2)))&&\text{(condition)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(GG\,1))&&\text{(predecessor)}\\&=\cdots\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1(GG\,0)))&&\text{(predecessor)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1(F(GG)0)))&&(GG=F(GG))\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1((\lambda f.\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(f(\mathrm{pred}\,n))))(GG)0)))&&\text{(definition)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1((\lambda n.\mathrm{isZero}\,n1(\mathrm{mul}\,n(GG(\mathrm{pred}\,n))))0)))&&\text{(β-reduction)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1(\mathrm{isZero}\,0\,1(\mathrm{mul}\,0(GG(\mathrm{pred}\,0))))))&&\text{(β-reduction)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1(\mathrm{true}\,1(\mathrm{mul}\,0(GG(\mathrm{pred}\,0))))))&&\text{(predicate)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2(\mathrm{mul}\,1\,1))&&\text{(condition)}\\&=\mathrm{mul}\,3(\mathrm{mul}\,2\,1)&&\text{(multiplication)}\\&=\mathrm{mul}\,3\,2&&\text{(multiplication)}\\&=6&&\text{(multiplication)}\end{aligned})]

이제 자연수의 나눗셈 연산 [math(\mathrm{div})]를 정의하자. 자연수의 나눗셈은 다음과 같이 재귀적으로 정의할 수 있다.

자연수의 나눗셈의 재귀적 정의

[math(\mathrm{div}(m,n):=\text{if }m<n\text{ then }0\text{ else }\mathrm{div}(m-n,n)+1)]

위의 방법으로 [math(\mathrm{div})]를 정의하면 다음과 같다.

나눗셈 연산의 정의

[math(\mathrm{div}:=Y\lambda f.\lambda m.\lambda n.\mathrm{lt}\,mn0(\mathrm{succ}(f(\mathrm{sub}\,mn)n)))]

4.1.6. 기타

여기서부터는 굳이 람다 항까지 도출하지는 말고, 감만 잡아 보는 느낌으로 정의해 보자.

예를 들어, 정수는 두 자연수의 쌍으로 구현할 수 있을 것이다. 이 자연수 쌍은 1번째에서 2번째를 뺀 값을 뜻하며, 조금만 생각하면 이렇게 부호화한 정수 사이의 사칙 연산도 구현할 수 있을 것이다. 비슷한 방식으로 유리수는 두 정수의 쌍으로 구현할 수 있다. 이 정수 쌍은 1번째를 2번째로 나눈 값을 뜻하며, 역시 이렇게 부호화한 유리수의 사칙 연산도 구현할 수 있다.

실수는 람다 항으로 부호화할 수 없다. 가능한 람다 항의 개수는 실수보다 작기 때문이다. 하지만 참값을 포기하고 특정한 유효 숫자 아래의 정보를 무시해 버리면 어느 정도의 오차율을 가지고 부호화할 수 있다. 이는 컴퓨터에서 실수를 그대로 표현할 수 없어 부동 소수점을 이용해 표현한다는 점과 비슷하다.

리스트는 쌍을 겹쳐서 표현할 수 있다. 예를 들어, [math((1,2,3,4,5))]는 [math(((1,(2,(3,(4,(5,\mathrm{false}))))),5))] 등으로 표현할 수도 있을 것이다. 리스트와 자연수를 받아서 원하는 위치의 원소를 꺼내는 연산, 새로운 원소를 추가하는 연산 등도 잘 생각해 보면 모두 구현할 수 있을 것이다.

지금까지 많은 대상을 람다 항으로 구현해 봤다. 사실 이를 어떻게 구현했는지는 중요하지 않다. 이는 컴퓨터에서 실수를 어떤 경우에는 부동 소수점으로, 어떤 경우에는 고정 소수점으로 부호화하고, 얼마나 정확하게 표현할지 등도 상황에 따라 달라지는 것을 생각하면 된다. 그저 부호화한 방법에 맞게 연산도 부호화하면 되는 것이다.

4.2. 프로그래밍 언어

람다 대수는 튜링 기계와 동치이기는 하지만, 컴퓨터는 기계이다 보니 람다 대수보다는 튜링 기계와 더 닮았다는 느낌이 들 것이다. 그래도 람다 대수가 더 활약할 만한 분야가 있는데, 바로 프로그래밍 언어 분야이다.

4.2.1. 익명 함수

람다 대수의 핵심은 함수를 값처럼 생각하는 것이다. 이렇게 함수를 값으로 보는 익명 함수의 개념은 모든 대상을 객체로 보는 객체 지향형 언어와 잘 맞는다. 함수도 하나의 객체로 본다면 이러한 객체를 입력받는다든지, 이러한 객체를 출력한다든지 하는 고차 함수를 생각할 수 있을 것이다. 이러한 고차 함수의 인자로 익명 함수를 사용하면 코드를 더 간단하고 가독성 있게 적을 수 있다.

다음은 Python 예시이다. Python에서는 익명 함수를 lambda로 선언하는데, 람다 대수 때문에 이렇게 선언한다고도 할 수 있다. map은 함수와 리스트 같은 인자를 받아 각 원소에 함수를 적용하는 함수[8]이다. 다음은 0부터 9까지 들어간 리스트에 [math(x\mapsto2x+1)]을 적용하는 예시이다.

#!syntax python
my_input = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
my_map = map(lambda x: 2*x + 1, my_input)
my_output = list(my_map)
print(my_output)  # [1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

4.2.2. 자료형

람다 대수는 안전한 자료형(type safety)을 만들 때도 이용된다. 일반적으로 프로그래밍 언어에는 여러 자료형이 존재하는데, 실행해 보기 전에 각 변수의 자료형이 어떻게 변할지 파악하는 건 기계적으로 계산 불가능하다. 그래서 과거 많은 언어에서는 각 변수의 자료형을 고정하고, 이를 모두 선언하게 하는 방식으로 해결했다. 하지만 람다 대수를 이용하면 굳이 이렇게 각 변수의 자료형을 명시하지 않아도 안전하게 자료형 추론을 할 수 있다. 이런 람다 대수의 특징을 가지고 만들어진 언어를 함수형 언어로 분류한다. 함수형 언어에서는 모든 알고리즘을 상수[9]와 함수만으로 정의할 수 있도록 설계돼 있다.

이제 람다 항에 자료형을 추가한 람다 대수를 생각해 보자. 이를 자료형 람다 대수(typed lambda calculus)라고 한다. 이에 반해 자료형이 없는 원래의 람다 대수를 무자료형 람다 대수(untyped lambda calculus)라고 하기도 한다. 자료형 람다 대수에서는 모든 람다 항이 자료형을 가지며, 이에 따라 함수의 적용에 제한이 생긴다. 즉, 자료형이 맞지 않는 연산은 허용되지 않는다.

자료형 람다 대수에서 어떤 람다 항이 어떤 자료형을 가지는지를 가지고 있는 집합을 자료형 환경(type environment)이라고 하고, 보통 [math(\Gamma)]로 나타낸다. 람다 항 [math(x)]의 자료형이 자료형 [math(\tau)]라는 것은 [math(x{:}\tau)]로 나타내며, 자료형 환경 [math(\Gamma)]에서 람다 항 [math(x)]의 자료형이 자료형 [math(\tau)]라는 것은 [math(\Gamma\vdash x:\tau)]로 나타낸다.

자료형 람다 대수에는 자료형의 범위와 제한에 따라 여러 종류가 있다. 일단은 간단하게 단순 자료형 람다 대수(simply typed lambda calculus)를 보자. 단순 자료형 람다 대수는 자료형이 기본 자료형과 함수 자료형만으로 이루어진 람다 대수이다. 단순 자료형 람다 대수에서 자료형은 다음과 같이 정의된다.

[math(\tau)]는 자료형이다.
자료형 [math(\sigma)], [math(\tau)]에 대해, [math(\sigma\rightarrow\tau)]는 자료형이다.

자료형 [math(\sigma\rightarrow\tau)]는 자료형이 [math(\sigma)]인 람다 항을 받아 변수형이 [math(\tau)]인 람다 항을 반환하는 함수의 자료형을 나타낸다. 당연히 함수를 받거나 함수를 반환하는 함수도 가능하며, 화살표의 우선순위는 오른쪽부터로 한다. 즉, 자료형 [math(\tau\rightarrow\sigma\rightarrow\tau)]는 자료형이 [math(\tau)]인 람다 항을 받아 자료형이 [math(\sigma\rightarrow\tau)]인 람다 항을 반환하는 함수의 자료형, [math(\tau\rightarrow(\sigma\rightarrow\tau))]를 뜻한다.

단순 자료형 람다 대수의 변환 규칙은 다음과 같다.

[math(x{:}\tau\in\Gamma\Rightarrow\Gamma\vdash x:\tau)]
[math(\Gamma\cup\{x{:}\sigma\}\vdash e:\tau\Rightarrow\Gamma\vdash(\lambda x{:}\sigma.e):\sigma\rightarrow\tau)]
[math(\Gamma\vdash e_1:\sigma\rightarrow\tau\land\Gamma\vdash e_2:\sigma\Rightarrow\Gamma\vdash e_1e_2:\tau)]

각각은 람다 항에서 자료형을 정하는 직관적인 규칙이다. 예를 들어, 위에서 정의한 자연수의 덧셈 연산 [math(\mathrm{add})]를 생각하면 이 람다 항의 자료형은 [math(\N\rightarrow\N\rightarrow\N)]이며, 자료형이 [math(\N)]인 람다 항 2개를 받아 자료형이 [math(\N)]인 람다 항을 내는 함수로 생각할 수 있다. 예시로 [math(\mathrm{add}\,2\,3)]의 자료형을 보면 다음과 같다.

[math(\begin{aligned}\mathrm{add}\,2\,3&=(\mathrm{add}{:}\N\rightarrow\N\rightarrow\N)(2{:}\N)(3{:}\N)\\&=((\mathrm{add}\,2){:}\N\rightarrow\N)(3{:}\N)\\&=(\mathrm{add}\,2\,3){:}\N\\&=5{:}\N\end{aligned})]

단순 자료형 람다 대수는 간단하면서도 유용하지만, 프로그래밍 언어로서는 많이 부족하다. 일단 자료형에 의한 제한 조건 때문에 모든 고정점 조합자가 불가능해지고, 이에 따라 재귀적인 정의도 불가능하다. 그래서 실제로 프로그래밍 언어를 설계할 때는 단순 자료형 람다 대수를 엄격하게 구현하는 대신, 재귀 함수 관련 문법을 직접 추가하는 등의 방법으로 이런 점들을 해결한다. 그래도 다른 부족한 점이 있는데, 바로 다형성이다.

다형성(polymorphism)이란 함수가 상황에 따라 여러 방식으로 사용될 수 있는 성질을 뜻한다. 다형성에도 여러 종류가 있지만, 여기서는 매개 변수 다형성을 주로 보도록 한다. 매개 변수 다형성(parametric polymorphism)이란 함수의 매개 변수가 상황에 따라 여러 자료형으로 해석될 수 있는 성질을 뜻한다. 예를 들어, 람다 대수에서의 항등 함수 [math(\lambda x.x)]는 어떤 람다 항에 대해서도 잘 작동한다.[10] 그렇다면 당연히 이 람다 항을 한 번만 정의해 여러 자료형에도 쓰고 싶을 것이다. 하지만 단순 자료형 람다 대수에서는 매개 변수의 자료형이 정해져야 하므로 그렇게 할 수 없다. 그래서 같은 일을 하는 함수를 각 자료형마다 정의해서 그때그때마다 알맞은 자료형의 함수를 사용해야 한다.[11] 이런 점에서 단순 자료형 람다 대수는 매개 변수 다형성이 없다고 할 수 있다. 그래서 단순 자료형 람다 대수에서 더 확장한 자료형 체계를 만들어야 하는데, 대표적인 예시가 바로 힌들리·밀너 자료형 체계이다.

힌들리·밀너 자료형 체계 또는 HM 자료형 체계(Hindley–Milner type system, HM type system)는 단순 자료형 람다 대수에 let 다형성을 추가한 자료형 체계이다. 그냥 일반적인 다형성을 추가하면 변수의 자료형을 판단하는 문제가 계산 불가능해지기 때문에 값과 범위를 미리 선언한 자료형[12]에 대해서만 다형성을 보장한다. 이를 통해 자료형을 명시적으로 선언하지 않아도 많은 경우 자료형을 기계적으로 추론할 수 있으며, 더 나아가 이렇게 추론이 가능한 경우에는 자료형 오류가 없음이 보장된다. 이러한 안정성 덕분에 HM 자료형 체계를 사용하는 언어에서는 명시적인 자료형 선언이 필요없다. HM 자료형 체계를 적용한 언어로는 ML, OCaml, F# Haskell 등이 있다.

[1] http://ropas.snu.ac.kr/~kwang/4190.310/11/pl-book-draft.pdf[2] 수열은 정의역이 자연수인 함수이다.[3] 정확히는 [math(0)], [math(n)]도 정의역에 포함해야 하지만, 일단 이 문단에서는 무시하자.[4] [math(\mathcal F(\R,\R))]는 [math(\R)]에서 [math(\R)]로 가는 함수의 집합을 뜻한다.[5] 프로그래밍 언어 Haskell의 명칭도 이 사람의 이름에서 따왔다.[6] 실제로는 람다 대수를 이용한 계산 불가능성 증명이 튜링 기계보다 먼저 나왔다.[7] 연산을 구분하기 위해 어떤 집합에서 정의된 연산인지를 아래첨자로 나타냈다.[8] 정확히는 클래스이다.[9] 명령형 언어에서 쓰이는 저장 공간으로서의 변수와는 다르다. 변수 같은 게 존재는 하는데, 함수의 매개 변수나 뒤에서 쓸 값을 지칭할 목적으로 이름을 붙이는 것일 뿐이다. 애초에 변수가 아닌 상수이므로 변경할 수도 없다.[10] 무자료형 람다 대수는 대입에 제한이 없으므로 여기서 잘 작동한다는 건 유의미한 출력을 반환한다는 의미라고 생각하자. 예를 들어, 위에서 본 자연수의 덧셈 연산 [math(\mathrm{add})]는 처치 부호화 한 자연수에 대해서는 잘 작동하지만, 다른 람다 항을 대입하면 가능은 하지만 딱히 의미는 없는 람다 항이 나올 것이다.[11] 실제로 C 등의 언어에서는 이렇게 해야 한다.[12] 많은 경우 'let ... in ...' 꼴로 선언하기 때문에 let 다형성이라고 한다.