호모토피 타입 이론(Homotopy type theory)

프로그래밍 언어에서 타입은 대략 '자료의 종류'입니다. 정수⁠(integer)⁠, 참·거짓, 문자열 같은 것이지요. 의존 타입⁠(dependent type)⁠ 이론에서는 명제도 타입으로 쓰고, 그 타입의 원소를 그 명제의 증명으로 봅니다. 그래서 $a = b$도 하나의 타입이고, 그 원소는 'a와 b가 같다'는 증명입니다. 그러면 물음이 생깁니다. 같은 등식에 서로 다른 증명이 둘 있을 수 있을까요? 보통의 수학에서 같음은 참이거나 거짓일 뿐이라, 증명이 여럿이라는 말이 어색합니다.

1994년 독일의 마르틴 호프만과 토마스 슈트라이허는 마르틴뢰프 타입 이론의 규칙만으로는 '같음의 증명은 모두 같다'를 증명할 수 없음을 보였습니다. 이 명제를 동일성 증명의 유일성(UIP)이라 합니다. 두 사람은 규칙을 모두 지키면서 UIP는 어기는 구체적인 예, 다시 말해 모형을 만들었습니다. 그 모형에서 타입은 집합⁠(set)⁠이 아니라 군류입니다. 군류⁠(groupoid)⁠는 원소들 사이에 화살표가 있고 모든 화살표를 거꾸로 되돌릴 수 있는 구조(범주⁠(category)⁠의 한 종류)이며, 두 원소 사이에 화살표가 여럿일 수 있습니다. 같음의 증명이 이 화살표 노릇을 하니 증명이 여럿일 수 있는 것입니다.

2006년 무렵 미국의 스티브 어우디와 마이클 워런, 그리고 따로 블라디미르 보예보츠키가 여기서 더 나아가, 같음의 증명이 공간 속의 경로처럼 행동한다는 것을 알아차렸습니다. 이 읽기 위에 세운 체계가 호모토피 타입 이론(HoTT)입니다.

구멍이 뚫린 평면에서 먼저 봅시다. 그림에서 두 점 a, b를 잇는 경로 p(파랑)와 q(분홍)의 가운데 손잡이를 끌어 보세요. 둘이 구멍의 같은 쪽을 지나면 구멍을 건너지 않고 p를 q로 밀어 옮길 수 있습니다. 서로 다른 쪽을 지나면 그런 변형이 없습니다. HoTT는 이것을 같음의 말로 읽습니다. 평면이 타입, 점 a와 b가 원소, 경로 p가 'a = b'의 증명 하나, p를 q로 미는 변형이 'p와 q가 같다'($p = q$)의 증명입니다. 그래서 같은 쪽을 지나면 $p = q$ 타입에 원소가 있고, 다른 쪽을 지나면 이 타입은 비어 있습니다. q가 떠나기 전에 a에서 구멍을 바퀴 돌게 할 수도 있습니다(음수는 시계 방향).

판정은 고리 $p\cdot q^{-1}$(p로 갔다가 q를 거꾸로 따라 돌아오는 길)가 구멍을 몇 번 감는지로 합니다. 이 횟수를 감긴 수라 합니다. 감긴 수⁠(winding number)⁠가 0일 때, 그리고 그때만 두 경로가 호모토픽합니다. 다시 말해 한쪽을 끊지 않고 다른 쪽으로 연속적으로 바꿀 수 있습니다. 한 점에서 떠나 돌아오는 고리들을 이렇게 변형으로 오갈 수 있는 것끼리 묶으면, 이어 붙이기를 연산으로 하는 군이 되는데 이것이 기본군입니다. 원의 기본군⁠(fundamental group)⁠은 정수의 덧셈군 ℤ입니다(구멍 뚫린 평면도 같습니다). 고리를 이으면 감긴 수가 더해지고, 거꾸로 돌면 부호가 바뀝니다.

그림에서 읽은 것을 사전으로 정리하면 이렇습니다. 타입은 공간, 원소는 점, $p : a = b$('p는 a = b의 원소'라 읽습니다)는 점 a에서 b로 가는 경로입니다. $\mathsf{refl}_a$('a의 반사')는 제자리에 머무는 경로로, a = a의 가장 당연한 증명입니다. 두 경로가 같다는 증명 $h : p = q$는 p를 끊지 않고 q로 연속적으로 바꾸는 변형, 다시 말해 위상수학⁠(topology)⁠의 호모토피입니다. 호모토피 사이의 호모토피가 또 있고, 그렇게 끝없이 올라갑니다. 대칭 $p^{-1} : b = a$는 경로를 거꾸로 가는 것, 추이 $p\cdot q$는 경로를 이어 가는 것입니다.

