데카르트 닫힌 범주(Cartesian closed category)

두 수를 더하는 함수⁠(function)⁠ add(x, y) = x + y를 조금 다르게 볼 수 있습니다. x를 받으면 'y를 받아 x + y를 돌려주는 함수'를 돌려주는 함수로 보는 것입니다. add 3은 '3 더하기'라는 함수이고, 그것에 4를 넣으면 7입니다. 두 인자 함수를 '한 인자 함수를 돌려주는 함수'로 바꾸는 이 일을 커링(currying)이라 합니다. 논리학자 해스켈 커리의 이름을 땄지만, 모제스 쇤핑켈이 1924년에, 더 앞서 프레게가 이미 썼습니다. 유한 집합⁠(set)⁠으로 세어 보면 정확한 대응이 보입니다. A = {0, 1, 2}, B = {0, 1}, C = {0, 1}이라 하면 A × B → C 함수는 여섯 칸짜리 표를 0과 1로 채우는 방법이라 $2^6 = 64$가지입니다. B → C 함수는 $2^2 = 4$가지이므로, A에서 그 넷으로 가는 함수는 $4^3 = 64$가지입니다. 지수법칙 $c^{ab} = (c^b)^a$가 곧 커링입니다.

다른 표

데카르트 닫힌 범주(cartesian closed category)는 이 일이 가능한 범주입니다. 끝 대상 1과 모든 두 대상의 곱 A × B가 있고(보편 성질⁠, universal property⁠), 모든 A, B에 대해 '지수 대상⁠(exponential object)⁠' $B^A$와 계산 화살표 $\mathrm{ev}: B^A\times A\to B$가 있어서, 아무 화살표 $f: C\times A\to B$에 대해 $\mathrm{ev}\circ(\lambda f\times\mathrm{id}_A) = f$인 $\lambda f: C\to B^A$가 정확히 하나 있습니다. 같은 말을 수반 함자⁠(adjoint functor)⁠로 하면

$$\mathrm{Hom}(C\times A,\,B)\;\cong\;\mathrm{Hom}(C,\,B^{A}),\qquad(-\times A)\dashv(-)^{A}$$

입니다. C = 1로 두면 $\mathrm{Hom}(1, B^A)\cong\mathrm{Hom}(A, B)$, 곧 $B^A$의 '점'(1에서 오는 화살표)들이 A → B 화살표들입니다. 범주 바깥에서 모으던 화살표들의 모음이 범주 안의 대상 하나로 들어온 것입니다. '닫혀 있다'는 말이 이 뜻입니다.

집합과 함수의 범주는 데카르트 닫힌 범주입니다. $B^A$는 A → B 함수 전체의 집합입니다. 순서에서는 곱이 하한⁠(lower bound)⁠ ∧이고, 지수는 $x\wedge a\le b\iff x\le(a\Rightarrow b)$를 만족하는 '이면' $a\Rightarrow b$입니다. 곱과 이면을 가진(그리고 합과 가장 작은 원소⁠(element)⁠도 가진) 이런 순서를 헤이팅 대수라 합니다. 불 대수⁠(Boolean algebra)⁠는 $a\Rightarrow b = \lnot a\vee b$로 헤이팅 대수⁠(Heyting algebra)⁠가 되지만, 헤이팅 대수에서는 배중률⁠(law of excluded middle)⁠ $a\vee\lnot a = 1$이 일반적으로 성립하지 않습니다. 실수⁠(real number)⁠ 직선의 열린 집합⁠(open set)⁠들이 좋은 예입니다. 여기서 부정 ¬U는 여집합⁠(complement)⁠의 내부입니다. U = (0, ∞)이면 ¬U = (−∞, 0)이고, U ∪ ¬U에는 0 하나가 빠져 전체가 되지 못합니다(위상수학⁠(topology)⁠). 이것이 직관주의 논리⁠(intuitionistic logic)⁠의 대수적 모습입니다. 작은 범주들의 범주 Cat(지수는 함자 범주⁠(functor category)⁠), 작은 범주에서 집합의 범주로 가는 함자⁠(functor)⁠들의 범주, 그리고 이것을 일반화한 토포스(topos)도 데카르트 닫힌 범주입니다.

