Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

핵심 개념: "회전하는" 집합의 우주 구축하기

당신이 객체(집합)들의 우주를 구축하고 있다고 상 imagin 해보십시오 (집합론적 방식). 전통적인 방식의 수학(소위 "정칙적(well-founded)" 집합론)에서는 모든 객체가 더 작은 객체들로부터 만들어지고, 그 작은 객체들은 다시 더 작은 것들로부터 만들어지며, 결국 아무것도 없는 상태까지 내려갑니다. 이것은 피라미드와 같습니다. 공중에 떠 있는 블록은 있을 수 없습니다. 반드시 아래에 무언가가 받치고 있어야 합니다.

하지만 만약 당신이 사물이 자기 자신 위에 놓일 수 있는 우주를 만들고 싶다면 어떨까요? 만약 어떤 상자가 그 안에 자기 자신을 포함하고 있다면 어떨까요? 혹은 상자 A가 상자 B 안에 있고, 상자 B가 상자 C 안에 있으며, 다시 상자 C가 상자 A 안에 있는 식의 사슬이 있다면 어떨까요? 전통적인 수학에서 이는 무한 루프를 생성하기 때문에 금지됩니다. 이 논문에서 저자들은 **호모토피 유형론(Homotopy Type Theory, HoTT)**이라는 현대적 프레임워크를 사용하여 이러한 루프를 허용하는 수학적 우주를 구축하는 방법을 탐구합니다.

이 논문은 두 가지 일을 수행합니다:

1. **스콧(Scott)**이라는 수학자가 정한 규칙을 따라 루프를 허용하는 집합 모델을 구축합니다.
2. **아첼(Aczel)**이라는 수학자가 정한 규칙을 따라 루프를 허용하는 또 다른 집합 모델을 구축합니다.

도구: 트리, 코알제브라(Coalgebra), 그리고 "펼치기(Unfolding)"

이들의 모델을 이해하기 위해, **트리(Tree)**를 상상해 보십시오.

• 정칙 트리(Well-founded trees) (기존 방식)는 가족 계보와 같습니다. 뿌리(root)가 있고, 가지(branch)가 있으며, 결국 잎(leaf)에서 끝납니다. 성장이 멈춥니다.
• 비정칙 트리(Non-wellfounded trees) (새로운 방식)는 **프랙탈(fractal)**이나 거울의 방과 같을 수 있습니다. 가지가 다시 돌아와 뿌리가 될 수도 있습니다. 또는 하나의 가지가 갈라져 나와 전체 트리와 똑같이 생긴 두 개의 동일한 가지가 될 수도 있습니다.

저자들은 이러한 트리들을 설명하기 위해 **코알제브라(Coalgebra)**라는 개념을 사용합니다. 코알제브라를 노드를 보고 다음에 무엇이 오는지를 알려주는 "기계"라고 생각하십시오.

• 기계가 "정지"라고 말하면, 그것은 잎입니다.
• 기계가 "이러한 자식들에게 가라"고 말하면, 그것은 가지입니다.
• 기계가 "실제로 당신 자신인 자식에게 가라"고 말하면, 그것은 루프입니다.

이 논문은 질문합니다: 모든 가능한 루프를 설명할 수 있는 "궁극적인" 기계는 무엇인가?

두 가지 모델: 스콧(Scott) vs 아첼(Aczel)

저자들은 이러한 루프를 처리하기 위해 두 가지 서로 다른 "궁극적인 기계"(수학적 모델)를 구축합니다. 이는 루핑되는 세계에서 등가성(equality)을 다루는 두 가지 서로 다른 철학에 대응합니다.

