A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

이 논문은 스테파노 베르나디 (Stefano Berardi) 의 64 세 생일을 기념하여 헌정된 논문집의 일부로, 마르크 베젬 (Marc Bezem), 티에리 쿵캉 (Thierry Coquand), 피터 디비어 (Peter Dybjer), 마르틴 에스카르도 (Mart´ın Escard´o) 에 의해 작성되었습니다. 이 논문은 명시적 우주 다형성 (Explicit Universe Polymorphism) 을 가진 타입 이론에 대응하는 **일반화 대수적 이론 (Generalized Algebraic Theories, GATs)**을 제시하고, 이를 통해 해당 타입 이론들을 추상적으로 특징짓는 것을 목표로 합니다.

다음은 논문의 문제 제기, 방법론, 주요 기여, 결과 및 의의에 대한 상세한 기술적 요약입니다.

1. 문제 제기 (Problem)

• 기존 접근법의 한계: 전통적인 타입 이론은 문법 (grammar) 과 추론 규칙 (inference rules) 으로 정의됩니다. 그러나 이러한 방식은 구체적인 구문 선택과 방대한 수의 서술 규칙 (bookkeeping rules, 예: 일반적 등식 규칙) 에 의존하여, 이론의 본질적인 구조를 파악하기 어렵게 만듭니다.
• 보편적 초기성 (Initiality) 의 필요성: 우보스키 (Voevodsky) 의 '초기성 추측 (Initiality Conjecture)' 프로젝트는 특정 클래스의 추론 규칙에 대해 '항 모델 (term model)'이 해당 모델 범주에서 초기 대상 (initial object) 임을 증명하는 것을 목표로 합니다. 이는 다양한 타입 이론에 대한 통일된 메타이론을 구축하는 데 필수적입니다.
• 우주 다형성의 복잡성: 명시적 우주 다형성 (universe polymorphism) 을 가진 타입 이론 (예: Agda, Lean 의 방식) 은 우주 레벨 (universe levels) 이 타입을 형성하지 않고, 별도의 판단 (judgment) 으로 다뤄지며, 레벨 인덱싱된 곱 (level-indexed products) 등이 추가되어 기존 모델론적 접근이 복잡해집니다.

2. 방법론 (Methodology)

저자들은 타입 이론을 **일반화 대수적 이론 (GATs)**과 **가족이 있는 범주 (Categories with Families, CwFs)**를 기반으로 재구성하는 방식을 취했습니다.

• GATs 와 CwFs 의 활용:

  • GATs 는 다중 정렬 대수 이론을 일반화한 것으로, 정렬 기호 (sort symbols) 와 연산 기호 (operator symbols) 가 의존적 타입을 가질 수 있습니다.
  • CwFs 는 의존 타입 이론의 기본 규칙 (문맥 형성, 치환, 투영 등) 을 모델링하는 범주론적 구조입니다.
  • 저자들은 GATs 를 사용하여 타입 이론의 추론 규칙을 고수준의 대수적 구조로 추상화하고, 이를 CwF 의 초기 모델 (initial model) 로서 특징짓습니다.

• 두 가지 주요 이론의 제시:

  1. 외부 우주 탑 (External Tower of Universes, $TT_{tower}$):
     • 자연수 $l \in \mathbb{N}$로 인덱싱된 외부 우주 탑을 가지는 마틴 - 뢰프 타입 이론.
     • 이에 대응하는 **무한 GAT($\Sigma_{tower}$)**를 정의합니다. 이는 표준 작은 타입 형성자 ($\Pi, \Sigma, N, W, Id$ 등) 와 외부 인덱싱된 우주 ($U_l$) 에 대한 구조를 포함합니다.
  2. 명시적 우주 다형성 (Explicit Universe Polymorphism, $TT_{up}$):
     • 우주 레벨 판단 ($l \text{ level}$) 과 내부적으로 인덱싱된 우주, 레벨 인덱싱된 곱 ($[\alpha]A$) 을 포함하는 이론.
     • 이에 대응하는 **유한 GAT($\Sigma_{up}$)**를 정의합니다. 이는 레벨 인덱싱된 CwF(레벨 인덱싱된 CwF 가 CwF 의 값으로 작용하는 presheaf) 구조를 기반으로 합니다.

• 초기 모델 구성:

  • 명시적 치환 (explicit substitution) 을 기반으로 한 일반적 구성을 통해 GAT 의 초기 모델 (항 모델) 을 구성합니다.
  • 또한, 암시적 치환 (implicit substitution) 을 가진 기존 타입 이론의 문법과 추론 규칙으로부터 초기 CwF 를 구성하여, 이것이 GAT 의 초기 모델과 동형임을 보여줍니다.

3. 주요 기여 및 기술적 내용 (Key Contributions & Technical Details)

A. 외부 우주 탑을 위한 GAT ($\Sigma_{tower}$)