대칭과 추이는 따로 공리⁠(axiom)⁠로 둘 필요가 없습니다. 경로 귀납(J 규칙)이라는 규칙 하나로 정의되는 프로그램입니다. 경로 귀납⁠(path induction)⁠은 '모든 x, y와 모든 p : x = y에 대해 무언가를 보이려면, y가 x이고 p가 refl인 경우만 보이면 된다'는 규칙입니다. 흔히 이것을 '모든 경로는 refl'이라는 뜻으로 오해하지만 그렇지 않습니다. 한쪽 끝이 자유로운 경로는 그 끝을 끌어당겨 제자리 경로로 줄일 수 있다는 뜻이고, 두 끝을 모두 고정하면 그림의 p와 q처럼 서로 바꿀 수 없는 경로들이 남을 수 있습니다. 또 $p\cdot p^{-1} = \mathsf{refl}$ 같은 법칙은 글자 그대로 같은 것이 아니라 '경로 사이의 경로'로 성립합니다.

타입의 층. 이 읽기에서 타입은 경로가 얼마나 복잡한지에 따라 층으로 나뉩니다. 어떤 두 원소 사이에도 경로가 있는 타입은 명제입니다. 모든 원소가 서로 같으니, 참인지 거짓인지만 있고 증명의 차이는 없습니다. 어떤 두 원소 사이의 경로들의 타입이 늘 명제인 타입은 집합입니다. 다시 말해 같은 두 점을 잇는 경로가 둘 있으면 그 둘이 늘 같습니다. 자연수⁠(natural number)⁠ ℕ이 그렇습니다. 두 원소가 같은지 아닌지를 늘 가려 주는 함수⁠(function)⁠가 있는 타입은 모두 집합이라는 것이 1998년 미카엘 헤드베리의 정리입니다. 경로 사이의 경로들이 늘 명제이면 군류, 그렇게 위로 끝없이 이어집니다. 보통의 수학은 대부분 집합의 층에서 일어나므로, HoTT는 보통의 수학을 품으면서 그 위에 더 높은 층을 둡니다.

일가성 공리. 타입들을 원소로 갖는 우주 𝒰 안에서, 두 타입 A, B가 같다는 타입 $A =_{\mathcal U} B$를 생각합니다. 한편 $A \simeq B$는 A와 B 사이의 동치들의 타입입니다. 동치란 대략 서로를 되돌리는 함수 쌍 f : A → B, g : B → A로, g(f(a)) = a와 f(g(b)) = b가 경로로 성립하는 것입니다(정확한 정의는 '동치임'이 명제가 되도록 조금 더 다듬습니다). 경로 귀납으로 함수 $\mathsf{idtoeqv} : (A = B)\to(A\simeq B)$를 정의할 수 있습니다. refl을 항등 동치로 보내면 됩니다. 보예보츠키의 일가성 공리는 이 함수 자체가 동치라는 것입니다.

$$\mathsf{idtoeqv} : (A =_{\mathcal U} B) \:\xrightarrow{\ \simeq\ }\: (A \simeq B)$$

뜻은 '동치인 타입은 같고, 두 타입이 같은 방법은 두 타입 사이의 동치와 정확히 하나씩 맞물린다'입니다. 그러면 A에 대해 증명한 것은 무엇이든 A와 동치인 B로 옮겨 갈 수 있습니다. 수학자들이 늘 해 오던 '동형⁠(isomorphism)⁠인 것은 같은 것으로 본다'가 느슨한 관습이 아니라 체계의 규칙이 되는 셈입니다. 대가도 분명합니다. Bool에서 Bool로 가는 동치는 항등과 뒤집기(참과 거짓을 맞바꾸기) 둘이므로, 일가성에 따라 $\mathrm{Bool} = \mathrm{Bool}$에는 서로 다른 원소가 둘 있습니다. 그래서 우주 𝒰는 집합이 아니고, UIP는 일가성과 함께 둘 수 없습니다. 보예보츠키는 일가성에서 함수 외연성(모든 x에서 f(x) = g(x)이면 f = g)이 따라 나온다는 것도 보였습니다.

정직하게 말하면. 일가성은 마르틴뢰프 타입 이론에서 증명되는 정리가 아니라, 새로 더하는 공리입니다. 모순이 없다는 보증은 모형에서 옵니다. 보예보츠키가 만들고 크리스 캐풀킨과 피터 럼스데인이 정리한 모형은 단체 집합 위에 지었습니다. 단체 집합은 점, 선분, 삼각형, 사면체 같은 조각을 이어 붙여 공간을 적는 조합적인 틀입니다. 이 모형은 ZFC(오늘날 수학의 표준 집합론⁠(set theory)⁠ 공리) 안에서 짓되, 아주 큰 무한인 '도달 불가능한 기수⁠(cardinal number)⁠'가 여럿 있다는 공리를 더해야 합니다. 우주 하나하나를 해석하는 데 그만큼 큰 무한이 필요하기 때문입니다. 그래서 그런 기수를 더한 ZFC가 무모순⁠(consistent)⁠이면, 일가성을 더한 체계도 무모순입니다.