1. "거울" 모델 (스콧의 반정칙 공리 - Scott's Anti-Foundation Axiom)

• 비유: 거울의 방을 상상해 보십시오. 거울 앞에 서면 자신의 모습이 보입니다. 그 모습이 또 다른 거울 속에 있다면, 반영된 모습의 반영이 보입니다.
• 규칙: 이 모델에서 두 객체는 그들의 **펼쳐지는 패턴(unfolding patterns)**이 동일할 때 "같다"고 간주됩니다. 만약 당신이 집합의 층을 계속해서 벗겨낸다면(양파 껍질을 까거나 트리를 펼치는 것처럼), 그 가지의 패턴이 다른 집합과 동일하다면 그것들은 같은 것입니다.
• 결과: 저자들은 이 모델 역할을 하는 특정한 유형의 트리 구조($V^0_\infty$)를 구축했습니다. 이것은 "고정점(fixed point)"입니다. 즉, 우주의 규칙을 적용하면 동일한 우주가 다시 돌아옵니다.
• 핵심 발견: 이 모델은 엄격한 의미에서의 "최종적(final)" 혹은 "터미널(terminal)" 기계가 아닙니다. 이것은 "제3의 선택지"입니다. 시작점(initial)도 아니고 절대적인 끝점(terminal)도 아닙니다. 루프를 식별하는 방식이 더 엄격한 스콧의 규칙을 따릅니다.

2. "보편적" 모델 (아첼의 반정칙 공리 - Aczel's Anti-Foundation Axiom)

• 비유: 당신이 할 수 있는 모든 이야기(자기 자신을 이야기하는 이야기까지 포함하여)의 마스터 카탈로그를 상상해 보십시오.
• 규칙: 이 모델에서는 어떤 그래프(점과 선으로 이루어진 그림)라도 집합으로 변환될 수 있습니다. 만약 루프를 나타내는 그림이 있다면, 그 그림과 완벽하게 일치하는 유일한 집합이 존재합니다.
• 결과: 저자들은 이 목적을 위해 "터미널 코알제브라(Terminal Coalgebra, 궁극의 기계)"를 구축했습니다. 그러나 이 특정 기계를 만들기 위해, 그들은 **명제 리사이징(Propositional Resizing)**이라는 특별하고 다소 논쟁적인 수학적 도구를 사용해야 했습니다.
  • 명제 리사이징이란 무엇인가? 거대한 도서관(명제들)이 있다고 상상해 보십시오. 이 도구는 도서관 전체를 내용의 손실 없이 단 하나의 선반에 들어갈 정도로 줄여주는 것을 허용합니다. 이것은 구성을 가능하게 만드는 강력한 지름길입니다.
• 핵심 발견: 이 모델은 아첼의 규칙을 만족합니다. 이것은 루핑되는 집합 우주의 가장 완전한 버전인 "터미널(terminal)" 객체입니다.

"동일성" 퍼즐: 무엇이 두 대상을 같게 만드는가?

이 논문의 주요 부분은 까다로운 퍼즐을 해결하는 것입니다: 두 개의 루핑 트리가 실제로 어떻게 같은지 어떻게 알 수 있는가?

표준 수학에서 두 대상이 똑같이 보이면 그것들은 같습니다. 하지만 루프가 있는 세상에서는 상황이 이상해집니다.

• 저자들은 두 지점 사이의 "동등성(equality)"이 또 다른 유형의 트리(인덱스된 M-타입)로 기술될 수 있다는 것을 발견했습니다.
• 비유: 두 개의 무한 프랙탈을 비교한다고 상상해 보십시오. 그것들이 같다는 것을 증명하려면, 단순히 전체 그림을 보는 것이 아니라, 모든 가지, 모든 하위 가지, 그리고 모든 하위-하위 가지를 하나하나 비교해야 합니다. 이 논문은 이러한 비교를 수행하는 정밀한 레시피(특성 기술)를 제공합니다. 그들은 이러한 복잡한 루프들의 "동등성" 자체가 구조화된 무한 객체임을 증명했습니다.

성과 요약

1. 스콧의 모델: 루프를 허용하며, 동등성이 "펼쳐지는" 트리의 형태에 의해 결정되는 집합의 우주를 구축했습니다. 이 모델은 고정점이지만 절대적인 "터미널"은 아닙니다.
2. 아첼의 모델: 어떤 그래프라도 집합으로 변환될 수 있는 루프 허용 "궁극의" 집합 우주를 구축했습니다. 이를 위해서는 명제 리사이징이라는 특별한 수학적 가정이 필요했습니다.
3. "동등성" 레시피: 이러한 무한하고 루핑되는 구조들에 대해 "같음"을 정의하는 정확한 방법을 찾아냈으며, 동등성이 그 자체로 또 다른 종류의 트리 구조임을 보여주었습니다.
4. 정형화(Formalization): 그들은 단순히 종이 위에 글을 쓴 것이 아니라, 논리적 단계를 검증하여 실수가 없음을 보장하는 Agda라는 컴퓨터 프로그램 내에 이를 구축했습니다.

이것이 왜 중요한가?

이 논문은 실세계의 엔지니어링 문제나 의료 문제를 해결한다고 주장하지 않습니다. 대신, 수학의 기초적인 퍼즐을 해결합니다. 이는 호모토피 유형론이라는 현대적 언어를 사용하여 "원"과 "루프"가 허용되는 일관되고 논리적인 우주를 구축할 수 있음을 보여줍니다. 이는 루프를 금지하는 고전적 집합론과, 스트림(streams)이나 전이 시스템(transition systems)과 같은 복잡하고 순환적인 데이터 구조를 다뤄야 하는 현대 컴퓨터 과학 논리 사이의 간극을 메워줍니다.

요약하자면, 그들은 사물이 자기 자신을 포함할 수 있는 두 가지 서로 다른 "우주"를 구축했고, 그것들이 특정 규칙에 따라 작동함을 증명했으며, 그러한 자기 포함적 대상들이 실제로 어떻게 같은지를 정확히 밝혀냈습니다.