단순 타입 람다 계산(Simply typed lambda calculus)

람다 계산에서는 아무 항에나 아무 항을 적용할 수 있습니다. 그래서 $\Omega = (\lambda x.\,x\,x)(\lambda x.\,x\,x)$처럼 줄여도 줄여도 제자리로 돌아오는 항이 생깁니다. 1940년 처치는 변수마다 타입을 붙인 체계를 내놓았고, 아래에서 보듯 이 체계에서는 이런 항이 아예 타입을 받지 못합니다. 타입은 A, B, C 같은 기본 타입에서 시작해 화살표로 짓습니다. $A \to B$는 'A를 받아 B를 돌려주는 함수⁠(function)⁠'의 타입입니다. 화살표는 오른쪽부터 묶어서, $A \to B \to C$는 $A \to (B \to C)$, 곧 A를 받아 'B를 받아 C를 돌려주는 함수'를 돌려주는 함수입니다. 두 인자를 받는 함수를 이렇게 한 번에 하나씩 받는 함수로 적습니다. 함수를 만들 때는 $\lambda x{:}A.\,M$처럼 입력의 타입을 적습니다.

규칙은 셋뿐입니다. 가로줄 위의 판단이 모두 성립하면 아래 판단도 성립한다고 읽습니다. Γ는 '어떤 변수가 어떤 타입이라고 가정하는지'를 적은 목록(문맥)입니다.

$$\dfrac{x : A \in \Gamma}{\Gamma \vdash x : A}\;\text{Var} \qquad \dfrac{\Gamma,\, x : A \vdash M : B}{\Gamma \vdash \lambda x{:}A.\,M : A \to B}\;\text{Abs} \qquad \dfrac{\Gamma \vdash M : A \to B \qquad \Gamma \vdash N : A}{\Gamma \vdash M\,N : B}\;\text{App}$$

Var는 가정해 둔 것은 쓸 수 있다는 규칙입니다. Abs는 'x가 A라고 두었을 때 M이 B이면, λx:A. M은 A에서 B로 가는 함수'라는 규칙인데, 아래 줄에서는 가정 x : A가 사라집니다. x가 λ에 묶여 더는 바깥의 가정이 아니기 때문입니다. App은 함수가 받는 타입과 인자의 타입이 같아야 적용할 수 있다는 규칙입니다. 이 규칙들로 한 항의 타입을 이끌어 낸 기록을 유도라고 하며, 결론을 맨 아래에 두고 위로 가지를 뻗는 나무로 적습니다.

검사할 항:

합성 함수 $\lambda f{:}B{\to}C.\,\lambda g{:}A{\to}B.\,\lambda x{:}A.\,f\,(g\,x)$를 따라가 봅시다. 검사기는 맨 아래의 목표에서 시작합니다. λ를 만날 때마다 Abs 규칙을 거꾸로 읽어 문맥에 가정을 하나씩 더하고 위로 올라갑니다. $f\,(g\,x)$에서는 App 규칙이 가지를 둘로 나눕니다. 잎⁠(leaf)⁠에 닿으면 Var 규칙으로 타입이 정해지고, 그 타입이 가지를 따라 아래로 내려오며 조립됩니다. $g : A \to B$와 $x : A$에서 $g\,x : B$, 그다음 $f : B \to C$이니 $f\,(g\,x) : C$, 끝으로 λ 셋을 거쳐 뿌리의 타입 $(B \to C) \to (A \to B) \to A \to C$가 나옵니다. 검사는 항의 각 부분을 한 번씩 방문하고 끝나며, 항을 한 번도 계산하지 않습니다.

자기 적용 $\lambda x{:}A.\,x\,x$를 고르면 App에서 검사가 실패합니다. x의 타입 A가 화살표 꼴이 아니기 때문입니다. x에 다른 타입 T를 적어도 소용없습니다. $x\,x$가 타입을 가지려면 앞의 x는 $T \to U$ 꼴이고 뒤의 x는 T여야 하므로 $T = T \to U$가 필요합니다. 타입은 유한한 식이고 $T \to U$는 T보다 엄격히 긴 식이니, 이런 T는 없습니다. 그래서 Ω도, 고정점⁠(fixed point)⁠을 만들어 되부름을 흉내 내던 Y 조합자⁠(Y combinator)⁠도 이 체계에서는 타입을 받지 못합니다.