또 공리로 더하면 계산이 막힙니다. 일가성을 쓴 증명에서 나온 자연수는 0, 1, 2 같은 숫자까지 계산되지 않고 공리 앞에서 멈출 수 있습니다. 이 문제는 2015년 무렵 시릴 코엔, 티에리 코캉, 지몬 후버, 안데르스 뫼르트베리의 입방 타입 이론이 풀었습니다. 입방 타입 이론은 경로를 구간 [0, 1]에서 공간으로 가는 함수처럼 직접 다룹니다. 경로 사이의 경로는 정사각형에서, 그 위의 층은 정육면체에서 오는 함수가 되므로 '입방'이라 부릅니다. 이 틀에서 일가성은 공리가 아니라 계산되는 정리이고, Cubical Agda에 구현되어 있습니다.

끝으로 HoTT는 수학의 기초⁠(basics)⁠로 제안된 여러 선택지 가운데 하나일 뿐입니다. 널리 쓰이는 수학 라이브러리 mathlib이 서 있는 Lean은 '같은 명제의 증명은 모두 같다'(증명 무관성⁠, proof irrelevance⁠)를 타입 검사기의 규칙으로 씁니다. 그러면 같음의 증명도 모두 같아져(UIP) 일가성과 함께 둘 수 없습니다. 대부분의 수학자는 여전히 집합론을 기초로 여깁니다.

공간을 타입으로 짓기. HoTT에서는 점뿐 아니라 경로까지 생성자로 주는 타입(고차 귀납적 타입⁠, higher inductive type⁠)을 정의할 수 있습니다. 원 S¹은 점 $\mathsf{base} : S^1$ 하나와 경로 $\mathsf{loop} : \mathsf{base} = \mathsf{base}$ 하나로 만들어지는 타입입니다. 2013년 댄 리카타와 마이클 슐먼은 이 타입에서 $(\mathsf{base} = \mathsf{base}) \simeq \mathbb Z$를 증명했습니다. 원의 기본군이 ℤ라는 위상수학의 고전적 정리를, 연속성⁠(continuity)⁠이나 실수를 한 번도 쓰지 않고 타입의 규칙만으로 증명한 것입니다(이 타입 S¹이 위상수학의 원에 해당한다는 것은 공간 모형에서 따로 확인합니다). 증명의 열쇠가 일가성입니다. loop를 따라 한 바퀴 도는 것을 '정수에 1을 더하는 동치 ℤ ≃ ℤ'에 대응시키는데, 그 동치를 경로로 바꿔 주는 것이 일가성이기 때문입니다. 위 그림의 감긴 수는 이 정리를 공간 쪽에서 본 모습이고, HoTT는 같은 결론을 공간을 그리지 않고 얻습니다.

2012–2013년 프린스턴 고등연구소의 특별 연구년에 모인 연구자들이 함께 『호모토피 타입 이론: 수학의 일가 기초』(2013)를 썼습니다. 대수기하의 한 이론인 모티브 코호몰로지⁠(motivic cohomology)⁠를 세운 연구로 2002년 필즈상⁠(Fields Medal)⁠을 받은 보예보츠키가 이 길로 들어선 계기는 자기 논문의 오류였습니다. 그는 2014년의 회고에서, 1989년 무렵 미하일 카프라노프와 함께 쓴 논문의 주요 결과가 틀렸다는 지적이 1998년에 나왔지만 자신이 오류를 확신한 것은 2013년이었다고 적었습니다. 복잡한 수학을 사람의 검토만으로는 믿을 수 없다고 본 그는, 컴퓨터가 검사할 수 있는 수학의 기초를 찾았습니다.

이어지는 곳.

• 의존 타입: 동일성 타입⁠(identity type)⁠과 경로 귀납의 바탕입니다.
• 위상수학: 경로, 호모토피, 기본군이라는 말을 그대로 빌려 온 곳입니다.
• 군: 고리를 이어 붙이는 연산이 군을 이룬다는 것이 기본군의 요점이고, 원의 기본군 ℤ가 그림의 감긴 수입니다.
• 동치 관계: 같은 것끼리 묶는다는 점에서 경로는 동치 관계를 넓힌 것입니다. 동치 관계가 '같은가'만 말한다면 경로는 '어떻게 같은가'까지 기억합니다.
• 범주: 모든 화살표를 되돌릴 수 있는 범주가 타입의 모형이 된다는 관찰에서 이야기가 시작되었습니다. 공간과 무한 군류를 같은 것으로 보자는 그로텐디크의 호모토피 가설이 그 배경에 있습니다.
• 표현 바꾸기: '동형인 것은 같다'를 규칙으로 삼는 일가성은 이 큰 생각⁠(big ideas)⁠을 기초에 새겨 넣은 것입니다.
• 증명 보조기⁠(proof assistant)⁠: 이런 증명을 실제로 컴퓨터로 검사하는 도구입니다.
• 수학 기초론 논쟁⁠(debate on the foundations of mathematics)⁠: 집합론 대신 무엇을 수학의 바탕으로 삼을지는 이 논쟁 이후로 이어지는 물음입니다.
• 토포스⁠(topos)⁠: 집합의 세계를 넓힌 것으로, 그 안의 논리를 타입 이론으로 적을 수 있습니다. 2019년 마이클 슐먼은 토포스를 호모토피 쪽으로 한 단계 더 넓힌 세계((∞, 1)-토포스) 어디에서든 일가성을 갖춘 우주를 해석할 수 있음을 보였습니다.