군의 범주와 벡터 공간⁠(vector space)⁠의 범주는 데카르트 닫힌 범주가 아닙니다. 이 둘에서는 원소 하나짜리 대상이 끝 대상이면서 동시에 시작 대상입니다. 그러면 $\mathrm{Hom}(A, B)\cong\mathrm{Hom}(1\times A, B)\cong\mathrm{Hom}(1, B^A)$이고, 1이 시작 대상⁠(initial object)⁠이라 마지막 집합의 원소는 하나뿐이니, 모든 Hom(A, B)가 원소 하나짜리가 되어야 합니다. 사실이 아니지요. 벡터 공간에는 대신 텐서곱⁠(tensor product)⁠으로 커링하는 다른 구조(닫힌 모노이드 범주⁠, closed monoidal category⁠)가 있습니다. 위상 공간⁠(topological space)⁠의 범주도 데카르트 닫힌 범주가 아니어서, 대수적 위상수학에서는 콤팩트 생성 공간처럼 좁힌 범주를 씁니다.

이 구조가 중요한 까닭은 단순 타입 람다 계산이 정확히 이 구조이기 때문입니다. 순서쌍 타입⁠(type)⁠과 단위 타입⁠(unit type)⁠을 가진 단순 타입 람다 계산에서 타입을 대상으로, '변수 x: A가 주어졌을 때 타입 B의 항'을 A → B 화살표로 두면 데카르트 닫힌 범주가 됩니다. 이때 아래의 βη-규칙으로 같아지는 항은 같은 화살표로 봅니다. 순서쌍 만들기는 곱의 ⟨f, g⟩, λ-추상화는 커링 λf, 함수 적용은 $\mathrm{ev}\circ\langle f, g\rangle$입니다. 람다 계산⁠(lambda calculus)⁠의 β-축약⁠(β-reduction)⁠ $(\lambda x.\,M)\,N\to M[x:=N]$은 등식 $\mathrm{ev}\circ(\lambda f\times\mathrm{id}) = f$에, η-규칙 $\lambda x.\,(M\,x) = M$(x가 M에 나오지 않을 때)은 'λf가 정확히 하나'라는 조건에 대응합니다. 정확히 말하면 이렇게 만든 범주는 기본 타입들에서 '자유롭게' 지은 데카르트 닫힌 범주입니다. 그래서 기본 타입의 뜻만 정해 주면 모든 항이 아무 데카르트 닫힌 범주에서나 하나의 화살표로 해석됩니다. 거꾸로 데카르트 닫힌 범주마다 그 대상들을 기본 타입으로 삼은 람다 계산(내부 언어)이 있어서, 그 범주 안의 계산을 람다 항으로 적을 수 있습니다. 1970–80년대 요아힘 람벡이 이 대응을 정리했고, 논리까지 더해 명제–타입–대상, 증명–프로그램–화살표를 잇는 이 삼각형을 커리–하워드–람벡 대응이라 부릅니다(커리–하워드 대응⁠, Curry–Howard correspondence⁠). '그리고'는 곱, '이면'은 지수, '참'은 끝 대상입니다. '또는'과 '거짓'까지 다루려면 쌍대곱⁠(coproduct)⁠과 시작 대상도 있어야 합니다.