이렇게 걸러 낸 대가로 얻는 것이 강정규화 정리입니다. 타입이 붙는 항은 어느 곳부터 어떤 순서로 줄이든 유한한 걸음 안에 더 줄일 곳이 없는 정규형⁠(normal form)⁠에 닿습니다. 당연해 보이지 않는 까닭은 β-축약⁠(β-reduction)⁠이 항을 길게 만들 수 있어서입니다. $g : A \to A \to A \to B$일 때 $(\lambda x{:}A.\,g\,x\,x\,x)\,N$은 N을 세 벌로 복사하고, N 안에 줄일 곳이 있었다면 그것도 세 벌이 됩니다. 핵심 관찰은 이것입니다. $(\lambda x{:}A.\,M)\,N$(함수의 타입 $A \to B$)을 줄여 새로 생기는 축약 가능한 곳은, N이 x 자리에 들어가 무엇에 적용되는 곳이거나 결과 전체가 무엇에 적용되는 곳뿐입니다. 그 새 함수들의 타입은 A 또는 B이고, 원래 함수의 타입 $A \to B$보다 짧습니다. 그래서 가장 긴 타입의 축약 가능한 곳 가운데 가장 오른쪽 것을 고르면, 복사되는 N 안에는 그만큼 긴 곳이 없습니다. 이 순서로 줄이면 가장 긴 타입의 축약 가능한 곳이 한 걸음마다 하나씩 줄고, 다 없어지면 한 단계 짧은 타입으로 내려가므로 결국 끝납니다. 튜링이 1940년대에 남긴 원고의 논증이 이것으로, 로빈 갠디가 1980년에 소개했습니다. 이 논증은 '잘 고른 순서로는 끝난다'(약정규화⁠, weak normalization⁠)까지를 보여 줍니다.

어떤 순서로 줄여도 끝난다는 강한 형태는 미국 논리학자 윌리엄 테이트가 1967년에 도입한 방법으로 증명합니다. '끝난다'를 직접 귀납으로 증명하려 하면 App 규칙에서 막힙니다. M과 N이 각각 끝나도 M N이 끝난다는 보장은 없기 때문입니다. 테이트는 더 강한 성질 '타입 A에서 환원 가능하다'를 항이 아니라 타입의 모양에 대한 귀납으로 정의했습니다. 기본 타입에서는 '어떤 순서로 줄여도 끝난다'이고, $A \to B$에서는 'A에서 환원 가능한 것을 넣으면 늘 B에서 환원 가능한 것이 나온다'입니다. 타입이 붙는 항은 모두 환원 가능하고, 환원 가능한 항은 끝난다는 두 단계로 정리가 증명됩니다. 타입이 없는 람다 계산에서는 이런 귀납을 걸 곳이 없습니다.

대가도 분명합니다. 모든 계산이 끝나는 언어는 튜링 기계⁠(Turing machine)⁠만큼 강할 수 없습니다. 이유는 정지 문제⁠(halting problem)⁠와 같은 대각선 논법입니다. 프로그램이 모두 끝나고, 프로그램을 수로 적어 입력으로 줄 수 있으며, 그 실행을 기계적으로 흉내 낼 수 있는 언어가 있다고 합시다. 그러면 '프로그램 p에 입력 p를 넣어 나온 값에 1을 더하라'는 함수는 늘 끝나는 계산 가능한 함수입니다. 이 함수가 그 언어의 프로그램 q로 적힌다면 q에 q를 넣은 값은 자기 자신보다 1이 커야 하니 모순입니다. 따라서 그 언어로 적을 수 없는, 늘 끝나는 계산 가능한 함수가 반드시 있습니다(칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠과 같은 모양입니다). 단순 타입 람다 계산의 한계는 훨씬 더 좁습니다. 처치 수⁠(Church numeral)⁠의 타입을 $N = (A \to A) \to A \to A$로 고정하면, N에서 N으로 가는 함수(여러 인자라면 N → ⋯ → N → N)로는 상수·덧셈·곱셈과 '0인지 보고 고르기'를 조합한 것만 적힙니다(헬무트 슈비히텐베르크, 1976). 거듭제곱 $m^n$은 n을 한 단계 높은 타입에 적용하면 만들 수 있지만, 그러면 입력과 출력의 타입이 같지 않습니다.