• 구조: CwF 에 작은 타입 형성자와 외부 자연수 $l$로 인덱싱된 우주 $U_l$에 대한 연산자를 추가합니다.
• 연산자:
  • $U_l$: $l$번째 우주.
  • $T_l$: $U_l$의 디코딩 (decoding) 맵.
  • $\Pi_{l,l'}$: 두 우주 $U_l, U_l'$에 대한 $\Pi$ 타입의 코드.
  • $U^m_l$: $U_l$이 더 큰 우주 $U_m$에 포함됨을 나타내는 코드 (누적성 포함 시).
• 방정식: 디코딩 방정식 ($T(\Pi(a,b)) = \Pi(T(a), T(b))$) 과 치환에 대한 교환 법칙을 정의합니다.
• 초기성: $\Sigma_{tower}$는 무한 GAT 이지만, 유한 부분 GAT 들의 증가하는 시퀀스로 접근하여 초기 모델 $T_{\Sigma_{tower}}$를 구성할 수 있습니다.

B. 명시적 우주 다형성을 위한 GAT ($\Sigma_{up}$)

• 레벨의 CwF (ucwf of levels):
  • 우주 레벨 자체를 하나의 CwF (단일 타입을 가진 CwF) 로 모델링합니다.
  • 정렬 기호: $lctx$(레벨 문맥),$lhom$(레벨 치환),$ltm$ (레벨 항).
  • 연산자: 레벨의 합집합 ($\vee$), 다음 레벨 ($+$), 그리고 **레벨 등식 (level equality)**을 위한 새로운 정렬 기호 $leq$.
  • 레벨 등식 정렬 ($leq$): GAT 에서 등식 가정을 직접 사용할 수 없으므로, $l < m$과 같은 제약 조건을 $p : leq(l+ \vee m, m)$과 같은 항의 존재로 인코딩합니다. 이는 명제적 등식 (propositional equality) 과 유사한 역할을 합니다.
• 레벨 인덱싱된 CwF:
  • 레벨 문맥 $n$에 대해 CwF $T(n)$이 매핑되는 presheaf 구조를 가집니다.
  • 작은 타입 형성자와 레벨 인덱싱된 우주 ($U_l$) 가 레벨 변수에 의존하도록 내부화합니다.
• 레벨 인덱싱된 곱 (Level-indexed products):
  • 보편적 레벨 양화 $\forall l$과 레벨 추상 $\lambda l$, 적용 $appl$을 위한 연산자를 도입합니다. 이는 무형식 논리 (untyped predicate logic) 의 보편 양화와 구조적으로 유사합니다.

C. 초기성 (Initiality) 증명

• 명시적 치환 기반: GAT $\Sigma$에 대해 항 모델 $T_\Sigma$를 구성하며, 이는 CwF $\Sigma$-구조를 가진 범주에서 초기 대상임을 보입니다.
• 암시적 치환 기반: 기존 타입 이론 ($TT_{tower}, TT_{up}$) 의 문법과 추론 규칙으로부터 CwF 를 구성하고, 이것이 GAT 의 초기 모델과 동형임을 보여줍니다. 이는 우보스키의 초기성 추측 프로젝트에 대한 구체적인 실례를 제공합니다.

4. 결과 (Results)

1. 추상적 특징화: 두 가지 타입 이론 ($TT_{tower}$와 $TT_{up}$) 이 각각 대응하는 GAT 의 초기 모델로서 추상적으로 특징지어졌습니다. 이는 문법과 추론 규칙의 세부 사항에서 벗어나 고수준의 대수적 구조를 강조합니다.
2. 통일된 접근법: GAT 와 CwF 를 기반으로 한 범주 논리 (categorical logic) 의 통일된 접근 방식을 제시했습니다. 이는 단순 타입 이론, 의존 타입 이론, 술어 논리 등 다양한 논리 시스템을 포괄할 수 있음을 보였습니다.
3. 초기성 추측 프로젝트 기여: 우보스키의 초기성 추측 프로젝트에 대해 GAT 와 CwF 기반의 구체적인 접근법을 제시했습니다. 특히, 레벨 인덱싱과 명시적 다형성을 가진 복잡한 타입 이론에 대해 초기 모델의 존재와 유일성을 증명하는 틀을 마련했습니다.
4. 레벨 등식의 형식화: GAT 내에서 등식 제약 조건을 처리하기 위해 '레벨 등식 정렬 ($leq$)'을 도입하여, 우주 레벨 간의 관계 ($l < m$) 를 대수적으로 인코딩하는 방법을 제시했습니다.

5. 의의 및 중요성 (Significance)

• 이론적 엄밀성: 타입 이론을 문법적 기술이 아닌 대수적 구조 (GAT) 로 재정의함으로써, 다양한 문법적 변형 간의 동등성을 증명하고 수학적 이론의 고유한 본질을 파악하는 데 기여합니다.
• 메타이론 개발: 새로운 타입 이론을 설계할 때, 구체적인 규칙을 일일이 증명하는 대신 일반 정리를 특수화 (specialization) 하여 결과를 얻을 수 있는 기반을 제공합니다.
• 실용적 적용: Agda 와 같은 증명 보조기 (proof assistant) 에서 초기성 정리를 구현하는 작업 (예: Brunerie 와 de Boer 의 작업) 을 일반화하고 확장할 수 있는 이론적 토대를 마련합니다.
• 미래 연구 방향:
  • GAT 와 논리 프레임워크 (Logical Framework, 예: LF, Dedukti) 간의 관계 규명.
  • SOGAT(Second-Order Generalized Algebraic Theories) 와의 연결.
  • Quotient Inductive-Inductive Types (QIITs) 와의 유사성 및 차이점 분석.

요약하자면, 이 논문은 복잡한 타입 이론 (특히 우주 다형성을 가진 이론) 을 범주론적 구조 (CwF) 와 일반화 대수적 이론 (GAT) 을 통해 고수준으로 추상화하고, 이를 초기 모델의 관점에서 엄밀하게 특징짓는 획기적인 시도를 제시합니다. 이는 우보스키의 초기성 추측을 실현하기 위한 핵심적인 단계로 평가됩니다.