이 틀에서 대각선 논법⁠(diagonal argument)⁠들이 한 정리로 모입니다. 1969년 로베어가 증명한 고정점 정리⁠(fixed-point theorem)⁠는, 데카르트 닫힌 범주에서 화살표 $\varphi: A\to B^A$가 $B^A$의 모든 점에 닿으면(점 전사⁠, point-surjective⁠), B에서 B로 가는 모든 화살표 f에 고정점⁠(fixed point)⁠이 있다는 것입니다. 증명은 대각선 하나입니다. 원소처럼 적어서 $q(a) = f(\varphi(a)(a))$로 두면 q도 $B^A$의 점이므로 어떤 $a_0$에 대해 $q = \varphi(a_0)$입니다. 그러면 $q(a_0) = f(\varphi(a_0)(a_0)) = f(q(a_0))$, 곧 $q(a_0)$이 f의 고정점입니다. 집합에서 B = {0, 1}, f = 부정(0과 1을 맞바꾸기)으로 두면 부정에는 고정점이 없으므로, A에서 A의 부분집합⁠(subset)⁠ 전체로 가는 전사⁠(surjective)⁠는 없습니다. 칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠입니다. 러셀의 역설⁠(Russell's paradox)⁠, 정지 문제⁠(halting problem)⁠, 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠의 논증도 같은 틀의 변형으로 읽을 수 있습니다. 반대로 타입이 없는 람다 계산에서는 모든 항이 함수이기도 해서, 1969년 데이나 스콧은 D와 (연속 함수만 모은) $D^D$가 동형⁠(isomorphism)⁠인 모형을 만들었습니다. 집합에서는 원소가 하나인 D만 이런 동형을 가지므로, 함수를 연속 함수로 좁히는 것이 핵심이었습니다. 그런 세계에서는 모든 (연속) 함수에 고정점이 있고, 람다 계산의 Y 조합자⁠(Y combinator)⁠가 그 고정점을 만듭니다.

프로그래밍에서 데카르트 닫힌 구조는 함수를 값으로 다루는 능력입니다. 함수를 인자로 넘기고, 함수를 돌려주고, 인자 일부만 먼저 넣어 새 함수를 만드는 일(부분 적용⁠, partial application⁠)이 모두 지수 대상과 커링입니다. Haskell에서는 모든 함수가 기본으로 커링되어 있어 add 3이 그대로 함수입니다. 다만 끝나지 않는 계산 같은 것 때문에 실제 언어가 이 구조를 엄밀히 만족하지는 않습니다. 상태 모나드⁠(monad)⁠ $S\to A\times S$도 커링의 수반에서 나옵니다(모나드).

이어지는 곳. 곱과 끝 대상의 정의는 보편 성질에, 커링이 수반이라는 관점은 수반 함자에 있습니다. 이 구조를 언어로 적은 것이 단순 타입 람다 계산이고, 타입을 명제로 읽으면 커리–하워드 대응, 순서로 읽으면 배중률이 없는 직관주의 논리입니다. 지수법칙 $c^{ab} = (c^b)^a$는 대수적 자료형⁠(algebraic data type)⁠에서 함수 타입의 값을 세는 법이 되고, 로베어의 고정점 정리는 대각선 논법, 고정점, 자기 참조⁠(self-reference)⁠를 한 줄로 잇습니다. 타입이 값에 따라 달라지는 의존 타입⁠(dependent type)⁠은 지수 대상을 Π 타입으로 넓힌 것이고, 그 위에서 증명을 검사하는 도구가 증명 보조기⁠(proof assistant)⁠입니다. 함수 집합의 크기⁠(cardinality)⁠ $|B^A| = |B|^{|A|}$에서 A를 무한으로 보내면 멱집합⁠(power set)⁠과 무한집합의 크기 이야기가 됩니다. 곱을 복사와 버리기가 없는 텐서곱으로 바꿔 커링하면 모노이드⁠(monoid)⁠ 범주와 선형 논리⁠(linear logic)⁠가 되고, 유한 극한⁠(limit)⁠과 부분 대상 분류자⁠(subobject classifier)⁠까지 갖추면 토포스가 됩니다. D ≅ D^D인 대상은 연속 함수만 모은 영역 이론⁠(domain theory)⁠의 세계에서 실제로 지어집니다.