되부름을 되찾는 방법은 상수 하나를 더하는 것입니다. $\mathrm{fix} : (A \to A) \to A$이고 $\mathrm{fix}\,f \to f\,(\mathrm{fix}\,f)$로 계산되는 상수를 넣은 언어가 1977년 고든 플롯킨이 연구한 PCF이며, 여러 함수형 언어⁠(functional programming language)⁠의 뼈대입니다. 그 순간 강정규화는 사라집니다. $\mathrm{fix}\,(\lambda x{:}A.\,x)$는 끝없이 자기 자신으로 펼쳐집니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 읽으면 더 심각합니다. 이 항은 아무 명제 A의 '증명'이 되어 버리므로, 논리로서는 모순입니다. 증명 보조기⁠(proof assistant)⁠가 되부름을 허락하되 끝남이 보장되는 모양(인자가 매번 작아지는 되부름)만 받아들이는 까닭이 이것입니다.

흔한 오해 둘을 짚어 둡니다. 하나, 타입 검사가 쉬우니 '이 타입의 항이 있는가'도 쉬울 것 같지만 그렇지 않습니다. 닫힌 항(자유 변수가 없는 항)으로 채워지는 타입인지 묻는 거주 문제⁠(type inhabitation)⁠는 PSPACE 완전입니다(리처드 스탯먼, 1979). PSPACE는 다항식⁠(polynomial)⁠ 크기의 기억 공간으로 풀리는 문제들의 부류로 NP를 포함하며, 그 안에서 가장 어려운 문제들과 같은 급이라는 뜻입니다(P 대 NP 문제⁠(P versus NP problem)⁠ 참고). 이 문제는 직관주의⁠(intuitionism)⁠ 명제 논리⁠(propositional logic)⁠에서 '이면'만 쓴 식이 증명되는지 묻는 문제와 같습니다. 둘, 이 체계는 장난감이 아닙니다. 곱 타입⁠(product type)⁠ $A \times B$와 원소⁠(element)⁠ 하나짜리 타입 1을 더한 단순 타입 람다 계산은 데카르트 닫힌 범주⁠(cartesian closed category)⁠의 내부 언어라서, 집합⁠(set)⁠과 함수, 영역 이론⁠(domain theory)⁠의 공간, 논리의 증명 등 서로 다른 세계를 한꺼번에 기술합니다.

이어지는 곳. 위의 규칙에서 항을 지우고 타입만 남기면 자연 연역⁠(natural deduction)⁠의 논리 규칙이 되고, App은 전건 긍정⁠(modus ponens)⁠, Abs는 가정 내려놓기가 됩니다. 이 관찰이 커리–하워드 대응이며, 같은 유도를 증명으로 읽는 그림이 거기에 있습니다. 타입을 적지 않은 항에서 가장 일반적인 타입을 찾아내는 방법이 힌들리–밀너 타입 추론⁠(type inference)⁠입니다. 타입 변수와 '모든 타입에 대해'를 더하면 시스템 F⁠(System F)⁠가 되고, 강정규화는 유지되지만 증명은 훨씬 어려워집니다. 모든 계산이 끝난다는 보장과 튜링 완전성이 함께할 수 없는 이유는 정지 문제의 대각선 논법⁠(diagonal argument)⁠과 같습니다. 유도의 모양은 수학적 귀납법⁠(mathematical induction)⁠의 구조를 따라가므로, 이 체계에 관한 정리는 거의 모두 유도나 타입에 대한 귀납으로 증명됩니다. 되부름 상수 fix를 더해 생기는 끝나지 않는 항들이 무엇을 뜻하는지를 '아직 모름' ⊥에서 시작한 가장 작은 고정점으로 정하는 것이 영역 이론입니다.